%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT001-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 09:36:31 AM UTC 2026
% Result : Satisfiable 20.10s 4.02s
% Output : Saturation 0.32s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u661,hypothesis,
codomain(b) = ifeq(codomain(g),domain(a),codomain(compose(compose(a,g),compose(a,b))),codomain(b)) ).
cnf(u248,hypothesis,
codomain(g) = ifeq(codomain(g),domain(a),codomain(compose(h,compose(a,g))),codomain(g)) ).
cnf(u5647,hypothesis,
compose(compose(domain(X0),compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,g),compose(a,g))),compose(compose(domain(X0),compose(a,g)),compose(a,g))),compose(compose(domain(X0),compose(a,g)),compose(a,g))) ).
cnf(u1553,hypothesis,
compose(compose(h,h),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(g),compose(h,compose(h,domain(X0))),compose(compose(h,h),domain(X0))),compose(compose(h,h),domain(X0))) ).
cnf(u1307,hypothesis,
compose(compose(a,a),codomain(X0)) = ifeq(domain(g),codomain(X0),ifeq(domain(g),domain(a),compose(a,compose(a,codomain(X0))),compose(compose(a,a),codomain(X0))),compose(compose(a,a),codomain(X0))) ).
cnf(u4356,hypothesis,
compose(compose(domain(X1),compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(domain(X1),domain(a),compose(domain(X1),compose(compose(a,b),domain(X0))),compose(compose(domain(X1),compose(a,b)),domain(X0))),compose(compose(domain(X1),compose(a,b)),domain(X0))) ).
cnf(u1294,hypothesis,
compose(compose(X0,b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(g),compose(X0,compose(b,compose(a,b))),compose(compose(X0,b),compose(a,b))),compose(compose(X0,b),compose(a,b))) ).
cnf(u21,hypothesis,
domain(b) = domain(g) ).
cnf(u3464,hypothesis,
compose(X0,compose(a,b)) = ifeq(codomain(X0),domain(a),compose(X0,compose(codomain(X0),compose(a,b))),compose(X0,compose(a,b))) ).
cnf(u151,hypothesis,
domain(a) = ifeq(codomain(b),domain(g),domain(compose(compose(a,b),h)),domain(a)) ).
cnf(u2706,hypothesis,
compose(h,domain(X0)) = ifeq(domain(X0),codomain(compose(h,domain(X0))),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),codomain(compose(h,domain(X0))))),compose(h,domain(X0))),compose(h,domain(X0))) ).
cnf(u3105,hypothesis,
compose(compose(domain(X0),compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,g),b)),compose(compose(domain(X0),compose(a,g)),b)),compose(compose(domain(X0),compose(a,g)),b)) ).
cnf(u3695,hypothesis,
compose(compose(h,compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),domain(X0))),compose(compose(h,compose(a,g)),domain(X0))),compose(compose(h,compose(a,g)),domain(X0))) ).
cnf(u1786,axiom,
compose(compose(domain(X0),codomain(X1)),codomain(X1)) = ifeq(domain(X0),codomain(X1),compose(domain(X0),codomain(X1)),compose(compose(domain(X0),codomain(X1)),codomain(X1))) ).
cnf(u3938,hypothesis,
compose(domain(X0),compose(a,b)) = ifeq(codomain(b),codomain(compose(domain(X0),compose(a,b))),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,b),codomain(compose(domain(X0),compose(a,b))))),compose(domain(X0),compose(a,b))),compose(domain(X0),compose(a,b))) ).
cnf(u3229,hypothesis,
compose(compose(compose(a,b),domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(domain(X0),h)),compose(compose(compose(a,b),domain(X0)),h)),compose(compose(compose(a,b),domain(X0)),h)) ).
cnf(u1944,axiom,
compose(compose(domain(X1),X2),domain(X0)) = ifeq(codomain(X2),domain(X0),ifeq(domain(X1),domain(X2),compose(domain(X1),compose(X2,domain(X0))),compose(compose(domain(X1),X2),domain(X0))),compose(compose(domain(X1),X2),domain(X0))) ).
cnf(u1327,hypothesis,
compose(compose(a,compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),b)),compose(compose(a,compose(a,b)),b)),compose(compose(a,compose(a,b)),b)) ).
cnf(u906,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(h,compose(a,b)),h,codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u1681,hypothesis,
compose(compose(compose(a,g),X1),codomain(X0)) = ifeq(codomain(X1),codomain(X0),ifeq(codomain(g),domain(X1),compose(compose(a,g),compose(X1,codomain(X0))),compose(compose(compose(a,g),X1),codomain(X0))),compose(compose(compose(a,g),X1),codomain(X0))) ).
cnf(u1572,hypothesis,
domain(a) = ifeq(codomain(X0),domain(a),ifeq(compose(a,b),compose(X0,compose(a,b)),X0,domain(a)),domain(a)) ).
cnf(u2203,hypothesis,
compose(compose(a,g),compose(a,g)) = ifeq(codomain(g),domain(a),compose(domain(a),compose(compose(a,g),compose(a,g))),compose(compose(a,g),compose(a,g))) ).
cnf(u678,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(X0),domain(a),domain(X0),domain(X0)),domain(X0)) ).
cnf(u4290,axiom,
compose(compose(codomain(X1),domain(X0)),codomain(X2)) = ifeq(domain(X0),codomain(X2),ifeq(codomain(X1),domain(X0),compose(codomain(X1),compose(domain(X0),codomain(X2))),compose(compose(codomain(X1),domain(X0)),codomain(X2))),compose(compose(codomain(X1),domain(X0)),codomain(X2))) ).
cnf(u1422,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,b),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u912,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(h,compose(a,b)),domain(X0),h),h),h) ).
cnf(u2089,hypothesis,
compose(domain(X0),compose(a,b)) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(domain(X0),compose(a,b))),compose(domain(X0),compose(a,b))) ).
cnf(u649,hypothesis,
codomain(g) = ifeq(codomain(g),domain(a),codomain(compose(compose(a,g),compose(a,g))),codomain(g)) ).
cnf(u1694,axiom,
compose(compose(X1,X0),codomain(X0)) = ifeq(codomain(X1),domain(X0),compose(X1,X0),compose(compose(X1,X0),codomain(X0))) ).
cnf(u4261,hypothesis,
compose(compose(domain(X1),compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(domain(X1),domain(a),compose(domain(X1),compose(compose(a,g),codomain(X0))),compose(compose(domain(X1),compose(a,g)),codomain(X0))),compose(compose(domain(X1),compose(a,g)),codomain(X0))) ).
cnf(u160,hypothesis,
domain(g) = ifeq(codomain(g),domain(X0),domain(compose(h,domain(X0))),domain(g)) ).
cnf(u3201,hypothesis,
compose(compose(codomain(X0),compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,g),h)),compose(compose(codomain(X0),compose(a,g)),h)),compose(compose(codomain(X0),compose(a,g)),h)) ).
cnf(u3481,hypothesis,
compose(compose(a,g),domain(X0)) = ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(codomain(g),domain(X0))),compose(compose(a,g),domain(X0))) ).
cnf(u1700,axiom,
compose(compose(domain(X0),X1),codomain(X1)) = ifeq(domain(X0),domain(X1),compose(domain(X0),X1),compose(compose(domain(X0),X1),codomain(X1))) ).
cnf(u1334,hypothesis,
compose(compose(codomain(X0),b),b) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,b)),compose(compose(codomain(X0),b),b)),compose(compose(codomain(X0),b),b)) ).
cnf(u61,hypothesis,
codomain(X0) = ifeq(domain(g),domain(X0),codomain(compose(a,X0)),codomain(X0)) ).
cnf(u2717,hypothesis,
compose(codomain(X0),h) = ifeq(codomain(g),codomain(compose(codomain(X0),h)),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,codomain(compose(codomain(X0),h)))),compose(codomain(X0),h)),compose(codomain(X0),h)) ).
cnf(u3224,hypothesis,
compose(h,h) = ifeq(codomain(g),domain(g),compose(h,compose(codomain(g),h)),compose(h,h)) ).
cnf(u423,axiom,
compose(compose(domain(X0),X1),X2) = ifeq(codomain(X1),domain(X2),ifeq(domain(X0),domain(X1),compose(domain(X0),compose(X1,X2)),compose(compose(domain(X0),X1),X2)),compose(compose(domain(X0),X1),X2)) ).
cnf(u1698,axiom,
compose(compose(X1,codomain(X2)),codomain(X0)) = ifeq(codomain(X2),codomain(X0),ifeq(codomain(X1),codomain(X2),compose(X1,compose(codomain(X2),codomain(X0))),compose(compose(X1,codomain(X2)),codomain(X0))),compose(compose(X1,codomain(X2)),codomain(X0))) ).
cnf(u1715,hypothesis,
compose(compose(X0,compose(a,g)),codomain(g)) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,g)),compose(compose(X0,compose(a,g)),codomain(g))) ).
cnf(u1947,hypothesis,
compose(compose(domain(X0),X1),compose(a,b)) = ifeq(codomain(X1),domain(a),ifeq(domain(X0),domain(X1),compose(domain(X0),compose(X1,compose(a,b))),compose(compose(domain(X0),X1),compose(a,b))),compose(compose(domain(X0),X1),compose(a,b))) ).
cnf(u2350,hypothesis,
compose(compose(codomain(X0),domain(a)),compose(a,b)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,b)),compose(compose(codomain(X0),domain(a)),compose(a,b))) ).
cnf(u1704,hypothesis,
compose(compose(a,X0),codomain(X0)) = ifeq(domain(g),domain(X0),compose(a,X0),compose(compose(a,X0),codomain(X0))) ).
cnf(u1338,hypothesis,
compose(compose(h,b),b) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(g),compose(h,compose(b,b)),compose(compose(h,b),b)),compose(compose(h,b),b)) ).
cnf(u666,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(X1,compose(a,b)),X1,codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u4666,hypothesis,
compose(compose(compose(a,b),compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),b)),compose(compose(compose(a,b),compose(a,b)),b)),compose(compose(compose(a,b),compose(a,b)),b)) ).
cnf(u1462,hypothesis,
compose(compose(h,h),b) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(g),compose(h,compose(h,b)),compose(compose(h,h),b)),compose(compose(h,h),b)) ).
cnf(u421,hypothesis,
compose(compose(X0,X1),b) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,b)),compose(compose(X0,X1),b)),compose(compose(X0,X1),b)) ).
cnf(u672,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(X0,compose(a,b)),compose(codomain(X1),compose(a,b)),codomain(X1),X0),X0),X0) = X0 ).
cnf(u4653,hypothesis,
compose(compose(compose(a,g),compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),b)),compose(compose(compose(a,g),compose(a,b)),b)),compose(compose(compose(a,g),compose(a,b)),b)) ).
cnf(u3259,hypothesis,
compose(compose(a,domain(X0)),domain(X1)) = ifeq(domain(X0),domain(X1),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),domain(X1))),compose(compose(a,domain(X0)),domain(X1))),compose(compose(a,domain(X0)),domain(X1))) ).
cnf(u1205,hypothesis,
compose(compose(X0,codomain(X1)),h) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X1),h)),compose(compose(X0,codomain(X1)),h)),compose(compose(X0,codomain(X1)),h)) ).
cnf(u1336,hypothesis,
compose(compose(compose(a,b),b),b) = ifeq(codomain(b),domain(g),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,b)),compose(compose(compose(a,b),b),b)),compose(compose(compose(a,b),b),b)) ).
cnf(u1466,hypothesis,
compose(compose(h,codomain(X0)),b) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),b)),compose(compose(h,codomain(X0)),b)),compose(compose(h,codomain(X0)),b)) ).
cnf(u3960,axiom,
compose(codomain(X0),codomain(X1)) = ifeq(codomain(X1),codomain(compose(codomain(X0),codomain(X1))),ifeq(codomain(X0),codomain(X1),compose(codomain(X0),compose(codomain(X1),codomain(compose(codomain(X0),codomain(X1))))),compose(codomain(X0),codomain(X1))),compose(codomain(X0),codomain(X1))) ).
cnf(u5167,hypothesis,
compose(compose(domain(compose(a,compose(a,b))),a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(domain(compose(a,compose(a,b))),domain(a),compose(a,compose(a,b)),compose(compose(domain(compose(a,compose(a,b))),a),compose(a,b))),compose(compose(domain(compose(a,compose(a,b))),a),compose(a,b))) ).
cnf(u5718,hypothesis,
compose(compose(compose(a,b),domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(domain(X0),compose(a,b))),compose(compose(compose(a,b),domain(X0)),compose(a,b))),compose(compose(compose(a,b),domain(X0)),compose(a,b))) ).
cnf(u6185,hypothesis,
compose(compose(compose(a,g),codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),compose(a,g))),compose(compose(compose(a,g),codomain(X0)),compose(a,g))),compose(compose(compose(a,g),codomain(X0)),compose(a,g))) ).
cnf(u179,hypothesis,
codomain(X0) = ifeq(codomain(g),domain(X0),codomain(compose(compose(a,g),X0)),codomain(X0)) ).
cnf(u5189,hypothesis,
compose(compose(h,compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),compose(a,g))),compose(compose(h,compose(a,b)),compose(a,g))),compose(compose(h,compose(a,b)),compose(a,g))) ).
cnf(u1087,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(a,compose(a,b)),X0,a,h),h),h),h) ).
cnf(u434,axiom,
compose(compose(X1,domain(X0)),X2) = ifeq(domain(X0),domain(X2),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),X2)),compose(compose(X1,domain(X0)),X2)),compose(compose(X1,domain(X0)),X2)) ).
cnf(u5373,hypothesis,
compose(compose(domain(compose(compose(a,g),b)),compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(domain(compose(compose(a,g),b)),domain(a),compose(compose(a,g),b),compose(compose(domain(compose(compose(a,g),b)),compose(a,g)),b)),compose(compose(domain(compose(compose(a,g),b)),compose(a,g)),b)) ).
cnf(u4457,hypothesis,
compose(compose(X0,compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,g),compose(a,g))),compose(compose(X0,compose(a,g)),compose(a,g))),compose(compose(X0,compose(a,g)),compose(a,g))) ).
cnf(u1710,hypothesis,
compose(compose(X0,b),codomain(b)) = ifeq(codomain(X0),domain(g),compose(X0,b),compose(compose(X0,b),codomain(b))) ).
cnf(u78,hypothesis,
domain(compose(a,b)) = domain(a) ).
cnf(u1464,hypothesis,
compose(compose(h,compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),b)),compose(compose(h,compose(a,b)),b)),compose(compose(h,compose(a,b)),b)) ).
cnf(u177,hypothesis,
compose(a,g) = compose(compose(a,g),codomain(g)) ).
cnf(u6738,hypothesis,
compose(compose(domain(compose(codomain(X0),compose(a,b))),codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(domain(compose(codomain(X0),compose(a,b))),codomain(X0),compose(codomain(X0),compose(a,b)),compose(compose(domain(compose(codomain(X0),compose(a,b))),codomain(X0)),compose(a,b))),compose(compose(domain(compose(codomain(X0),compose(a,b))),codomain(X0)),compose(a,b))) ).
cnf(u432,hypothesis,
compose(compose(X0,compose(a,g)),X1) = ifeq(codomain(g),domain(X1),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,g),X1)),compose(compose(X0,compose(a,g)),X1)),compose(compose(X0,compose(a,g)),X1)) ).
cnf(u1215,hypothesis,
compose(compose(a,X0),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(domain(g),domain(X0),compose(a,compose(X0,codomain(X1))),compose(compose(a,X0),codomain(X1))),compose(compose(a,X0),codomain(X1))) ).
cnf(u76,hypothesis,
domain(a) = domain(compose(a,g)) ).
cnf(u206,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),X1),X1),X1),X1) = X1 ).
cnf(u1117,hypothesis,
compose(compose(compose(a,b),a),b) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,b)),compose(compose(compose(a,b),a),b)) ).
cnf(u847,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(X0,compose(a,b)),compose(a,b),X0),X0),X0) = X0 ).
cnf(u1098,hypothesis,
compose(compose(compose(a,g),a),X0) = ifeq(domain(g),domain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,X0)),compose(compose(compose(a,g),a),X0)),compose(compose(compose(a,g),a),X0)) ).
cnf(u5201,hypothesis,
compose(compose(h,compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),compose(a,b))),compose(compose(h,compose(a,b)),compose(a,b))),compose(compose(h,compose(a,b)),compose(a,b))) ).
cnf(u2652,hypothesis,
compose(X0,a) = ifeq(domain(g),codomain(compose(X0,a)),ifeq(codomain(X0),domain(a),compose(X0,compose(a,codomain(compose(X0,a)))),compose(X0,a)),compose(X0,a)) ).
cnf(u91,hypothesis,
compose(a,b) = compose(domain(a),compose(a,b)) ).
cnf(u1092,hypothesis,
compose(compose(X0,a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),compose(X0,compose(a,compose(a,g))),compose(compose(X0,a),compose(a,g))),compose(compose(X0,a),compose(a,g))) ).
cnf(u1222,hypothesis,
compose(compose(a,b),X0) = ifeq(codomain(b),domain(X0),compose(a,compose(b,X0)),compose(compose(a,b),X0)) ).
cnf(u4450,hypothesis,
compose(compose(compose(a,g),X0),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(X0,compose(a,g))),compose(compose(compose(a,g),X0),compose(a,g))),compose(compose(compose(a,g),X0),compose(a,g))) ).
cnf(u66,hypothesis,
codomain(b) = ifeq(codomain(X0),domain(g),codomain(compose(X0,b)),codomain(b)) ).
cnf(u1353,hypothesis,
compose(compose(a,codomain(X0)),h) = ifeq(codomain(X0),domain(g),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),h)),compose(compose(a,codomain(X0)),h)),compose(compose(a,codomain(X0)),h)) ).
cnf(u204,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(domain(X2),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(domain(X2),compose(a,b)),X0,domain(X2),X1),X1),X1),X1) = X1 ).
cnf(u1243,hypothesis,
compose(compose(a,g),codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(a,compose(h,codomain(X0))),compose(compose(a,g),codomain(X0))) ).
cnf(u1245,hypothesis,
compose(compose(a,g),compose(a,b)) = ifeq(codomain(g),domain(a),compose(a,compose(h,compose(a,b))),compose(compose(a,g),compose(a,b))) ).
cnf(u1376,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X0,ifeq(compose(h,compose(a,b)),X0,h,compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u1096,hypothesis,
compose(compose(domain(X0),a),X1) = ifeq(domain(g),domain(X1),ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,X1)),compose(compose(domain(X0),a),X1)),compose(compose(domain(X0),a),X1)) ).
cnf(u1226,hypothesis,
compose(compose(a,codomain(X0)),X1) = ifeq(codomain(X0),domain(X1),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),X1)),compose(compose(a,codomain(X0)),X1)),compose(compose(a,codomain(X0)),X1)) ).
cnf(u89,hypothesis,
domain(a) = ifeq(domain(g),domain(a),domain(compose(a,compose(a,g))),domain(a)) ).
cnf(u1500,hypothesis,
compose(compose(h,b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(g),compose(h,compose(b,compose(a,g))),compose(compose(h,b),compose(a,g))),compose(compose(h,b),compose(a,g))) ).
cnf(u2261,hypothesis,
compose(compose(X0,domain(g)),b) = ifeq(codomain(X0),domain(g),compose(X0,b),compose(compose(X0,domain(g)),b)) ).
cnf(u873,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(a,compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,b),a),a),a) ).
cnf(u116,hypothesis,
domain(X0) = ifeq(domain(X0),domain(g),domain(compose(domain(X0),h)),domain(X0)) ).
cnf(u1235,hypothesis,
compose(compose(a,g),h) = ifeq(codomain(g),domain(g),compose(a,compose(g,h)),compose(compose(a,g),h)) ).
cnf(u842,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(X0,compose(a,b)),compose(a,compose(a,b)),X0,a),a),a) ).
cnf(u1389,hypothesis,
compose(compose(h,X0),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(h,compose(X0,compose(a,g))),compose(compose(h,X0),compose(a,g))),compose(compose(h,X0),compose(a,g))) ).
cnf(u887,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(a,compose(a,b)),compose(a,b),a),a),a) ).
cnf(u6325,axiom,
compose(compose(domain(compose(codomain(X0),domain(X1))),codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(domain(compose(codomain(X0),domain(X1))),codomain(X0),compose(codomain(X0),domain(X1)),compose(compose(domain(compose(codomain(X0),domain(X1))),codomain(X0)),domain(X1))),compose(compose(domain(compose(codomain(X0),domain(X1))),codomain(X0)),domain(X1))) ).
cnf(u1224,hypothesis,
compose(compose(a,compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),X0)),compose(compose(a,compose(a,b)),X0)),compose(compose(a,compose(a,b)),X0)) ).
cnf(u217,hypothesis,
codomain(b) = ifeq(codomain(g),domain(g),codomain(compose(h,b)),codomain(b)) ).
cnf(u996,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(compose(a,b),compose(compose(a,g),compose(a,b)),domain(a),compose(a,g)),compose(a,g)) ).
cnf(u2262,hypothesis,
compose(compose(X0,domain(g)),h) = ifeq(codomain(X0),domain(g),compose(X0,h),compose(compose(X0,domain(g)),h)) ).
cnf(u2671,hypothesis,
compose(h,a) = ifeq(domain(g),codomain(compose(h,a)),ifeq(codomain(g),domain(a),compose(h,compose(a,codomain(compose(h,a)))),compose(h,a)),compose(h,a)) ).
cnf(u106,hypothesis,
domain(X0) = ifeq(domain(X0),domain(g),domain(compose(domain(X0),b)),domain(X0)) ).
cnf(u3520,hypothesis,
compose(compose(a,b),compose(a,g)) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(codomain(b),compose(a,g))),compose(compose(a,b),compose(a,g))) ).
cnf(u1487,hypothesis,
compose(compose(h,codomain(X0)),h) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),h)),compose(compose(h,codomain(X0)),h)),compose(compose(h,codomain(X0)),h)) ).
cnf(u1147,hypothesis,
compose(compose(codomain(X0),X1),b) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(X1,b)),compose(compose(codomain(X0),X1),b)),compose(compose(codomain(X0),X1),b)) ).
cnf(u2012,hypothesis,
compose(b,h) = ifeq(codomain(b),domain(g),compose(domain(g),compose(b,h)),compose(b,h)) ).
cnf(u2285,hypothesis,
compose(compose(h,domain(a)),compose(a,b)) = ifeq(codomain(g),domain(a),compose(h,compose(a,b)),compose(compose(h,domain(a)),compose(a,b))) ).
cnf(u1015,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(codomain(X1),compose(a,b)),compose(codomain(X0),compose(a,b)),codomain(X1),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u3144,hypothesis,
compose(compose(a,b),b) = ifeq(codomain(b),domain(g),compose(compose(a,b),compose(codomain(b),b)),compose(compose(a,b),b)) ).
cnf(u6156,hypothesis,
compose(compose(codomain(X0),compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,g),compose(a,b))),compose(compose(codomain(X0),compose(a,g)),compose(a,b))),compose(compose(codomain(X0),compose(a,g)),compose(a,b))) ).
cnf(u2481,hypothesis,
domain(X1) = ifeq(domain(X1),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(domain(X1),compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),domain(X1)),domain(X1)),domain(X1)),domain(X1)) ).
cnf(u3444,hypothesis,
compose(compose(X0,codomain(X1)),compose(a,b)) = ifeq(codomain(X1),domain(a),ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X1),compose(a,b))),compose(compose(X0,codomain(X1)),compose(a,b))),compose(compose(X0,codomain(X1)),compose(a,b))) ).
cnf(u1747,hypothesis,
compose(compose(domain(X0),b),codomain(b)) = ifeq(domain(X0),domain(g),compose(domain(X0),b),compose(compose(domain(X0),b),codomain(b))) ).
cnf(u478,hypothesis,
domain(a) = ifeq(codomain(g),domain(X0),domain(compose(compose(a,g),domain(X0))),domain(a)) ).
cnf(u877,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(a,compose(a,b)),a,domain(X0)),domain(X0)),domain(X0)) ).
cnf(u2016,hypothesis,
compose(compose(a,g),h) = ifeq(codomain(g),domain(g),compose(domain(a),compose(compose(a,g),h)),compose(compose(a,g),h)) ).
cnf(u1399,hypothesis,
compose(compose(X1,h),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(X1),domain(g),compose(X1,compose(h,domain(X0))),compose(compose(X1,h),domain(X0))),compose(compose(X1,h),domain(X0))) ).
cnf(u234,hypothesis,
codomain(g) = ifeq(codomain(b),domain(g),codomain(compose(compose(a,b),h)),codomain(g)) ).
cnf(u1521,hypothesis,
codomain(X1) = ifeq(codomain(X1),domain(a),ifeq(compose(codomain(X1),compose(a,b)),X0,ifeq(compose(a,b),X0,domain(a),codomain(X1)),codomain(X1)),codomain(X1)) ).
cnf(u891,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(domain(X0),compose(a,b)),a,domain(X0)),domain(X0)),domain(X0)) ).
cnf(u875,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(h,compose(a,b)),h,a),a),a) ).
cnf(u4620,hypothesis,
compose(compose(compose(a,g),a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,compose(a,b))),compose(compose(compose(a,g),a),compose(a,b))),compose(compose(compose(a,g),a),compose(a,b))) ).
cnf(u3317,hypothesis,
compose(a,compose(a,g)) = ifeq(domain(g),domain(a),compose(a,compose(domain(g),compose(a,g))),compose(a,compose(a,g))) ).
cnf(codomain_composition,axiom,
compose(X0,codomain(X0)) = X0 ).
cnf(u3183,hypothesis,
compose(compose(domain(X1),domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),h)),compose(compose(domain(X1),domain(X0)),h)),compose(compose(domain(X1),domain(X0)),h)) ).
cnf(u2291,hypothesis,
compose(compose(domain(X0),domain(g)),b) = ifeq(domain(X0),domain(g),compose(domain(X0),b),compose(compose(domain(X0),domain(g)),b)) ).
cnf(u2046,hypothesis,
compose(compose(a,b),domain(X0)) = ifeq(codomain(b),domain(X0),compose(domain(a),compose(compose(a,b),domain(X0))),compose(compose(a,b),domain(X0))) ).
cnf(u2568,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),ifeq(compose(a,b),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),domain(a)),domain(a)),domain(a)) ).
cnf(u232,hypothesis,
codomain(g) = ifeq(codomain(X0),domain(g),codomain(compose(codomain(X0),h)),codomain(g)) ).
cnf(u3340,hypothesis,
compose(compose(compose(a,b),b),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,domain(X0))),compose(compose(compose(a,b),b),domain(X0))),compose(compose(compose(a,b),b),domain(X0))) ).
cnf(u1291,hypothesis,
compose(compose(X1,b),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(X1),domain(g),compose(X1,compose(b,domain(X0))),compose(compose(X1,b),domain(X0))),compose(compose(X1,b),domain(X0))) ).
cnf(u1406,hypothesis,
compose(compose(codomain(X0),h),X1) = ifeq(codomain(g),domain(X1),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,X1)),compose(compose(codomain(X0),h),X1)),compose(compose(codomain(X0),h),X1)) ).
cnf(u5,axiom,
codomain(X0) = domain(codomain(X0)) ).
cnf(u1922,hypothesis,
compose(compose(compose(a,b),compose(a,b)),codomain(b)) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,b)),compose(compose(compose(a,b),compose(a,b)),codomain(b))) ).
cnf(u273,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),domain(compose(domain(X0),compose(a,b))),domain(X0)) ).
cnf(u6199,hypothesis,
compose(compose(compose(a,g),codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),compose(a,b))),compose(compose(compose(a,g),codomain(X0)),compose(a,b))),compose(compose(compose(a,g),codomain(X0)),compose(a,b))) ).
cnf(u2300,hypothesis,
compose(compose(compose(a,g),domain(g)),h) = ifeq(codomain(g),domain(g),compose(compose(a,g),h),compose(compose(compose(a,g),domain(g)),h)) ).
cnf(u1787,axiom,
compose(compose(domain(X1),domain(X0)),domain(X0)) = ifeq(domain(X1),domain(X0),compose(domain(X1),domain(X0)),compose(compose(domain(X1),domain(X0)),domain(X0))) ).
cnf(u5303,hypothesis,
compose(compose(domain(compose(h,domain(X0))),h),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(domain(compose(h,domain(X0))),domain(g),compose(h,domain(X0)),compose(compose(domain(compose(h,domain(X0))),h),domain(X0))),compose(compose(domain(compose(h,domain(X0))),h),domain(X0))) ).
cnf(u3661,hypothesis,
compose(compose(domain(compose(b,h)),b),h) = ifeq(codomain(b),domain(g),ifeq(domain(compose(b,h)),domain(g),compose(b,h),compose(compose(domain(compose(b,h)),b),h)),compose(compose(domain(compose(b,h)),b),h)) ).
cnf(u3591,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3337,hypothesis,
compose(compose(domain(X0),b),domain(X1)) = ifeq(codomain(b),domain(X1),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,domain(X1))),compose(compose(domain(X0),b),domain(X1))),compose(compose(domain(X0),b),domain(X1))) ).
cnf(u1556,hypothesis,
compose(compose(h,h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(g),compose(h,compose(h,compose(a,b))),compose(compose(h,h),compose(a,b))),compose(compose(h,h),compose(a,b))) ).
cnf(u662,hypothesis,
codomain(b) = ifeq(codomain(b),domain(a),codomain(compose(compose(a,b),compose(a,b))),codomain(b)) ).
cnf(u1573,hypothesis,
domain(a) = ifeq(domain(X0),domain(a),ifeq(compose(a,b),compose(domain(X0),compose(a,b)),domain(X0),domain(a)),domain(a)) ).
cnf(u3846,hypothesis,
compose(compose(domain(compose(h,b)),h),b) = ifeq(codomain(g),domain(g),ifeq(domain(compose(h,b)),domain(g),compose(h,b),compose(compose(domain(compose(h,b)),h),b)),compose(compose(domain(compose(h,b)),h),b)) ).
cnf(u1805,axiom,
compose(compose(codomain(X1),domain(X0)),domain(X0)) = ifeq(codomain(X1),domain(X0),compose(codomain(X1),domain(X0)),compose(compose(codomain(X1),domain(X0)),domain(X0))) ).
cnf(u896,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(h,compose(a,b)),a,h),h),h) ).
cnf(u1679,axiom,
compose(compose(domain(X1),X2),codomain(X0)) = ifeq(codomain(X2),codomain(X0),ifeq(domain(X1),domain(X2),compose(domain(X1),compose(X2,codomain(X0))),compose(compose(domain(X1),X2),codomain(X0))),compose(compose(domain(X1),X2),codomain(X0))) ).
cnf(u1554,hypothesis,
compose(compose(h,h),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(g),domain(g),compose(h,compose(h,codomain(X0))),compose(compose(h,h),codomain(X0))),compose(compose(h,h),codomain(X0))) ).
cnf(u2073,axiom,
compose(domain(X0),codomain(X1)) = ifeq(domain(X0),codomain(X1),compose(domain(X0),compose(domain(X0),codomain(X1))),compose(domain(X0),codomain(X1))) ).
cnf(u1803,hypothesis,
compose(compose(codomain(X0),compose(a,g)),codomain(g)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,g)),compose(compose(codomain(X0),compose(a,g)),codomain(g))) ).
cnf(u4866,hypothesis,
compose(compose(domain(compose(codomain(X0),b)),codomain(X0)),b) = ifeq(codomain(X0),domain(g),ifeq(domain(compose(codomain(X0),b)),codomain(X0),compose(codomain(X0),b),compose(compose(domain(compose(codomain(X0),b)),codomain(X0)),b)),compose(compose(domain(compose(codomain(X0),b)),codomain(X0)),b)) ).
cnf(u3472,hypothesis,
compose(h,X0) = ifeq(codomain(g),domain(X0),compose(h,compose(codomain(g),X0)),compose(h,X0)) ).
cnf(u4386,axiom,
compose(compose(domain(compose(domain(X0),X1)),domain(X0)),X1) = ifeq(domain(X0),domain(X1),ifeq(domain(compose(domain(X0),X1)),domain(X0),compose(domain(X0),X1),compose(compose(domain(compose(domain(X0),X1)),domain(X0)),X1)),compose(compose(domain(compose(domain(X0),X1)),domain(X0)),X1)) ).
cnf(u1577,hypothesis,
domain(a) = ifeq(domain(g),domain(a),ifeq(compose(a,b),compose(a,compose(a,b)),a,domain(a)),domain(a)) ).
cnf(u1809,hypothesis,
compose(compose(compose(a,b),codomain(X0)),codomain(X0)) = ifeq(codomain(b),codomain(X0),compose(compose(a,b),codomain(X0)),compose(compose(compose(a,b),codomain(X0)),codomain(X0))) ).
cnf(u915,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(h,compose(a,b)),compose(a,b),h),h),h) ).
cnf(u1701,axiom,
compose(compose(codomain(X1),X0),codomain(X0)) = ifeq(codomain(X1),domain(X0),compose(codomain(X1),X0),compose(compose(codomain(X1),X0),codomain(X0))) ).
cnf(u2701,hypothesis,
compose(h,b) = ifeq(codomain(b),codomain(compose(h,b)),ifeq(codomain(g),domain(g),compose(h,compose(b,codomain(compose(h,b)))),compose(h,b)),compose(h,b)) ).
cnf(u3208,hypothesis,
compose(compose(compose(a,b),codomain(X0)),h) = ifeq(codomain(X0),domain(g),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),h)),compose(compose(compose(a,b),codomain(X0)),h)),compose(compose(compose(a,b),codomain(X0)),h)) ).
cnf(u1823,hypothesis,
compose(compose(compose(a,b),domain(X0)),domain(X0)) = ifeq(codomain(b),domain(X0),compose(compose(a,b),domain(X0)),compose(compose(compose(a,b),domain(X0)),domain(X0))) ).
cnf(u1682,hypothesis,
compose(compose(compose(a,b),X1),codomain(X0)) = ifeq(codomain(X1),codomain(X0),ifeq(codomain(b),domain(X1),compose(compose(a,b),compose(X1,codomain(X0))),compose(compose(compose(a,b),X1),codomain(X0))),compose(compose(compose(a,b),X1),codomain(X0))) ).
cnf(u300,axiom,
codomain(X1) = ifeq(domain(X0),codomain(X1),codomain(compose(domain(X0),codomain(X1))),codomain(X1)) ).
cnf(u1699,axiom,
compose(compose(X1,domain(X0)),codomain(X2)) = ifeq(domain(X0),codomain(X2),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),codomain(X2))),compose(compose(X1,domain(X0)),codomain(X2))),compose(compose(X1,domain(X0)),codomain(X2))) ).
cnf(u1153,hypothesis,
compose(compose(X0,h),b) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(g),compose(X0,compose(h,b)),compose(compose(X0,h),b)),compose(compose(X0,h),b)) ).
cnf(u3980,hypothesis,
compose(compose(a,g),domain(X0)) = ifeq(domain(X0),codomain(compose(compose(a,g),domain(X0))),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(domain(X0),codomain(compose(compose(a,g),domain(X0))))),compose(compose(a,g),domain(X0))),compose(compose(a,g),domain(X0))) ).
cnf(u150,hypothesis,
codomain(b) = ifeq(domain(g),domain(a),codomain(compose(a,compose(a,b))),codomain(b)) ).
cnf(u3104,hypothesis,
compose(compose(domain(X0),compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,b),b)),compose(compose(domain(X0),compose(a,b)),b)),compose(compose(domain(X0),compose(a,b)),b)) ).
cnf(u1408,hypothesis,
compose(compose(compose(a,b),h),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,X0)),compose(compose(compose(a,b),h),X0)),compose(compose(compose(a,b),h),X0)) ).
cnf(u650,hypothesis,
codomain(g) = ifeq(codomain(b),domain(a),codomain(compose(compose(a,b),compose(a,g))),codomain(g)) ).
cnf(u3228,hypothesis,
compose(compose(compose(a,g),domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(domain(X0),h)),compose(compose(compose(a,g),domain(X0)),h)),compose(compose(compose(a,g),domain(X0)),h)) ).
cnf(u2459,hypothesis,
compose(compose(compose(a,b),domain(a)),compose(a,g)) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,g)),compose(compose(compose(a,b),domain(a)),compose(a,g))) ).
cnf(u1446,hypothesis,
compose(compose(h,a),codomain(X0)) = ifeq(domain(g),codomain(X0),ifeq(codomain(g),domain(a),compose(h,compose(a,codomain(X0))),compose(compose(h,a),codomain(X0))),compose(compose(h,a),codomain(X0))) ).
cnf(u5068,hypothesis,
compose(compose(domain(compose(b,codomain(X0))),b),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(domain(compose(b,codomain(X0))),domain(g),compose(b,codomain(X0)),compose(compose(domain(compose(b,codomain(X0))),b),codomain(X0))),compose(compose(domain(compose(b,codomain(X0))),b),codomain(X0))) ).
cnf(u1951,axiom,
compose(compose(domain(compose(X0,X1)),X0),X1) = ifeq(codomain(X0),domain(X1),ifeq(domain(compose(X0,X1)),domain(X0),compose(X0,X1),compose(compose(domain(compose(X0,X1)),X0),X1)),compose(compose(domain(compose(X0,X1)),X0),X1)) ).
cnf(u2202,hypothesis,
compose(compose(a,b),compose(a,g)) = ifeq(codomain(b),domain(a),compose(domain(a),compose(compose(a,b),compose(a,g))),compose(compose(a,b),compose(a,g))) ).
cnf(u673,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(X0,compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,g),X0),X0),X0) = X0 ).
cnf(u428,hypothesis,
compose(compose(h,X0),X1) = ifeq(codomain(X0),domain(X1),ifeq(codomain(g),domain(X0),compose(h,compose(X0,X1)),compose(compose(h,X0),X1)),compose(compose(h,X0),X1)) ).
cnf(u62,axiom,
codomain(X1) = ifeq(domain(X0),domain(X1),codomain(compose(domain(X0),X1)),codomain(X1)) ).
cnf(u148,hypothesis,
domain(X0) = ifeq(domain(g),domain(X0),codomain(compose(a,domain(X0))),domain(X0)) ).
cnf(u2088,hypothesis,
compose(domain(X0),compose(a,g)) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(domain(X0),compose(a,g))),compose(domain(X0),compose(a,g))) ).
cnf(u3383,hypothesis,
compose(compose(codomain(X0),b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,compose(a,g))),compose(compose(codomain(X0),b),compose(a,g))),compose(compose(codomain(X0),b),compose(a,g))) ).
cnf(u3493,hypothesis,
compose(compose(a,g),codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(g),codomain(X0))),compose(compose(a,g),codomain(X0))) ).
cnf(u163,hypothesis,
domain(g) = ifeq(codomain(g),domain(a),domain(compose(h,compose(a,b))),domain(g)) ).
cnf(u1973,hypothesis,
compose(X0,compose(a,g)) = ifeq(codomain(X0),domain(a),compose(domain(X0),compose(X0,compose(a,g))),compose(X0,compose(a,g))) ).
cnf(u2480,hypothesis,
domain(X1) = ifeq(domain(X1),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(domain(X1),compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),domain(X1)),domain(X1)),domain(X1)),domain(X1)) ).
cnf(u418,axiom,
compose(compose(X0,X1),codomain(X2)) = ifeq(codomain(X1),codomain(X2),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,codomain(X2))),compose(compose(X0,X1),codomain(X2))),compose(compose(X0,X1),codomain(X2))) ).
cnf(u60,axiom,
domain(X0) = ifeq(domain(X0),domain(X1),domain(compose(domain(X0),X1)),domain(X0)) ).
cnf(u1971,axiom,
compose(X0,domain(X1)) = ifeq(codomain(X0),domain(X1),compose(domain(X0),compose(X0,domain(X1))),compose(X0,domain(X1))) ).
cnf(u190,hypothesis,
codomain(X0) = ifeq(codomain(b),domain(X0),codomain(compose(compose(a,b),X0)),codomain(X0)) ).
cnf(u1333,hypothesis,
compose(compose(domain(X0),b),b) = ifeq(codomain(b),domain(g),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,b)),compose(compose(domain(X0),b),b)),compose(compose(domain(X0),b),b)) ).
cnf(u1448,hypothesis,
compose(compose(h,a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),compose(h,compose(a,compose(a,b))),compose(compose(h,a),compose(a,b))),compose(compose(h,a),compose(a,b))) ).
cnf(u1082,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(domain(X0),compose(a,b)),X1,ifeq(compose(a,compose(a,b)),X1,a,domain(X0)),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u1977,hypothesis,
compose(b,X0) = ifeq(codomain(b),domain(X0),compose(domain(g),compose(b,X0)),compose(b,X0)) ).
cnf(u161,hypothesis,
domain(g) = ifeq(codomain(g),codomain(X0),domain(compose(h,codomain(X0))),domain(g)) ).
cnf(u940,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(a,b),domain(a),domain(X0)),domain(X0)) ).
cnf(u1206,hypothesis,
compose(compose(X1,domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),h)),compose(compose(X1,domain(X0)),h)),compose(compose(X1,domain(X0)),h)) ).
cnf(u6588,hypothesis,
compose(compose(domain(compose(compose(a,g),codomain(X0))),compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(domain(compose(compose(a,g),codomain(X0))),domain(a),compose(compose(a,g),codomain(X0)),compose(compose(domain(compose(compose(a,g),codomain(X0))),compose(a,g)),codomain(X0))),compose(compose(domain(compose(compose(a,g),codomain(X0))),compose(a,g)),codomain(X0))) ).
cnf(u1199,hypothesis,
compose(compose(h,X0),h) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(h,compose(X0,h)),compose(compose(h,X0),h)),compose(compose(h,X0),h)) ).
cnf(u50,hypothesis,
domain(a) = ifeq(domain(g),domain(X0),domain(compose(a,X0)),domain(a)) ).
cnf(u945,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(a,b),domain(a),h),h) ).
cnf(u188,hypothesis,
compose(a,b) = compose(compose(a,b),codomain(b)) ).
cnf(u1101,hypothesis,
compose(compose(h,a),X0) = ifeq(domain(g),domain(X0),ifeq(codomain(g),domain(a),compose(h,compose(a,X0)),compose(compose(h,a),X0)),compose(compose(h,a),X0)) ).
cnf(u5463,hypothesis,
compose(compose(a,b),compose(a,b)) = ifeq(codomain(b),codomain(compose(compose(a,b),compose(a,b))),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),codomain(compose(compose(a,b),compose(a,b))))),compose(compose(a,b),compose(a,b))),compose(compose(a,b),compose(a,b))) ).
cnf(u4528,hypothesis,
compose(compose(compose(a,b),compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),X0)),compose(compose(compose(a,b),compose(a,b)),X0)),compose(compose(compose(a,b),compose(a,b)),X0)) ).
cnf(u3716,hypothesis,
compose(compose(h,compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),codomain(X0))),compose(compose(h,compose(a,g)),codomain(X0))),compose(compose(h,compose(a,g)),codomain(X0))) ).
cnf(u1204,hypothesis,
compose(compose(X0,compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,g),h)),compose(compose(X0,compose(a,g)),h)),compose(compose(X0,compose(a,g)),h)) ).
cnf(u4667,hypothesis,
compose(compose(compose(a,b),compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),b)),compose(compose(compose(a,b),compose(a,g)),b)),compose(compose(compose(a,b),compose(a,g)),b)) ).
cnf(u1465,hypothesis,
compose(compose(h,compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),b)),compose(compose(h,compose(a,g)),b)),compose(compose(h,compose(a,g)),b)) ).
cnf(u1091,hypothesis,
compose(compose(X0,a),codomain(X1)) = ifeq(domain(g),codomain(X1),ifeq(codomain(X0),domain(a),compose(X0,compose(a,codomain(X1))),compose(compose(X0,a),codomain(X1))),compose(compose(X0,a),codomain(X1))) ).
cnf(u846,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(X0,compose(a,b)),compose(a,g),X0),X0),X0) = X0 ).
cnf(u1229,hypothesis,
compose(compose(a,g),X0) = ifeq(codomain(g),domain(X0),compose(a,compose(h,X0)),compose(compose(a,g),X0)) ).
cnf(u1360,hypothesis,
compose(compose(compose(a,g),b),h) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,h)),compose(compose(compose(a,g),b),h)),compose(compose(compose(a,g),b),h)) ).
cnf(u5596,hypothesis,
compose(compose(compose(a,b),compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),codomain(X0))),compose(compose(compose(a,b),compose(a,g)),codomain(X0))),compose(compose(compose(a,b),compose(a,g)),codomain(X0))) ).
cnf(u1118,hypothesis,
compose(compose(a,a),b) = ifeq(domain(g),domain(a),compose(a,compose(a,b)),compose(compose(a,a),b)) ).
cnf(u1297,hypothesis,
compose(compose(domain(X0),b),X1) = ifeq(codomain(b),domain(X1),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,X1)),compose(compose(domain(X0),b),X1)),compose(compose(domain(X0),b),X1)) ).
cnf(u1111,hypothesis,
compose(compose(a,a),g) = ifeq(domain(g),domain(a),compose(a,compose(a,g)),compose(compose(a,a),g)) ).
cnf(u3414,hypothesis,
compose(compose(X1,compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(X1),domain(a),compose(X1,compose(compose(a,g),domain(X0))),compose(compose(X1,compose(a,g)),domain(X0))),compose(compose(X1,compose(a,g)),domain(X0))) ).
cnf(u1373,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(domain(X0),compose(a,b)),X1,ifeq(compose(h,compose(a,b)),X1,h,domain(X0)),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u871,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(a,compose(a,b)),compose(codomain(X0),compose(a,b)),codomain(X0),a),a),a) ).
cnf(u1697,hypothesis,
compose(compose(X1,compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(X1),domain(a),compose(X1,compose(compose(a,g),codomain(X0))),compose(compose(X1,compose(a,g)),codomain(X0))),compose(compose(X1,compose(a,g)),codomain(X0))) ).
cnf(u6155,hypothesis,
compose(compose(codomain(X0),compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,b),compose(a,b))),compose(compose(codomain(X0),compose(a,b)),compose(a,b))),compose(compose(codomain(X0),compose(a,b)),compose(a,b))) ).
cnf(u3549,hypothesis,
codomain(X1) = ifeq(codomain(X1),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(codomain(X1),compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),codomain(X1)),codomain(X1)),codomain(X1)),codomain(X1)) ).
cnf(u201,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X0,ifeq(compose(X1,compose(a,b)),X0,X1,compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u980,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(domain(X1),compose(a,b)),compose(domain(X0),compose(a,b)),domain(X1),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u5331,hypothesis,
compose(compose(domain(compose(h,codomain(X0))),h),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(domain(compose(h,codomain(X0))),domain(g),compose(h,codomain(X0)),compose(compose(domain(compose(h,codomain(X0))),h),codomain(X0))),compose(compose(domain(compose(h,codomain(X0))),h),codomain(X0))) ).
cnf(u1246,hypothesis,
compose(compose(a,g),b) = ifeq(codomain(g),domain(g),compose(a,compose(h,b)),compose(compose(a,g),b)) ).
cnf(u1239,hypothesis,
compose(compose(a,b),compose(a,b)) = ifeq(codomain(b),domain(a),compose(a,compose(b,compose(a,b))),compose(compose(a,b),compose(a,b))) ).
cnf(u5228,hypothesis,
compose(compose(compose(a,b),h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,compose(a,b))),compose(compose(compose(a,b),h),compose(a,b))),compose(compose(compose(a,b),h),compose(a,b))) ).
cnf(u147,hypothesis,
codomain(X0) = ifeq(domain(g),codomain(X0),codomain(compose(a,codomain(X0))),codomain(X0)) ).
cnf(u1501,hypothesis,
compose(compose(h,b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(g),compose(h,compose(b,compose(a,b))),compose(compose(h,b),compose(a,b))),compose(compose(h,b),compose(a,b))) ).
cnf(u1120,hypothesis,
compose(compose(domain(X0),a),h) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,g)),compose(compose(domain(X0),a),h)) ).
cnf(u999,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(compose(a,b),compose(h,compose(a,b)),domain(a),h),h) ).
cnf(u3369,hypothesis,
compose(compose(domain(X0),b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,compose(a,b))),compose(compose(domain(X0),b),compose(a,b))),compose(compose(domain(X0),b),compose(a,b))) ).
cnf(u2709,hypothesis,
compose(compose(a,g),b) = ifeq(codomain(b),codomain(compose(compose(a,g),b)),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,codomain(compose(compose(a,g),b)))),compose(compose(a,g),b)),compose(compose(a,g),b)) ).
cnf(u207,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),X1),X1),X1),X1) = X1 ).
cnf(u1244,hypothesis,
compose(compose(a,g),compose(a,g)) = ifeq(codomain(g),domain(a),compose(a,compose(h,compose(a,g))),compose(compose(a,g),compose(a,g))) ).
cnf(u1731,hypothesis,
compose(compose(a,codomain(X0)),codomain(X0)) = ifeq(domain(g),codomain(X0),compose(a,codomain(X0)),compose(compose(a,codomain(X0)),codomain(X0))) ).
cnf(u2902,hypothesis,
compose(compose(codomain(X1),a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(a,domain(X0))),compose(compose(codomain(X1),a),domain(X0))),compose(compose(codomain(X1),a),domain(X0))) ).
cnf(u2000,hypothesis,
compose(h,b) = ifeq(codomain(g),domain(g),compose(domain(g),compose(h,b)),compose(h,b)) ).
cnf(u1505,hypothesis,
codomain(X2) = ifeq(codomain(X2),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(codomain(X2),compose(a,b)),X1,ifeq(compose(domain(X0),compose(a,b)),X1,domain(X0),codomain(X2)),codomain(X2)),codomain(X2)),codomain(X2)) ).
cnf(u2260,hypothesis,
compose(compose(X0,domain(a)),compose(a,b)) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,b)),compose(compose(X0,domain(a)),compose(a,b))) ).
cnf(u1491,hypothesis,
compose(compose(codomain(X0),h),h) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,h)),compose(compose(codomain(X0),h),h)),compose(compose(codomain(X0),h),h)) ).
cnf(u3301,hypothesis,
compose(compose(a,domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),compose(a,g))),compose(compose(a,domain(X0)),compose(a,g))),compose(compose(a,domain(X0)),compose(a,g))) ).
cnf(u119,hypothesis,
domain(g) = ifeq(codomain(b),domain(X0),domain(compose(b,domain(X0))),domain(g)) ).
cnf(u968,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(codomain(X1),compose(a,b)),codomain(X1),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u2230,axiom,
compose(compose(X1,domain(X2)),domain(X0)) = ifeq(domain(X2),domain(X0),ifeq(codomain(X1),domain(X2),compose(X1,compose(domain(X2),domain(X0))),compose(compose(X1,domain(X2)),domain(X0))),compose(compose(X1,domain(X2)),domain(X0))) ).
cnf(u3282,hypothesis,
compose(compose(a,compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),codomain(X0))),compose(compose(a,compose(a,g)),codomain(X0))),compose(compose(a,compose(a,g)),codomain(X0))) ).
cnf(u1576,hypothesis,
domain(a) = ifeq(codomain(b),domain(a),ifeq(compose(a,b),compose(compose(a,b),compose(a,b)),compose(a,b),domain(a)),domain(a)) ).
cnf(u7281,hypothesis,
compose(compose(domain(compose(compose(a,b),compose(a,g))),compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(domain(compose(compose(a,b),compose(a,g))),domain(a),compose(compose(a,b),compose(a,g)),compose(compose(domain(compose(compose(a,b),compose(a,g))),compose(a,b)),compose(a,g))),compose(compose(domain(compose(compose(a,b),compose(a,g))),compose(a,b)),compose(a,g))) ).
cnf(u4732,hypothesis,
compose(compose(a,compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),compose(a,g))),compose(compose(a,compose(a,b)),compose(a,g))),compose(compose(a,compose(a,b)),compose(a,g))) ).
cnf(u3036,hypothesis,
compose(compose(codomain(X0),a),codomain(X1)) = ifeq(domain(g),codomain(X1),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,codomain(X1))),compose(compose(codomain(X0),a),codomain(X1))),compose(compose(codomain(X0),a),codomain(X1))) ).
cnf(u1390,hypothesis,
compose(compose(h,X0),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(h,compose(X0,compose(a,b))),compose(compose(h,X0),compose(a,b))),compose(compose(h,X0),compose(a,b))) ).
cnf(u5704,hypothesis,
compose(compose(compose(a,b),domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(domain(X0),compose(a,g))),compose(compose(compose(a,b),domain(X0)),compose(a,g))),compose(compose(compose(a,b),domain(X0)),compose(a,g))) ).
cnf(u880,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(domain(g),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(a,compose(a,b)),a,compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u247,hypothesis,
codomain(b) = ifeq(codomain(g),domain(a),codomain(compose(h,compose(a,b))),codomain(b)) ).
cnf(u7290,hypothesis,
compose(compose(domain(compose(compose(a,g),compose(a,g))),compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(domain(compose(compose(a,g),compose(a,g))),domain(a),compose(compose(a,g),compose(a,g)),compose(compose(domain(compose(compose(a,g),compose(a,g))),compose(a,g)),compose(a,g))),compose(compose(domain(compose(compose(a,g),compose(a,g))),compose(a,g)),compose(a,g))) ).
cnf(u3073,hypothesis,
compose(compose(codomain(X0),a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,compose(a,b))),compose(compose(codomain(X0),a),compose(a,b))),compose(compose(codomain(X0),a),compose(a,b))) ).
cnf(u479,axiom,
codomain(X0) = ifeq(codomain(X0),domain(X1),domain(compose(codomain(X0),domain(X1))),codomain(X0)) ).
cnf(u1754,hypothesis,
compose(compose(domain(X0),a),domain(g)) = ifeq(domain(X0),domain(a),compose(domain(X0),a),compose(compose(domain(X0),a),domain(g))) ).
cnf(u2284,hypothesis,
compose(compose(h,domain(a)),compose(a,g)) = ifeq(codomain(g),domain(a),compose(h,compose(a,g)),compose(compose(h,domain(a)),compose(a,g))) ).
cnf(u3439,axiom,
compose(compose(codomain(X1),codomain(X2)),X0) = ifeq(codomain(X2),domain(X0),ifeq(codomain(X1),codomain(X2),compose(codomain(X1),compose(codomain(X2),X0)),compose(compose(codomain(X1),codomain(X2)),X0)),compose(compose(codomain(X1),codomain(X2)),X0)) ).
cnf(u1760,hypothesis,
compose(compose(domain(X0),h),codomain(g)) = ifeq(domain(X0),domain(g),compose(domain(X0),h),compose(compose(domain(X0),h),codomain(g))) ).
cnf(u3055,hypothesis,
compose(compose(domain(compose(a,X0)),a),X0) = ifeq(domain(g),domain(X0),ifeq(domain(compose(a,X0)),domain(a),compose(a,X0),compose(compose(domain(compose(a,X0)),a),X0)),compose(compose(domain(compose(a,X0)),a),X0)) ).
cnf(u1394,hypothesis,
compose(compose(h,h),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(g),compose(h,compose(h,X0)),compose(compose(h,h),X0)),compose(compose(h,h),X0)) ).
cnf(u3449,hypothesis,
compose(compose(compose(a,g),codomain(X1)),X0) = ifeq(codomain(X1),domain(X0),ifeq(codomain(g),codomain(X1),compose(compose(a,g),compose(codomain(X1),X0)),compose(compose(compose(a,g),codomain(X1)),X0)),compose(compose(compose(a,g),codomain(X1)),X0)) ).
cnf(u2299,hypothesis,
compose(compose(codomain(X0),domain(g)),h) = ifeq(codomain(X0),domain(g),compose(codomain(X0),h),compose(compose(codomain(X0),domain(g)),h)) ).
cnf(u2259,hypothesis,
compose(compose(X0,domain(a)),compose(a,g)) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,g)),compose(compose(X0,domain(a)),compose(a,g))) ).
cnf(u3958,hypothesis,
compose(codomain(X0),compose(a,b)) = ifeq(codomain(b),codomain(compose(codomain(X0),compose(a,b))),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,b),codomain(compose(codomain(X0),compose(a,b))))),compose(codomain(X0),compose(a,b))),compose(codomain(X0),compose(a,b))) ).
cnf(u2685,hypothesis,
compose(a,codomain(X0)) = ifeq(codomain(X0),codomain(compose(a,codomain(X0))),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),codomain(compose(a,codomain(X0))))),compose(a,codomain(X0))),compose(a,codomain(X0))) ).
cnf(u4615,hypothesis,
compose(compose(compose(a,b),a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,compose(a,g))),compose(compose(compose(a,b),a),compose(a,g))),compose(compose(compose(a,b),a),compose(a,g))) ).
cnf(u1555,hypothesis,
compose(compose(h,h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(g),compose(h,compose(h,compose(a,g))),compose(compose(h,h),compose(a,g))),compose(compose(h,h),compose(a,g))) ).
cnf(u3316,hypothesis,
compose(a,codomain(X0)) = ifeq(domain(g),codomain(X0),compose(a,compose(domain(g),codomain(X0))),compose(a,codomain(X0))) ).
cnf(u2683,hypothesis,
compose(a,compose(a,b)) = ifeq(codomain(b),codomain(compose(a,compose(a,b))),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),codomain(compose(a,compose(a,b))))),compose(a,compose(a,b))),compose(a,compose(a,b))) ).
cnf(domain_composition,axiom,
compose(domain(X0),X0) = X0 ).
cnf(u901,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(h,compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,b),h),h),h) ).
cnf(u6893,hypothesis,
compose(compose(compose(a,g),compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),compose(a,b))),compose(compose(compose(a,g),compose(a,b)),compose(a,b))),compose(compose(compose(a,g),compose(a,b)),compose(a,b))) ).
cnf(u1522,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X0,ifeq(compose(a,b),X0,domain(a),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u5121,hypothesis,
compose(compose(codomain(X1),compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(compose(a,g),domain(X0))),compose(compose(codomain(X1),compose(a,g)),domain(X0))),compose(compose(codomain(X1),compose(a,g)),domain(X0))) ).
cnf(u899,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(h,compose(a,b)),compose(codomain(X0),compose(a,b)),codomain(X0),h),h),h) ).
cnf(u1302,hypothesis,
compose(compose(h,b),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(g),compose(h,compose(b,X0)),compose(compose(h,b),X0)),compose(compose(h,b),X0)) ).
cnf(u29,axiom,
codomain(X0) = compose(codomain(X0),codomain(X0)) ).
cnf(u3450,hypothesis,
compose(compose(compose(a,b),codomain(X1)),X0) = ifeq(codomain(X1),domain(X0),ifeq(codomain(b),codomain(X1),compose(compose(a,b),compose(codomain(X1),X0)),compose(compose(compose(a,b),codomain(X1)),X0)),compose(compose(compose(a,b),codomain(X1)),X0)) ).
cnf(u1574,hypothesis,
domain(a) = ifeq(codomain(X0),domain(a),ifeq(compose(a,b),compose(codomain(X0),compose(a,b)),codomain(X0),domain(a)),domain(a)) ).
cnf(u3469,hypothesis,
compose(compose(a,g),X0) = ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(codomain(g),X0)),compose(compose(a,g),X0)) ).
cnf(u1306,hypothesis,
compose(compose(a,a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(domain(g),domain(a),compose(a,compose(a,domain(X0))),compose(compose(a,a),domain(X0))),compose(compose(a,a),domain(X0))) ).
cnf(u1520,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),X1,ifeq(compose(a,b),X1,domain(a),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u1300,hypothesis,
compose(compose(compose(a,b),b),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,X0)),compose(compose(compose(a,b),b),X0)),compose(compose(compose(a,b),b),X0)) ).
cnf(prove_h_equals_g,negated_conjecture,
h != g ).
cnf(u1430,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,g),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u157,hypothesis,
codomain(g) = ifeq(codomain(X0),domain(g),codomain(compose(X0,h)),codomain(g)) ).
cnf(u303,axiom,
codomain(X1) = ifeq(codomain(X0),codomain(X1),codomain(compose(codomain(X0),codomain(X1))),codomain(X1)) ).
cnf(u3473,hypothesis,
compose(h,domain(X0)) = ifeq(codomain(g),domain(X0),compose(h,compose(codomain(g),domain(X0))),compose(h,domain(X0))) ).
cnf(u1702,hypothesis,
compose(compose(compose(a,g),X0),codomain(X0)) = ifeq(codomain(g),domain(X0),compose(compose(a,g),X0),compose(compose(compose(a,g),X0),codomain(X0))) ).
cnf(u3715,hypothesis,
compose(compose(h,compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),codomain(X0))),compose(compose(h,compose(a,b)),codomain(X0))),compose(compose(h,compose(a,b)),codomain(X0))) ).
cnf(u2072,axiom,
compose(codomain(X0),codomain(X1)) = ifeq(codomain(X0),codomain(X1),compose(codomain(X0),compose(codomain(X0),codomain(X1))),compose(codomain(X0),codomain(X1))) ).
cnf(u671,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(X0,compose(a,b)),compose(domain(X1),compose(a,b)),domain(X1),X0),X0),X0) = X0 ).
cnf(u1434,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(domain(X0),compose(a,b)),compose(a,b),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u4769,hypothesis,
compose(compose(compose(a,b),b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,compose(a,g))),compose(compose(compose(a,b),b),compose(a,g))),compose(compose(compose(a,b),b),compose(a,g))) ).
cnf(codomain_of_a_equals_domain_of_g,hypothesis,
codomain(a) = domain(g) ).
cnf(u1428,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(codomain(X0),compose(a,b)),compose(a,g),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u3475,hypothesis,
compose(h,compose(a,g)) = ifeq(codomain(g),domain(a),compose(h,compose(codomain(g),compose(a,g))),compose(h,compose(a,g))) ).
cnf(u2718,hypothesis,
compose(compose(a,g),h) = ifeq(codomain(g),codomain(compose(compose(a,g),h)),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,codomain(compose(compose(a,g),h)))),compose(compose(a,g),h)),compose(compose(a,g),h)) ).
cnf(u301,axiom,
domain(X0) = ifeq(domain(X1),domain(X0),codomain(compose(domain(X1),domain(X0))),domain(X0)) ).
cnf(u431,hypothesis,
compose(compose(X0,compose(a,b)),X1) = ifeq(codomain(b),domain(X1),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,b),X1)),compose(compose(X0,compose(a,b)),X1)),compose(compose(X0,compose(a,b)),X1)) ).
cnf(u3735,hypothesis,
compose(compose(h,domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),compose(a,g))),compose(compose(h,domain(X0)),compose(a,g))),compose(compose(h,domain(X0)),compose(a,g))) ).
cnf(u3401,hypothesis,
compose(compose(compose(a,g),X1),domain(X0)) = ifeq(codomain(X1),domain(X0),ifeq(codomain(g),domain(X1),compose(compose(a,g),compose(X1,domain(X0))),compose(compose(compose(a,g),X1),domain(X0))),compose(compose(compose(a,g),X1),domain(X0))) ).
cnf(u1435,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(codomain(X0),compose(a,b)),compose(a,b),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u4621,hypothesis,
compose(compose(compose(a,b),a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,compose(a,b))),compose(compose(compose(a,b),a),compose(a,b))),compose(compose(compose(a,b),a),compose(a,b))) ).
cnf(u3631,hypothesis,
compose(compose(domain(compose(b,b)),b),b) = ifeq(codomain(b),domain(g),ifeq(domain(compose(b,b)),domain(g),compose(b,b),compose(compose(domain(compose(b,b)),b),b)),compose(compose(domain(compose(b,b)),b),b)) ).
cnf(u674,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(X0,compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,b),X0),X0),X0) = X0 ).
cnf(u1961,hypothesis,
compose(compose(domain(X1),compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(domain(X1),domain(a),compose(domain(X1),compose(compose(a,b),X0)),compose(compose(domain(X1),compose(a,b)),X0)),compose(compose(domain(X1),compose(a,b)),X0)) ).
cnf(u59,axiom,
codomain(X0) = ifeq(codomain(X0),domain(X1),domain(compose(codomain(X0),X1)),codomain(X0)) ).
cnf(u145,hypothesis,
codomain(b) = codomain(compose(a,b)) ).
cnf(u6725,hypothesis,
compose(compose(domain(compose(codomain(X0),compose(a,g))),codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(domain(compose(codomain(X0),compose(a,g))),codomain(X0),compose(codomain(X0),compose(a,g)),compose(compose(domain(compose(codomain(X0),compose(a,g))),codomain(X0)),compose(a,g))),compose(compose(domain(compose(codomain(X0),compose(a,g))),codomain(X0)),compose(a,g))) ).
cnf(u429,hypothesis,
compose(compose(X0,b),X1) = ifeq(codomain(b),domain(X1),ifeq(codomain(X0),domain(g),compose(X0,compose(b,X1)),compose(compose(X0,b),X1)),compose(compose(X0,b),X1)) ).
cnf(u680,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),compose(a,g),compose(a,g)),compose(a,g)) ).
cnf(u1975,hypothesis,
compose(X0,b) = ifeq(codomain(X0),domain(g),compose(domain(X0),compose(X0,b)),compose(X0,b)) ).
cnf(u929,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(domain(X0),compose(a,b)),domain(X0),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u4403,axiom,
compose(compose(codomain(X2),domain(X0)),domain(X1)) = ifeq(domain(X0),domain(X1),ifeq(codomain(X2),domain(X0),compose(codomain(X2),compose(domain(X0),domain(X1))),compose(compose(codomain(X2),domain(X0)),domain(X1))),compose(compose(codomain(X2),domain(X0)),domain(X1))) ).
cnf(u3583,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u1445,hypothesis,
compose(compose(h,a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(codomain(g),domain(a),compose(h,compose(a,domain(X0))),compose(compose(h,a),domain(X0))),compose(compose(h,a),domain(X0))) ).
cnf(u4451,hypothesis,
compose(compose(compose(a,b),X0),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(X0,compose(a,g))),compose(compose(compose(a,b),X0),compose(a,g))),compose(compose(compose(a,b),X0),compose(a,g))) ).
cnf(u943,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(a,b),domain(a),compose(a,b)),compose(a,b)) ).
cnf(u1194,hypothesis,
compose(compose(domain(X0),X1),h) = ifeq(codomain(X1),domain(g),ifeq(domain(X0),domain(X1),compose(domain(X0),compose(X1,h)),compose(compose(domain(X0),X1),h)),compose(compose(domain(X0),X1),h)) ).
cnf(u57,hypothesis,
domain(g) = ifeq(codomain(b),domain(X0),domain(compose(b,X0)),domain(g)) ).
cnf(u1468,hypothesis,
compose(compose(domain(X0),h),b) = ifeq(codomain(g),domain(g),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,b)),compose(compose(domain(X0),h),b)),compose(compose(domain(X0),h),b)) ).
cnf(u4242,axiom,
compose(compose(domain(compose(X0,codomain(X1))),X0),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(domain(compose(X0,codomain(X1))),domain(X0),compose(X0,codomain(X1)),compose(compose(domain(compose(X0,codomain(X1))),X0),codomain(X1))),compose(compose(domain(compose(X0,codomain(X1))),X0),codomain(X1))) ).
cnf(u419,hypothesis,
compose(compose(X0,X1),compose(a,g)) = ifeq(codomain(X1),domain(a),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,compose(a,g))),compose(compose(X0,X1),compose(a,g))),compose(compose(X0,X1),compose(a,g))) ).
cnf(u3964,hypothesis,
compose(compose(a,g),codomain(X0)) = ifeq(codomain(X0),codomain(compose(compose(a,g),codomain(X0))),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),codomain(compose(compose(a,g),codomain(X0))))),compose(compose(a,g),codomain(X0))),compose(compose(a,g),codomain(X0))) ).
cnf(u2668,hypothesis,
compose(compose(a,g),a) = ifeq(domain(g),codomain(compose(compose(a,g),a)),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,codomain(compose(compose(a,g),a)))),compose(compose(a,g),a)),compose(compose(a,g),a)) ).
cnf(u3519,hypothesis,
compose(compose(a,g),compose(a,g)) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(codomain(g),compose(a,g))),compose(compose(a,g),compose(a,g))) ).
cnf(u2662,hypothesis,
compose(X0,compose(a,b)) = ifeq(codomain(b),codomain(compose(X0,compose(a,b))),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,b),codomain(compose(X0,compose(a,b))))),compose(X0,compose(a,b))),compose(X0,compose(a,b))) ).
cnf(u5452,hypothesis,
compose(compose(a,g),compose(a,g)) = ifeq(codomain(g),codomain(compose(compose(a,g),compose(a,g))),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),codomain(compose(compose(a,g),compose(a,g))))),compose(compose(a,g),compose(a,g))),compose(compose(a,g),compose(a,g))) ).
cnf(u162,hypothesis,
domain(g) = ifeq(codomain(g),domain(a),domain(compose(h,compose(a,g))),domain(g)) ).
cnf(u2729,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X1,ifeq(compose(codomain(X0),compose(a,b)),X1,codomain(X0),compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u1203,hypothesis,
compose(compose(X0,compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,b),h)),compose(compose(X0,compose(a,b)),h)),compose(compose(X0,compose(a,b)),h)) ).
cnf(u3093,hypothesis,
compose(compose(domain(compose(X0,b)),X0),b) = ifeq(codomain(X0),domain(g),ifeq(domain(compose(X0,b)),domain(X0),compose(X0,b),compose(compose(domain(compose(X0,b)),X0),b)),compose(compose(domain(compose(X0,b)),X0),b)) ).
cnf(u63,axiom,
codomain(X1) = ifeq(codomain(X0),domain(X1),codomain(compose(codomain(X0),X1)),codomain(X1)) ).
cnf(u1974,hypothesis,
compose(X0,compose(a,b)) = ifeq(codomain(X0),domain(a),compose(domain(X0),compose(X0,compose(a,b))),compose(X0,compose(a,b))) ).
cnf(u1717,axiom,
compose(compose(X1,domain(X0)),domain(X0)) = ifeq(codomain(X1),domain(X0),compose(X1,domain(X0)),compose(compose(X1,domain(X0)),domain(X0))) ).
cnf(u841,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(X0,compose(a,b)),compose(compose(a,b),compose(a,b)),X0,compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u2730,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X1,ifeq(compose(codomain(X0),compose(a,b)),X1,codomain(X0),compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u1980,hypothesis,
compose(compose(a,g),X0) = ifeq(codomain(g),domain(X0),compose(domain(a),compose(compose(a,g),X0)),compose(compose(a,g),X0)) ).
cnf(u4775,hypothesis,
compose(compose(compose(a,g),b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,compose(a,b))),compose(compose(compose(a,g),b),compose(a,b))),compose(compose(compose(a,g),b),compose(a,b))) ).
cnf(u3761,hypothesis,
compose(compose(domain(X0),h),codomain(X1)) = ifeq(codomain(g),codomain(X1),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,codomain(X1))),compose(compose(domain(X0),h),codomain(X1))),compose(compose(domain(X0),h),codomain(X1))) ).
cnf(u1978,hypothesis,
compose(h,X0) = ifeq(codomain(g),domain(X0),compose(domain(g),compose(h,X0)),compose(h,X0)) ).
cnf(u964,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(a,compose(a,b)),X0,a,a),a),a),a) ).
cnf(u1230,hypothesis,
compose(compose(a,g),domain(X0)) = ifeq(codomain(g),domain(X0),compose(a,compose(g,domain(X0))),compose(compose(a,g),domain(X0))) ).
cnf(u3402,hypothesis,
compose(compose(compose(a,b),X1),domain(X0)) = ifeq(codomain(X1),domain(X0),ifeq(codomain(b),domain(X1),compose(compose(a,b),compose(X1,domain(X0))),compose(compose(compose(a,b),X1),domain(X0))),compose(compose(compose(a,b),X1),domain(X0))) ).
cnf(u969,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(codomain(X1),compose(a,b)),codomain(X1),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u1115,hypothesis,
compose(compose(codomain(X0),a),b) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,b)),compose(compose(codomain(X0),a),b)) ).
cnf(u3526,hypothesis,
compose(compose(a,b),compose(a,b)) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(codomain(b),compose(a,b))),compose(compose(a,b),compose(a,b))) ).
cnf(u2253,hypothesis,
compose(compose(compose(a,b),domain(X0)),X0) = ifeq(codomain(b),domain(X0),compose(compose(a,b),X0),compose(compose(compose(a,b),domain(X0)),X0)) ).
cnf(u3784,hypothesis,
compose(compose(domain(compose(h,X0)),h),X0) = ifeq(codomain(g),domain(X0),ifeq(domain(compose(h,X0)),domain(g),compose(h,X0),compose(compose(domain(compose(h,X0)),h),X0)),compose(compose(domain(compose(h,X0)),h),X0)) ).
cnf(u4733,hypothesis,
compose(compose(a,compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),compose(a,g))),compose(compose(a,compose(a,g)),compose(a,g))),compose(compose(a,compose(a,g)),compose(a,g))) ).
cnf(u3961,axiom,
compose(codomain(X1),domain(X0)) = ifeq(domain(X0),codomain(compose(codomain(X1),domain(X0))),ifeq(codomain(X1),domain(X0),compose(codomain(X1),compose(domain(X0),codomain(compose(codomain(X1),domain(X0))))),compose(codomain(X1),domain(X0))),compose(codomain(X1),domain(X0))) ).
cnf(u5227,hypothesis,
compose(compose(compose(a,g),h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,compose(a,b))),compose(compose(compose(a,g),h),compose(a,b))),compose(compose(compose(a,g),h),compose(a,b))) ).
cnf(u3796,hypothesis,
compose(compose(codomain(X0),h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,compose(a,b))),compose(compose(codomain(X0),h),compose(a,b))),compose(compose(codomain(X0),h),compose(a,b))) ).
cnf(u2656,hypothesis,
compose(compose(a,g),X0) = ifeq(codomain(X0),codomain(compose(compose(a,g),X0)),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(X0,codomain(compose(compose(a,g),X0)))),compose(compose(a,g),X0)),compose(compose(a,g),X0)) ).
cnf(u3941,axiom,
compose(domain(X1),domain(X0)) = ifeq(domain(X0),codomain(compose(domain(X1),domain(X0))),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),codomain(compose(domain(X1),domain(X0))))),compose(domain(X1),domain(X0))),compose(domain(X1),domain(X0))) ).
cnf(u845,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(codomain(X1),compose(a,b)),compose(X0,compose(a,b)),codomain(X1),X0),X0),X0) = X0 ).
cnf(u72,hypothesis,
domain(a) = ifeq(domain(g),codomain(X0),domain(compose(a,codomain(X0))),domain(a)) ).
cnf(u1367,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),h),h),h),h) ).
cnf(u202,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(X1,compose(a,b)),X0,X1,a),a),a),a) ).
cnf(u963,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),a),a),a),a) ).
cnf(u3939,hypothesis,
compose(domain(X0),compose(a,g)) = ifeq(codomain(g),codomain(compose(domain(X0),compose(a,g))),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,g),codomain(compose(domain(X0),compose(a,g))))),compose(domain(X0),compose(a,g))),compose(domain(X0),compose(a,g))) ).
cnf(u843,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(X0,compose(a,b)),compose(h,compose(a,b)),X0,h),h),h) ).
cnf(u1232,hypothesis,
compose(compose(a,g),compose(a,g)) = ifeq(codomain(g),domain(a),compose(a,compose(g,compose(a,g))),compose(compose(a,g),compose(a,g))) ).
cnf(u103,hypothesis,
domain(g) = ifeq(codomain(b),domain(g),domain(compose(b,b)),domain(g)) ).
cnf(u2658,hypothesis,
compose(a,X0) = ifeq(codomain(X0),codomain(compose(a,X0)),ifeq(domain(g),domain(X0),compose(a,compose(X0,codomain(compose(a,X0)))),compose(a,X0)),compose(a,X0)) ).
cnf(u3151,hypothesis,
compose(compose(compose(a,b),domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(domain(X0),b)),compose(compose(compose(a,b),domain(X0)),b)),compose(compose(compose(a,b),domain(X0)),b)) ).
cnf(u4938,hypothesis,
compose(compose(domain(compose(domain(X0),h)),domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(domain(compose(domain(X0),h)),domain(X0),compose(domain(X0),h),compose(compose(domain(compose(domain(X0),h)),domain(X0)),h)),compose(compose(domain(compose(domain(X0),h)),domain(X0)),h)) ).
cnf(u1298,hypothesis,
compose(compose(codomain(X0),b),X1) = ifeq(codomain(b),domain(X1),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,X1)),compose(compose(codomain(X0),b),X1)),compose(compose(codomain(X0),b),X1)) ).
cnf(u3181,hypothesis,
compose(compose(domain(X0),compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,g),h)),compose(compose(domain(X0),compose(a,g)),h)),compose(compose(domain(X0),compose(a,g)),h)) ).
cnf(u2664,axiom,
compose(X0,codomain(X1)) = ifeq(codomain(X1),codomain(compose(X0,codomain(X1))),ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X1),codomain(compose(X0,codomain(X1))))),compose(X0,codomain(X1))),compose(X0,codomain(X1))) ).
cnf(u3959,hypothesis,
compose(codomain(X0),compose(a,g)) = ifeq(codomain(g),codomain(compose(codomain(X0),compose(a,g))),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,g),codomain(compose(codomain(X0),compose(a,g))))),compose(codomain(X0),compose(a,g))),compose(codomain(X0),compose(a,g))) ).
cnf(u1507,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X1,ifeq(compose(domain(X0),compose(a,b)),X1,domain(X0),compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u200,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X0,ifeq(compose(X1,compose(a,b)),X0,X1,compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3289,hypothesis,
compose(compose(a,codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),compose(a,g))),compose(compose(a,codomain(X0)),compose(a,g))),compose(compose(a,codomain(X0)),compose(a,g))) ).
cnf(u2020,hypothesis,
compose(b,domain(X0)) = ifeq(codomain(b),domain(X0),compose(domain(g),compose(b,domain(X0))),compose(b,domain(X0))) ).
cnf(u1387,hypothesis,
compose(compose(h,X0),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(codomain(g),domain(X0),compose(h,compose(X0,domain(X1))),compose(compose(h,X0),domain(X1))),compose(compose(h,X0),domain(X1))) ).
cnf(u2286,hypothesis,
compose(compose(h,domain(g)),b) = ifeq(codomain(g),domain(g),compose(h,b),compose(compose(h,domain(g)),b)) ).
cnf(u6096,hypothesis,
compose(compose(compose(a,b),compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),domain(X0))),compose(compose(compose(a,b),compose(a,g)),domain(X0))),compose(compose(compose(a,b),compose(a,g)),domain(X0))) ).
cnf(u971,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(codomain(X0),compose(a,b)),codomain(X0),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u1374,hypothesis,
codomain(X1) = ifeq(codomain(X1),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(codomain(X1),compose(a,b)),X0,ifeq(compose(h,compose(a,b)),X0,h,codomain(X1)),codomain(X1)),codomain(X1)),codomain(X1)) ).
cnf(u1757,hypothesis,
compose(compose(compose(a,b),a),domain(g)) = ifeq(codomain(b),domain(a),compose(compose(a,b),a),compose(compose(compose(a,b),a),domain(g))) ).
cnf(u231,hypothesis,
codomain(g) = ifeq(domain(X0),domain(g),codomain(compose(domain(X0),h)),codomain(g)) ).
cnf(u2018,hypothesis,
compose(domain(X0),h) = ifeq(domain(X0),domain(g),compose(domain(X0),compose(domain(X0),h)),compose(domain(X0),h)) ).
cnf(u5190,hypothesis,
compose(compose(h,compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),compose(a,g))),compose(compose(h,compose(a,g)),compose(a,g))),compose(compose(h,compose(a,g)),compose(a,g))) ).
cnf(u1755,hypothesis,
compose(compose(codomain(X0),a),domain(g)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),a),compose(compose(codomain(X0),a),domain(g))) ).
cnf(u885,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(a,compose(a,b)),codomain(X0),a),a),a) ).
cnf(u1407,hypothesis,
compose(compose(compose(a,g),h),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,X0)),compose(compose(compose(a,g),h),X0)),compose(compose(compose(a,g),h),X0)) ).
cnf(u5574,hypothesis,
compose(compose(compose(a,g),compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),codomain(X0))),compose(compose(compose(a,g),compose(a,b)),codomain(X0))),compose(compose(compose(a,g),compose(a,b)),codomain(X0))) ).
cnf(u1744,hypothesis,
compose(compose(h,compose(a,g)),codomain(g)) = ifeq(codomain(g),domain(a),compose(h,compose(a,g)),compose(compose(h,compose(a,g)),codomain(g))) ).
cnf(u3290,hypothesis,
compose(compose(a,codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),compose(a,b))),compose(compose(a,codomain(X0)),compose(a,b))),compose(compose(a,codomain(X0)),compose(a,b))) ).
cnf(u1761,hypothesis,
compose(compose(codomain(X0),h),codomain(g)) = ifeq(codomain(X0),domain(g),compose(codomain(X0),h),compose(compose(codomain(X0),h),codomain(g))) ).
cnf(u4468,hypothesis,
compose(compose(compose(a,g),X0),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(X0,compose(a,b))),compose(compose(compose(a,g),X0),compose(a,b))),compose(compose(compose(a,g),X0),compose(a,b))) ).
cnf(u1984,hypothesis,
compose(a,codomain(X0)) = ifeq(domain(g),codomain(X0),compose(domain(a),compose(a,codomain(X0))),compose(a,codomain(X0))) ).
cnf(u1541,hypothesis,
domain(a) = ifeq(compose(a,b),X0,ifeq(compose(a,b),X0,domain(a),domain(a)),domain(a)) ).
cnf(u2669,hypothesis,
compose(compose(a,b),a) = ifeq(domain(g),codomain(compose(compose(a,b),a)),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,codomain(compose(compose(a,b),a)))),compose(compose(a,b),a)),compose(compose(a,b),a)) ).
cnf(u1121,hypothesis,
compose(compose(codomain(X0),a),h) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,g)),compose(compose(codomain(X0),a),h)) ).
cnf(u484,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),domain(compose(codomain(X0),compose(a,b))),codomain(X0)) ).
cnf(u2667,hypothesis,
compose(codomain(X0),a) = ifeq(domain(g),codomain(compose(codomain(X0),a)),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,codomain(compose(codomain(X0),a)))),compose(codomain(X0),a)),compose(codomain(X0),a)) ).
cnf(u4359,axiom,
compose(compose(domain(X1),domain(X0)),domain(X2)) = ifeq(domain(X0),domain(X2),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),domain(X2))),compose(compose(domain(X1),domain(X0)),domain(X2))),compose(compose(domain(X1),domain(X0)),domain(X2))) ).
cnf(u1506,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X1,ifeq(compose(domain(X0),compose(a,b)),X1,domain(X0),compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3315,hypothesis,
compose(a,domain(X0)) = ifeq(domain(g),domain(X0),compose(a,compose(domain(g),domain(X0))),compose(a,domain(X0))) ).
cnf(u13,axiom,
compose(compose(X2,X0),X1) = ifeq(codomain(X0),domain(X1),ifeq(codomain(X2),domain(X0),compose(X2,compose(X0,X1)),compose(compose(X2,X0),X1)),compose(compose(X2,X0),X1)) ).
cnf(u219,hypothesis,
domain(g) = ifeq(domain(X0),domain(a),codomain(compose(domain(X0),a)),domain(g)) ).
cnf(u28,hypothesis,
b = compose(domain(g),b) ).
cnf(u2029,hypothesis,
compose(h,compose(a,b)) = ifeq(codomain(g),domain(a),compose(domain(g),compose(h,compose(a,b))),compose(h,compose(a,b))) ).
cnf(u6894,hypothesis,
compose(compose(compose(a,g),compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),compose(a,b))),compose(compose(compose(a,g),compose(a,g)),compose(a,b))),compose(compose(compose(a,g),compose(a,g)),compose(a,b))) ).
cnf(u513,hypothesis,
domain(X0) = ifeq(codomain(g),domain(X0),codomain(compose(compose(a,g),domain(X0))),domain(X0)) ).
cnf(u268,axiom,
codomain(X0) = ifeq(codomain(X0),codomain(X1),domain(compose(codomain(X0),codomain(X1))),codomain(X0)) ).
cnf(u5398,hypothesis,
compose(compose(domain(compose(b,compose(a,b))),b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(domain(compose(b,compose(a,b))),domain(g),compose(b,compose(a,b)),compose(compose(domain(compose(b,compose(a,b))),b),compose(a,b))),compose(compose(domain(compose(b,compose(a,b))),b),compose(a,b))) ).
cnf(u2027,hypothesis,
compose(h,codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(domain(g),compose(h,codomain(X0))),compose(h,codomain(X0))) ).
cnf(u4357,hypothesis,
compose(compose(domain(X1),compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(domain(X1),domain(a),compose(domain(X1),compose(compose(a,g),domain(X0))),compose(compose(domain(X1),compose(a,g)),domain(X0))),compose(compose(domain(X1),compose(a,g)),domain(X0))) ).
cnf(u1784,hypothesis,
compose(compose(domain(X0),compose(a,b)),codomain(b)) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,b)),compose(compose(domain(X0),compose(a,b)),codomain(b))) ).
cnf(u3207,hypothesis,
compose(compose(compose(a,g),codomain(X0)),h) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),h)),compose(compose(compose(a,g),codomain(X0)),h)),compose(compose(compose(a,g),codomain(X0)),h)) ).
cnf(u898,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(h,compose(a,b)),compose(domain(X0),compose(a,b)),domain(X0),h),h),h) ).
cnf(u1504,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(domain(X0),compose(a,b)),X2,ifeq(compose(domain(X1),compose(a,b)),X2,domain(X1),domain(X0)),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u2287,hypothesis,
compose(compose(h,domain(g)),h) = ifeq(codomain(g),domain(g),compose(h,h),compose(compose(h,domain(g)),h)) ).
cnf(u3,axiom,
domain(X0) = codomain(domain(X0)) ).
cnf(u1414,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,g),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u141,hypothesis,
domain(a) = ifeq(codomain(g),domain(g),domain(compose(compose(a,g),b)),domain(a)) ).
cnf(u2320,hypothesis,
compose(compose(domain(X0),domain(a)),compose(a,b)) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,b)),compose(compose(domain(X0),domain(a)),compose(a,b))) ).
cnf(u2047,hypothesis,
compose(compose(a,g),domain(X0)) = ifeq(codomain(g),domain(X0),compose(domain(a),compose(compose(a,g),domain(X0))),compose(compose(a,g),domain(X0))) ).
cnf(u2298,hypothesis,
compose(compose(domain(X0),domain(g)),h) = ifeq(domain(X0),domain(g),compose(domain(X0),h),compose(compose(domain(X0),domain(g)),h)) ).
cnf(u7308,hypothesis,
compose(compose(domain(compose(compose(a,g),compose(a,b))),compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(domain(compose(compose(a,g),compose(a,b))),domain(a),compose(compose(a,g),compose(a,b)),compose(compose(domain(compose(compose(a,g),compose(a,b))),compose(a,g)),compose(a,b))),compose(compose(domain(compose(compose(a,g),compose(a,b))),compose(a,g)),compose(a,b))) ).
cnf(u30,hypothesis,
a = compose(a,domain(g)) ).
cnf(u5126,hypothesis,
compose(compose(compose(a,g),codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),domain(X1))),compose(compose(compose(a,g),codomain(X0)),domain(X1))),compose(compose(compose(a,g),codomain(X0)),domain(X1))) ).
cnf(u1157,hypothesis,
compose(compose(X0,codomain(X1)),b) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X1),b)),compose(compose(X0,codomain(X1)),b)),compose(compose(X0,codomain(X1)),b)) ).
cnf(u3200,hypothesis,
compose(compose(codomain(X0),compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,b),h)),compose(compose(codomain(X0),compose(a,b)),h)),compose(compose(codomain(X0),compose(a,b)),h)) ).
cnf(u3351,hypothesis,
compose(compose(codomain(X0),b),codomain(X1)) = ifeq(codomain(b),codomain(X1),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,codomain(X1))),compose(compose(codomain(X0),b),codomain(X1))),compose(compose(codomain(X0),b),codomain(X1))) ).
cnf(u4340,axiom,
compose(compose(domain(compose(X0,domain(X1))),X0),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(domain(compose(X0,domain(X1))),domain(X0),compose(X0,domain(X1)),compose(compose(domain(compose(X0,domain(X1))),X0),domain(X1))),compose(compose(domain(compose(X0,domain(X1))),X0),domain(X1))) ).
cnf(ifeq_axiom,axiom,
ifeq(X0,X0,X1,X2) = X1 ).
cnf(u1309,hypothesis,
compose(compose(a,a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(domain(g),domain(a),compose(a,compose(a,compose(a,b))),compose(compose(a,a),compose(a,b))),compose(compose(a,a),compose(a,b))) ).
cnf(u2702,hypothesis,
compose(h,h) = ifeq(codomain(g),codomain(compose(h,h)),ifeq(codomain(g),domain(g),compose(h,compose(h,codomain(compose(h,h)))),compose(h,h)),compose(h,h)) ).
cnf(u415,hypothesis,
compose(compose(X0,a),X1) = ifeq(domain(g),domain(X1),ifeq(codomain(X0),domain(a),compose(X0,compose(a,X1)),compose(compose(X0,a),X1)),compose(compose(X0,a),X1)) ).
cnf(u3584,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u3124,hypothesis,
compose(compose(codomain(X0),compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,g),b)),compose(compose(codomain(X0),compose(a,g)),b)),compose(compose(codomain(X0),compose(a,g)),b)) ).
cnf(u2708,hypothesis,
compose(codomain(X0),b) = ifeq(codomain(b),codomain(compose(codomain(X0),b)),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,codomain(compose(codomain(X0),b)))),compose(codomain(X0),b)),compose(codomain(X0),b)) ).
cnf(u158,hypothesis,
domain(g) = ifeq(codomain(g),domain(g),domain(compose(h,b)),domain(g)) ).
cnf(u4493,hypothesis,
compose(compose(compose(a,g),compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),X0)),compose(compose(compose(a,g),compose(a,g)),X0)),compose(compose(compose(a,g),compose(a,g)),X0)) ).
cnf(u1416,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,g),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u1623,hypothesis,
domain(a) = ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(a,b),a,domain(a)),domain(a)) ).
cnf(u6710,hypothesis,
compose(compose(domain(compose(compose(a,g),domain(X0))),compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(domain(compose(compose(a,g),domain(X0))),domain(a),compose(compose(a,g),domain(X0)),compose(compose(domain(compose(compose(a,g),domain(X0))),compose(a,g)),domain(X0))),compose(compose(domain(compose(compose(a,g),domain(X0))),compose(a,g)),domain(X0))) ).
cnf(u908,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(h,compose(a,b)),h,compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u2215,hypothesis,
compose(compose(a,g),compose(a,b)) = ifeq(codomain(g),domain(a),compose(domain(a),compose(compose(a,g),compose(a,b))),compose(compose(a,g),compose(a,b))) ).
cnf(u298,hypothesis,
codomain(b) = ifeq(domain(X0),domain(a),codomain(compose(domain(X0),compose(a,b))),codomain(b)) ).
cnf(u3461,axiom,
compose(X1,domain(X0)) = ifeq(codomain(X1),domain(X0),compose(X1,compose(codomain(X1),domain(X0))),compose(X1,domain(X0))) ).
cnf(ah_equals_ag,hypothesis,
compose(a,h) = compose(a,g) ).
cnf(u913,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(h,compose(a,b)),codomain(X0),h),h),h) ).
cnf(u156,hypothesis,
domain(g) = ifeq(codomain(g),domain(X0),domain(compose(h,X0)),domain(g)) ).
cnf(u5166,hypothesis,
compose(compose(domain(compose(a,compose(a,g))),a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(domain(compose(a,compose(a,g))),domain(a),compose(a,compose(a,g)),compose(compose(domain(compose(a,compose(a,g))),a),compose(a,g))),compose(compose(domain(compose(a,compose(a,g))),a),compose(a,g))) ).
cnf(u1197,hypothesis,
compose(compose(compose(a,b),X0),h) = ifeq(codomain(X0),domain(g),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(X0,h)),compose(compose(compose(a,b),X0),h)),compose(compose(compose(a,b),X0),h)) ).
cnf(u1328,hypothesis,
compose(compose(a,compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),b)),compose(compose(a,compose(a,g)),b)),compose(compose(a,compose(a,g)),b)) ).
cnf(u927,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(domain(X1),compose(a,b)),domain(X1),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u5667,hypothesis,
compose(compose(domain(X0),compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,b),compose(a,b))),compose(compose(domain(X0),compose(a,b)),compose(a,b))),compose(compose(domain(X0),compose(a,b)),compose(a,b))) ).
cnf(u426,hypothesis,
compose(compose(compose(a,b),X0),X1) = ifeq(codomain(X0),domain(X1),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(X0,X1)),compose(compose(compose(a,b),X0),X1)),compose(compose(compose(a,b),X0),X1)) ).
cnf(u146,hypothesis,
codomain(g) = ifeq(domain(g),domain(a),codomain(compose(a,compose(a,g))),codomain(g)) ).
cnf(u942,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(a,b),domain(a),compose(a,g)),compose(a,g)) ).
cnf(u1084,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X0,ifeq(compose(a,compose(a,b)),X0,a,compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u5646,hypothesis,
compose(compose(domain(X0),compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,b),compose(a,g))),compose(compose(domain(X0),compose(a,b)),compose(a,g))),compose(compose(domain(X0),compose(a,b)),compose(a,g))) ).
cnf(u1214,hypothesis,
compose(compose(a,X0),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(domain(g),domain(X0),compose(a,compose(X0,domain(X1))),compose(compose(a,X0),domain(X1))),compose(compose(a,X0),domain(X1))) ).
cnf(u668,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(X0,compose(a,b)),X0,compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u2214,hypothesis,
compose(compose(a,b),compose(a,b)) = ifeq(codomain(b),domain(a),compose(domain(a),compose(compose(a,b),compose(a,b))),compose(compose(a,b),compose(a,b))) ).
cnf(u424,axiom,
compose(compose(codomain(X0),X1),X2) = ifeq(codomain(X1),domain(X2),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(X1,X2)),compose(compose(codomain(X0),X1),X2)),compose(compose(codomain(X0),X1),X2)) ).
cnf(u6906,hypothesis,
compose(compose(compose(a,b),compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),compose(a,b))),compose(compose(compose(a,b),compose(a,g)),compose(a,b))),compose(compose(compose(a,b),compose(a,g)),compose(a,b))) ).
cnf(u3762,hypothesis,
compose(compose(codomain(X0),h),codomain(X1)) = ifeq(codomain(g),codomain(X1),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,codomain(X1))),compose(compose(codomain(X0),h),codomain(X1))),compose(compose(codomain(X0),h),codomain(X1))) ).
cnf(u1964,axiom,
compose(compose(domain(X1),domain(X0)),X2) = ifeq(domain(X0),domain(X2),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),X2)),compose(compose(domain(X1),domain(X0)),X2)),compose(compose(domain(X1),domain(X0)),X2)) ).
cnf(u683,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),h,h),h) ).
cnf(u2237,axiom,
compose(compose(codomain(X2),domain(X1)),X0) = ifeq(domain(X1),domain(X0),ifeq(codomain(X2),domain(X1),compose(codomain(X2),compose(domain(X1),X0)),compose(compose(codomain(X2),domain(X1)),X0)),compose(compose(codomain(X2),domain(X1)),X0)) ).
cnf(u839,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(X1,compose(a,b)),compose(codomain(X0),compose(a,b)),X1,codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u1962,hypothesis,
compose(compose(domain(X1),compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(domain(X1),domain(a),compose(domain(X1),compose(compose(a,g),X0)),compose(compose(domain(X1),compose(a,g)),X0)),compose(compose(domain(X1),compose(a,g)),X0)) ).
cnf(u3721,hypothesis,
compose(compose(h,codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),compose(a,g))),compose(compose(h,codomain(X0)),compose(a,g))),compose(compose(h,codomain(X0)),compose(a,g))) ).
cnf(u3781,hypothesis,
compose(compose(domain(X0),h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,compose(a,b))),compose(compose(domain(X0),h),compose(a,b))),compose(compose(domain(X0),h),compose(a,b))) ).
cnf(u430,hypothesis,
compose(compose(X0,h),X1) = ifeq(codomain(g),domain(X1),ifeq(codomain(X0),domain(g),compose(X0,compose(h,X1)),compose(compose(X0,h),X1)),compose(compose(X0,h),X1)) ).
cnf(u56,hypothesis,
domain(X0) = ifeq(codomain(X0),domain(g),domain(compose(X0,h)),domain(X0)) ).
cnf(u4287,hypothesis,
compose(compose(codomain(X1),compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(compose(a,b),codomain(X0))),compose(compose(codomain(X1),compose(a,b)),codomain(X0))),compose(compose(codomain(X1),compose(a,b)),codomain(X0))) ).
cnf(u1099,hypothesis,
compose(compose(compose(a,b),a),X0) = ifeq(domain(g),domain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,X0)),compose(compose(compose(a,b),a),X0)),compose(compose(compose(a,b),a),X0)) ).
cnf(u1705,hypothesis,
compose(compose(h,X0),codomain(X0)) = ifeq(codomain(g),domain(X0),compose(h,X0),compose(compose(h,X0),codomain(X0))) ).
cnf(u5404,hypothesis,
compose(compose(domain(compose(h,compose(a,b))),h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(domain(compose(h,compose(a,b))),domain(g),compose(h,compose(a,b)),compose(compose(domain(compose(h,compose(a,b))),h),compose(a,b))),compose(compose(domain(compose(h,compose(a,b))),h),compose(a,b))) ).
cnf(u3722,hypothesis,
compose(compose(h,codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),compose(a,b))),compose(compose(h,codomain(X0)),compose(a,b))),compose(compose(h,codomain(X0)),compose(a,b))) ).
cnf(u3107,hypothesis,
compose(compose(domain(X1),domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),b)),compose(compose(domain(X1),domain(X0)),b)),compose(compose(domain(X1),domain(X0)),b)) ).
cnf(u1351,hypothesis,
compose(compose(a,compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),h)),compose(compose(a,compose(a,b)),h)),compose(compose(a,compose(a,b)),h)) ).
cnf(u4425,hypothesis,
compose(compose(codomain(X0),domain(X1)),compose(a,b)) = ifeq(domain(X1),domain(a),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(domain(X1),compose(a,b))),compose(compose(codomain(X0),domain(X1)),compose(a,b))),compose(compose(codomain(X0),domain(X1)),compose(a,b))) ).
cnf(u4692,hypothesis,
compose(compose(compose(a,g),compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),h)),compose(compose(compose(a,g),compose(a,g)),h)),compose(compose(compose(a,g),compose(a,g)),h)) ).
cnf(u1724,hypothesis,
compose(compose(a,a),domain(g)) = ifeq(domain(g),domain(a),compose(a,a),compose(compose(a,a),domain(g))) ).
cnf(u3780,hypothesis,
compose(compose(domain(X0),h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,compose(a,g))),compose(compose(domain(X0),h),compose(a,g))),compose(compose(domain(X0),h),compose(a,g))) ).
cnf(u6857,hypothesis,
compose(compose(compose(a,g),compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),compose(a,g))),compose(compose(compose(a,g),compose(a,b)),compose(a,g))),compose(compose(compose(a,g),compose(a,b)),compose(a,g))) ).
cnf(u1216,hypothesis,
compose(compose(a,X0),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(domain(g),domain(X0),compose(a,compose(X0,compose(a,g))),compose(compose(a,X0),compose(a,g))),compose(compose(a,X0),compose(a,g))) ).
cnf(u1124,hypothesis,
compose(compose(a,a),h) = ifeq(domain(g),domain(a),compose(a,compose(a,g)),compose(compose(a,a),h)) ).
cnf(u4260,hypothesis,
compose(compose(domain(X1),compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(domain(X1),domain(a),compose(domain(X1),compose(compose(a,b),codomain(X0))),compose(compose(domain(X1),compose(a,b)),codomain(X0))),compose(compose(domain(X1),compose(a,b)),codomain(X0))) ).
cnf(u3318,hypothesis,
compose(a,compose(a,b)) = ifeq(domain(g),domain(a),compose(a,compose(domain(g),compose(a,b))),compose(a,compose(a,b))) ).
cnf(u3146,hypothesis,
compose(h,b) = ifeq(codomain(g),domain(g),compose(h,compose(codomain(g),b)),compose(h,b)) ).
cnf(u2004,hypothesis,
compose(codomain(X0),b) = ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(codomain(X0),b)),compose(codomain(X0),b)) ).
cnf(u2270,hypothesis,
compose(compose(a,domain(a)),compose(a,g)) = ifeq(domain(g),domain(a),compose(a,compose(a,g)),compose(compose(a,domain(a)),compose(a,g))) ).
cnf(u4837,hypothesis,
compose(compose(domain(compose(a,codomain(X0))),a),codomain(X0)) = ifeq(domain(g),codomain(X0),ifeq(domain(compose(a,codomain(X0))),domain(a),compose(a,codomain(X0)),compose(compose(domain(compose(a,codomain(X0))),a),codomain(X0))),compose(compose(domain(compose(a,codomain(X0))),a),codomain(X0))) ).
cnf(u1358,hypothesis,
compose(compose(domain(X0),b),h) = ifeq(codomain(b),domain(g),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,h)),compose(compose(domain(X0),b),h)),compose(compose(domain(X0),b),h)) ).
cnf(u85,hypothesis,
domain(X0) = ifeq(codomain(X0),domain(a),domain(compose(X0,compose(a,g))),domain(X0)) ).
cnf(u848,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(X0,compose(a,b)),a,X0),X0),X0) = X0 ).
cnf(u215,hypothesis,
codomain(b) = ifeq(codomain(b),domain(g),codomain(compose(compose(a,b),b)),codomain(b)) ).
cnf(u2002,hypothesis,
compose(compose(a,b),b) = ifeq(codomain(b),domain(g),compose(domain(a),compose(compose(a,b),b)),compose(compose(a,b),b)) ).
cnf(u3169,hypothesis,
compose(compose(domain(compose(X0,h)),X0),h) = ifeq(codomain(X0),domain(g),ifeq(domain(compose(X0,h)),domain(X0),compose(X0,h),compose(compose(domain(compose(X0,h)),X0),h)),compose(compose(domain(compose(X0,h)),X0),h)) ).
cnf(u2252,hypothesis,
compose(compose(compose(a,g),domain(X0)),X0) = ifeq(codomain(g),domain(X0),compose(compose(a,g),X0),compose(compose(compose(a,g),domain(X0)),X0)) ).
cnf(u1739,hypothesis,
compose(compose(h,b),codomain(b)) = ifeq(codomain(g),domain(g),compose(h,b),compose(compose(h,b),codomain(b))) ).
cnf(u4504,hypothesis,
compose(compose(domain(compose(X0,compose(a,g))),X0),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(domain(compose(X0,compose(a,g))),domain(X0),compose(X0,compose(a,g)),compose(compose(domain(compose(X0,compose(a,g))),X0),compose(a,g))),compose(compose(domain(compose(X0,compose(a,g))),X0),compose(a,g))) ).
cnf(u970,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(codomain(X0),compose(a,b)),codomain(X0),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u1745,hypothesis,
compose(compose(h,codomain(X0)),codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(h,codomain(X0)),compose(compose(h,codomain(X0)),codomain(X0))) ).
cnf(u2665,axiom,
compose(X1,domain(X0)) = ifeq(domain(X0),codomain(compose(X1,domain(X0))),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),codomain(compose(X1,domain(X0))))),compose(X1,domain(X0))),compose(X1,domain(X0))) ).
cnf(u1499,hypothesis,
compose(compose(h,b),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(g),domain(g),compose(h,compose(b,codomain(X0))),compose(compose(h,b),codomain(X0))),compose(compose(h,b),codomain(X0))) ).
cnf(u1486,hypothesis,
compose(compose(h,compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),h)),compose(compose(h,compose(a,g)),h)),compose(compose(h,compose(a,g)),h)) ).
cnf(u213,hypothesis,
codomain(b) = ifeq(codomain(X0),domain(g),codomain(compose(codomain(X0),b)),codomain(b)) ).
cnf(u637,hypothesis,
domain(a) = ifeq(codomain(b),domain(a),domain(compose(compose(a,b),compose(a,b))),domain(a)) ).
cnf(u2479,hypothesis,
domain(X1) = ifeq(domain(X1),domain(a),ifeq(codomain(X2),domain(a),ifeq(compose(domain(X1),compose(a,b)),X0,ifeq(compose(codomain(X2),compose(a,b)),X0,codomain(X2),domain(X1)),domain(X1)),domain(X1)),domain(X1)) ).
cnf(u849,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(X0,compose(a,b)),h,X0),X0),X0) = X0 ).
cnf(u1105,hypothesis,
compose(compose(X0,a),b) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,b)),compose(compose(X0,a),b)) ).
cnf(u3284,hypothesis,
compose(compose(a,domain(X0)),codomain(X1)) = ifeq(domain(X0),codomain(X1),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),codomain(X1))),compose(compose(a,domain(X0)),codomain(X1))),compose(compose(a,domain(X0)),codomain(X1))) ).
cnf(u997,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(compose(a,b),compose(compose(a,b),compose(a,b)),domain(a),compose(a,b)),compose(a,b)) ).
cnf(u224,hypothesis,
domain(g) = ifeq(codomain(g),domain(a),codomain(compose(h,a)),domain(g)) ).
cnf(u1519,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(a,b),X0,domain(a),X1),X1),X1) = X1 ).
cnf(u882,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(a,compose(a,b)),a,h),h),h) ).
cnf(u1490,hypothesis,
compose(compose(domain(X0),h),h) = ifeq(codomain(g),domain(g),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,h)),compose(compose(domain(X0),h),h)),compose(compose(domain(X0),h),h)) ).
cnf(u3180,hypothesis,
compose(compose(domain(X0),compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,b),h)),compose(compose(domain(X0),compose(a,b)),h)),compose(compose(domain(X0),compose(a,b)),h)) ).
cnf(u995,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(compose(a,b),compose(codomain(X0),compose(a,b)),domain(a),codomain(X0)),codomain(X0)) ).
cnf(u1398,hypothesis,
compose(compose(h,domain(X0)),X1) = ifeq(domain(X0),domain(X1),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),X1)),compose(compose(h,domain(X0)),X1)),compose(compose(h,domain(X0)),X1)) ).
cnf(u1756,hypothesis,
compose(compose(compose(a,g),a),domain(g)) = ifeq(codomain(g),domain(a),compose(compose(a,g),a),compose(compose(compose(a,g),a),domain(g))) ).
cnf(u203,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(X1,compose(a,b)),X0,X1,h),h),h),h) ).
cnf(u2013,hypothesis,
compose(h,h) = ifeq(codomain(g),domain(g),compose(domain(g),compose(h,h)),compose(h,h)) ).
cnf(u1762,hypothesis,
compose(compose(compose(a,g),h),codomain(g)) = ifeq(codomain(g),domain(g),compose(compose(a,g),h),compose(compose(compose(a,g),h),codomain(g))) ).
cnf(u625,hypothesis,
domain(a) = ifeq(codomain(b),domain(a),domain(compose(compose(a,b),compose(a,g))),domain(a)) ).
cnf(u6570,hypothesis,
compose(compose(domain(compose(compose(a,b),codomain(X0))),compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(domain(compose(compose(a,b),codomain(X0))),domain(a),compose(compose(a,b),codomain(X0)),compose(compose(domain(compose(compose(a,b),codomain(X0))),compose(a,b)),codomain(X0))),compose(compose(domain(compose(compose(a,b),codomain(X0))),compose(a,b)),codomain(X0))) ).
cnf(u1107,hypothesis,
compose(compose(domain(X0),a),g) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,g)),compose(compose(domain(X0),a),g)) ).
cnf(u1233,hypothesis,
compose(compose(a,g),compose(a,b)) = ifeq(codomain(g),domain(a),compose(a,compose(g,compose(a,b))),compose(compose(a,g),compose(a,b))) ).
cnf(u4529,hypothesis,
compose(compose(compose(a,b),compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),X0)),compose(compose(compose(a,b),compose(a,g)),X0)),compose(compose(compose(a,b),compose(a,g)),X0)) ).
cnf(u5388,hypothesis,
compose(compose(domain(compose(compose(a,g),h)),compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(domain(compose(compose(a,g),h)),domain(a),compose(compose(a,g),h),compose(compose(domain(compose(compose(a,g),h)),compose(a,g)),h)),compose(compose(domain(compose(compose(a,g),h)),compose(a,g)),h)) ).
cnf(u1402,hypothesis,
compose(compose(X0,h),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(g),compose(X0,compose(h,compose(a,b))),compose(compose(X0,h),compose(a,b))),compose(compose(X0,h),compose(a,b))) ).
cnf(u2049,axiom,
compose(domain(X0),domain(X1)) = ifeq(domain(X0),domain(X1),compose(domain(X0),compose(domain(X0),domain(X1))),compose(domain(X0),domain(X1))) ).
cnf(u2271,hypothesis,
compose(compose(a,domain(a)),compose(a,b)) = ifeq(domain(g),domain(a),compose(a,compose(a,b)),compose(compose(a,domain(a)),compose(a,b))) ).
cnf(u1122,hypothesis,
compose(compose(compose(a,g),a),h) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,g)),compose(compose(compose(a,g),a),h)) ).
cnf(u2017,hypothesis,
compose(codomain(X0),h) = ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(codomain(X0),h)),compose(codomain(X0),h)) ).
cnf(u1396,hypothesis,
compose(compose(h,compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),X0)),compose(compose(h,compose(a,g)),X0)),compose(compose(h,compose(a,g)),X0)) ).
cnf(u115,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(g),domain(compose(codomain(X0),h)),codomain(X0)) ).
cnf(u2686,hypothesis,
compose(a,domain(X0)) = ifeq(domain(X0),codomain(compose(a,domain(X0))),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),codomain(compose(a,domain(X0))))),compose(a,domain(X0))),compose(a,domain(X0))) ).
cnf(u4288,hypothesis,
compose(compose(codomain(X1),compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(compose(a,g),codomain(X0))),compose(compose(codomain(X1),compose(a,g)),codomain(X0))),compose(compose(codomain(X1),compose(a,g)),codomain(X0))) ).
cnf(u508,hypothesis,
codomain(g) = ifeq(codomain(X0),domain(a),codomain(compose(codomain(X0),compose(a,g))),codomain(g)) ).
cnf(u6261,axiom,
compose(compose(domain(compose(domain(X0),codomain(X1))),domain(X0)),codomain(X1)) = ifeq(domain(X0),codomain(X1),ifeq(domain(compose(domain(X0),codomain(X1))),domain(X0),compose(domain(X0),codomain(X1)),compose(compose(domain(compose(domain(X0),codomain(X1))),domain(X0)),codomain(X1))),compose(compose(domain(compose(domain(X0),codomain(X1))),domain(X0)),codomain(X1))) ).
cnf(u886,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(a,compose(a,b)),compose(a,g),a),a),a) ).
cnf(u208,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(domain(g),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(a,compose(a,b)),X0,a,X1),X1),X1),X1) = X1 ).
cnf(u514,hypothesis,
domain(X0) = ifeq(codomain(b),domain(X0),codomain(compose(compose(a,b),domain(X0))),domain(X0)) ).
cnf(u25,axiom,
domain(X0) = domain(domain(X0)) ).
cnf(u4492,hypothesis,
compose(compose(compose(a,g),compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),X0)),compose(compose(compose(a,g),compose(a,b)),X0)),compose(compose(compose(a,g),compose(a,b)),X0)) ).
cnf(u113,hypothesis,
domain(g) = ifeq(codomain(b),domain(g),domain(compose(b,h)),domain(g)) ).
cnf(u892,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(codomain(X0),compose(a,b)),a,codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u269,axiom,
domain(X0) = ifeq(domain(X0),codomain(X1),domain(compose(domain(X0),codomain(X1))),domain(X0)) ).
cnf(u2071,hypothesis,
compose(compose(a,g),codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(domain(a),compose(compose(a,g),codomain(X0))),compose(compose(a,g),codomain(X0))) ).
cnf(u3696,hypothesis,
compose(compose(h,codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),domain(X1))),compose(compose(h,codomain(X0)),domain(X1))),compose(compose(h,codomain(X0)),domain(X1))) ).
cnf(u1151,hypothesis,
compose(compose(h,X0),b) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(h,compose(X0,b)),compose(compose(h,X0),b)),compose(compose(h,X0),b)) ).
cnf(u6137,hypothesis,
compose(compose(codomain(X0),compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,b),compose(a,g))),compose(compose(codomain(X0),compose(a,b)),compose(a,g))),compose(compose(codomain(X0),compose(a,b)),compose(a,g))) ).
cnf(u1923,hypothesis,
compose(compose(compose(a,b),compose(a,g)),codomain(g)) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,g)),compose(compose(compose(a,b),compose(a,g)),codomain(g))) ).
cnf(u142,hypothesis,
domain(a) = ifeq(codomain(g),domain(X0),domain(compose(compose(a,g),X0)),domain(a)) ).
cnf(u1363,hypothesis,
compose(compose(h,b),h) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(g),compose(h,compose(b,h)),compose(compose(h,b),h)),compose(compose(h,b),h)) ).
cnf(u3051,hypothesis,
compose(compose(domain(X0),a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,compose(a,b))),compose(compose(domain(X0),a),compose(a,b))),compose(compose(domain(X0),a),compose(a,b))) ).
cnf(u1014,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(codomain(X1),compose(a,b)),compose(domain(X0),compose(a,b)),codomain(X1),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u3463,hypothesis,
compose(X0,compose(a,g)) = ifeq(codomain(X0),domain(a),compose(X0,compose(codomain(X0),compose(a,g))),compose(X0,compose(a,g))) ).
cnf(u4362,hypothesis,
compose(compose(domain(X1),codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(domain(X1),codomain(X0),compose(domain(X1),compose(codomain(X0),compose(a,g))),compose(compose(domain(X1),codomain(X0)),compose(a,g))),compose(compose(domain(X1),codomain(X0)),compose(a,g))) ).
cnf(u2070,hypothesis,
compose(compose(a,b),codomain(X0)) = ifeq(codomain(b),codomain(X0),compose(domain(a),compose(compose(a,b),codomain(X0))),compose(compose(a,b),codomain(X0))) ).
cnf(u1308,hypothesis,
compose(compose(a,a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(domain(g),domain(a),compose(a,compose(a,compose(a,g))),compose(compose(a,a),compose(a,g))),compose(compose(a,a),compose(a,g))) ).
cnf(u27,hypothesis,
h = compose(domain(g),h) ).
cnf(u4474,hypothesis,
compose(compose(X0,compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,b),compose(a,b))),compose(compose(X0,compose(a,b)),compose(a,b))),compose(compose(X0,compose(a,b)),compose(a,b))) ).
cnf(u6869,hypothesis,
compose(compose(compose(a,b),compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),compose(a,g))),compose(compose(compose(a,b),compose(a,b)),compose(a,g))),compose(compose(compose(a,b),compose(a,b)),compose(a,g))) ).
cnf(u1158,hypothesis,
compose(compose(X1,domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),b)),compose(compose(X1,domain(X0)),b)),compose(compose(X1,domain(X0)),b)) ).
cnf(u5146,hypothesis,
compose(compose(codomain(X1),codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(X1),codomain(X0),compose(codomain(X1),compose(codomain(X0),compose(a,g))),compose(compose(codomain(X1),codomain(X0)),compose(a,g))),compose(compose(codomain(X1),codomain(X0)),compose(a,g))) ).
cnf(u2569,hypothesis,
domain(a) = ifeq(codomain(b),domain(a),ifeq(compose(a,b),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),domain(a)),domain(a)),domain(a)) ).
cnf(u140,hypothesis,
domain(a) = ifeq(codomain(g),domain(g),domain(compose(compose(a,g),h)),domain(a)) ).
cnf(u2710,hypothesis,
compose(compose(a,b),b) = ifeq(codomain(b),codomain(compose(compose(a,b),b)),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,codomain(compose(compose(a,b),b)))),compose(compose(a,b),b)),compose(compose(a,b),b)) ).
cnf(u1413,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,g),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u2449,hypothesis,
compose(compose(compose(a,g),domain(a)),compose(a,g)) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,g)),compose(compose(compose(a,g),domain(a)),compose(a,g))) ).
cnf(u2716,hypothesis,
compose(domain(X0),h) = ifeq(codomain(g),codomain(compose(domain(X0),h)),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,codomain(compose(domain(X0),h)))),compose(domain(X0),h)),compose(domain(X0),h)) ).
cnf(u155,hypothesis,
codomain(h) = codomain(g) ).
cnf(u6905,hypothesis,
compose(compose(compose(a,b),compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),compose(a,b))),compose(compose(compose(a,b),compose(a,b)),compose(a,b))),compose(compose(compose(a,b),compose(a,b)),compose(a,b))) ).
cnf(u1156,hypothesis,
compose(compose(X0,compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,g),b)),compose(compose(X0,compose(a,g)),b)),compose(compose(X0,compose(a,g)),b)) ).
cnf(u3470,hypothesis,
compose(compose(a,b),X0) = ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(codomain(b),X0)),compose(compose(a,b),X0)) ).
cnf(u6695,hypothesis,
compose(compose(domain(compose(compose(a,b),domain(X0))),compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(domain(compose(compose(a,b),domain(X0))),domain(a),compose(compose(a,b),domain(X0)),compose(compose(domain(compose(compose(a,b),domain(X0))),compose(a,b)),domain(X0))),compose(compose(domain(compose(compose(a,b),domain(X0))),compose(a,b)),domain(X0))) ).
cnf(u2570,hypothesis,
domain(a) = ifeq(domain(g),domain(a),ifeq(compose(a,b),X0,ifeq(compose(a,compose(a,b)),X0,a,domain(a)),domain(a)),domain(a)) ).
cnf(u926,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(domain(X1),compose(a,b)),domain(X1),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u4366,axiom,
compose(compose(domain(compose(codomain(X0),X1)),codomain(X0)),X1) = ifeq(codomain(X0),domain(X1),ifeq(domain(compose(codomain(X0),X1)),codomain(X0),compose(codomain(X0),X1),compose(compose(domain(compose(codomain(X0),X1)),codomain(X0)),X1)),compose(compose(domain(compose(codomain(X0),X1)),codomain(X0)),X1)) ).
cnf(u4749,hypothesis,
compose(compose(a,compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),compose(a,b))),compose(compose(a,compose(a,g)),compose(a,b))),compose(compose(a,compose(a,g)),compose(a,b))) ).
cnf(u31,axiom,
domain(X0) = compose(domain(X0),domain(X0)) ).
cnf(u3474,hypothesis,
compose(h,codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(g),codomain(X0))),compose(h,codomain(X0))) ).
cnf(u153,hypothesis,
domain(a) = ifeq(codomain(b),domain(X0),domain(compose(compose(a,b),X0)),domain(a)) ).
cnf(u3748,hypothesis,
compose(compose(codomain(X1),h),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(X1),domain(g),compose(codomain(X1),compose(h,domain(X0))),compose(compose(codomain(X1),h),domain(X0))),compose(compose(codomain(X1),h),domain(X0))) ).
cnf(u299,hypothesis,
codomain(g) = ifeq(domain(X0),domain(a),codomain(compose(domain(X0),compose(a,g))),codomain(g)) ).
cnf(u1198,hypothesis,
compose(compose(a,X0),h) = ifeq(codomain(X0),domain(g),ifeq(domain(g),domain(X0),compose(a,compose(X0,h)),compose(compose(a,X0),h)),compose(compose(a,X0),h)) ).
cnf(u669,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(a,compose(a,b)),compose(X0,compose(a,b)),X0,a),a),a) ).
cnf(u1329,hypothesis,
compose(compose(a,codomain(X0)),b) = ifeq(codomain(X0),domain(g),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),b)),compose(compose(a,codomain(X0)),b)),compose(compose(a,codomain(X0)),b)) ).
cnf(u1083,hypothesis,
codomain(X1) = ifeq(codomain(X1),domain(a),ifeq(domain(g),domain(a),ifeq(compose(codomain(X1),compose(a,b)),X0,ifeq(compose(a,compose(a,b)),X0,a,codomain(X1)),codomain(X1)),codomain(X1)),codomain(X1)) ).
cnf(u667,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(X0,compose(a,b)),X0,compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3494,hypothesis,
compose(compose(a,b),codomain(X0)) = ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(b),codomain(X0))),compose(compose(a,b),codomain(X0))) ).
cnf(u3125,hypothesis,
compose(compose(codomain(X0),codomain(X1)),b) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),codomain(X1),compose(codomain(X0),compose(codomain(X1),b)),compose(compose(codomain(X0),codomain(X1)),b)),compose(compose(codomain(X0),codomain(X1)),b)) ).
cnf(u1959,axiom,
compose(X0,X1) = ifeq(codomain(X0),domain(X1),compose(domain(X0),compose(X0,X1)),compose(X0,X1)) ).
cnf(u2704,hypothesis,
compose(h,compose(a,g)) = ifeq(codomain(g),codomain(compose(h,compose(a,g))),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),codomain(compose(h,compose(a,g))))),compose(h,compose(a,g))),compose(h,compose(a,g))) ).
cnf(u159,hypothesis,
domain(g) = ifeq(codomain(g),domain(g),domain(compose(h,h)),domain(g)) ).
cnf(u3106,hypothesis,
compose(compose(domain(X0),codomain(X1)),b) = ifeq(codomain(X1),domain(g),ifeq(domain(X0),codomain(X1),compose(domain(X0),compose(codomain(X1),b)),compose(compose(domain(X0),codomain(X1)),b)),compose(compose(domain(X0),codomain(X1)),b)) ).
cnf(u1196,hypothesis,
compose(compose(compose(a,g),X0),h) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(X0,h)),compose(compose(compose(a,g),X0),h)),compose(compose(compose(a,g),X0),h)) ).
cnf(u427,hypothesis,
compose(compose(a,X0),X1) = ifeq(codomain(X0),domain(X1),ifeq(domain(g),domain(X0),compose(a,compose(X0,X1)),compose(compose(a,X0),X1)),compose(compose(a,X0),X1)) ).
cnf(u1335,hypothesis,
compose(compose(compose(a,g),b),b) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,b)),compose(compose(compose(a,g),b),b)),compose(compose(compose(a,g),b),b)) ).
cnf(u961,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(codomain(X1),compose(a,b)),X0,codomain(X1),a),a),a),a) ).
cnf(u3129,hypothesis,
compose(compose(compose(a,g),codomain(X0)),b) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),b)),compose(compose(compose(a,g),codomain(X0)),b)),compose(compose(compose(a,g),codomain(X0)),b)) ).
cnf(u4505,hypothesis,
compose(compose(domain(compose(X0,compose(a,b))),X0),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(domain(compose(X0,compose(a,b))),domain(X0),compose(X0,compose(a,b)),compose(compose(domain(compose(X0,compose(a,b))),X0),compose(a,b))),compose(compose(domain(compose(X0,compose(a,b))),X0),compose(a,b))) ).
cnf(u3126,hypothesis,
compose(compose(codomain(X1),domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(codomain(X1),domain(X0),compose(codomain(X1),compose(domain(X0),b)),compose(compose(codomain(X1),domain(X0)),b)),compose(compose(codomain(X1),domain(X0)),b)) ).
cnf(u1200,hypothesis,
compose(compose(X0,b),h) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(g),compose(X0,compose(b,h)),compose(compose(X0,b),h)),compose(compose(X0,b),h)) ).
cnf(u920,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(codomain(X0),compose(a,b)),h,codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u1703,hypothesis,
compose(compose(compose(a,b),X0),codomain(X0)) = ifeq(codomain(b),domain(X0),compose(compose(a,b),X0),compose(compose(compose(a,b),X0),codomain(X0))) ).
cnf(u1578,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),ifeq(compose(a,b),compose(h,compose(a,b)),h,domain(a)),domain(a)) ).
cnf(u425,hypothesis,
compose(compose(compose(a,g),X0),X1) = ifeq(codomain(X0),domain(X1),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(X0,X1)),compose(compose(compose(a,g),X0),X1)),compose(compose(compose(a,g),X0),X1)) ).
cnf(u1982,axiom,
compose(domain(X0),X1) = ifeq(domain(X0),domain(X1),compose(domain(X0),compose(domain(X0),X1)),compose(domain(X0),X1)) ).
cnf(u5387,hypothesis,
compose(compose(domain(compose(compose(a,b),h)),compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(domain(compose(compose(a,b),h)),domain(a),compose(compose(a,b),h),compose(compose(domain(compose(compose(a,b),h)),compose(a,b)),h)),compose(compose(domain(compose(compose(a,b),h)),compose(a,b)),h)) ).
cnf(u941,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(a,b),domain(a),codomain(X0)),codomain(X0)) ).
cnf(u3130,hypothesis,
compose(compose(compose(a,b),codomain(X0)),b) = ifeq(codomain(X0),domain(g),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),b)),compose(compose(compose(a,b),codomain(X0)),b)),compose(compose(compose(a,b),codomain(X0)),b)) ).
cnf(u3257,hypothesis,
compose(compose(a,compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),domain(X0))),compose(compose(a,compose(a,g)),domain(X0))),compose(compose(a,compose(a,g)),domain(X0))) ).
cnf(u939,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(compose(X0,compose(a,b)),compose(a,b),domain(a),X0),X0) = X0 ).
cnf(u2493,hypothesis,
domain(a) = ifeq(codomain(X1),domain(a),ifeq(compose(a,b),X0,ifeq(compose(X1,compose(a,b)),X0,X1,domain(a)),domain(a)),domain(a)) ).
cnf(u71,hypothesis,
domain(a) = ifeq(domain(g),domain(X0),domain(compose(a,domain(X0))),domain(a)) ).
cnf(u4691,hypothesis,
compose(compose(compose(a,g),compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),h)),compose(compose(compose(a,g),compose(a,b)),h)),compose(compose(compose(a,g),compose(a,b)),h)) ).
cnf(u1485,hypothesis,
compose(compose(h,compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),h)),compose(compose(h,compose(a,b)),h)),compose(compose(h,compose(a,b)),h)) ).
cnf(u1712,hypothesis,
compose(compose(X0,a),domain(g)) = ifeq(codomain(X0),domain(a),compose(X0,a),compose(compose(X0,a),domain(g))) ).
cnf(u3258,hypothesis,
compose(compose(a,codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),domain(X1))),compose(compose(a,codomain(X0)),domain(X1))),compose(compose(a,codomain(X0)),domain(X1))) ).
cnf(u2254,hypothesis,
compose(compose(a,domain(X0)),X0) = ifeq(domain(g),domain(X0),compose(a,X0),compose(compose(a,domain(X0)),X0)) ).
cnf(u1470,hypothesis,
compose(compose(compose(a,g),h),b) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,b)),compose(compose(compose(a,g),h),b)),compose(compose(compose(a,g),h),b)) ).
cnf(u69,axiom,
codomain(X1) = ifeq(codomain(X0),codomain(X1),codomain(compose(X0,codomain(X1))),codomain(X1)) ).
cnf(u3302,hypothesis,
compose(compose(a,domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),compose(a,b))),compose(compose(a,domain(X0)),compose(a,b))),compose(compose(a,domain(X0)),compose(a,b))) ).
cnf(u199,hypothesis,
codomain(X1) = ifeq(codomain(X1),domain(a),ifeq(codomain(X2),domain(a),ifeq(compose(codomain(X1),compose(a,b)),X0,ifeq(compose(X2,compose(a,b)),X0,X2,codomain(X1)),codomain(X1)),codomain(X1)),codomain(X1)) ).
cnf(u1986,hypothesis,
compose(a,compose(a,b)) = ifeq(domain(g),domain(a),compose(domain(a),compose(a,compose(a,b))),compose(a,compose(a,b))) ).
cnf(u3140,hypothesis,
compose(X0,b) = ifeq(codomain(X0),domain(g),compose(X0,compose(codomain(X0),b)),compose(X0,b)) ).
cnf(u5717,hypothesis,
compose(compose(compose(a,g),domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(domain(X0),compose(a,b))),compose(compose(compose(a,g),domain(X0)),compose(a,b))),compose(compose(compose(a,g),domain(X0)),compose(a,b))) ).
cnf(u80,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(X0,compose(a,b)),X2,ifeq(compose(X1,compose(a,b)),X2,X1,X0),X0),X0),X0) = X0 ).
cnf(u1375,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),X0,ifeq(compose(h,compose(a,b)),X0,h,compose(a,g)),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u5595,hypothesis,
compose(compose(compose(a,b),compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),codomain(X0))),compose(compose(compose(a,b),compose(a,b)),codomain(X0))),compose(compose(compose(a,b),compose(a,b)),codomain(X0))) ).
cnf(u1729,hypothesis,
compose(compose(a,compose(a,b)),codomain(b)) = ifeq(domain(g),domain(a),compose(a,compose(a,b)),compose(compose(a,compose(a,b)),codomain(b))) ).
cnf(u1620,hypothesis,
domain(a) = ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(a,b),codomain(X0),domain(a)),domain(a)) ).
cnf(u2251,axiom,
compose(compose(codomain(X1),domain(X0)),X0) = ifeq(codomain(X1),domain(X0),compose(codomain(X1),X0),compose(compose(codomain(X1),domain(X0)),X0)) ).
cnf(u1946,hypothesis,
compose(compose(domain(X0),X1),compose(a,g)) = ifeq(codomain(X1),domain(a),ifeq(domain(X0),domain(X1),compose(domain(X0),compose(X1,compose(a,g))),compose(compose(domain(X0),X1),compose(a,g))),compose(compose(domain(X0),X1),compose(a,g))) ).
cnf(u3525,hypothesis,
compose(compose(a,g),compose(a,b)) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(codomain(g),compose(a,b))),compose(compose(a,g),compose(a,b))) ).
cnf(u960,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(a,compose(a,b)),X1,ifeq(compose(domain(X0),compose(a,b)),X1,domain(X0),a),a),a),a) ).
cnf(u1743,hypothesis,
compose(compose(h,compose(a,b)),codomain(b)) = ifeq(codomain(g),domain(a),compose(h,compose(a,b)),compose(compose(h,compose(a,b)),codomain(b))) ).
cnf(u1618,hypothesis,
domain(a) = ifeq(codomain(X0),domain(a),ifeq(compose(X0,compose(a,b)),compose(a,b),X0,domain(a)),domain(a)) ).
cnf(u3182,hypothesis,
compose(compose(domain(X0),codomain(X1)),h) = ifeq(codomain(X1),domain(g),ifeq(domain(X0),codomain(X1),compose(domain(X0),compose(codomain(X1),h)),compose(compose(domain(X0),codomain(X1)),h)),compose(compose(domain(X0),codomain(X1)),h)) ).
cnf(u1742,hypothesis,
compose(compose(h,h),codomain(g)) = ifeq(codomain(g),domain(g),compose(h,h),compose(compose(h,h),codomain(g))) ).
cnf(u981,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(domain(X1),compose(a,b)),compose(codomain(X0),compose(a,b)),domain(X1),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u1624,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(a,b),h,domain(a)),domain(a)) ).
cnf(u1741,hypothesis,
compose(compose(h,a),domain(g)) = ifeq(codomain(g),domain(a),compose(h,a),compose(compose(h,a),domain(g))) ).
cnf(u1748,hypothesis,
compose(compose(codomain(X0),b),codomain(b)) = ifeq(codomain(X0),domain(g),compose(codomain(X0),b),compose(compose(codomain(X0),b),codomain(b))) ).
cnf(u3283,hypothesis,
compose(compose(a,codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(domain(g),codomain(X0),compose(a,compose(codomain(X0),codomain(X1))),compose(compose(a,codomain(X0)),codomain(X1))),compose(compose(a,codomain(X0)),codomain(X1))) ).
cnf(u154,hypothesis,
codomain(b) = ifeq(codomain(X0),domain(a),codomain(compose(X0,compose(a,b))),codomain(b)) ).
cnf(u872,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,g),a),a),a) ).
cnf(u4294,hypothesis,
compose(compose(compose(a,b),codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),codomain(X1))),compose(compose(compose(a,b),codomain(X0)),codomain(X1))),compose(compose(compose(a,b),codomain(X0)),codomain(X1))) ).
cnf(u1746,hypothesis,
compose(compose(h,domain(X0)),domain(X0)) = ifeq(codomain(g),domain(X0),compose(h,domain(X0)),compose(compose(h,domain(X0)),domain(X0))) ).
cnf(u3425,hypothesis,
compose(compose(codomain(X0),X1),compose(a,g)) = ifeq(codomain(X1),domain(a),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(X1,compose(a,g))),compose(compose(codomain(X0),X1),compose(a,g))),compose(compose(codomain(X0),X1),compose(a,g))) ).
cnf(u1217,hypothesis,
compose(compose(a,X0),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(domain(g),domain(X0),compose(a,compose(X0,compose(a,b))),compose(compose(a,X0),compose(a,b))),compose(compose(a,X0),compose(a,b))) ).
cnf(u214,hypothesis,
codomain(b) = ifeq(codomain(g),domain(g),codomain(compose(compose(a,g),b)),codomain(b)) ).
cnf(u1125,hypothesis,
compose(compose(h,a),h) = ifeq(codomain(g),domain(a),compose(h,compose(a,g)),compose(compose(h,a),h)) ).
cnf(u994,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(compose(a,b),compose(domain(X0),compose(a,b)),domain(a),domain(X0)),domain(X0)) ).
cnf(u2255,hypothesis,
compose(compose(h,domain(X0)),X0) = ifeq(codomain(g),domain(X0),compose(h,X0),compose(compose(h,domain(X0)),X0)) ).
cnf(u1106,hypothesis,
compose(compose(X0,a),h) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,g)),compose(compose(X0,a),h)) ).
cnf(u2670,hypothesis,
compose(a,a) = ifeq(domain(g),codomain(compose(a,a)),ifeq(domain(g),domain(a),compose(a,compose(a,codomain(compose(a,a)))),compose(a,a)),compose(a,a)) ).
cnf(u2904,hypothesis,
compose(compose(compose(a,b),a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,domain(X0))),compose(compose(compose(a,b),a),domain(X0))),compose(compose(compose(a,b),a),domain(X0))) ).
cnf(u2015,hypothesis,
compose(compose(a,b),h) = ifeq(codomain(b),domain(g),compose(domain(a),compose(compose(a,b),h)),compose(compose(a,b),h)) ).
cnf(u4293,hypothesis,
compose(compose(compose(a,g),codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(codomain(g),codomain(X0),compose(compose(a,g),compose(codomain(X0),codomain(X1))),compose(compose(compose(a,g),codomain(X0)),codomain(X1))),compose(compose(compose(a,g),codomain(X0)),codomain(X1))) ).
cnf(u1116,hypothesis,
compose(compose(compose(a,g),a),b) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,b)),compose(compose(compose(a,g),a),b)) ).
cnf(u212,hypothesis,
codomain(b) = ifeq(domain(X0),domain(g),codomain(compose(domain(X0),b)),codomain(b)) ).
cnf(u3795,hypothesis,
compose(compose(codomain(X0),h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,compose(a,g))),compose(compose(codomain(X0),h),compose(a,g))),compose(compose(codomain(X0),h),compose(a,g))) ).
cnf(u870,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(a,compose(a,b)),compose(domain(X0),compose(a,b)),domain(X0),a),a),a) ).
cnf(u3038,hypothesis,
compose(compose(compose(a,b),a),codomain(X0)) = ifeq(domain(g),codomain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,codomain(X0))),compose(compose(compose(a,b),a),codomain(X0))),compose(compose(compose(a,b),a),codomain(X0))) ).
cnf(u6095,hypothesis,
compose(compose(compose(a,b),compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),domain(X0))),compose(compose(compose(a,b),compose(a,b)),domain(X0))),compose(compose(compose(a,b),compose(a,b)),domain(X0))) ).
cnf(u626,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),domain(compose(compose(a,g),compose(a,g))),domain(a)) ).
cnf(u983,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(compose(a,b),compose(a,b)),domain(X0),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u1234,hypothesis,
compose(compose(a,g),b) = ifeq(codomain(g),domain(g),compose(a,compose(g,b)),compose(compose(a,g),b)) ).
cnf(u97,hypothesis,
domain(a) = ifeq(domain(g),domain(a),domain(compose(a,compose(a,b))),domain(a)) ).
cnf(u3981,hypothesis,
compose(compose(a,b),domain(X0)) = ifeq(domain(X0),codomain(compose(compose(a,b),domain(X0))),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(domain(X0),codomain(compose(compose(a,b),domain(X0))))),compose(compose(a,b),domain(X0))),compose(compose(a,b),domain(X0))) ).
cnf(u3037,hypothesis,
compose(compose(compose(a,g),a),codomain(X0)) = ifeq(domain(g),codomain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,codomain(X0))),compose(compose(compose(a,g),a),codomain(X0))),compose(compose(compose(a,g),a),codomain(X0))) ).
cnf(u3697,hypothesis,
compose(compose(h,domain(X0)),domain(X1)) = ifeq(domain(X0),domain(X1),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),domain(X1))),compose(compose(h,domain(X0)),domain(X1))),compose(compose(h,domain(X0)),domain(X1))) ).
cnf(u1361,hypothesis,
compose(compose(compose(a,b),b),h) = ifeq(codomain(b),domain(g),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,h)),compose(compose(compose(a,b),b),h)),compose(compose(compose(a,b),b),h)) ).
cnf(u2566,hypothesis,
domain(a) = ifeq(domain(X0),domain(a),ifeq(compose(a,b),X1,ifeq(compose(domain(X0),compose(a,b)),X1,domain(X0),domain(a)),domain(a)),domain(a)) ).
cnf(u3035,hypothesis,
compose(compose(domain(X0),a),codomain(X1)) = ifeq(domain(g),codomain(X1),ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,codomain(X1))),compose(compose(domain(X0),a),codomain(X1))),compose(compose(domain(X0),a),codomain(X1))) ).
cnf(u998,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(compose(a,b),compose(a,compose(a,b)),domain(a),a),a) ).
cnf(u1397,hypothesis,
compose(compose(h,codomain(X0)),X1) = ifeq(codomain(X0),domain(X1),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),X1)),compose(compose(h,codomain(X0)),X1)),compose(compose(h,codomain(X0)),X1)) ).
cnf(u1146,hypothesis,
compose(compose(domain(X0),X1),b) = ifeq(codomain(X1),domain(g),ifeq(domain(X0),domain(X1),compose(domain(X0),compose(X1,b)),compose(compose(domain(X0),X1),b)),compose(compose(domain(X0),X1),b)) ).
cnf(u1292,hypothesis,
compose(compose(X0,b),codomain(X1)) = ifeq(codomain(b),codomain(X1),ifeq(codomain(X0),domain(g),compose(X0,compose(b,codomain(X1))),compose(compose(X0,b),codomain(X1))),compose(compose(X0,b),codomain(X1))) ).
cnf(u11,axiom,
codomain(X1) = ifeq(codomain(X0),domain(X1),codomain(compose(X0,X1)),codomain(X1)) ).
cnf(u4317,hypothesis,
compose(compose(compose(a,b),domain(X1)),codomain(X0)) = ifeq(domain(X1),codomain(X0),ifeq(codomain(b),domain(X1),compose(compose(a,b),compose(domain(X1),codomain(X0))),compose(compose(compose(a,b),domain(X1)),codomain(X0))),compose(compose(compose(a,b),domain(X1)),codomain(X0))) ).
cnf(u5703,hypothesis,
compose(compose(compose(a,g),domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(domain(X0),compose(a,g))),compose(compose(compose(a,g),domain(X0)),compose(a,g))),compose(compose(compose(a,g),domain(X0)),compose(a,g))) ).
cnf(u2048,axiom,
compose(codomain(X0),domain(X1)) = ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(codomain(X0),domain(X1))),compose(codomain(X0),domain(X1))) ).
cnf(u266,hypothesis,
domain(a) = ifeq(codomain(b),codomain(X0),domain(compose(compose(a,b),codomain(X0))),domain(a)) ).
cnf(u3050,hypothesis,
compose(compose(domain(X0),a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,compose(a,g))),compose(compose(domain(X0),a),compose(a,g))),compose(compose(domain(X0),a),compose(a,g))) ).
cnf(u1401,hypothesis,
compose(compose(X0,h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(g),compose(X0,compose(h,compose(a,g))),compose(compose(X0,h),compose(a,g))),compose(compose(X0,h),compose(a,g))) ).
cnf(u5575,hypothesis,
compose(compose(compose(a,g),compose(a,g)),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),codomain(X0))),compose(compose(compose(a,g),compose(a,g)),codomain(X0))),compose(compose(compose(a,g),compose(a,g)),codomain(X0))) ).
cnf(u1525,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(a,b),X0,domain(a),h),h),h) ).
cnf(u2567,hypothesis,
domain(a) = ifeq(codomain(X1),domain(a),ifeq(compose(a,b),X0,ifeq(compose(codomain(X1),compose(a,b)),X0,codomain(X1),domain(a)),domain(a)),domain(a)) ).
cnf(u9,axiom,
domain(X0) = ifeq(codomain(X0),domain(X1),domain(compose(X0,X1)),domain(X0)) ).
cnf(u1420,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,b),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u139,hypothesis,
codomain(compose(a,g)) = codomain(g) ).
cnf(u3694,hypothesis,
compose(compose(h,compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),domain(X0))),compose(compose(h,compose(a,b)),domain(X0))),compose(compose(h,compose(a,b)),domain(X0))) ).
cnf(u3203,hypothesis,
compose(compose(codomain(X1),domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(codomain(X1),domain(X0),compose(codomain(X1),compose(domain(X0),h)),compose(compose(codomain(X1),domain(X0)),h)),compose(compose(codomain(X1),domain(X0)),h)) ).
cnf(u1804,axiom,
compose(compose(codomain(X1),codomain(X0)),codomain(X0)) = ifeq(codomain(X1),codomain(X0),compose(codomain(X1),codomain(X0)),compose(compose(codomain(X1),codomain(X0)),codomain(X0))) ).
cnf(u1155,hypothesis,
compose(compose(X0,compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,b),b)),compose(compose(X0,compose(a,b)),b)),compose(compose(X0,compose(a,b)),b)) ).
cnf(u3350,hypothesis,
compose(compose(domain(X0),b),codomain(X1)) = ifeq(codomain(b),codomain(X1),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,codomain(X1))),compose(compose(domain(X0),b),codomain(X1))),compose(compose(domain(X0),b),codomain(X1))) ).
cnf(u2077,hypothesis,
compose(codomain(X0),compose(a,b)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(codomain(X0),compose(a,b))),compose(codomain(X0),compose(a,b))) ).
cnf(u1802,hypothesis,
compose(compose(codomain(X0),compose(a,b)),codomain(b)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,b)),compose(compose(codomain(X0),compose(a,b)),codomain(b))) ).
cnf(u137,hypothesis,
domain(g) = ifeq(domain(g),domain(a),codomain(compose(a,a)),domain(g)) ).
cnf(u5147,hypothesis,
compose(compose(codomain(X1),codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(X1),codomain(X0),compose(codomain(X1),compose(codomain(X0),compose(a,b))),compose(compose(codomain(X1),codomain(X0)),compose(a,b))),compose(compose(codomain(X1),codomain(X0)),compose(a,b))) ).
cnf(u3313,hypothesis,
compose(a,X0) = ifeq(domain(g),domain(X0),compose(a,compose(domain(g),X0)),compose(a,X0)) ).
cnf(u3749,hypothesis,
compose(compose(compose(a,g),h),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,domain(X0))),compose(compose(compose(a,g),h),domain(X0))),compose(compose(compose(a,g),h),domain(X0))) ).
cnf(u270,axiom,
domain(X1) = ifeq(domain(X1),domain(X0),domain(compose(domain(X1),domain(X0))),domain(X1)) ).
cnf(u1808,hypothesis,
compose(compose(compose(a,g),codomain(X0)),codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(compose(a,g),codomain(X0)),compose(compose(compose(a,g),codomain(X0)),codomain(X0))) ).
cnf(u26,axiom,
codomain(X0) = codomain(codomain(X0)) ).
cnf(u921,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(compose(a,g),compose(a,b)),h,compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3747,hypothesis,
compose(compose(domain(X0),h),domain(X1)) = ifeq(codomain(g),domain(X1),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,domain(X1))),compose(compose(domain(X0),h),domain(X1))),compose(compose(domain(X0),h),domain(X1))) ).
cnf(u4748,hypothesis,
compose(compose(a,compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),compose(a,b))),compose(compose(a,compose(a,b)),compose(a,b))),compose(compose(a,compose(a,b)),compose(a,b))) ).
cnf(u1299,hypothesis,
compose(compose(compose(a,g),b),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,X0)),compose(compose(compose(a,g),b),X0)),compose(compose(compose(a,g),b),X0)) ).
cnf(u4382,hypothesis,
compose(compose(domain(X1),domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),compose(a,b))),compose(compose(domain(X1),domain(X0)),compose(a,b))),compose(compose(domain(X1),domain(X0)),compose(a,b))) ).
cnf(u3736,hypothesis,
compose(compose(h,domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),compose(a,b))),compose(compose(h,domain(X0)),compose(a,b))),compose(compose(h,domain(X0)),compose(a,b))) ).
cnf(u143,hypothesis,
codomain(g) = ifeq(codomain(X0),domain(a),codomain(compose(X0,compose(a,g))),codomain(g)) ).
cnf(u2705,hypothesis,
compose(h,codomain(X0)) = ifeq(codomain(X0),codomain(compose(h,codomain(X0))),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),codomain(compose(h,codomain(X0))))),compose(h,codomain(X0))),compose(h,codomain(X0))) ).
cnf(u2460,hypothesis,
compose(compose(compose(a,b),domain(a)),compose(a,b)) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,b)),compose(compose(compose(a,b),domain(a)),compose(a,b))) ).
cnf(u3750,hypothesis,
compose(compose(compose(a,b),h),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,domain(X0))),compose(compose(compose(a,b),h),domain(X0))),compose(compose(compose(a,b),h),domain(X0))) ).
cnf(u304,hypothesis,
codomain(X0) = ifeq(codomain(g),codomain(X0),codomain(compose(compose(a,g),codomain(X0))),codomain(X0)) ).
cnf(u2719,hypothesis,
compose(compose(a,b),h) = ifeq(codomain(g),codomain(compose(compose(a,b),h)),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,codomain(compose(compose(a,b),h)))),compose(compose(a,b),h)),compose(compose(a,b),h)) ).
cnf(u3482,hypothesis,
compose(compose(a,b),domain(X0)) = ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(codomain(b),domain(X0))),compose(compose(a,b),domain(X0))) ).
cnf(u1195,hypothesis,
compose(compose(codomain(X0),X1),h) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(X1,h)),compose(compose(codomain(X0),X1),h)),compose(compose(codomain(X0),X1),h)) ).
cnf(u1427,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(domain(X0),compose(a,b)),compose(a,g),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u670,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(h,compose(a,b)),compose(X0,compose(a,b)),X0,h),h),h) ).
cnf(u2349,hypothesis,
compose(compose(codomain(X0),domain(a)),compose(a,g)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,g)),compose(compose(codomain(X0),domain(a)),compose(a,g))) ).
cnf(u3368,hypothesis,
compose(compose(domain(X0),b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,compose(a,g))),compose(compose(domain(X0),b),compose(a,g))),compose(compose(domain(X0),b),compose(a,g))) ).
cnf(u55,hypothesis,
domain(X0) = ifeq(codomain(X0),domain(g),domain(compose(X0,b)),domain(X0)) ).
cnf(u93,hypothesis,
domain(X0) = ifeq(codomain(X0),domain(a),domain(compose(X0,compose(a,b))),domain(X0)) ).
cnf(u3218,hypothesis,
compose(X0,h) = ifeq(codomain(X0),domain(g),compose(X0,compose(codomain(X0),h)),compose(X0,h)) ).
cnf(u676,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(X0,compose(a,b)),compose(h,compose(a,b)),h,X0),X0),X0) = X0 ).
cnf(u4880,hypothesis,
compose(compose(domain(compose(domain(X0),b)),domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(domain(compose(domain(X0),b)),domain(X0),compose(domain(X0),b),compose(compose(domain(compose(domain(X0),b)),domain(X0)),b)),compose(compose(domain(compose(domain(X0),b)),domain(X0)),b)) ).
cnf(u4424,hypothesis,
compose(compose(codomain(X0),domain(X1)),compose(a,g)) = ifeq(domain(X1),domain(a),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(domain(X1),compose(a,g))),compose(compose(codomain(X0),domain(X1)),compose(a,g))),compose(compose(codomain(X0),domain(X1)),compose(a,g))) ).
cnf(u152,hypothesis,
domain(a) = ifeq(codomain(b),domain(g),domain(compose(compose(a,b),b)),domain(a)) ).
cnf(u1447,hypothesis,
compose(compose(h,a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),compose(h,compose(a,compose(a,g))),compose(compose(h,a),compose(a,g))),compose(compose(h,a),compose(a,g))) ).
cnf(u1972,axiom,
compose(X0,codomain(X1)) = ifeq(codomain(X0),codomain(X1),compose(domain(X0),compose(X0,codomain(X1))),compose(X0,codomain(X1))) ).
cnf(u2238,hypothesis,
compose(compose(compose(a,g),domain(X1)),X0) = ifeq(domain(X1),domain(X0),ifeq(codomain(g),domain(X1),compose(compose(a,g),compose(domain(X1),X0)),compose(compose(compose(a,g),domain(X1)),X0)),compose(compose(compose(a,g),domain(X1)),X0)) ).
cnf(u53,axiom,
domain(X0) = ifeq(codomain(X0),domain(X1),domain(compose(X0,domain(X1))),domain(X0)) ).
cnf(u3763,hypothesis,
compose(compose(compose(a,g),h),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,codomain(X0))),compose(compose(compose(a,g),h),codomain(X0))),compose(compose(compose(a,g),h),codomain(X0))) ).
cnf(u1469,hypothesis,
compose(compose(codomain(X0),h),b) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(h,b)),compose(compose(codomain(X0),h),b)),compose(compose(codomain(X0),h),b)) ).
cnf(u1976,hypothesis,
compose(X0,h) = ifeq(codomain(X0),domain(g),compose(domain(X0),compose(X0,h)),compose(X0,h)) ).
cnf(u1696,hypothesis,
compose(compose(X1,compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(X1),domain(a),compose(X1,compose(compose(a,b),codomain(X0))),compose(compose(X1,compose(a,b)),codomain(X0))),compose(compose(X1,compose(a,b)),codomain(X0))) ).
cnf(u3965,hypothesis,
compose(compose(a,b),codomain(X0)) = ifeq(codomain(X0),codomain(compose(compose(a,b),codomain(X0))),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),codomain(compose(compose(a,b),codomain(X0))))),compose(compose(a,b),codomain(X0))),compose(compose(a,b),codomain(X0))) ).
cnf(u1330,hypothesis,
compose(compose(a,domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),b)),compose(compose(a,domain(X0)),b)),compose(compose(a,domain(X0)),b)) ).
cnf(u1713,hypothesis,
compose(compose(X0,h),codomain(g)) = ifeq(codomain(X0),domain(g),compose(X0,h),compose(compose(X0,h),codomain(g))) ).
cnf(u1467,hypothesis,
compose(compose(h,domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),b)),compose(compose(h,domain(X0)),b)),compose(compose(h,domain(X0)),b)) ).
cnf(u1436,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,b),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u944,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(a,b),domain(a),a),a) ).
cnf(u5451,hypothesis,
compose(compose(a,g),compose(a,b)) = ifeq(codomain(b),codomain(compose(compose(a,g),compose(a,b))),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),codomain(compose(compose(a,g),compose(a,b))))),compose(compose(a,g),compose(a,b))),compose(compose(a,g),compose(a,b))) ).
cnf(u681,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(b),domain(a),compose(a,b),compose(a,b)),compose(a,b)) ).
cnf(u6078,hypothesis,
compose(compose(compose(a,g),compose(a,g)),domain(X0)) = ifeq(codomain(g),domain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),domain(X0))),compose(compose(compose(a,g),compose(a,g)),domain(X0))),compose(compose(compose(a,g),compose(a,g)),domain(X0))) ).
cnf(u1359,hypothesis,
compose(compose(codomain(X0),b),h) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,h)),compose(compose(codomain(X0),b),h)),compose(compose(codomain(X0),b),h)) ).
cnf(u3764,hypothesis,
compose(compose(compose(a,b),h),codomain(X0)) = ifeq(codomain(g),codomain(X0),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,codomain(X0))),compose(compose(compose(a,b),h),codomain(X0))),compose(compose(compose(a,b),h),codomain(X0))) ).
cnf(u1621,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(a,b),compose(a,g),domain(a)),domain(a)) ).
cnf(u1981,axiom,
compose(codomain(X0),X1) = ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(codomain(X0),X1)),compose(codomain(X0),X1)) ).
cnf(u3256,hypothesis,
compose(compose(a,compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),domain(X0))),compose(compose(a,compose(a,b)),domain(X0))),compose(compose(a,compose(a,b)),domain(X0))) ).
cnf(u1085,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(domain(g),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X0,ifeq(compose(a,compose(a,b)),X0,a,compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u1619,hypothesis,
domain(a) = ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(a,b),domain(X0),domain(a)),domain(a)) ).
cnf(u1201,hypothesis,
compose(compose(X0,h),h) = ifeq(codomain(g),domain(g),ifeq(codomain(X0),domain(g),compose(X0,compose(h,h)),compose(compose(X0,h),h)),compose(compose(X0,h),h)) ).
cnf(u1979,hypothesis,
compose(compose(a,b),X0) = ifeq(codomain(b),domain(X0),compose(domain(a),compose(compose(a,b),X0)),compose(compose(a,b),X0)) ).
cnf(u70,axiom,
domain(X1) = ifeq(codomain(X0),domain(X1),codomain(compose(X0,domain(X1))),domain(X1)) ).
cnf(u965,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(h,compose(a,b)),X0,h,a),a),a),a) ).
cnf(u2239,hypothesis,
compose(compose(compose(a,b),domain(X1)),X0) = ifeq(domain(X1),domain(X0),ifeq(codomain(b),domain(X1),compose(compose(a,b),compose(domain(X1),X0)),compose(compose(compose(a,b),domain(X1)),X0)),compose(compose(compose(a,b),domain(X1)),X0)) ).
cnf(u1732,hypothesis,
compose(compose(a,domain(X0)),domain(X0)) = ifeq(domain(g),domain(X0),compose(a,domain(X0)),compose(compose(a,domain(X0)),domain(X0))) ).
cnf(u2901,hypothesis,
compose(compose(domain(X0),a),domain(X1)) = ifeq(domain(g),domain(X1),ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,domain(X1))),compose(compose(domain(X0),a),domain(X1))),compose(compose(domain(X0),a),domain(X1))) ).
cnf(u1366,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(codomain(X1),compose(a,b)),X0,codomain(X1),h),h),h),h) ).
cnf(u1749,hypothesis,
compose(compose(compose(a,g),b),codomain(b)) = ifeq(codomain(g),domain(g),compose(compose(a,g),b),compose(compose(compose(a,g),b),codomain(b))) ).
cnf(u4807,hypothesis,
compose(compose(domain(compose(a,domain(X0))),a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(domain(compose(a,domain(X0))),domain(a),compose(a,domain(X0)),compose(compose(domain(compose(a,domain(X0))),a),domain(X0))),compose(compose(domain(compose(a,domain(X0))),a),domain(X0))) ).
cnf(u1730,hypothesis,
compose(compose(a,compose(a,g)),codomain(g)) = ifeq(domain(g),domain(a),compose(a,compose(a,g)),compose(compose(a,compose(a,g)),codomain(g))) ).
cnf(u2249,axiom,
compose(compose(X1,domain(X0)),X0) = ifeq(codomain(X1),domain(X0),compose(X1,X0),compose(compose(X1,domain(X0)),X0)) ).
cnf(u3353,hypothesis,
compose(compose(compose(a,b),b),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,codomain(X0))),compose(compose(compose(a,b),b),codomain(X0))),compose(compose(compose(a,b),b),codomain(X0))) ).
cnf(u68,hypothesis,
domain(g) = ifeq(codomain(X0),domain(a),codomain(compose(X0,a)),domain(g)) ).
cnf(u198,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(domain(X0),compose(a,b)),X2,ifeq(compose(X1,compose(a,b)),X2,X1,domain(X0)),domain(X0)),domain(X0)),domain(X0)) ).
cnf(u1109,hypothesis,
compose(compose(compose(a,g),a),g) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,g)),compose(compose(compose(a,g),a),g)) ).
cnf(u2657,hypothesis,
compose(compose(a,b),X0) = ifeq(codomain(X0),codomain(compose(compose(a,b),X0)),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(X0,codomain(compose(compose(a,b),X0)))),compose(compose(a,b),X0)),compose(compose(a,b),X0)) ).
cnf(u1370,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(h,compose(a,b)),X0,h,h),h),h),h) ).
cnf(u4705,hypothesis,
compose(compose(compose(a,b),compose(a,b)),h) = ifeq(codomain(b),domain(g),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,b),h)),compose(compose(compose(a,b),compose(a,b)),h)),compose(compose(compose(a,b),compose(a,b)),h)) ).
cnf(u1090,hypothesis,
compose(compose(X1,a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(codomain(X1),domain(a),compose(X1,compose(a,domain(X0))),compose(compose(X1,a),domain(X0))),compose(compose(X1,a),domain(X0))) ).
cnf(u1985,hypothesis,
compose(a,compose(a,g)) = ifeq(domain(g),domain(a),compose(domain(a),compose(a,compose(a,g))),compose(a,compose(a,g))) ).
cnf(u83,hypothesis,
compose(a,g) = compose(domain(a),compose(a,g)) ).
cnf(u2654,axiom,
compose(domain(X0),X1) = ifeq(codomain(X1),codomain(compose(domain(X0),X1)),ifeq(domain(X0),domain(X1),compose(domain(X0),compose(X1,codomain(compose(domain(X0),X1)))),compose(domain(X0),X1)),compose(domain(X0),X1)) ).
cnf(u221,hypothesis,
domain(g) = ifeq(codomain(g),domain(a),codomain(compose(compose(a,g),a)),domain(g)) ).
cnf(u1999,hypothesis,
compose(b,b) = ifeq(codomain(b),domain(g),compose(domain(g),compose(b,b)),compose(b,b)) ).
cnf(u2250,axiom,
compose(compose(domain(X0),domain(X1)),X1) = ifeq(domain(X0),domain(X1),compose(domain(X0),X1),compose(compose(domain(X0),domain(X1)),X1)) ).
cnf(u2660,hypothesis,
compose(X0,b) = ifeq(codomain(b),codomain(compose(X0,b)),ifeq(codomain(X0),domain(g),compose(X0,compose(b,codomain(compose(X0,b)))),compose(X0,b)),compose(X0,b)) ).
cnf(u1237,hypothesis,
compose(compose(a,b),codomain(X0)) = ifeq(codomain(b),codomain(X0),compose(a,compose(b,codomain(X0))),compose(compose(a,b),codomain(X0))) ).
cnf(u1368,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(h,compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),h),h),h),h) ).
cnf(u1498,hypothesis,
compose(compose(h,b),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(g),compose(h,compose(b,domain(X0))),compose(compose(h,b),domain(X0))),compose(compose(h,b),domain(X0))) ).
cnf(u5220,hypothesis,
compose(compose(compose(a,b),h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,compose(a,g))),compose(compose(compose(a,b),h),compose(a,g))),compose(compose(compose(a,b),h),compose(a,g))) ).
cnf(u1524,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(a,b),X0,domain(a),a),a),a) ).
cnf(u1492,hypothesis,
compose(compose(compose(a,g),h),h) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,h)),compose(compose(compose(a,g),h),h)),compose(compose(compose(a,g),h),h)) ).
cnf(u211,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(X1,compose(a,b)),compose(X0,compose(a,b)),X1,X0),X0),X0) = X0 ).
cnf(u2021,hypothesis,
compose(b,codomain(X0)) = ifeq(codomain(b),codomain(X0),compose(domain(g),compose(b,codomain(X0))),compose(b,codomain(X0))) ).
cnf(u1100,hypothesis,
compose(compose(a,a),X0) = ifeq(domain(g),domain(X0),ifeq(domain(g),domain(a),compose(a,compose(a,X0)),compose(compose(a,a),X0)),compose(compose(a,a),X0)) ).
cnf(u1911,hypothesis,
compose(compose(compose(a,g),compose(a,g)),codomain(g)) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,g)),compose(compose(compose(a,g),compose(a,g)),codomain(g))) ).
cnf(u1488,hypothesis,
compose(compose(h,domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),h)),compose(compose(h,domain(X0)),h)),compose(compose(h,domain(X0)),h)) ).
cnf(u1119,hypothesis,
compose(compose(h,a),b) = ifeq(codomain(g),domain(a),compose(h,compose(a,b)),compose(compose(h,a),b)) ).
cnf(u417,axiom,
compose(compose(X0,X1),domain(X2)) = ifeq(codomain(X1),domain(X2),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,domain(X2))),compose(compose(X0,X1),domain(X2))),compose(compose(X0,X1),domain(X2))) ).
cnf(u1241,hypothesis,
compose(compose(a,b),h) = ifeq(codomain(b),domain(g),compose(a,compose(b,h)),compose(compose(a,b),h)) ).
cnf(u1149,hypothesis,
compose(compose(compose(a,b),X0),b) = ifeq(codomain(X0),domain(g),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(X0,b)),compose(compose(compose(a,b),X0),b)),compose(compose(compose(a,b),X0),b)) ).
cnf(u1227,hypothesis,
compose(compose(a,domain(X0)),X1) = ifeq(domain(X0),domain(X1),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),X1)),compose(compose(a,domain(X0)),X1)),compose(compose(a,domain(X0)),X1)) ).
cnf(u982,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(compose(a,g),compose(a,b)),domain(X0),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u6240,axiom,
compose(compose(domain(compose(codomain(X0),codomain(X1))),codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(domain(compose(codomain(X0),codomain(X1))),codomain(X0),compose(codomain(X0),codomain(X1)),compose(compose(domain(compose(codomain(X0),codomain(X1))),codomain(X0)),codomain(X1))),compose(compose(domain(compose(codomain(X0),codomain(X1))),codomain(X0)),codomain(X1))) ).
cnf(u879,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(a,compose(a,b)),a,compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u2684,hypothesis,
compose(a,compose(a,g)) = ifeq(codomain(g),codomain(compose(a,compose(a,g))),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),codomain(compose(a,compose(a,g))))),compose(a,compose(a,g))),compose(a,compose(a,g))) ).
cnf(u209,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(h,compose(a,b)),X0,h,X1),X1),X1),X1) = X1 ).
cnf(u4316,hypothesis,
compose(compose(compose(a,g),domain(X1)),codomain(X0)) = ifeq(domain(X1),codomain(X0),ifeq(codomain(g),domain(X1),compose(compose(a,g),compose(domain(X1),codomain(X0))),compose(compose(compose(a,g),domain(X1)),codomain(X0))),compose(compose(compose(a,g),domain(X1)),codomain(X0))) ).
cnf(u5219,hypothesis,
compose(compose(compose(a,g),h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(h,compose(a,g))),compose(compose(compose(a,g),h),compose(a,g))),compose(compose(compose(a,g),h),compose(a,g))) ).
cnf(u3438,hypothesis,
compose(compose(codomain(X1),compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(compose(a,g),X0)),compose(compose(codomain(X1),compose(a,g)),X0)),compose(compose(codomain(X1),compose(a,g)),X0)) ).
cnf(u1247,hypothesis,
compose(compose(a,g),h) = ifeq(codomain(g),domain(g),compose(a,compose(h,h)),compose(compose(a,g),h)) ).
cnf(u993,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(compose(a,b),compose(X0,compose(a,b)),domain(a),X0),X0) = X0 ).
cnf(u236,hypothesis,
codomain(g) = ifeq(codomain(g),domain(g),codomain(compose(h,h)),codomain(g)) ).
cnf(u894,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(compose(a,b),compose(a,b)),a,compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u7299,hypothesis,
compose(compose(domain(compose(compose(a,b),compose(a,b))),compose(a,b)),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(domain(compose(compose(a,b),compose(a,b))),domain(a),compose(compose(a,b),compose(a,b)),compose(compose(domain(compose(compose(a,b),compose(a,b))),compose(a,b)),compose(a,b))),compose(compose(domain(compose(compose(a,b),compose(a,b))),compose(a,b)),compose(a,b))) ).
cnf(u4263,axiom,
compose(compose(domain(X1),domain(X0)),codomain(X2)) = ifeq(domain(X0),codomain(X2),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),codomain(X2))),compose(compose(domain(X1),domain(X0)),codomain(X2))),compose(compose(domain(X1),domain(X0)),codomain(X2))) ).
cnf(u1575,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),ifeq(compose(a,b),compose(compose(a,g),compose(a,b)),compose(a,g),domain(a)),domain(a)) ).
cnf(u4456,hypothesis,
compose(compose(X0,compose(a,b)),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,b),compose(a,g))),compose(compose(X0,compose(a,b)),compose(a,g))),compose(compose(X0,compose(a,b)),compose(a,g))) ).
cnf(u3400,axiom,
compose(compose(codomain(X1),X2),domain(X0)) = ifeq(codomain(X2),domain(X0),ifeq(codomain(X1),domain(X2),compose(codomain(X1),compose(X2,domain(X0))),compose(compose(codomain(X1),X2),domain(X0))),compose(compose(codomain(X1),X2),domain(X0))) ).
cnf(u121,hypothesis,
domain(g) = ifeq(codomain(b),domain(a),domain(compose(b,compose(a,g))),domain(g)) ).
cnf(u483,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),domain(compose(codomain(X0),compose(a,g))),codomain(X0)) ).
cnf(u1910,hypothesis,
compose(compose(compose(a,g),compose(a,b)),codomain(b)) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,b)),compose(compose(compose(a,g),compose(a,b)),codomain(b))) ).
cnf(u2293,hypothesis,
compose(compose(compose(a,g),domain(g)),b) = ifeq(codomain(g),domain(g),compose(compose(a,g),b),compose(compose(compose(a,g),domain(g)),b)) ).
cnf(u3413,hypothesis,
compose(compose(X1,compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(X1),domain(a),compose(X1,compose(compose(a,b),domain(X0))),compose(compose(X1,compose(a,b)),domain(X0))),compose(compose(X1,compose(a,b)),domain(X0))) ).
cnf(u6752,hypothesis,
compose(compose(domain(compose(domain(X0),compose(a,g))),domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(domain(compose(domain(X0),compose(a,g))),domain(X0),compose(domain(X0),compose(a,g)),compose(compose(domain(compose(domain(X0),compose(a,g))),domain(X0)),compose(a,g))),compose(compose(domain(compose(domain(X0),compose(a,g))),domain(X0)),compose(a,g))) ).
cnf(u20,hypothesis,
domain(h) = domain(g) ).
cnf(u2666,hypothesis,
compose(domain(X0),a) = ifeq(domain(g),codomain(compose(domain(X0),a)),ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,codomain(compose(domain(X0),a)))),compose(domain(X0),a)),compose(domain(X0),a)) ).
cnf(u6769,hypothesis,
compose(compose(domain(compose(domain(X0),compose(a,b))),domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(domain(compose(domain(X0),compose(a,b))),domain(X0),compose(domain(X0),compose(a,b)),compose(compose(domain(compose(domain(X0),compose(a,b))),domain(X0)),compose(a,b))),compose(compose(domain(compose(domain(X0),compose(a,b))),domain(X0)),compose(a,b))) ).
cnf(u4475,hypothesis,
compose(compose(X0,compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,g),compose(a,b))),compose(compose(X0,compose(a,g)),compose(a,b))),compose(compose(X0,compose(a,g)),compose(a,b))) ).
cnf(u914,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(h,compose(a,b)),compose(a,g),h),h),h) ).
cnf(u1293,hypothesis,
compose(compose(X0,b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(g),compose(X0,compose(b,compose(a,g))),compose(compose(X0,b),compose(a,g))),compose(compose(X0,b),compose(a,g))) ).
cnf(u3592,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),compose(a,b)),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u3437,hypothesis,
compose(compose(codomain(X1),compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(compose(a,b),X0)),compose(compose(codomain(X1),compose(a,b)),X0)),compose(compose(codomain(X1),compose(a,b)),X0)) ).
cnf(u4776,hypothesis,
compose(compose(compose(a,b),b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(b,compose(a,b))),compose(compose(compose(a,b),b),compose(a,b))),compose(compose(compose(a,b),b),compose(a,b))) ).
cnf(u6870,hypothesis,
compose(compose(compose(a,b),compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),compose(a,g))),compose(compose(compose(a,b),compose(a,g)),compose(a,g))),compose(compose(compose(a,b),compose(a,g)),compose(a,g))) ).
cnf(u249,hypothesis,
codomain(X0) = ifeq(codomain(g),codomain(X0),codomain(compose(h,codomain(X0))),codomain(X0)) ).
cnf(u900,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(compose(a,g),compose(a,b)),compose(a,g),h),h),h) ).
cnf(u267,hypothesis,
domain(a) = ifeq(codomain(g),codomain(X0),domain(compose(compose(a,g),codomain(X0))),domain(a)) ).
cnf(u2294,hypothesis,
compose(compose(compose(a,b),domain(g)),b) = ifeq(codomain(b),domain(g),compose(compose(a,b),b),compose(compose(compose(a,b),domain(g)),b)) ).
cnf(u5120,hypothesis,
compose(compose(codomain(X1),compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(X1),domain(a),compose(codomain(X1),compose(compose(a,b),domain(X0))),compose(compose(codomain(X1),compose(a,b)),domain(X0))),compose(compose(codomain(X1),compose(a,b)),domain(X0))) ).
cnf(u3338,hypothesis,
compose(compose(codomain(X1),b),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(X1),domain(g),compose(codomain(X1),compose(b,domain(X0))),compose(compose(codomain(X1),b),domain(X0))),compose(compose(codomain(X1),b),domain(X0))) ).
cnf(u905,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(h,compose(a,b)),h,domain(X0)),domain(X0)),domain(X0)) ).
cnf(u2076,hypothesis,
compose(codomain(X0),compose(a,g)) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(codomain(X0),compose(a,g))),compose(codomain(X0),compose(a,g))) ).
cnf(u5372,hypothesis,
compose(compose(domain(compose(compose(a,b),b)),compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(domain(compose(compose(a,b),b)),domain(a),compose(compose(a,b),b),compose(compose(domain(compose(compose(a,b),b)),compose(a,b)),b)),compose(compose(domain(compose(compose(a,b),b)),compose(a,b)),b)) ).
cnf(u272,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),domain(compose(domain(X0),compose(a,g))),domain(X0)) ).
cnf(u3462,axiom,
compose(X0,codomain(X1)) = ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X0),codomain(X1))),compose(X0,codomain(X1))) ).
cnf(u1421,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(compose(a,b),compose(a,b)),compose(a,b),codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u919,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(domain(X0),compose(a,b)),h,domain(X0)),domain(X0)),domain(X0)) ).
cnf(u3443,hypothesis,
compose(compose(X0,codomain(X1)),compose(a,g)) = ifeq(codomain(X1),domain(a),ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X1),compose(a,g))),compose(compose(X0,codomain(X1)),compose(a,g))),compose(compose(X0,codomain(X1)),compose(a,g))) ).
cnf(u1822,hypothesis,
compose(compose(compose(a,g),domain(X0)),domain(X0)) = ifeq(codomain(g),domain(X0),compose(compose(a,g),domain(X0)),compose(compose(compose(a,g),domain(X0)),domain(X0))) ).
cnf(u3877,hypothesis,
compose(compose(domain(compose(h,h)),h),h) = ifeq(codomain(g),domain(g),ifeq(domain(compose(h,h)),domain(g),compose(h,h),compose(compose(domain(compose(h,h)),h),h)),compose(compose(domain(compose(h,h)),h),h)) ).
cnf(u510,axiom,
domain(X0) = ifeq(codomain(X1),domain(X0),codomain(compose(codomain(X1),domain(X0))),domain(X0)) ).
cnf(u4614,hypothesis,
compose(compose(compose(a,g),a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,compose(a,g))),compose(compose(compose(a,g),a),compose(a,g))),compose(compose(compose(a,g),a),compose(a,g))) ).
cnf(u2703,hypothesis,
compose(h,compose(a,b)) = ifeq(codomain(b),codomain(compose(h,compose(a,b))),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),codomain(compose(h,compose(a,b))))),compose(h,compose(a,b))),compose(h,compose(a,b))) ).
cnf(u1785,hypothesis,
compose(compose(domain(X0),compose(a,g)),codomain(g)) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,g)),compose(compose(domain(X0),compose(a,g)),codomain(g))) ).
cnf(u3221,hypothesis,
compose(compose(a,g),h) = ifeq(codomain(g),domain(g),compose(compose(a,g),compose(codomain(g),h)),compose(compose(a,g),h)) ).
cnf(u3352,hypothesis,
compose(compose(compose(a,g),b),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,codomain(X0))),compose(compose(compose(a,g),b),codomain(X0))),compose(compose(compose(a,g),b),codomain(X0))) ).
cnf(u1400,hypothesis,
compose(compose(X0,h),codomain(X1)) = ifeq(codomain(g),codomain(X1),ifeq(codomain(X0),domain(g),compose(X0,compose(h,codomain(X1))),compose(compose(X0,h),codomain(X1))),compose(compose(X0,h),codomain(X1))) ).
cnf(u1016,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(compose(a,g),compose(a,b)),codomain(X0),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3202,hypothesis,
compose(compose(codomain(X0),codomain(X1)),h) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),codomain(X1),compose(codomain(X0),compose(codomain(X1),h)),compose(compose(codomain(X0),codomain(X1)),h)),compose(compose(codomain(X0),codomain(X1)),h)) ).
cnf(u3476,hypothesis,
compose(h,compose(a,b)) = ifeq(codomain(g),domain(a),compose(h,compose(codomain(g),compose(a,b))),compose(h,compose(a,b))) ).
cnf(u5403,hypothesis,
compose(compose(domain(compose(h,compose(a,g))),h),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(domain(compose(h,compose(a,g))),domain(g),compose(h,compose(a,g)),compose(compose(domain(compose(h,compose(a,g))),h),compose(a,g))),compose(compose(domain(compose(h,compose(a,g))),h),compose(a,g))) ).
cnf(u677,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(X0),domain(a),X0,X0),X0) = X0 ).
cnf(u4289,axiom,
compose(compose(codomain(X2),codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(codomain(X2),codomain(X0),compose(codomain(X2),compose(codomain(X0),codomain(X1))),compose(compose(codomain(X2),codomain(X0)),codomain(X1))),compose(compose(codomain(X2),codomain(X0)),codomain(X1))) ).
cnf(u2450,hypothesis,
compose(compose(compose(a,g),domain(a)),compose(a,b)) = ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,b)),compose(compose(compose(a,g),domain(a)),compose(a,b))) ).
cnf(u3372,hypothesis,
compose(compose(domain(compose(b,X0)),b),X0) = ifeq(codomain(b),domain(X0),ifeq(domain(compose(b,X0)),domain(g),compose(b,X0),compose(compose(domain(compose(b,X0)),b),X0)),compose(compose(domain(compose(b,X0)),b),X0)) ).
cnf(u675,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(X0,compose(a,b)),compose(a,compose(a,b)),a,X0),X0),X0) = X0 ).
cnf(u907,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(h,compose(a,b)),h,compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u3222,hypothesis,
compose(compose(a,b),h) = ifeq(codomain(b),domain(g),compose(compose(a,b),compose(codomain(b),h)),compose(compose(a,b),h)) ).
cnf(u1693,axiom,
compose(X0,X1) = ifeq(codomain(X1),codomain(compose(X0,X1)),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,codomain(compose(X0,X1)))),compose(X0,X1)),compose(X0,X1)) ).
cnf(u167,hypothesis,
codomain(X0) = ifeq(codomain(g),domain(X0),codomain(compose(h,X0)),codomain(X0)) ).
cnf(u305,hypothesis,
codomain(X0) = ifeq(codomain(b),codomain(X0),codomain(compose(compose(a,b),codomain(X0))),codomain(X0)) ).
cnf(u5668,hypothesis,
compose(compose(domain(X0),compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),compose(domain(X0),compose(compose(a,g),compose(a,b))),compose(compose(domain(X0),compose(a,g)),compose(a,b))),compose(compose(domain(X0),compose(a,g)),compose(a,b))) ).
cnf(u422,hypothesis,
compose(compose(X0,X1),h) = ifeq(codomain(X1),domain(g),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,h)),compose(compose(X0,X1),h)),compose(compose(X0,X1),h)) ).
cnf(u2728,hypothesis,
codomain(X2) = ifeq(codomain(X2),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X2),compose(a,b)),X1,ifeq(compose(codomain(X0),compose(a,b)),X1,codomain(X0),codomain(X2)),codomain(X2)),codomain(X2)),codomain(X2)) ).
cnf(u5202,hypothesis,
compose(compose(h,compose(a,g)),compose(a,b)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,g),compose(a,b))),compose(compose(h,compose(a,g)),compose(a,b))),compose(compose(h,compose(a,g)),compose(a,b))) ).
cnf(u1680,axiom,
compose(compose(codomain(X1),X2),codomain(X0)) = ifeq(codomain(X2),codomain(X0),ifeq(codomain(X1),domain(X2),compose(codomain(X1),compose(X2,codomain(X0))),compose(compose(codomain(X1),X2),codomain(X0))),compose(compose(codomain(X1),X2),codomain(X0))) ).
cnf(u4511,hypothesis,
compose(compose(domain(compose(compose(a,g),X0)),compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(domain(compose(compose(a,g),X0)),domain(a),compose(compose(a,g),X0),compose(compose(domain(compose(compose(a,g),X0)),compose(a,g)),X0)),compose(compose(domain(compose(compose(a,g),X0)),compose(a,g)),X0)) ).
cnf(u922,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(compose(a,b),compose(a,b)),h,compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u2571,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),ifeq(compose(a,b),X0,ifeq(compose(h,compose(a,b)),X0,h,domain(a)),domain(a)),domain(a)) ).
cnf(u4404,hypothesis,
compose(compose(compose(a,g),domain(X0)),domain(X1)) = ifeq(domain(X0),domain(X1),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(domain(X0),domain(X1))),compose(compose(compose(a,g),domain(X0)),domain(X1))),compose(compose(compose(a,g),domain(X0)),domain(X1))) ).
cnf(u3123,hypothesis,
compose(compose(codomain(X0),compose(a,b)),b) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,b),b)),compose(compose(codomain(X0),compose(a,b)),b)),compose(compose(codomain(X0),compose(a,b)),b)) ).
cnf(u165,hypothesis,
h = compose(h,codomain(g)) ).
cnf(u928,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(compose(a,g),compose(a,b)),compose(domain(X0),compose(a,b)),domain(X0),compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u4510,hypothesis,
compose(compose(domain(compose(compose(a,b),X0)),compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(domain(compose(compose(a,b),X0)),domain(a),compose(compose(a,b),X0),compose(compose(domain(compose(compose(a,b),X0)),compose(a,b)),X0)),compose(compose(domain(compose(compose(a,b),X0)),compose(a,b)),X0)) ).
cnf(u433,axiom,
compose(compose(X0,codomain(X1)),X2) = ifeq(codomain(X1),domain(X2),ifeq(codomain(X0),codomain(X1),compose(X0,compose(codomain(X1),X2)),compose(compose(X0,codomain(X1)),X2)),compose(compose(X0,codomain(X1)),X2)) ).
cnf(u665,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(X1,compose(a,b)),X1,domain(X0)),domain(X0)),domain(X0)) ).
cnf(u420,hypothesis,
compose(compose(X0,X1),compose(a,b)) = ifeq(codomain(X1),domain(a),ifeq(codomain(X0),domain(X1),compose(X0,compose(X1,compose(a,b))),compose(compose(X0,X1),compose(a,b))),compose(compose(X0,X1),compose(a,b))) ).
cnf(u54,axiom,
domain(X0) = ifeq(codomain(X0),codomain(X1),domain(compose(X0,codomain(X1))),domain(X0)) ).
cnf(u5040,hypothesis,
compose(compose(domain(compose(b,domain(X0))),b),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(domain(compose(b,domain(X0))),domain(g),compose(b,domain(X0)),compose(compose(domain(compose(b,domain(X0))),b),domain(X0))),compose(compose(domain(compose(b,domain(X0))),b),domain(X0))) ).
cnf(u1471,hypothesis,
compose(compose(compose(a,b),h),b) = ifeq(codomain(g),domain(g),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,b)),compose(compose(compose(a,b),h),b)),compose(compose(compose(a,b),h),b)) ).
cnf(u679,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(codomain(X0),domain(a),codomain(X0),codomain(X0)),codomain(X0)) ).
cnf(u6186,hypothesis,
compose(compose(compose(a,b),codomain(X0)),compose(a,g)) = ifeq(codomain(X0),domain(a),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),compose(a,g))),compose(compose(compose(a,b),codomain(X0)),compose(a,g))),compose(compose(compose(a,b),codomain(X0)),compose(a,g))) ).
cnf(u1716,axiom,
compose(compose(X1,codomain(X0)),codomain(X0)) = ifeq(codomain(X1),codomain(X0),compose(X1,codomain(X0)),compose(compose(X1,codomain(X0)),codomain(X0))) ).
cnf(u4262,axiom,
compose(compose(domain(X2),codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(domain(X2),codomain(X0),compose(domain(X2),compose(codomain(X0),codomain(X1))),compose(compose(domain(X2),codomain(X0)),codomain(X1))),compose(compose(domain(X2),codomain(X0)),codomain(X1))) ).
cnf(u4654,hypothesis,
compose(compose(compose(a,g),compose(a,g)),b) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),b)),compose(compose(compose(a,g),compose(a,g)),b)),compose(compose(compose(a,g),compose(a,g)),b)) ).
cnf(u1714,hypothesis,
compose(compose(X0,compose(a,b)),codomain(b)) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,b)),compose(compose(X0,compose(a,b)),codomain(b))) ).
cnf(u2233,hypothesis,
compose(compose(X1,domain(X0)),compose(a,b)) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),compose(a,b))),compose(compose(X1,domain(X0)),compose(a,b))),compose(compose(X1,domain(X0)),compose(a,b))) ).
cnf(u3150,hypothesis,
compose(compose(compose(a,g),domain(X0)),b) = ifeq(domain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(domain(X0),b)),compose(compose(compose(a,g),domain(X0)),b)),compose(compose(compose(a,g),domain(X0)),b)) ).
cnf(u1963,axiom,
compose(compose(domain(X1),codomain(X2)),X0) = ifeq(codomain(X2),domain(X0),ifeq(domain(X1),codomain(X2),compose(domain(X1),compose(codomain(X2),X0)),compose(compose(domain(X1),codomain(X2)),X0)),compose(compose(domain(X1),codomain(X2)),X0)) ).
cnf(u3072,hypothesis,
compose(compose(codomain(X0),a),compose(a,g)) = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,compose(a,g))),compose(compose(codomain(X0),a),compose(a,g))),compose(compose(codomain(X0),a),compose(a,g))) ).
cnf(u3143,hypothesis,
compose(compose(a,g),b) = ifeq(codomain(g),domain(g),compose(compose(a,g),compose(codomain(g),b)),compose(compose(a,g),b)) ).
cnf(u4768,hypothesis,
compose(compose(compose(a,g),b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,compose(a,g))),compose(compose(compose(a,g),b),compose(a,g))),compose(compose(compose(a,g),b),compose(a,g))) ).
cnf(u5122,axiom,
compose(compose(codomain(X2),codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(codomain(X2),codomain(X0),compose(codomain(X2),compose(codomain(X0),domain(X1))),compose(compose(codomain(X2),codomain(X0)),domain(X1))),compose(compose(codomain(X2),codomain(X0)),domain(X1))) ).
cnf(u682,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(domain(g),domain(a),a,a),a) ).
cnf(u1969,hypothesis,
compose(a,X0) = ifeq(domain(g),domain(X0),compose(domain(a),compose(a,X0)),compose(a,X0)) ).
cnf(u2707,hypothesis,
compose(domain(X0),b) = ifeq(codomain(b),codomain(compose(domain(X0),b)),ifeq(domain(X0),domain(g),compose(domain(X0),compose(b,codomain(compose(domain(X0),b)))),compose(domain(X0),b)),compose(domain(X0),b)) ).
cnf(u840,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(X0,compose(a,b)),compose(compose(a,g),compose(a,b)),X0,compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u2903,hypothesis,
compose(compose(compose(a,g),a),domain(X0)) = ifeq(domain(g),domain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(a,domain(X0))),compose(compose(compose(a,g),a),domain(X0))),compose(compose(compose(a,g),a),domain(X0))) ).
cnf(u1983,hypothesis,
compose(a,domain(X0)) = ifeq(domain(g),domain(X0),compose(domain(a),compose(a,domain(X0))),compose(a,domain(X0))) ).
cnf(u3426,hypothesis,
compose(compose(codomain(X0),X1),compose(a,b)) = ifeq(codomain(X1),domain(a),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(X1,compose(a,b))),compose(compose(codomain(X0),X1),compose(a,b))),compose(compose(codomain(X0),X1),compose(a,b))) ).
cnf(u1622,hypothesis,
domain(a) = ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),compose(a,b),compose(a,b),domain(a)),domain(a)) ).
cnf(u4924,hypothesis,
compose(compose(domain(compose(codomain(X0),h)),codomain(X0)),h) = ifeq(codomain(X0),domain(g),ifeq(domain(compose(codomain(X0),h)),codomain(X0),compose(codomain(X0),h),compose(compose(domain(compose(codomain(X0),h)),codomain(X0)),h)),compose(compose(domain(compose(codomain(X0),h)),codomain(X0)),h)) ).
cnf(u1483,hypothesis,
compose(compose(h,h),h) = ifeq(codomain(g),domain(g),ifeq(codomain(g),domain(g),compose(h,compose(h,h)),compose(compose(h,h),h)),compose(compose(h,h),h)) ).
cnf(u1093,hypothesis,
compose(compose(X0,a),compose(a,b)) = ifeq(domain(g),domain(a),ifeq(codomain(X0),domain(a),compose(X0,compose(a,compose(a,b))),compose(compose(X0,a),compose(a,b))),compose(compose(X0,a),compose(a,b))) ).
cnf(u1354,hypothesis,
compose(compose(a,domain(X0)),h) = ifeq(domain(X0),domain(g),ifeq(domain(g),domain(X0),compose(a,compose(domain(X0),h)),compose(compose(a,domain(X0)),h)),compose(compose(a,domain(X0)),h)) ).
cnf(u6345,axiom,
compose(compose(domain(compose(domain(X0),domain(X1))),domain(X0)),domain(X1)) = ifeq(domain(X0),domain(X1),ifeq(domain(compose(domain(X0),domain(X1))),domain(X0),compose(domain(X0),domain(X1)),compose(compose(domain(compose(domain(X0),domain(X1))),domain(X0)),domain(X1))),compose(compose(domain(compose(domain(X0),domain(X1))),domain(X0)),domain(X1))) ).
cnf(u3339,hypothesis,
compose(compose(compose(a,g),b),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(g),compose(compose(a,g),compose(b,domain(X0))),compose(compose(compose(a,g),b),domain(X0))),compose(compose(compose(a,g),b),domain(X0))) ).
cnf(u205,hypothesis,
ifeq(codomain(X1),domain(a),ifeq(codomain(X2),domain(a),ifeq(compose(X1,compose(a,b)),X0,ifeq(compose(codomain(X2),compose(a,b)),X0,codomain(X2),X1),X1),X1),X1) = X1 ).
cnf(u2655,axiom,
compose(codomain(X0),X1) = ifeq(codomain(X1),codomain(compose(codomain(X0),X1)),ifeq(codomain(X0),domain(X1),compose(codomain(X0),compose(X1,codomain(compose(codomain(X0),X1)))),compose(codomain(X0),X1)),compose(codomain(X0),X1)) ).
cnf(u6077,hypothesis,
compose(compose(compose(a,g),compose(a,b)),domain(X0)) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,b),domain(X0))),compose(compose(compose(a,g),compose(a,b)),domain(X0))),compose(compose(compose(a,g),compose(a,b)),domain(X0))) ).
cnf(u1097,hypothesis,
compose(compose(codomain(X0),a),X1) = ifeq(domain(g),domain(X1),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,X1)),compose(compose(codomain(X0),a),X1)),compose(compose(codomain(X0),a),X1)) ).
cnf(u1750,hypothesis,
compose(compose(compose(a,b),b),codomain(b)) = ifeq(codomain(b),domain(g),compose(compose(a,b),b),compose(compose(compose(a,b),b),codomain(b))) ).
cnf(u2661,hypothesis,
compose(X0,h) = ifeq(codomain(g),codomain(compose(X0,h)),ifeq(codomain(X0),domain(g),compose(X0,compose(h,codomain(compose(X0,h)))),compose(X0,h)),compose(X0,h)) ).
cnf(u838,hypothesis,
domain(X0) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(X1,compose(a,b)),compose(domain(X0),compose(a,b)),X1,domain(X0)),domain(X0)),domain(X0)) ).
cnf(u1221,hypothesis,
compose(compose(a,g),X0) = ifeq(codomain(g),domain(X0),compose(a,compose(g,X0)),compose(compose(a,g),X0)) ).
cnf(u1352,hypothesis,
compose(compose(a,compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),h)),compose(compose(a,compose(a,g)),h)),compose(compose(a,compose(a,g)),h)) ).
cnf(u3415,axiom,
compose(compose(X1,codomain(X2)),domain(X0)) = ifeq(codomain(X2),domain(X0),ifeq(codomain(X1),codomain(X2),compose(X1,compose(codomain(X2),domain(X0))),compose(compose(X1,codomain(X2)),domain(X0))),compose(compose(X1,codomain(X2)),domain(X0))) ).
cnf(u3940,axiom,
compose(domain(X0),codomain(X1)) = ifeq(codomain(X1),codomain(compose(domain(X0),codomain(X1))),ifeq(domain(X0),codomain(X1),compose(domain(X0),compose(codomain(X1),codomain(compose(domain(X0),codomain(X1))))),compose(domain(X0),codomain(X1))),compose(domain(X0),codomain(X1))) ).
cnf(u2659,hypothesis,
compose(h,X0) = ifeq(codomain(X0),codomain(compose(h,X0)),ifeq(codomain(g),domain(X0),compose(h,compose(X0,codomain(compose(h,X0)))),compose(h,X0)),compose(h,X0)) ).
cnf(u844,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(domain(X1),domain(a),ifeq(compose(domain(X1),compose(a,b)),compose(X0,compose(a,b)),domain(X1),X0),X0),X0) = X0 ).
cnf(u6138,hypothesis,
compose(compose(codomain(X0),compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(compose(a,g),compose(a,g))),compose(compose(codomain(X0),compose(a,g)),compose(a,g))),compose(compose(codomain(X0),compose(a,g)),compose(a,g))) ).
cnf(u1110,hypothesis,
compose(compose(compose(a,b),a),g) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,g)),compose(compose(compose(a,b),a),g)) ).
cnf(u2005,hypothesis,
compose(domain(X0),b) = ifeq(domain(X0),domain(g),compose(domain(X0),compose(domain(X0),b)),compose(domain(X0),b)) ).
cnf(u5464,hypothesis,
compose(compose(a,b),compose(a,g)) = ifeq(codomain(g),codomain(compose(compose(a,b),compose(a,g))),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),codomain(compose(compose(a,b),compose(a,g))))),compose(compose(a,b),compose(a,g))),compose(compose(a,b),compose(a,g))) ).
cnf(u4706,hypothesis,
compose(compose(compose(a,b),compose(a,g)),h) = ifeq(codomain(g),domain(g),ifeq(codomain(b),domain(a),compose(compose(a,b),compose(compose(a,g),h)),compose(compose(compose(a,b),compose(a,g)),h)),compose(compose(compose(a,b),compose(a,g)),h)) ).
cnf(u1103,hypothesis,
compose(compose(X0,a),g) = ifeq(codomain(X0),domain(a),compose(X0,compose(a,g)),compose(compose(X0,a),g)) ).
cnf(u1225,hypothesis,
compose(compose(a,compose(a,g)),X0) = ifeq(codomain(g),domain(X0),ifeq(domain(g),domain(a),compose(a,compose(compose(a,g),X0)),compose(compose(a,compose(a,g)),X0)),compose(compose(a,compose(a,g)),X0)) ).
cnf(u2003,hypothesis,
compose(compose(a,g),b) = ifeq(codomain(g),domain(g),compose(domain(a),compose(compose(a,g),b)),compose(compose(a,g),b)) ).
cnf(u222,hypothesis,
domain(g) = ifeq(codomain(b),domain(a),codomain(compose(compose(a,b),a)),domain(g)) ).
cnf(u1365,hypothesis,
h = ifeq(codomain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(h,compose(a,b)),X1,ifeq(compose(domain(X0),compose(a,b)),X1,domain(X0),h),h),h),h) ).
cnf(u1114,hypothesis,
compose(compose(domain(X0),a),b) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,b)),compose(compose(domain(X0),a),b)) ).
cnf(u1388,hypothesis,
compose(compose(h,X0),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(codomain(g),domain(X0),compose(h,compose(X0,codomain(X1))),compose(compose(h,X0),codomain(X1))),compose(compose(h,X0),codomain(X1))) ).
cnf(u1108,hypothesis,
compose(compose(codomain(X0),a),g) = ifeq(codomain(X0),domain(a),compose(codomain(X0),compose(a,g)),compose(compose(codomain(X0),a),g)) ).
cnf(u1238,hypothesis,
compose(compose(a,b),compose(a,g)) = ifeq(codomain(b),domain(a),compose(a,compose(b,compose(a,g))),compose(compose(a,b),compose(a,g))) ).
cnf(u477,hypothesis,
domain(a) = ifeq(codomain(b),domain(X0),domain(compose(compose(a,b),domain(X0))),domain(a)) ).
cnf(u2023,hypothesis,
compose(b,compose(a,b)) = ifeq(codomain(b),domain(a),compose(domain(g),compose(b,compose(a,b))),compose(b,compose(a,b))) ).
cnf(u1231,hypothesis,
compose(compose(a,g),codomain(X0)) = ifeq(codomain(g),codomain(X0),compose(a,compose(g,codomain(X0))),compose(compose(a,g),codomain(X0))) ).
cnf(u3384,hypothesis,
compose(compose(codomain(X0),b),compose(a,b)) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(g),compose(codomain(X0),compose(b,compose(a,b))),compose(compose(codomain(X0),b),compose(a,b))),compose(compose(codomain(X0),b),compose(a,b))) ).
cnf(u220,hypothesis,
domain(g) = ifeq(codomain(X0),domain(a),codomain(compose(codomain(X0),a)),domain(g)) ).
cnf(u1123,hypothesis,
compose(compose(compose(a,b),a),h) = ifeq(codomain(b),domain(a),compose(compose(a,b),compose(a,g)),compose(compose(compose(a,b),a),h)) ).
cnf(u878,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(a),ifeq(domain(g),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(a,compose(a,b)),a,codomain(X0)),codomain(X0)),codomain(X0)) ).
cnf(u4469,hypothesis,
compose(compose(compose(a,b),X0),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(X0,compose(a,b))),compose(compose(compose(a,b),X0),compose(a,b))),compose(compose(compose(a,b),X0),compose(a,b))) ).
cnf(u1493,hypothesis,
compose(compose(compose(a,b),h),h) = ifeq(codomain(g),domain(g),ifeq(codomain(b),domain(g),compose(compose(a,b),compose(h,h)),compose(compose(compose(a,b),h),h)),compose(compose(compose(a,b),h),h)) ).
cnf(u1112,hypothesis,
compose(compose(h,a),g) = ifeq(codomain(g),domain(a),compose(h,compose(a,g)),compose(compose(h,a),g)) ).
cnf(u2663,hypothesis,
compose(X0,compose(a,g)) = ifeq(codomain(g),codomain(compose(X0,compose(a,g))),ifeq(codomain(X0),domain(a),compose(X0,compose(compose(a,g),codomain(compose(X0,compose(a,g))))),compose(X0,compose(a,g))),compose(X0,compose(a,g))) ).
cnf(u1242,hypothesis,
compose(compose(a,g),domain(X0)) = ifeq(codomain(g),domain(X0),compose(a,compose(h,domain(X0))),compose(compose(a,g),domain(X0))) ).
cnf(u105,hypothesis,
codomain(X0) = ifeq(codomain(X0),domain(g),domain(compose(codomain(X0),b)),codomain(X0)) ).
cnf(u884,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(domain(X0),domain(a),ifeq(compose(domain(X0),compose(a,b)),compose(a,compose(a,b)),domain(X0),a),a),a) ).
cnf(u1150,hypothesis,
compose(compose(a,X0),b) = ifeq(codomain(X0),domain(g),ifeq(domain(g),domain(X0),compose(a,compose(X0,b)),compose(compose(a,X0),b)),compose(compose(a,X0),b)) ).
cnf(u1236,hypothesis,
compose(compose(a,b),domain(X0)) = ifeq(codomain(b),domain(X0),compose(a,compose(b,domain(X0))),compose(compose(a,b),domain(X0))) ).
cnf(u3550,hypothesis,
codomain(X1) = ifeq(codomain(X1),domain(a),ifeq(codomain(b),domain(a),ifeq(compose(codomain(X1),compose(a,b)),X0,ifeq(compose(compose(a,b),compose(a,b)),X0,compose(a,b),codomain(X1)),codomain(X1)),codomain(X1)),codomain(X1)) ).
cnf(u889,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(h,compose(a,b)),compose(a,compose(a,b)),h,a),a),a) ).
cnf(u2232,hypothesis,
compose(compose(X1,domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(codomain(X1),domain(X0),compose(X1,compose(domain(X0),compose(a,g))),compose(compose(X1,domain(X0)),compose(a,g))),compose(compose(X1,domain(X0)),compose(a,g))) ).
cnf(u210,hypothesis,
ifeq(codomain(X0),domain(a),ifeq(codomain(X1),domain(a),ifeq(compose(X0,compose(a,b)),compose(X1,compose(a,b)),X1,X0),X0),X0) = X0 ).
cnf(u1405,hypothesis,
compose(compose(domain(X0),h),X1) = ifeq(codomain(g),domain(X1),ifeq(domain(X0),domain(g),compose(domain(X0),compose(h,X1)),compose(compose(domain(X0),h),X1)),compose(compose(domain(X0),h),X1)) ).
cnf(u4405,hypothesis,
compose(compose(compose(a,b),domain(X0)),domain(X1)) = ifeq(domain(X0),domain(X1),ifeq(codomain(b),domain(X0),compose(compose(a,b),compose(domain(X0),domain(X1))),compose(compose(compose(a,b),domain(X0)),domain(X1))),compose(compose(compose(a,b),domain(X0)),domain(X1))) ).
cnf(u5127,hypothesis,
compose(compose(compose(a,b),codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),domain(X1))),compose(compose(compose(a,b),codomain(X0)),domain(X1))),compose(compose(compose(a,b),codomain(X0)),domain(X1))) ).
cnf(u4381,hypothesis,
compose(compose(domain(X1),domain(X0)),compose(a,g)) = ifeq(domain(X0),domain(a),ifeq(domain(X1),domain(X0),compose(domain(X1),compose(domain(X0),compose(a,g))),compose(compose(domain(X1),domain(X0)),compose(a,g))),compose(compose(domain(X1),domain(X0)),compose(a,g))) ).
cnf(u1240,hypothesis,
compose(compose(a,b),b) = ifeq(codomain(b),domain(g),compose(a,compose(b,b)),compose(compose(a,b),b)) ).
cnf(u233,hypothesis,
codomain(g) = ifeq(codomain(g),domain(g),codomain(compose(compose(a,g),h)),codomain(g)) ).
cnf(u1148,hypothesis,
compose(compose(compose(a,g),X0),b) = ifeq(codomain(X0),domain(g),ifeq(codomain(g),domain(X0),compose(compose(a,g),compose(X0,b)),compose(compose(compose(a,g),X0),b)),compose(compose(compose(a,g),X0),b)) ).
cnf(u6858,hypothesis,
compose(compose(compose(a,g),compose(a,g)),compose(a,g)) = ifeq(codomain(g),domain(a),ifeq(codomain(g),domain(a),compose(compose(a,g),compose(compose(a,g),compose(a,g))),compose(compose(compose(a,g),compose(a,g)),compose(a,g))),compose(compose(compose(a,g),compose(a,g)),compose(a,g))) ).
cnf(u3281,hypothesis,
compose(compose(a,compose(a,b)),codomain(X0)) = ifeq(codomain(b),codomain(X0),ifeq(domain(g),domain(a),compose(a,compose(compose(a,b),codomain(X0))),compose(compose(a,compose(a,b)),codomain(X0))),compose(compose(a,compose(a,b)),codomain(X0))) ).
cnf(u3717,hypothesis,
compose(compose(h,codomain(X0)),codomain(X1)) = ifeq(codomain(X0),codomain(X1),ifeq(codomain(g),codomain(X0),compose(h,compose(codomain(X0),codomain(X1))),compose(compose(h,codomain(X0)),codomain(X1))),compose(compose(h,codomain(X0)),codomain(X1))) ).
cnf(u2022,hypothesis,
compose(b,compose(a,g)) = ifeq(codomain(b),domain(a),compose(domain(g),compose(b,compose(a,g))),compose(b,compose(a,g))) ).
cnf(u6200,hypothesis,
compose(compose(compose(a,b),codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(codomain(b),codomain(X0),compose(compose(a,b),compose(codomain(X0),compose(a,b))),compose(compose(compose(a,b),codomain(X0)),compose(a,b))),compose(compose(compose(a,b),codomain(X0)),compose(a,b))) ).
cnf(u122,hypothesis,
domain(g) = ifeq(codomain(b),domain(a),domain(compose(b,compose(a,b))),domain(g)) ).
cnf(u1017,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(codomain(X0),domain(a),ifeq(compose(codomain(X0),compose(a,b)),compose(compose(a,b),compose(a,b)),codomain(X0),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u4363,hypothesis,
compose(compose(domain(X1),codomain(X0)),compose(a,b)) = ifeq(codomain(X0),domain(a),ifeq(domain(X1),codomain(X0),compose(domain(X1),compose(codomain(X0),compose(a,b))),compose(compose(domain(X1),codomain(X0)),compose(a,b))),compose(compose(domain(X1),codomain(X0)),compose(a,b))) ).
cnf(u962,hypothesis,
a = ifeq(domain(g),domain(a),ifeq(codomain(g),domain(a),ifeq(compose(a,compose(a,b)),X0,ifeq(compose(compose(a,g),compose(a,b)),X0,compose(a,g),a),a),a),a) ).
cnf(u2028,hypothesis,
compose(h,compose(a,g)) = ifeq(codomain(g),domain(a),compose(domain(g),compose(h,compose(a,g))),compose(h,compose(a,g))) ).
cnf(u1395,hypothesis,
compose(compose(h,compose(a,b)),X0) = ifeq(codomain(b),domain(X0),ifeq(codomain(g),domain(a),compose(h,compose(compose(a,b),X0)),compose(compose(h,compose(a,b)),X0)),compose(compose(h,compose(a,b)),X0)) ).
cnf(u638,hypothesis,
domain(a) = ifeq(codomain(g),domain(a),domain(compose(compose(a,g),compose(a,b))),domain(a)) ).
cnf(u2301,hypothesis,
compose(compose(compose(a,b),domain(g)),h) = ifeq(codomain(b),domain(g),compose(compose(a,b),h),compose(compose(compose(a,b),domain(g)),h)) ).
cnf(u2319,hypothesis,
compose(compose(domain(X0),domain(a)),compose(a,g)) = ifeq(domain(X0),domain(a),compose(domain(X0),compose(a,g)),compose(compose(domain(X0),domain(a)),compose(a,g))) ).
cnf(u2026,hypothesis,
compose(h,domain(X0)) = ifeq(codomain(g),domain(X0),compose(domain(g),compose(h,domain(X0))),compose(h,domain(X0))) ).
cnf(u507,hypothesis,
codomain(b) = ifeq(codomain(X0),domain(a),codomain(compose(codomain(X0),compose(a,b))),codomain(b)) ).
cnf(u3718,hypothesis,
compose(compose(h,domain(X0)),codomain(X1)) = ifeq(domain(X0),codomain(X1),ifeq(codomain(g),domain(X0),compose(h,compose(domain(X0),codomain(X1))),compose(compose(h,domain(X0)),codomain(X1))),compose(compose(h,domain(X0)),codomain(X1))) ).
cnf(u5397,hypothesis,
compose(compose(domain(compose(b,compose(a,g))),b),compose(a,g)) = ifeq(codomain(b),domain(a),ifeq(domain(compose(b,compose(a,g))),domain(g),compose(b,compose(a,g)),compose(compose(domain(compose(b,compose(a,g))),b),compose(a,g))),compose(compose(domain(compose(b,compose(a,g))),b),compose(a,g))) ).
cnf(u1763,hypothesis,
compose(compose(compose(a,b),h),codomain(g)) = ifeq(codomain(b),domain(g),compose(compose(a,b),h),compose(compose(compose(a,b),h),codomain(g))) ).
cnf(u893,hypothesis,
compose(a,g) = ifeq(codomain(g),domain(a),ifeq(domain(g),domain(a),ifeq(compose(a,compose(a,b)),compose(compose(a,g),compose(a,b)),a,compose(a,g)),compose(a,g)),compose(a,g)) ).
cnf(u120,hypothesis,
domain(g) = ifeq(codomain(b),codomain(X0),domain(compose(b,codomain(X0))),domain(g)) ).
cnf(u250,hypothesis,
domain(X0) = ifeq(codomain(g),domain(X0),codomain(compose(h,domain(X0))),domain(X0)) ).
cnf(u2292,hypothesis,
compose(compose(codomain(X0),domain(g)),b) = ifeq(codomain(X0),domain(g),compose(codomain(X0),b),compose(compose(codomain(X0),domain(g)),b)) ).
cnf(u1523,hypothesis,
compose(a,b) = ifeq(codomain(b),domain(a),ifeq(compose(compose(a,b),compose(a,b)),X0,ifeq(compose(a,b),X0,domain(a),compose(a,b)),compose(a,b)),compose(a,b)) ).
cnf(u4358,axiom,
compose(compose(domain(X2),codomain(X0)),domain(X1)) = ifeq(codomain(X0),domain(X1),ifeq(domain(X2),codomain(X0),compose(domain(X2),compose(codomain(X0),domain(X1))),compose(compose(domain(X2),codomain(X0)),domain(X1))),compose(compose(domain(X2),codomain(X0)),domain(X1))) ).
cnf(u1152,hypothesis,
compose(compose(X0,b),b) = ifeq(codomain(b),domain(g),ifeq(codomain(X0),domain(g),compose(X0,compose(b,b)),compose(compose(X0,b),b)),compose(compose(X0,b),b)) ).
cnf(u3460,axiom,
compose(X0,X1) = ifeq(codomain(X0),domain(X1),compose(X0,compose(codomain(X0),X1)),compose(X0,X1)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CAT001-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.29 % Computer : n005.cluster.edu
% 0.11/0.29 % Model : x86_64 x86_64
% 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.29 % Memory : 8046.5625MB
% 0.11/0.29 % OS : Linux 6.8.0-71-generic
% 0.11/0.29 % CPULimit : 300
% 0.11/0.29 % WCLimit : 300
% 0.11/0.29 % DateTime : Mon Sep 28 21:11:02 UTC 2026
% 0.11/0.29 % CPUTime :
% 0.11/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.34 Running first-order theorem proving
% 0.28/0.34 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.10/4.02 % (1181117)Detected a unit-equality problem, will run specialized UEQ schedule.
% 20.10/4.02 % (1181125)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3189085356:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 20.10/4.02 % (1181123)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2854120463:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 20.10/4.02 % (1181124)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1064393831:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 20.10/4.02 % (1181122)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=292228346:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 20.10/4.02 % (1181125)Instruction limit reached!
% 20.10/4.02 % (1181125)------------------------------
% 20.10/4.02 % (1181125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181125)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181125)Termination reason: Instruction limit
% 20.10/4.02 % (1181125)Termination phase: Saturation
% 20.10/4.02 % (1181125)Time elapsed: 0.071 s
% 20.10/4.02 % (1181125)Peak memory usage: 89 MB
% 20.10/4.02 % (1181125)Instructions burned: 137 (million)
% 20.10/4.02 % (1181128)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=110669398:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 20.10/4.02 % (1181126)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3798201895:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 20.10/4.02 % (1181127)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2017644691:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 20.10/4.02 % (1181136)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2860285483:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 20.10/4.02 % (1181126)Instruction limit reached!
% 20.10/4.02 % (1181126)------------------------------
% 20.10/4.02 % (1181126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181126)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181126)Termination reason: Instruction limit
% 20.10/4.02 % (1181126)Termination phase: Saturation
% 20.10/4.02 % (1181126)Time elapsed: 0.164 s
% 20.10/4.02 % (1181126)Peak memory usage: 89 MB
% 20.10/4.02 % (1181126)Instructions burned: 181 (million)
% 20.10/4.02 % (1181127)Instruction limit reached!
% 20.10/4.02 % (1181127)------------------------------
% 20.10/4.02 % (1181127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181127)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181127)Termination reason: Instruction limit
% 20.10/4.02 % (1181127)Termination phase: Saturation
% 20.10/4.02 % (1181127)Time elapsed: 0.260 s
% 20.10/4.02 % (1181127)Peak memory usage: 91 MB
% 20.10/4.02 % (1181127)Instructions burned: 257 (million)
% 20.10/4.02 % (1181138)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=579846409:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 20.10/4.02 % (1181139)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2526339188:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 20.10/4.02 % (1181139)Instruction limit reached!
% 20.10/4.02 % (1181139)------------------------------
% 20.10/4.02 % (1181139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181139)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181139)Termination reason: Instruction limit
% 20.10/4.02 % (1181139)Termination phase: Saturation
% 20.10/4.02 % (1181139)Time elapsed: 0.181 s
% 20.10/4.02 % (1181139)Peak memory usage: 91 MB
% 20.10/4.02 % (1181139)Instructions burned: 215 (million)
% 20.10/4.02 % (1181142)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=3076029730:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/317Mi)
% 20.10/4.02 % (1181142)Instruction limit reached!
% 20.10/4.02 % (1181142)------------------------------
% 20.10/4.02 % (1181142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181142)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181142)Termination reason: Instruction limit
% 20.10/4.02 % (1181142)Termination phase: Saturation
% 20.10/4.02 % (1181142)Time elapsed: 0.165 s
% 20.10/4.02 % (1181142)Peak memory usage: 92 MB
% 20.10/4.02 % (1181142)Instructions burned: 319 (million)
% 20.10/4.02 % (1181128)Instruction limit reached!
% 20.10/4.02 % (1181128)------------------------------
% 20.10/4.02 % (1181128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181128)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181128)Termination reason: Instruction limit
% 20.10/4.02 % (1181128)Termination phase: Saturation
% 20.10/4.02 % (1181128)Time elapsed: 1.096 s
% 20.10/4.02 % (1181128)Peak memory usage: 96 MB
% 20.10/4.02 % (1181128)Instructions burned: 1188 (million)
% 20.10/4.02 % (1181144)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=224235380:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/12125Mi)
% 20.10/4.02 % (1181145)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3052531321:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2986 on theBenchmark for (2986ds/2836Mi)
% 20.10/4.02 % (1181136)Instruction limit reached!
% 20.10/4.02 % (1181136)------------------------------
% 20.10/4.02 % (1181136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.10/4.02 % (1181136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.10/4.02 % (1181136)CaDiCaL version: 2.1.3
% 20.10/4.02 % (1181136)Termination reason: Instruction limit
% 20.10/4.02 % (1181136)Termination phase: Saturation
% 20.10/4.02 % (1181136)Time elapsed: 1.924 s
% 20.10/4.02 % (1181136)Peak memory usage: 141 MB
% 20.10/4.02 % (1181136)Instructions burned: 2051 (million)
% 20.10/4.02 % (1181145)First to succeed.
% 20.10/4.02 % (1181145)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1181117"
% 20.10/4.02 % (1181148)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2299444582:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2976 on theBenchmark for (2976ds/14534Mi)
% 20.10/4.02 % SZS status Satisfiable for theBenchmark
% 20.10/4.02 % SZS output start Saturation.
% See solution above
% 0.32/4.40 % SZS output start Definitions and Model Updates.
% 0.32/4.40 % SZS output end Definitions and Model Updates.
% 0.32/4.40 % (1181145)------------------------------
% 0.32/4.40 % (1181145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.32/4.40 % (1181145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/4.40 % (1181145)CaDiCaL version: 2.1.3
% 0.32/4.40 % (1181145)Termination reason: Satisfiable
% 0.32/4.40 % (1181145)Time elapsed: 0.941 s
% 0.32/4.40 % (1181145)Peak memory usage: 102 MB
% 0.32/4.40 % (1181145)Instructions burned: 930 (million)
% 0.32/4.40 % (1181145)------------------------------
% 0.32/4.40 % (1181145)------------------------------
% 0.32/4.40 % (1181117)Success in time 2.915 s
% 0.32/4.40 % Vampire exiting
%------------------------------------------------------------------------------