%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT002-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:33 AM UTC 2026
% Result : Satisfiable 10.75s 2.50s
% Output : Saturation 12.56s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u6429,hypothesis,
( codomain(X0) != domain(a)
| compose(h,compose(codomain(X0),compose(a,b))) = compose(compose(h,codomain(X0)),compose(a,b)) ) ).
cnf(u9527,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(X2)
| compose(domain(X2),compose(codomain(X0),codomain(X1))) = compose(compose(domain(X2),codomain(X0)),codomain(X1)) ) ).
cnf(u14387,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(compose(h,a),compose(h,a))) = compose(compose(a,compose(h,a)),compose(h,a)) ) ).
cnf(u8703,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(compose(h,a),compose(codomain(X0),domain(X1))) = compose(compose(compose(h,a),codomain(X0)),domain(X1)) ) ).
cnf(u2896,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(h,a),codomain(X0)) = compose(compose(compose(h,a),codomain(X0)),codomain(X0)) ) ).
cnf(u21,hypothesis,
( compose(X0,a) != compose(X2,a)
| domain(b) != codomain(X2)
| codomain(X0) != domain(a)
| X0 = X2 ) ).
cnf(u6792,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(g,a),g)) ) ).
cnf(u5271,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(a,compose(h,compose(h,a))) = compose(compose(a,h),compose(h,a)) ) ).
cnf(u10746,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,a)) = compose(domain(a),compose(compose(a,b),compose(h,a))) ) ).
cnf(u4662,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),compose(g,a))) = compose(compose(domain(X0),compose(a,b)),compose(g,a)) ) ).
cnf(u1675,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != domain(h)
| compose(domain(X1),compose(h,codomain(X0))) = compose(compose(domain(X1),h),codomain(X0)) ) ).
cnf(u13731,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != codomain(X1)
| compose(codomain(X0),compose(codomain(X1),compose(g,a))) = compose(compose(codomain(X0),codomain(X1)),compose(g,a)) ) ).
cnf(u32,hypothesis,
( domain(a) != codomain(h)
| domain(X0) != domain(b)
| compose(g,compose(a,X0)) = compose(compose(g,a),X0) ) ).
cnf(u5276,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(h,a))) = compose(compose(h,h),compose(h,a)) ) ).
cnf(u2066,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),X0) = compose(compose(compose(g,a),X0),codomain(X0)) ) ).
cnf(u1681,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(h,compose(a,b)))) = compose(compose(domain(X0),h),compose(h,compose(a,b))) ) ).
cnf(u6948,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(h,a),g)) ) ).
cnf(u7214,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(a,compose(codomain(X0),X1)) = compose(compose(a,codomain(X0)),X1) ) ).
cnf(u7300,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(g,a)) = compose(X0,compose(codomain(X0),compose(g,a))) ) ).
cnf(u8338,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,compose(a,b))) = compose(compose(compose(a,b),compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u295,axiom,
compose(X0,compose(codomain(X0),codomain(X0))) = X0 ).
cnf(u10237,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,compose(a,b)),compose(compose(h,a),compose(a,b))) = compose(compose(compose(h,compose(a,b)),compose(h,a)),compose(a,b)) ) ).
cnf(u417,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(a)
| compose(X0,compose(compose(h,a),compose(a,b))) = compose(compose(X0,compose(h,a)),compose(a,b)) ) ).
cnf(u14388,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(compose(h,a),compose(h,a))) = compose(compose(compose(g,a),compose(h,a)),compose(h,a)) ) ).
cnf(u7219,axiom,
( codomain(X0) != domain(X1)
| compose(X0,X1) = compose(X0,compose(codomain(X0),X1)) ) ).
cnf(u15753,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(codomain(X0),compose(compose(g,a),compose(h,a))) = compose(compose(codomain(X0),compose(g,a)),compose(h,a)) ) ).
cnf(u1576,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(a)
| compose(compose(a,b),compose(domain(X0),compose(a,b))) = compose(compose(compose(a,b),domain(X0)),compose(a,b)) ) ).
cnf(u8070,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(g,a)) = compose(compose(a,domain(h)),compose(g,a)) ) ).
cnf(u2079,axiom,
( domain(X0) != codomain(X1)
| compose(X1,domain(X0)) = compose(compose(X1,domain(X0)),domain(X0)) ) ).
cnf(u9106,hypothesis,
( codomain(X0) != domain(b)
| domain(a) != domain(h)
| compose(h,compose(compose(h,a),codomain(X0))) = compose(compose(h,compose(h,a)),codomain(X0)) ) ).
cnf(u9895,hypothesis,
( codomain(X0) != codomain(b)
| domain(b) != domain(h)
| compose(compose(g,a),compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(compose(g,a),compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u5795,hypothesis,
( domain(X0) != domain(a)
| compose(h,domain(X0)) = compose(h,compose(domain(a),domain(X0))) ) ).
cnf(u201,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(compose(domain(X0),a),b) ) ).
cnf(u8211,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(g,compose(g,a))) = compose(compose(g,g),compose(g,a)) ) ).
cnf(u17414,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(h,compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(h,compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u9780,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != domain(b)
| compose(codomain(X1),compose(compose(h,a),codomain(X0))) = compose(compose(codomain(X1),compose(h,a)),codomain(X0)) ) ).
cnf(u2996,hypothesis,
( codomain(X0) != codomain(b)
| domain(b) != domain(a)
| compose(a,compose(compose(a,b),codomain(X0))) = compose(compose(a,compose(a,b)),codomain(X0)) ) ).
cnf(u7938,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,a)) = compose(compose(compose(a,b),domain(h)),compose(h,a)) ) ).
cnf(u6484,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,b)) = compose(X0,compose(codomain(X0),compose(a,b))) ) ).
cnf(u3501,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(X0,domain(X1))) = compose(compose(compose(h,a),X0),domain(X1)) ) ).
cnf(u2472,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(g,compose(compose(g,a),X0)) = compose(compose(g,compose(g,a)),X0) ) ).
cnf(u575,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != domain(h)
| compose(domain(X1),compose(g,codomain(X0))) = compose(compose(domain(X1),g),codomain(X0)) ) ).
cnf(u17418,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(compose(g,a),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u2622,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(compose(h,a),compose(compose(a,b),X0)) = compose(compose(compose(h,a),compose(a,b)),X0) ) ).
cnf(u952,hypothesis,
( domain(b) != domain(a)
| codomain(b) = codomain(compose(compose(g,a),compose(a,b))) ) ).
cnf(u5133,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(a,compose(g,codomain(X0))) = compose(compose(a,g),codomain(X0)) ) ).
cnf(u89,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != codomain(b)
| compose(X1,compose(compose(h,compose(a,b)),X0)) = compose(compose(X1,compose(h,compose(a,b))),X0) ) ).
cnf(u11695,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(h,domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u3505,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != domain(a)
| compose(g,compose(X0,domain(X1))) = compose(compose(g,X0),domain(X1)) ) ).
cnf(u444,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,compose(a,b))) = compose(compose(a,g),compose(a,b)) ) ).
cnf(u5266,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(codomain(X0),compose(h,compose(h,a))) = compose(compose(codomain(X0),h),compose(h,a)) ) ).
cnf(u1606,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(compose(domain(X0),domain(a)),compose(a,b)) ) ).
cnf(u8384,hypothesis,
( domain(b) != domain(a)
| compose(compose(h,a),a) = compose(compose(compose(h,a),a),domain(b)) ) ).
cnf(u8366,hypothesis,
( domain(b) != domain(a)
| compose(compose(g,a),a) = compose(compose(compose(g,a),a),domain(b)) ) ).
cnf(u13732,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(h)
| compose(compose(a,b),compose(codomain(X0),compose(g,a))) = compose(compose(compose(a,b),codomain(X0)),compose(g,a)) ) ).
cnf(u573,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(g,compose(h,a))) = compose(compose(domain(X0),g),compose(h,a)) ) ).
cnf(u4428,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(X2)
| compose(codomain(X2),compose(X1,codomain(X0))) = compose(compose(codomain(X2),X1),codomain(X0)) ) ).
cnf(u5718,hypothesis,
( domain(b) != domain(a)
| compose(compose(h,a),compose(a,compose(a,b))) = compose(compose(compose(h,a),a),compose(a,b)) ) ).
cnf(u4276,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(h,compose(h,domain(b))) = compose(compose(h,h),domain(b)) ) ).
cnf(u179,hypothesis,
compose(h,a) = compose(domain(h),compose(h,a)) ).
cnf(u1861,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(compose(h,a),X0)) = compose(compose(a,compose(h,a)),X0) ) ).
cnf(u10361,hypothesis,
( domain(b) != domain(h)
| domain(a) = codomain(compose(compose(g,a),g)) ) ).
cnf(u434,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(a,b))) = compose(compose(g,h),compose(a,b)) ) ).
cnf(u9375,hypothesis,
( domain(b) != domain(a)
| compose(g,compose(domain(b),domain(a))) = compose(compose(g,domain(b)),domain(a)) ) ).
cnf(u1859,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(compose(h,a),X0)) = compose(compose(compose(h,a),compose(h,a)),X0) ) ).
cnf(u78,hypothesis,
( codomain(X0) != domain(a)
| codomain(b) = codomain(compose(X0,compose(a,b))) ) ).
cnf(u11725,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,compose(a,b))) = compose(compose(compose(g,a),domain(h)),compose(h,compose(a,b))) ) ).
cnf(u11691,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(h)
| compose(compose(h,compose(a,b)),compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u10824,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(a,b),compose(compose(g,a),domain(X0))) = compose(compose(compose(a,b),compose(g,a)),domain(X0)) ) ).
cnf(u7101,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(compose(g,a),compose(codomain(X0),X1)) = compose(compose(compose(g,a),codomain(X0)),X1) ) ).
cnf(u1674,hypothesis,
( domain(X1) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X1),compose(h,domain(X0))) = compose(compose(domain(X1),h),domain(X0)) ) ).
cnf(u6473,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(a)
| compose(compose(h,a),compose(codomain(X0),compose(a,b))) = compose(compose(compose(h,a),codomain(X0)),compose(a,b)) ) ).
cnf(u7131,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,a)) = compose(compose(g,a),compose(domain(b),compose(h,a))) ) ).
cnf(u4284,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(h,domain(X0))) = compose(compose(g,h),domain(X0)) ) ).
cnf(u5197,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(X0,compose(a,compose(g,a))) = compose(compose(X0,a),compose(g,a)) ) ).
cnf(u2145,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(a,compose(a,domain(X0))) = compose(compose(a,a),domain(X0)) ) ).
cnf(u11694,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(a,domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u432,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,compose(a,b))) = compose(compose(a,h),compose(a,b)) ) ).
cnf(u833,axiom,
( domain(X0) != codomain(X1)
| domain(X0) != domain(X2)
| compose(X1,compose(domain(X0),X2)) = compose(compose(X1,domain(X0)),X2) ) ).
cnf(u11330,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(g,compose(h,compose(a,b)))) = compose(compose(g,g),compose(h,compose(a,b))) ) ).
cnf(u7995,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,a),compose(h,compose(h,compose(a,b)))) = compose(compose(compose(h,a),h),compose(h,compose(a,b))) ) ).
cnf(u5991,hypothesis,
( codomain(X0) != domain(b)
| domain(X1) != domain(h)
| compose(domain(X1),compose(compose(g,a),codomain(X0))) = compose(compose(domain(X1),compose(g,a)),codomain(X0)) ) ).
cnf(u8034,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(h)
| compose(compose(a,b),compose(domain(X0),compose(g,a))) = compose(compose(compose(a,b),domain(X0)),compose(g,a)) ) ).
cnf(u4546,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),domain(X0)) = compose(domain(a),compose(compose(a,b),domain(X0))) ) ).
cnf(u5393,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(g,a))) = compose(compose(compose(h,compose(a,b)),h),compose(g,a)) ) ).
cnf(u91,hypothesis,
domain(h) = domain(compose(h,a)) ).
cnf(u6841,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,a),compose(a,b))) = compose(compose(domain(X0),compose(h,a)),compose(a,b)) ) ).
cnf(u551,hypothesis,
( domain(X0) != domain(h)
| domain(b) = codomain(compose(domain(X0),compose(h,a))) ) ).
cnf(u17120,hypothesis,
( domain(b) != domain(h)
| compose(domain(b),compose(compose(g,a),compose(g,a))) = compose(compose(domain(b),compose(g,a)),compose(g,a)) ) ).
cnf(u3423,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(a,b))) = compose(compose(h,compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u12531,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(b)
| compose(compose(g,a),compose(codomain(X0),codomain(X1))) = compose(compose(compose(g,a),codomain(X0)),codomain(X1)) ) ).
cnf(u66,hypothesis,
( domain(X0) != codomain(b)
| codomain(h) = domain(compose(compose(a,b),X0)) ) ).
cnf(u12361,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),domain(X0)) = compose(domain(h),compose(compose(h,a),domain(X0))) ) ).
cnf(u5204,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(X0,compose(compose(h,a),compose(g,a))) = compose(compose(X0,compose(h,a)),compose(g,a)) ) ).
cnf(u14512,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),compose(domain(X0),domain(b))) = compose(compose(compose(h,a),domain(X0)),domain(b)) ) ).
cnf(u6245,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(g,a),compose(g,a))) ) ).
cnf(u5207,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(h)
| compose(X1,compose(codomain(X0),compose(g,a))) = compose(compose(X1,codomain(X0)),compose(g,a)) ) ).
cnf(u14597,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(g,compose(compose(g,a),compose(g,a))) = compose(compose(g,compose(g,a)),compose(g,a)) ) ).
cnf(u2513,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) = codomain(compose(compose(a,b),codomain(X0))) ) ).
cnf(u9180,hypothesis,
( domain(b) != domain(a)
| compose(h,compose(domain(b),domain(a))) = compose(compose(h,domain(b)),domain(a)) ) ).
cnf(u3701,hypothesis,
( domain(X0) != domain(b)
| domain(h) = domain(compose(compose(g,a),domain(X0))) ) ).
cnf(u3368,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(g,g)) ) ).
cnf(u13152,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(h)
| compose(compose(a,b),compose(codomain(X0),compose(h,a))) = compose(compose(compose(a,b),codomain(X0)),compose(h,a)) ) ).
cnf(u7125,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),domain(X0)) = compose(compose(g,a),compose(domain(b),domain(X0))) ) ).
cnf(u5208,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(h)
| compose(X1,compose(domain(X0),compose(g,a))) = compose(compose(X1,domain(X0)),compose(g,a)) ) ).
cnf(u13734,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(h,a),compose(codomain(X0),compose(g,a))) = compose(compose(compose(h,a),codomain(X0)),compose(g,a)) ) ).
cnf(u15504,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(X1)
| compose(domain(X1),compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(domain(X1),codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u603,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(g,a)) = compose(compose(codomain(X0),g),a) ) ).
cnf(u3430,hypothesis,
( domain(X0) != domain(a)
| compose(h,domain(X0)) = compose(compose(h,domain(X0)),domain(X0)) ) ).
cnf(u7912,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(domain(X0),compose(h,a))) = compose(compose(g,domain(X0)),compose(h,a)) ) ).
cnf(u2640,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,a)) = compose(g,compose(compose(a,b),compose(g,a))) ) ).
cnf(u95,hypothesis,
( domain(X0) != domain(a)
| domain(h) = domain(compose(h,X0)) ) ).
cnf(u8033,hypothesis,
( codomain(X0) != domain(X1)
| domain(X1) != domain(h)
| compose(codomain(X0),compose(domain(X1),compose(g,a))) = compose(compose(codomain(X0),domain(X1)),compose(g,a)) ) ).
cnf(u5996,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(g,a),compose(h,a))) = compose(compose(domain(X0),compose(g,a)),compose(h,a)) ) ).
cnf(u363,hypothesis,
( a != compose(X0,a)
| domain(b) != domain(a)
| codomain(X0) != domain(a)
| domain(a) = X0 ) ).
cnf(u3702,hypothesis,
( domain(X0) != domain(b)
| domain(h) = domain(compose(compose(h,a),domain(X0))) ) ).
cnf(u15349,hypothesis,
( domain(a) != domain(h)
| compose(domain(a),compose(g,compose(h,compose(a,b)))) = compose(compose(domain(a),g),compose(h,compose(a,b))) ) ).
cnf(u2936,hypothesis,
( domain(a) != domain(h)
| domain(b) = codomain(compose(h,compose(g,a))) ) ).
cnf(u12133,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(compose(g,a),compose(compose(a,b),domain(X0))) = compose(compose(compose(g,a),compose(a,b)),domain(X0)) ) ).
cnf(u5216,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(codomain(X0),compose(a,compose(g,a))) = compose(compose(codomain(X0),a),compose(g,a)) ) ).
cnf(u6511,hypothesis,
( domain(b) != domain(a)
| compose(compose(h,a),compose(a,b)) = compose(compose(h,a),compose(domain(b),compose(a,b))) ) ).
cnf(u106,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(a,X0)) = compose(compose(compose(h,a),a),X0) ) ).
cnf(u1001,hypothesis,
( domain(X0) != domain(h)
| domain(X0) = domain(compose(domain(X0),compose(h,a))) ) ).
cnf(u5108,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(a,domain(X0))) = compose(compose(compose(h,compose(a,b)),a),domain(X0)) ) ).
cnf(u1147,hypothesis,
( codomain(X0) != domain(a)
| domain(h) = domain(compose(g,codomain(X0))) ) ).
cnf(u4441,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != codomain(b)
| compose(codomain(X1),compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(codomain(X1),compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u1379,hypothesis,
( domain(X1) != codomain(b)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,compose(a,b)),X1)) = compose(compose(domain(X0),compose(h,compose(a,b))),X1) ) ).
cnf(u5998,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(g,a),g)) = compose(compose(domain(X0),compose(g,a)),g) ) ).
cnf(u7487,hypothesis,
( domain(X0) != domain(a)
| domain(X0) != domain(X1)
| compose(h,compose(domain(X0),X1)) = compose(compose(h,domain(X0)),X1) ) ).
cnf(u6000,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(compose(domain(X0),compose(g,a)),b) ) ).
cnf(u5131,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(compose(h,a),compose(g,codomain(X0))) = compose(compose(compose(h,a),g),codomain(X0)) ) ).
cnf(u8143,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(g,compose(h,a))) = compose(compose(g,g),compose(h,a)) ) ).
cnf(u628,hypothesis,
( domain(b) != domain(h)
| domain(a) = domain(compose(a,compose(h,compose(a,b)))) ) ).
cnf(u17711,hypothesis,
( domain(b) != domain(h)
| compose(domain(b),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(domain(b),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u7173,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),g) = compose(compose(h,a),compose(domain(b),g)) ) ).
cnf(u478,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(g,a),compose(g,X0)) = compose(compose(compose(g,a),g),X0) ) ).
cnf(u8202,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(codomain(X0),compose(g,compose(g,a))) = compose(compose(codomain(X0),g),compose(g,a)) ) ).
cnf(u2016,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != codomain(b)
| compose(X1,compose(compose(a,b),codomain(X0))) = compose(compose(X1,compose(a,b)),codomain(X0)) ) ).
cnf(u9711,hypothesis,
( domain(b) != domain(h)
| domain(b) = codomain(compose(compose(g,a),compose(g,a))) ) ).
cnf(u1796,hypothesis,
( codomain(b) != domain(h)
| domain(a) = domain(compose(compose(a,b),compose(g,a))) ) ).
cnf(u5218,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,compose(g,a))) = compose(compose(compose(h,compose(a,b)),a),compose(g,a)) ) ).
cnf(u2062,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),X1) = compose(compose(codomain(X0),X1),codomain(X1)) ) ).
cnf(u2276,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(compose(domain(X0),compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u3190,hypothesis,
( domain(X0) != domain(a)
| compose(g,domain(X0)) = compose(domain(h),compose(g,domain(X0))) ) ).
cnf(u1264,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != domain(b)
| compose(codomain(X0),compose(a,domain(X1))) = compose(compose(codomain(X0),a),domain(X1)) ) ).
cnf(u1794,hypothesis,
( codomain(b) != domain(h)
| domain(a) = domain(compose(compose(a,b),compose(h,compose(a,b)))) ) ).
cnf(u4627,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(codomain(X0),compose(a,compose(h,a))) = compose(compose(codomain(X0),a),compose(h,a)) ) ).
cnf(u4614,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(X0,compose(compose(g,a),compose(h,a))) = compose(compose(X0,compose(g,a)),compose(h,a)) ) ).
cnf(u7301,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,a)) = compose(X0,compose(codomain(X0),compose(h,a))) ) ).
cnf(u4213,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),a) = compose(compose(compose(a,b),a),domain(b)) ) ).
cnf(u16153,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(g,codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u7295,axiom,
( domain(X0) != codomain(X1)
| compose(X1,domain(X0)) = compose(X1,compose(codomain(X1),domain(X0))) ) ).
cnf(u10241,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(h,compose(compose(h,a),compose(a,b))) = compose(compose(h,compose(h,a)),compose(a,b)) ) ).
cnf(u7132,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,compose(a,b))) = compose(compose(g,a),compose(domain(b),compose(h,compose(a,b)))) ) ).
cnf(u13150,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != codomain(X1)
| compose(domain(X0),compose(codomain(X1),compose(h,a))) = compose(compose(domain(X0),codomain(X1)),compose(h,a)) ) ).
cnf(domain_composition,axiom,
compose(domain(X0),X0) = X0 ).
cnf(u4344,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(compose(codomain(X0),compose(a,b)),codomain(b)) ) ).
cnf(u5391,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(codomain(X0),compose(h,compose(g,a))) = compose(compose(codomain(X0),h),compose(g,a)) ) ).
cnf(u273,hypothesis,
( codomain(X0) != domain(b)
| domain(X1) != domain(a)
| compose(domain(X1),compose(a,codomain(X0))) = compose(compose(domain(X1),a),codomain(X0)) ) ).
cnf(u540,axiom,
( codomain(X0) != domain(X1)
| codomain(X1) = codomain(compose(codomain(X0),X1)) ) ).
cnf(u633,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,compose(h,compose(a,b)))) = compose(compose(domain(X0),a),compose(h,compose(a,b))) ) ).
cnf(u7171,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,a)) = compose(compose(h,a),compose(domain(b),compose(h,a))) ) ).
cnf(u12911,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(compose(h,a),compose(g,a))) = compose(compose(compose(h,compose(a,b)),compose(h,a)),compose(g,a)) ) ).
cnf(codomain_of_h_equals_domain_of_ab,hypothesis,
codomain(h) = domain(compose(a,b)) ).
cnf(u11645,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(a)
| compose(h,compose(codomain(X0),compose(h,a))) = compose(compose(h,codomain(X0)),compose(h,a)) ) ).
cnf(u14380,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(compose(h,a),compose(h,a))) = compose(compose(compose(h,compose(a,b)),compose(h,a)),compose(h,a)) ) ).
cnf(u5417,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(g,a),compose(h,compose(a,b)))) ) ).
cnf(u2074,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(g,a)) = compose(compose(X0,compose(g,a)),domain(b)) ) ).
cnf(u1419,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(a)
| compose(codomain(X0),compose(h,X1)) = compose(compose(codomain(X0),h),X1) ) ).
cnf(u6024,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(compose(codomain(X0),compose(g,a)),b) ) ).
cnf(u10812,hypothesis,
( domain(b) != domain(a)
| compose(compose(h,a),compose(a,b)) = compose(compose(compose(h,a),compose(a,b)),codomain(b)) ) ).
cnf(u133,hypothesis,
( codomain(X0) != domain(h)
| domain(X0) = domain(compose(X0,compose(g,a))) ) ).
cnf(u4224,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(compose(g,a),compose(h,codomain(X0))) = compose(compose(compose(g,a),h),codomain(X0)) ) ).
cnf(u1679,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(g,a))) = compose(compose(domain(X0),h),compose(g,a)) ) ).
cnf(u2073,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,a)) = compose(compose(X0,compose(h,a)),domain(b)) ) ).
cnf(u7071,hypothesis,
( codomain(b) != domain(h)
| codomain(b) = codomain(compose(compose(a,b),compose(h,compose(a,b)))) ) ).
cnf(u5764,hypothesis,
( domain(a) != domain(h)
| domain(X0) != codomain(b)
| compose(h,compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(h,compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u22,hypothesis,
( compose(X0,b) != compose(X2,b)
| domain(b) != codomain(X2)
| codomain(X0) != domain(a)
| X0 = X2 ) ).
cnf(u917,hypothesis,
( domain(b) != domain(a)
| compose(h,a) = compose(g,a) ) ).
cnf(u144,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(a,X0)) = compose(compose(compose(g,a),a),X0) ) ).
cnf(u4391,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) = domain(compose(codomain(X0),compose(h,a))) ) ).
cnf(u4608,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(X0,compose(a,compose(h,a))) = compose(compose(X0,a),compose(h,a)) ) ).
cnf(u2063,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),X0) = compose(compose(compose(a,b),X0),codomain(X0)) ) ).
cnf(u8066,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(g,a)) = compose(compose(compose(a,b),domain(h)),compose(g,a)) ) ).
cnf(u915,hypothesis,
( compose(X0,b) != compose(h,compose(a,b))
| domain(b) != domain(a)
| codomain(X0) != domain(b)
| compose(h,a) = X0 ) ).
cnf(u1318,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,a),compose(h,X0)) = compose(compose(compose(h,a),h),X0) ) ).
cnf(u45,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != domain(b)
| compose(compose(a,b),compose(a,X0)) = compose(compose(compose(a,b),a),X0) ) ).
cnf(u12003,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(a,b),compose(compose(g,a),compose(a,b))) = compose(compose(compose(a,b),compose(g,a)),compose(a,b)) ) ).
cnf(u4642,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(compose(h,a),compose(compose(a,b),compose(a,b))) = compose(compose(compose(h,a),compose(a,b)),compose(a,b)) ) ).
cnf(u1682,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(h,g)) = compose(compose(domain(X0),h),g) ) ).
cnf(u13323,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(a,b),compose(compose(g,a),codomain(X0))) = compose(compose(compose(a,b),compose(g,a)),codomain(X0)) ) ).
cnf(u4389,hypothesis,
( codomain(b) != domain(h)
| domain(h) = domain(compose(compose(h,compose(a,b)),compose(h,a))) ) ).
cnf(u7215,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) != domain(X1)
| compose(h,compose(codomain(X0),X1)) = compose(compose(h,codomain(X0)),X1) ) ).
cnf(u1322,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(h,X0)) = compose(compose(g,h),X0) ) ).
cnf(u11689,hypothesis,
( codomain(X0) != domain(X1)
| domain(X1) != domain(h)
| compose(codomain(X0),compose(domain(X1),compose(h,compose(a,b)))) = compose(compose(codomain(X0),domain(X1)),compose(h,compose(a,b))) ) ).
cnf(u14004,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(h)
| compose(codomain(X1),compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(codomain(X1),codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u7358,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(a,b))) = compose(g,compose(domain(a),compose(h,compose(a,b)))) ) ).
cnf(u1316,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(a,b),compose(h,X0)) = compose(compose(compose(a,b),h),X0) ) ).
cnf(u1446,hypothesis,
( codomain(X0) != domain(a)
| codomain(b) = codomain(compose(codomain(X0),compose(a,b))) ) ).
cnf(u7216,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) != domain(X1)
| compose(g,compose(codomain(X0),X1)) = compose(compose(g,codomain(X0)),X1) ) ).
cnf(u5269,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,a),compose(h,compose(h,a))) = compose(compose(compose(h,a),h),compose(h,a)) ) ).
cnf(u3304,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(h,compose(h,compose(a,b)))) ) ).
cnf(u1951,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != domain(b)
| compose(X1,compose(a,codomain(X0))) = compose(compose(X1,a),codomain(X0)) ) ).
cnf(u428,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,compose(a,b))) = compose(compose(compose(a,b),h),compose(a,b)) ) ).
cnf(u4895,hypothesis,
( codomain(X0) != domain(h)
| codomain(b) = codomain(compose(codomain(X0),compose(h,compose(a,b)))) ) ).
cnf(u62,hypothesis,
( codomain(X0) != codomain(h)
| domain(X0) = domain(compose(X0,compose(a,b))) ) ).
cnf(u15763,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(compose(g,a),compose(h,a))) = compose(compose(compose(g,a),compose(g,a)),compose(h,a)) ) ).
cnf(u6928,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,a)) = compose(compose(compose(h,compose(a,b)),compose(g,a)),domain(b)) ) ).
cnf(u1320,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(a,compose(h,X0)) = compose(compose(a,h),X0) ) ).
cnf(u3508,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != codomain(b)
| compose(X0,compose(compose(h,compose(a,b)),domain(X1))) = compose(compose(X0,compose(h,compose(a,b))),domain(X1)) ) ).
cnf(u73,hypothesis,
domain(a) = codomain(h) ).
cnf(u3504,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != domain(a)
| compose(h,compose(X0,domain(X1))) = compose(compose(h,X0),domain(X1)) ) ).
cnf(u4270,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(h,domain(X0))) = compose(compose(h,h),domain(X0)) ) ).
cnf(u7344,hypothesis,
( domain(a) != domain(h)
| compose(h,g) = compose(h,compose(domain(a),g)) ) ).
cnf(u2973,hypothesis,
( domain(a) != domain(h)
| domain(a) = codomain(compose(g,g)) ) ).
cnf(u418,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != codomain(b)
| compose(X0,compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(X0,compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u4155,hypothesis,
( domain(X0) != domain(b)
| compose(a,domain(X0)) = compose(a,compose(domain(b),domain(X0))) ) ).
cnf(u9105,hypothesis,
( codomain(X0) != domain(b)
| domain(a) != domain(h)
| compose(h,compose(compose(g,a),codomain(X0))) = compose(compose(h,compose(g,a)),codomain(X0)) ) ).
cnf(u5134,hypothesis,
( codomain(X0) != domain(a)
| domain(a) != domain(h)
| compose(h,compose(g,codomain(X0))) = compose(compose(h,g),codomain(X0)) ) ).
cnf(u4387,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(g,a),compose(h,a))) ) ).
cnf(u14384,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(h,compose(compose(h,a),compose(h,a))) = compose(compose(h,compose(h,a)),compose(h,a)) ) ).
cnf(u12005,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(compose(g,a),compose(a,b))) = compose(compose(compose(h,a),compose(g,a)),compose(a,b)) ) ).
cnf(u17660,hypothesis,
( domain(b) != domain(h)
| compose(domain(b),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(domain(b),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u445,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(a,b))) = compose(compose(h,g),compose(a,b)) ) ).
cnf(u1863,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(g,compose(compose(h,a),X0)) = compose(compose(g,compose(h,a)),X0) ) ).
cnf(u13733,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(h)
| compose(compose(h,compose(a,b)),compose(codomain(X0),compose(g,a))) = compose(compose(compose(h,compose(a,b)),codomain(X0)),compose(g,a)) ) ).
cnf(u416,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(a)
| compose(X0,compose(compose(g,a),compose(a,b))) = compose(compose(X0,compose(g,a)),compose(a,b)) ) ).
cnf(u9710,hypothesis,
( domain(b) != domain(h)
| domain(b) = codomain(compose(compose(h,a),compose(g,a))) ) ).
cnf(u3515,axiom,
( domain(X0) != codomain(X1)
| domain(X0) != domain(X2)
| compose(X1,compose(domain(X0),domain(X2))) = compose(compose(X1,domain(X0)),domain(X2)) ) ).
cnf(u12065,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(compose(h,a),compose(domain(X0),domain(X1))) = compose(compose(compose(h,a),domain(X0)),domain(X1)) ) ).
cnf(u2992,hypothesis,
( codomain(X0) != codomain(b)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(compose(a,b),codomain(X0))) = compose(compose(compose(a,b),compose(a,b)),codomain(X0)) ) ).
cnf(u9454,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(compose(codomain(X0),domain(h)),compose(h,compose(a,b))) ) ).
cnf(u2636,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),codomain(X0)) = compose(g,compose(compose(a,b),codomain(X0))) ) ).
cnf(u13155,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(g,a),compose(codomain(X0),compose(h,a))) = compose(compose(compose(g,a),codomain(X0)),compose(h,a)) ) ).
cnf(u6480,hypothesis,
( codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),compose(a,b))) = compose(compose(g,codomain(X0)),compose(a,b)) ) ).
cnf(u5213,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(X0,compose(compose(a,b),compose(g,a))) = compose(compose(X0,compose(a,b)),compose(g,a)) ) ).
cnf(u1052,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) = domain(compose(codomain(X0),g)) ) ).
cnf(u11722,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,compose(a,b))) = compose(compose(compose(a,b),domain(h)),compose(h,compose(a,b))) ) ).
cnf(u5288,axiom,
( domain(X0) != domain(X1)
| domain(X0) = domain(compose(domain(X0),X1)) ) ).
cnf(u2560,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) = codomain(compose(a,codomain(X0))) ) ).
cnf(u9145,hypothesis,
( codomain(X0) != domain(a)
| compose(h,compose(codomain(X0),domain(a))) = compose(compose(h,codomain(X0)),domain(a)) ) ).
cnf(u2372,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,a)) = compose(compose(a,compose(h,a)),domain(b)) ) ).
cnf(u2758,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(a)
| compose(codomain(X0),compose(h,domain(X1))) = compose(compose(codomain(X0),h),domain(X1)) ) ).
cnf(u5395,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(g,a),compose(h,compose(g,a))) = compose(compose(compose(g,a),h),compose(g,a)) ) ).
cnf(u852,hypothesis,
( domain(X0) != domain(b)
| domain(X0) = codomain(compose(a,domain(X0))) ) ).
cnf(u2899,hypothesis,
( codomain(X0) != domain(a)
| compose(h,codomain(X0)) = compose(compose(h,codomain(X0)),codomain(X0)) ) ).
cnf(u11692,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(compose(h,a),domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u1862,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(h,compose(compose(h,a),X0)) = compose(compose(h,compose(h,a)),X0) ) ).
cnf(u10841,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(compose(h,a),domain(X0))) = compose(compose(compose(h,a),compose(h,a)),domain(X0)) ) ).
cnf(u100,hypothesis,
domain(b) = codomain(compose(h,a)) ).
cnf(u11971,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),compose(g,a))) = compose(compose(g,codomain(X0)),compose(g,a)) ) ).
cnf(u7907,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(h)
| compose(compose(h,compose(a,b)),compose(domain(X0),compose(h,a))) = compose(compose(compose(h,compose(a,b)),domain(X0)),compose(h,a)) ) ).
cnf(u4440,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != domain(b)
| compose(codomain(X1),compose(compose(h,a),domain(X0))) = compose(compose(codomain(X1),compose(h,a)),domain(X0)) ) ).
cnf(u2624,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != codomain(b)
| compose(compose(a,b),compose(compose(a,b),X0)) = compose(compose(compose(a,b),compose(a,b)),X0) ) ).
cnf(u79,hypothesis,
( domain(b) != domain(a)
| codomain(b) = codomain(compose(a,compose(a,b))) ) ).
cnf(u4290,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(g,compose(h,domain(b))) = compose(compose(g,h),domain(b)) ) ).
cnf(u2641,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,a)) = compose(g,compose(compose(a,b),compose(h,a))) ) ).
cnf(u3796,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),g)) = compose(compose(domain(X1),domain(X0)),g) ) ).
cnf(u7141,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(compose(h,a),compose(codomain(X0),X1)) = compose(compose(compose(h,a),codomain(X0)),X1) ) ).
cnf(u7910,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(domain(X0),compose(h,a))) = compose(compose(a,domain(X0)),compose(h,a)) ) ).
cnf(u17415,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(g,compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(g,compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u8204,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,compose(g,a))) = compose(compose(compose(h,compose(a,b)),g),compose(g,a)) ) ).
cnf(u7880,hypothesis,
( codomain(b) != domain(h)
| domain(b) = codomain(compose(compose(h,compose(a,b)),compose(g,a))) ) ).
cnf(u90,hypothesis,
( domain(X0) != codomain(b)
| domain(h) = domain(compose(compose(h,compose(a,b)),X0)) ) ).
cnf(u6508,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(codomain(X0),compose(codomain(X0),compose(a,b))) ) ).
cnf(u5717,hypothesis,
( domain(b) != domain(a)
| compose(compose(g,a),compose(a,compose(a,b))) = compose(compose(compose(g,a),a),compose(a,b)) ) ).
cnf(u8139,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(a,compose(g,compose(h,a))) = compose(compose(a,g),compose(h,a)) ) ).
cnf(u8203,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(a,b),compose(g,compose(g,a))) = compose(compose(compose(a,b),g),compose(g,a)) ) ).
cnf(u999,hypothesis,
( domain(X0) != domain(h)
| domain(X0) = domain(compose(domain(X0),g)) ) ).
cnf(u7906,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(h)
| compose(compose(a,b),compose(domain(X0),compose(h,a))) = compose(compose(compose(a,b),domain(X0)),compose(h,a)) ) ).
cnf(u1589,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,b)) = compose(compose(X0,domain(a)),compose(a,b)) ) ).
cnf(u345,hypothesis,
( domain(X0) != domain(a)
| domain(X0) = domain(compose(domain(X0),compose(a,b))) ) ).
cnf(u8409,hypothesis,
( domain(X0) != domain(b)
| domain(X0) = codomain(compose(compose(g,a),domain(X0))) ) ).
cnf(u629,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,compose(a,b))) = compose(h,compose(a,compose(h,compose(a,b)))) ) ).
cnf(u8159,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(b)
| compose(compose(h,compose(a,b)),compose(X1,codomain(X0))) = compose(compose(compose(h,compose(a,b)),X1),codomain(X0)) ) ).
cnf(u11728,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(a,b))) = compose(compose(g,domain(h)),compose(h,compose(a,b))) ) ).
cnf(u1383,hypothesis,
( domain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(g,a),compose(compose(h,compose(a,b)),X0)) = compose(compose(compose(g,a),compose(h,compose(a,b))),X0) ) ).
cnf(u15733,hypothesis,
( domain(a) != codomain(b)
| compose(codomain(b),compose(compose(a,b),compose(a,b))) = compose(compose(codomain(b),compose(a,b)),compose(a,b)) ) ).
cnf(u3177,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(a)
| compose(codomain(X0),compose(g,domain(X1))) = compose(compose(codomain(X0),g),domain(X1)) ) ).
cnf(u6636,axiom,
( codomain(X0) != domain(X2)
| codomain(X0) != domain(X1)
| compose(domain(X2),compose(codomain(X0),domain(X1))) = compose(compose(domain(X2),codomain(X0)),domain(X1)) ) ).
cnf(u5706,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(a,compose(a,b))) = compose(compose(compose(a,b),a),compose(a,b)) ) ).
cnf(u8351,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(a,domain(X0))) = compose(compose(compose(g,a),a),domain(X0)) ) ).
cnf(u4613,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(X0,compose(g,compose(h,a))) = compose(compose(X0,g),compose(h,a)) ) ).
cnf(u5992,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(g,a),compose(a,b))) = compose(compose(domain(X0),compose(g,a)),compose(a,b)) ) ).
cnf(u7110,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),X0) = compose(compose(g,a),compose(domain(b),X0)) ) ).
cnf(u4296,hypothesis,
( domain(a) != domain(h)
| compose(g,h) = compose(compose(g,h),domain(a)) ) ).
cnf(u9998,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),domain(X0)) = compose(compose(compose(g,a),domain(X0)),domain(X0)) ) ).
cnf(u7286,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),X1) = compose(codomain(X0),compose(codomain(X0),X1)) ) ).
cnf(u2680,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),codomain(X0)) = compose(h,compose(compose(a,b),codomain(X0))) ) ).
cnf(u3305,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(h,g)) ) ).
cnf(u3452,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(a,b))) = compose(compose(g,compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u755,hypothesis,
( domain(b) != domain(a)
| compose(g,compose(a,domain(a))) = compose(compose(g,a),domain(a)) ) ).
cnf(u8069,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(g,a)) = compose(compose(compose(g,a),domain(h)),compose(g,a)) ) ).
cnf(u1113,hypothesis,
( domain(X0) != domain(a)
| domain(X0) = codomain(compose(g,domain(X0))) ) ).
cnf(u8215,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(g,a),compose(h,domain(X0))) = compose(compose(compose(g,a),h),domain(X0)) ) ).
cnf(u2541,hypothesis,
( domain(X0) != domain(a)
| domain(X0) = codomain(compose(h,domain(X0))) ) ).
cnf(u8183,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(a,b),domain(X0))) = compose(compose(compose(h,compose(a,b)),compose(a,b)),domain(X0)) ) ).
cnf(u2512,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) = codomain(compose(compose(h,compose(a,b)),codomain(X0))) ) ).
cnf(u479,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,a),compose(g,X0)) = compose(compose(compose(h,a),g),X0) ) ).
cnf(u4630,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(a,compose(h,a))) = compose(compose(compose(h,a),a),compose(h,a)) ) ).
cnf(u372,hypothesis,
( codomain(X0) != domain(b)
| domain(a) = domain(compose(a,codomain(X0))) ) ).
cnf(u5219,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(a,compose(g,a))) = compose(compose(compose(h,a),a),compose(g,a)) ) ).
cnf(u8038,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(domain(X0),compose(g,a))) = compose(compose(a,domain(X0)),compose(g,a)) ) ).
cnf(u8135,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(a,b),compose(g,compose(h,a))) = compose(compose(compose(a,b),g),compose(h,a)) ) ).
cnf(u15764,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(compose(g,a),compose(h,a))) = compose(compose(compose(h,a),compose(g,a)),compose(h,a)) ) ).
cnf(u6634,hypothesis,
( domain(X1) != domain(h)
| domain(X0) != codomain(b)
| compose(domain(X1),compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(domain(X1),compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u29,hypothesis,
( codomain(X0) != codomain(g)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(a,b))) = compose(compose(X1,X0),compose(a,b)) ) ).
cnf(u5472,axiom,
( codomain(X0) != domain(X1)
| domain(X1) != codomain(X2)
| compose(codomain(X0),compose(domain(X1),codomain(X2))) = compose(compose(codomain(X0),domain(X1)),codomain(X2)) ) ).
cnf(u15754,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(a,b),compose(compose(g,a),compose(h,a))) = compose(compose(compose(a,b),compose(g,a)),compose(h,a)) ) ).
cnf(u13154,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(h,a),compose(codomain(X0),compose(h,a))) = compose(compose(compose(h,a),codomain(X0)),compose(h,a)) ) ).
cnf(u8343,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),compose(a,b)) = compose(compose(compose(a,b),compose(a,b)),codomain(b)) ) ).
cnf(u2685,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,a)) = compose(h,compose(compose(a,b),compose(h,a))) ) ).
cnf(u12528,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != codomain(X1)
| compose(compose(a,b),compose(codomain(X0),codomain(X1))) = compose(compose(compose(a,b),codomain(X0)),codomain(X1)) ) ).
cnf(u1382,hypothesis,
( domain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(h,a),compose(compose(h,compose(a,b)),X0)) = compose(compose(compose(h,a),compose(h,compose(a,b))),X0) ) ).
cnf(u385,hypothesis,
( domain(b) != domain(h)
| compose(g,compose(a,compose(h,a))) = compose(compose(g,a),compose(h,a)) ) ).
cnf(u11421,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(a,b),compose(h,domain(X0))) = compose(compose(compose(a,b),h),domain(X0)) ) ).
cnf(u2547,hypothesis,
( domain(b) != domain(a)
| domain(b) = codomain(compose(h,domain(b))) ) ).
cnf(codomain_composition,axiom,
compose(X0,codomain(X0)) = X0 ).
cnf(u128,hypothesis,
compose(h,compose(a,b)) = compose(compose(g,a),b) ).
cnf(u8170,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(compose(g,a),domain(X0))) = compose(compose(compose(h,compose(a,b)),compose(g,a)),domain(X0)) ) ).
cnf(u5121,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),a) = compose(compose(compose(h,compose(a,b)),a),domain(b)) ) ).
cnf(u7948,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),compose(h,a))) = compose(compose(a,codomain(X0)),compose(h,a)) ) ).
cnf(u5763,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(h,compose(compose(h,a),domain(X0))) = compose(compose(h,compose(h,a)),domain(X0)) ) ).
cnf(u2509,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) = codomain(compose(h,codomain(X0))) ) ).
cnf(u7357,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,a)) = compose(g,compose(domain(a),compose(h,a))) ) ).
cnf(u10650,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(g,domain(b))) = compose(compose(compose(g,a),g),domain(b)) ) ).
cnf(u17254,hypothesis,
( domain(b) != domain(h)
| compose(domain(b),compose(compose(g,a),compose(h,a))) = compose(compose(domain(b),compose(g,a)),compose(h,a)) ) ).
cnf(u391,hypothesis,
( b != compose(h,compose(a,b))
| domain(b) != domain(a)
| domain(b) = compose(g,a) ) ).
cnf(u14238,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),compose(compose(a,b),domain(a))) = compose(compose(compose(a,b),compose(a,b)),domain(a)) ) ).
cnf(u1683,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,a)) = compose(compose(domain(X0),h),a) ) ).
cnf(u1574,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != domain(X1)
| compose(domain(X0),compose(domain(X1),compose(a,b))) = compose(compose(domain(X0),domain(X1)),compose(a,b)) ) ).
cnf(u8935,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(a,compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(a,compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u4624,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(X0,compose(compose(a,b),compose(h,a))) = compose(compose(X0,compose(a,b)),compose(h,a)) ) ).
cnf(u5475,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(domain(X0),codomain(X1))) = compose(compose(compose(h,a),domain(X0)),codomain(X1)) ) ).
cnf(u17605,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(h,compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(h,compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u1580,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(a)
| compose(a,compose(domain(X0),compose(a,b))) = compose(compose(a,domain(X0)),compose(a,b)) ) ).
cnf(u14601,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(compose(g,a),compose(g,a))) = compose(compose(compose(h,a),compose(g,a)),compose(g,a)) ) ).
cnf(u8076,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),compose(g,a))) = compose(compose(a,codomain(X0)),compose(g,a)) ) ).
cnf(h_ab_equals_g_ab,hypothesis,
compose(h,compose(a,b)) = compose(g,compose(a,b)) ).
cnf(u11411,hypothesis,
( domain(a) != domain(h)
| compose(domain(a),compose(h,compose(h,compose(a,b)))) = compose(compose(domain(a),h),compose(h,compose(a,b))) ) ).
cnf(u303,hypothesis,
compose(h,compose(a,b)) = compose(compose(h,compose(a,b)),compose(codomain(b),codomain(b))) ).
cnf(u389,hypothesis,
( codomain(X0) != domain(h)
| domain(b) = codomain(compose(X0,compose(h,a))) ) ).
cnf(u640,hypothesis,
( domain(b) != domain(h)
| codomain(b) = codomain(compose(a,compose(h,compose(a,b)))) ) ).
cnf(u274,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(compose(codomain(X0),a),b) ) ).
cnf(u8035,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(h)
| compose(compose(h,compose(a,b)),compose(domain(X0),compose(g,a))) = compose(compose(compose(h,compose(a,b)),domain(X0)),compose(g,a)) ) ).
cnf(u12323,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(h)
| compose(compose(h,a),compose(compose(h,a),codomain(X0))) = compose(compose(compose(h,a),compose(h,a)),codomain(X0)) ) ).
cnf(u10745,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(g,a)) = compose(domain(a),compose(compose(a,b),compose(g,a))) ) ).
cnf(u132,hypothesis,
( compose(X0,b) != compose(h,compose(a,b))
| codomain(X0) != domain(a)
| compose(g,a) = X0 ) ).
cnf(u4227,hypothesis,
( codomain(X0) != domain(a)
| domain(a) != domain(h)
| compose(g,compose(h,codomain(X0))) = compose(compose(g,h),codomain(X0)) ) ).
cnf(u4340,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,a)) = compose(compose(codomain(X0),compose(h,a)),domain(b)) ) ).
cnf(u2072,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,compose(a,b))) = compose(compose(X0,compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u5135,hypothesis,
( codomain(X0) != domain(a)
| domain(a) != domain(h)
| compose(g,compose(g,codomain(X0))) = compose(compose(g,g),codomain(X0)) ) ).
cnf(u4124,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(a,compose(g,domain(X0))) = compose(compose(a,g),domain(X0)) ) ).
cnf(u147,hypothesis,
( domain(X0) != domain(b)
| domain(h) = domain(compose(compose(g,a),X0)) ) ).
cnf(u10767,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(g,a)) = compose(compose(compose(g,a),compose(g,a)),domain(b)) ) ).
cnf(u4339,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(compose(codomain(X0),compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u2464,hypothesis,
( domain(X1) != domain(b)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(g,a),X1)) = compose(compose(domain(X0),compose(g,a)),X1) ) ).
cnf(u10630,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,a),compose(g,domain(X0))) = compose(compose(compose(h,a),g),domain(X0)) ) ).
cnf(u10809,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(g,a)) = compose(compose(compose(h,a),compose(g,a)),domain(b)) ) ).
cnf(u4129,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(a,compose(codomain(X0),domain(X1))) = compose(compose(a,codomain(X0)),domain(X1)) ) ).
cnf(u44,hypothesis,
( domain(X0) != codomain(b)
| codomain(X0) = codomain(compose(compose(a,b),X0)) ) ).
cnf(u174,axiom,
domain(X0) = domain(domain(X0)) ).
cnf(u4664,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),compose(h,compose(a,b)))) = compose(compose(domain(X0),compose(a,b)),compose(h,compose(a,b))) ) ).
cnf(u4651,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),compose(compose(a,b),compose(a,b))) = compose(compose(compose(a,b),compose(a,b)),compose(a,b)) ) ).
cnf(u1317,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(h,X0)) = compose(compose(compose(h,compose(a,b)),h),X0) ) ).
cnf(u1961,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != codomain(b)
| compose(X1,compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(X1,compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u15759,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(h,compose(compose(g,a),compose(h,a))) = compose(compose(h,compose(g,a)),compose(h,a)) ) ).
cnf(u59,hypothesis,
( domain(X0) != codomain(h)
| domain(g) = domain(compose(g,X0)) ) ).
cnf(u5401,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(g,a))) = compose(compose(h,h),compose(g,a)) ) ).
cnf(u12324,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(h)
| compose(compose(g,a),compose(compose(h,a),codomain(X0))) = compose(compose(compose(g,a),compose(h,a)),codomain(X0)) ) ).
cnf(u2470,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(compose(g,a),X0)) = compose(compose(a,compose(g,a)),X0) ) ).
cnf(u429,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(compose(compose(h,compose(a,b)),h),compose(a,b)) ) ).
cnf(u10770,hypothesis,
( domain(b) != domain(a)
| compose(compose(g,a),compose(a,b)) = compose(compose(compose(g,a),compose(a,b)),codomain(b)) ) ).
cnf(u1321,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(h,X0)) = compose(compose(h,h),X0) ) ).
cnf(u3499,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != codomain(b)
| compose(compose(a,b),compose(X0,domain(X1))) = compose(compose(compose(a,b),X0),domain(X1)) ) ).
cnf(u103,hypothesis,
compose(h,a) = compose(compose(h,a),domain(b)) ).
cnf(u8936,hypothesis,
( domain(a) != codomain(b)
| domain(a) != domain(h)
| compose(h,compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(h,compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u1445,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) = domain(compose(codomain(X0),compose(a,b))) ) ).
cnf(u2155,hypothesis,
( domain(b) != domain(a)
| compose(a,compose(a,domain(a))) = compose(compose(a,a),domain(a)) ) ).
cnf(u2615,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != codomain(b)
| compose(X0,compose(compose(a,b),X1)) = compose(compose(X0,compose(a,b)),X1) ) ).
cnf(u9894,hypothesis,
( codomain(X0) != codomain(b)
| domain(b) != domain(h)
| compose(compose(h,a),compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(compose(h,a),compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u8369,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(a,domain(X0))) = compose(compose(compose(h,a),a),domain(X0)) ) ).
cnf(u187,hypothesis,
compose(g,a) = compose(domain(h),compose(g,a)) ).
cnf(u7784,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(domain(X0),compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u7905,hypothesis,
( codomain(X0) != domain(X1)
| domain(X1) != domain(h)
| compose(codomain(X0),compose(domain(X1),compose(h,a))) = compose(compose(codomain(X0),domain(X1)),compose(h,a)) ) ).
cnf(u3502,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(X0,domain(X1))) = compose(compose(compose(g,a),X0),domain(X1)) ) ).
cnf(u7997,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(a,compose(h,compose(h,compose(a,b)))) = compose(compose(a,h),compose(h,compose(a,b))) ) ).
cnf(u5176,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(g,domain(X0))) = compose(compose(g,g),domain(X0)) ) ).
cnf(u442,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,compose(a,b))) = compose(compose(compose(h,a),g),compose(a,b)) ) ).
cnf(u17599,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(codomain(X0),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(codomain(X0),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u1449,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(a)
| compose(X1,compose(codomain(X0),compose(a,b))) = compose(compose(X1,codomain(X0)),compose(a,b)) ) ).
cnf(u14520,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(h,a),compose(codomain(X0),domain(b))) = compose(compose(compose(h,a),codomain(X0)),domain(b)) ) ).
cnf(u14439,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),compose(domain(X0),domain(b))) = compose(compose(compose(g,a),domain(X0)),domain(b)) ) ).
cnf(u1007,axiom,
( domain(X0) != domain(X1)
| domain(X1) = domain(compose(domain(X1),domain(X0))) ) ).
cnf(u4631,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(a,compose(h,a))) = compose(compose(compose(g,a),a),compose(h,a)) ) ).
cnf(u836,axiom,
( domain(X0) != codomain(X1)
| domain(X1) = domain(compose(X1,domain(X0))) ) ).
cnf(u4663,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),compose(h,a))) = compose(compose(domain(X0),compose(a,b)),compose(h,a)) ) ).
cnf(u10320,hypothesis,
( domain(b) != domain(h)
| domain(a) = codomain(compose(compose(h,a),g)) ) ).
cnf(u7631,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,compose(a,b))) = compose(compose(a,b),compose(codomain(b),compose(h,compose(a,b)))) ) ).
cnf(u440,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,compose(a,b))) = compose(compose(compose(a,b),g),compose(a,b)) ) ).
cnf(u84,hypothesis,
compose(h,compose(a,b)) = compose(compose(h,compose(a,b)),codomain(b)) ).
cnf(u11723,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(compose(compose(h,compose(a,b)),domain(h)),compose(h,compose(a,b))) ) ).
cnf(u13793,hypothesis,
( domain(a) != domain(h)
| compose(domain(a),compose(g,compose(h,a))) = compose(compose(domain(a),g),compose(h,a)) ) ).
cnf(u10839,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(a,b),compose(compose(h,a),domain(X0))) = compose(compose(compose(a,b),compose(h,a)),domain(X0)) ) ).
cnf(u3968,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,a)) = compose(compose(domain(X0),domain(h)),compose(h,a)) ) ).
cnf(u7941,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,a)) = compose(compose(compose(g,a),domain(h)),compose(h,a)) ) ).
cnf(u2625,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != codomain(b)
| compose(codomain(X0),compose(compose(a,b),X1)) = compose(compose(codomain(X0),compose(a,b)),X1) ) ).
cnf(u2380,hypothesis,
( domain(b) != domain(h)
| compose(a,g) = compose(compose(a,g),domain(a)) ) ).
cnf(u11726,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,compose(a,b))) = compose(compose(a,domain(h)),compose(h,compose(a,b))) ) ).
cnf(u446,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(a,b))) = compose(compose(g,g),compose(a,b)) ) ).
cnf(u2373,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(g,a)) = compose(compose(a,compose(g,a)),domain(b)) ) ).
cnf(u1856,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(b)
| compose(codomain(X0),compose(compose(h,a),X1)) = compose(compose(codomain(X0),compose(h,a)),X1) ) ).
cnf(u74,hypothesis,
( codomain(X0) != domain(a)
| domain(X0) = domain(compose(X0,compose(a,b))) ) ).
cnf(u5815,hypothesis,
( codomain(X0) != domain(a)
| compose(h,codomain(X0)) = compose(h,compose(domain(a),codomain(X0))) ) ).
cnf(u11322,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(a,b),compose(g,compose(h,compose(a,b)))) = compose(compose(compose(a,b),g),compose(h,compose(a,b))) ) ).
cnf(u11449,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != codomain(b)
| compose(compose(a,b),compose(compose(a,b),domain(X0))) = compose(compose(compose(a,b),compose(a,b)),domain(X0)) ) ).
cnf(u7787,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,compose(a,b)),compose(g,a))) = compose(compose(domain(X0),compose(h,compose(a,b))),compose(g,a)) ) ).
cnf(u13326,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(h)
| compose(compose(g,a),compose(compose(g,a),codomain(X0))) = compose(compose(compose(g,a),compose(g,a)),codomain(X0)) ) ).
cnf(u5473,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != codomain(X1)
| compose(compose(a,b),compose(domain(X0),codomain(X1))) = compose(compose(compose(a,b),domain(X0)),codomain(X1)) ) ).
cnf(u1607,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(compose(codomain(X0),domain(a)),compose(a,b)) ) ).
cnf(u5705,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(a)
| compose(codomain(X0),compose(a,compose(a,b))) = compose(compose(codomain(X0),a),compose(a,b)) ) ).
cnf(u3132,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),h) = compose(compose(codomain(X0),h),domain(a)) ) ).
cnf(u3798,axiom,
( domain(X0) != domain(X1)
| compose(domain(X0),X1) = compose(compose(domain(X0),domain(X1)),X1) ) ).
cnf(u14592,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(compose(g,a),compose(g,a))) = compose(compose(compose(h,compose(a,b)),compose(g,a)),compose(g,a)) ) ).
cnf(u10727,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),X0) = compose(domain(a),compose(compose(a,b),X0)) ) ).
cnf(u845,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != domain(b)
| compose(domain(X1),compose(a,domain(X0))) = compose(compose(domain(X1),a),domain(X0)) ) ).
cnf(u72,hypothesis,
domain(a) = codomain(g) ).
cnf(u370,hypothesis,
( domain(b) != domain(h)
| domain(a) = domain(compose(a,compose(g,a))) ) ).
cnf(u3794,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),compose(h,a))) = compose(compose(domain(X1),domain(X0)),compose(h,a)) ) ).
cnf(u5220,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(a,compose(g,a))) = compose(compose(compose(g,a),a),compose(g,a)) ) ).
cnf(u1612,hypothesis,
( domain(b) != domain(a)
| compose(a,compose(a,b)) = compose(compose(a,domain(a)),compose(a,b)) ) ).
cnf(u12008,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(h,compose(compose(g,a),compose(a,b))) = compose(compose(h,compose(g,a)),compose(a,b)) ) ).
cnf(u12009,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(g,compose(compose(g,a),compose(a,b))) = compose(compose(g,compose(g,a)),compose(a,b)) ) ).
cnf(u5479,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(a)
| compose(g,compose(domain(X0),codomain(X1))) = compose(compose(g,domain(X0)),codomain(X1)) ) ).
cnf(u5418,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(h,a),compose(h,compose(a,b)))) ) ).
cnf(u1610,hypothesis,
( domain(b) != domain(a)
| compose(compose(h,a),compose(a,b)) = compose(compose(compose(h,a),domain(a)),compose(a,b)) ) ).
cnf(u2897,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(g,a),codomain(X0)) = compose(compose(compose(g,a),codomain(X0)),codomain(X0)) ) ).
cnf(u1577,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(domain(X0),compose(a,b))) = compose(compose(compose(h,compose(a,b)),domain(X0)),compose(a,b)) ) ).
cnf(u200,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,g)) = compose(compose(domain(X0),a),g) ) ).
cnf(u12299,hypothesis,
( domain(X0) != domain(a)
| compose(domain(a),compose(domain(X0),compose(a,b))) = compose(compose(domain(a),domain(X0)),compose(a,b)) ) ).
cnf(u2514,axiom,
( codomain(X0) != codomain(X1)
| codomain(X1) = codomain(compose(codomain(X0),codomain(X1))) ) ).
cnf(u9297,hypothesis,
( codomain(X0) != codomain(b)
| domain(a) != domain(h)
| compose(g,compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(g,compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u630,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,compose(a,b))) = compose(g,compose(a,compose(h,compose(a,b)))) ) ).
cnf(u7293,hypothesis,
( domain(X0) != domain(a)
| compose(g,X0) = compose(g,compose(domain(a),X0)) ) ).
cnf(u7943,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,a)) = compose(compose(h,domain(h)),compose(h,a)) ) ).
cnf(u8937,hypothesis,
( domain(a) != codomain(b)
| domain(a) != domain(h)
| compose(g,compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(g,compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u5856,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),a),compose(h,compose(a,b))) ) ).
cnf(u12108,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(b)
| compose(compose(g,a),compose(X1,codomain(X0))) = compose(compose(compose(g,a),X1),codomain(X0)) ) ).
cnf(u14389,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(compose(h,a),compose(h,a))) = compose(compose(compose(h,a),compose(h,a)),compose(h,a)) ) ).
cnf(u3433,hypothesis,
( domain(a) != domain(h)
| compose(h,g) = compose(compose(h,g),domain(a)) ) ).
cnf(u1652,hypothesis,
( codomain(X0) != codomain(b)
| domain(h) = domain(compose(compose(h,compose(a,b)),codomain(X0))) ) ).
cnf(u2283,axiom,
( domain(X0) != domain(X1)
| compose(domain(X1),domain(X0)) = compose(compose(domain(X1),domain(X0)),domain(X0)) ) ).
cnf(u2771,hypothesis,
( domain(X0) != domain(a)
| compose(h,domain(X0)) = compose(domain(h),compose(h,domain(X0))) ) ).
cnf(u8212,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(g,compose(g,a))) = compose(compose(h,g),compose(g,a)) ) ).
cnf(u229,hypothesis,
( domain(b) != domain(h)
| compose(h,compose(a,compose(g,a))) = compose(compose(h,a),compose(g,a)) ) ).
cnf(u7287,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),X0) = compose(compose(a,b),compose(codomain(b),X0)) ) ).
cnf(u1650,hypothesis,
( codomain(X0) != domain(b)
| domain(h) = domain(compose(compose(g,a),codomain(X0))) ) ).
cnf(u8136,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,compose(h,a))) = compose(compose(compose(h,compose(a,b)),g),compose(h,a)) ) ).
cnf(u8002,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(h,compose(a,b)))) = compose(compose(h,h),compose(h,compose(a,b))) ) ).
cnf(u6419,hypothesis,
( domain(b) != domain(h)
| domain(b) = codomain(compose(compose(g,a),compose(h,a))) ) ).
cnf(u7150,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),X0) = compose(compose(h,a),compose(domain(b),X0)) ) ).
cnf(u3453,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,a)) = compose(compose(g,compose(h,a)),domain(b)) ) ).
cnf(u7288,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),X0) = compose(compose(h,compose(a,b)),compose(codomain(b),X0)) ) ).
cnf(u10242,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(g,compose(compose(h,a),compose(a,b))) = compose(compose(g,compose(h,a)),compose(a,b)) ) ).
cnf(u11360,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(h)
| compose(a,compose(compose(h,a),codomain(X0))) = compose(compose(a,compose(h,a)),codomain(X0)) ) ).
cnf(u2068,hypothesis,
( domain(X0) != domain(a)
| compose(h,X0) = compose(compose(h,X0),codomain(X0)) ) ).
cnf(u7291,hypothesis,
( domain(X0) != domain(b)
| compose(a,X0) = compose(a,compose(domain(b),X0)) ) ).
cnf(u13735,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(g,a),compose(codomain(X0),compose(g,a))) = compose(compose(compose(g,a),codomain(X0)),compose(g,a)) ) ).
cnf(u9997,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),domain(X0)) = compose(compose(compose(h,a),domain(X0)),domain(X0)) ) ).
cnf(u12002,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(a)
| compose(codomain(X0),compose(compose(g,a),compose(a,b))) = compose(compose(codomain(X0),compose(g,a)),compose(a,b)) ) ).
cnf(u6510,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,b)) = compose(compose(h,compose(a,b)),compose(codomain(b),compose(a,b))) ) ).
cnf(u17417,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(a,compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u624,hypothesis,
( codomain(X0) != domain(h)
| domain(X0) = domain(compose(X0,compose(h,compose(a,b)))) ) ).
cnf(u268,axiom,
( codomain(X0) != codomain(X1)
| codomain(codomain(X0)) = codomain(compose(X1,codomain(X0))) ) ).
cnf(u10747,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,compose(a,b))) = compose(domain(a),compose(compose(a,b),compose(h,compose(a,b)))) ) ).
cnf(u3662,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(h)
| compose(X0,compose(compose(h,compose(a,b)),compose(h,compose(a,b)))) = compose(compose(X0,compose(h,compose(a,b))),compose(h,compose(a,b))) ) ).
cnf(u4125,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(compose(g,a),domain(X0))) = compose(compose(a,compose(g,a)),domain(X0)) ) ).
cnf(u12049,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(b)
| compose(compose(h,a),compose(X1,codomain(X0))) = compose(compose(compose(h,a),X1),codomain(X0)) ) ).
cnf(u17609,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(compose(g,a),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u5762,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(h,compose(compose(g,a),domain(X0))) = compose(compose(h,compose(g,a)),domain(X0)) ) ).
cnf(u2065,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),X0) = compose(compose(compose(h,a),X0),codomain(X0)) ) ).
cnf(u8930,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != codomain(b)
| compose(codomain(X0),compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(codomain(X0),compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u3705,axiom,
( codomain(X0) != domain(X1)
| codomain(X0) = domain(compose(codomain(X0),domain(X1))) ) ).
cnf(u5891,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(g,compose(compose(g,a),domain(X0))) = compose(compose(g,compose(g,a)),domain(X0)) ) ).
cnf(u4110,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(a,compose(h,domain(X0))) = compose(compose(a,h),domain(X0)) ) ).
cnf(u141,hypothesis,
compose(g,a) = compose(compose(g,a),domain(b)) ).
cnf(u7380,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(a)
| compose(a,compose(domain(a),X0)) = compose(compose(a,domain(a)),X0) ) ).
cnf(u4639,hypothesis,
( codomain(X0) != domain(a)
| domain(a) != codomain(b)
| compose(codomain(X0),compose(compose(a,b),compose(a,b))) = compose(compose(codomain(X0),compose(a,b)),compose(a,b)) ) ).
cnf(u641,hypothesis,
( codomain(X0) != domain(h)
| codomain(b) = codomain(compose(X0,compose(h,compose(a,b)))) ) ).
cnf(u5396,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(a,compose(h,compose(g,a))) = compose(compose(a,h),compose(g,a)) ) ).
cnf(u30,hypothesis,
( codomain(X1) != domain(g)
| domain(X0) != codomain(h)
| compose(X1,compose(g,X0)) = compose(compose(X1,g),X0) ) ).
cnf(u7342,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,a)) = compose(h,compose(domain(a),compose(h,a))) ) ).
cnf(u4616,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(h)
| compose(X0,compose(compose(h,compose(a,b)),compose(h,a))) = compose(compose(X0,compose(h,compose(a,b))),compose(h,a)) ) ).
cnf(u230,hypothesis,
( domain(b) != domain(h)
| compose(h,compose(a,g)) = compose(compose(h,a),g) ) ).
cnf(u1418,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != codomain(b)
| compose(codomain(X0),compose(compose(h,compose(a,b)),X1)) = compose(compose(codomain(X0),compose(h,compose(a,b))),X1) ) ).
cnf(u12918,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(compose(h,a),compose(g,a))) = compose(compose(a,compose(h,a)),compose(g,a)) ) ).
cnf(u8227,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),h) = compose(compose(compose(g,a),h),domain(a)) ) ).
cnf(u1412,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != domain(b)
| compose(codomain(X0),compose(a,X1)) = compose(compose(codomain(X0),a),X1) ) ).
cnf(u131,hypothesis,
( compose(X0,b) != compose(h,compose(a,b))
| domain(b) != domain(a)
| codomain(X0) != domain(b)
| compose(g,a) = X0 ) ).
cnf(u2326,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),g) = compose(compose(codomain(X0),g),domain(a)) ) ).
cnf(u5400,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(g,a))) = compose(compose(g,h),compose(g,a)) ) ).
cnf(u41,hypothesis,
codomain(b) = codomain(compose(h,compose(a,b))) ).
cnf(u8701,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(X1)
| compose(compose(a,b),compose(codomain(X0),domain(X1))) = compose(compose(compose(a,b),codomain(X0)),domain(X1)) ) ).
cnf(u386,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,compose(h,a))) = compose(compose(domain(X0),a),compose(h,a)) ) ).
cnf(u6417,hypothesis,
( codomain(b) != domain(h)
| domain(b) = codomain(compose(compose(h,compose(a,b)),compose(h,a))) ) ).
cnf(u28,hypothesis,
codomain(h) = codomain(g) ).
cnf(u5116,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,domain(a))) = compose(compose(compose(h,compose(a,b)),a),domain(a)) ) ).
cnf(u6165,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(X1)
| compose(compose(h,compose(a,b)),compose(codomain(X0),X1)) = compose(compose(compose(h,compose(a,b)),codomain(X0)),X1) ) ).
cnf(u6931,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,b)) = compose(compose(compose(h,compose(a,b)),compose(a,b)),codomain(b)) ) ).
cnf(u4897,hypothesis,
( codomain(X0) != domain(h)
| domain(b) = codomain(compose(codomain(X0),compose(g,a))) ) ).
cnf(u17410,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u1609,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,b)) = compose(compose(compose(h,compose(a,b)),domain(a)),compose(a,b)) ) ).
cnf(u7992,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(codomain(X0),compose(h,compose(h,compose(a,b)))) = compose(compose(codomain(X0),h),compose(h,compose(a,b))) ) ).
cnf(u1959,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != domain(b)
| compose(X1,compose(compose(g,a),codomain(X0))) = compose(compose(X1,compose(g,a)),codomain(X0)) ) ).
cnf(u9896,hypothesis,
( codomain(X0) != codomain(b)
| domain(b) != domain(h)
| compose(a,compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(a,compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u384,hypothesis,
( domain(b) != domain(h)
| compose(h,compose(a,compose(h,a))) = compose(compose(h,a),compose(h,a)) ) ).
cnf(u18,hypothesis,
domain(compose(a,b)) = codomain(g) ).
cnf(u7328,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,compose(a,b))) = compose(a,compose(domain(b),compose(h,compose(a,b)))) ) ).
cnf(u7733,axiom,
( codomain(X0) != codomain(X1)
| compose(codomain(X0),codomain(X1)) = compose(codomain(X0),compose(codomain(X0),codomain(X1))) ) ).
cnf(u17419,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(compose(h,a),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u7566,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(g,compose(domain(b),X0)) = compose(compose(g,domain(b)),X0) ) ).
cnf(u4130,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(a,compose(domain(X0),domain(X1))) = compose(compose(a,domain(X0)),domain(X1)) ) ).
cnf(u2465,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(b)
| compose(codomain(X0),compose(compose(g,a),X1)) = compose(compose(codomain(X0),compose(g,a)),X1) ) ).
cnf(u8207,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(a,compose(g,compose(g,a))) = compose(compose(a,g),compose(g,a)) ) ).
cnf(u171,axiom,
( codomain(X2) != domain(domain(X0))
| domain(X0) != domain(X1)
| compose(X2,compose(domain(X0),X1)) = compose(compose(X2,domain(X0)),X1) ) ).
cnf(u4643,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(compose(g,a),compose(compose(a,b),compose(a,b))) = compose(compose(compose(g,a),compose(a,b)),compose(a,b)) ) ).
cnf(u403,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,compose(a,b))) = compose(compose(X0,h),compose(a,b)) ) ).
cnf(u87,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(a,X0)) = compose(compose(compose(h,compose(a,b)),a),X0) ) ).
cnf(u3503,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != domain(b)
| compose(a,compose(X0,domain(X1))) = compose(compose(a,X0),domain(X1)) ) ).
cnf(u10783,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,a)) = compose(compose(h,compose(a,b)),compose(codomain(b),compose(h,a))) ) ).
cnf(u146,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != domain(b)
| compose(X1,compose(compose(g,a),X0)) = compose(compose(X1,compose(g,a)),X0) ) ).
cnf(u2468,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(compose(g,a),X0)) = compose(compose(compose(h,a),compose(g,a)),X0) ) ).
cnf(u555,hypothesis,
( domain(X0) != domain(a)
| codomain(b) = codomain(compose(domain(X0),compose(a,b))) ) ).
cnf(u5294,hypothesis,
( domain(X0) != domain(b)
| domain(b) = domain(compose(domain(b),X0)) ) ).
cnf(u2109,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(a)
| compose(compose(h,a),compose(a,codomain(X0))) = compose(compose(compose(h,a),a),codomain(X0)) ) ).
cnf(u2616,hypothesis,
( domain(X0) != codomain(b)
| compose(h,compose(compose(a,b),X0)) = compose(compose(h,compose(a,b)),X0) ) ).
cnf(u1381,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,compose(a,b)),X0)) = compose(compose(compose(h,compose(a,b)),compose(h,compose(a,b))),X0) ) ).
cnf(u169,axiom,
( domain(X0) != domain(X1)
| codomain(X1) = codomain(compose(domain(X0),X1)) ) ).
cnf(u2995,hypothesis,
( codomain(X0) != codomain(b)
| domain(b) != domain(a)
| compose(compose(g,a),compose(compose(a,b),codomain(X0))) = compose(compose(compose(g,a),compose(a,b)),codomain(X0)) ) ).
cnf(u302,hypothesis,
compose(a,b) = compose(compose(a,b),compose(codomain(b),codomain(b))) ).
cnf(u2623,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(a,b),X0)) = compose(compose(compose(h,compose(a,b)),compose(a,b)),X0) ) ).
cnf(u58,hypothesis,
( domain(X0) != domain(b)
| domain(a) = domain(compose(a,X0)) ) ).
cnf(u953,hypothesis,
( domain(b) != domain(a)
| codomain(b) = codomain(compose(compose(h,a),compose(a,b))) ) ).
cnf(u7329,hypothesis,
( domain(b) != domain(h)
| compose(a,g) = compose(a,compose(domain(b),g)) ) ).
cnf(u1964,axiom,
( domain(X0) != codomain(X2)
| domain(X0) != codomain(X1)
| compose(X2,compose(domain(X0),codomain(X1))) = compose(compose(X2,domain(X0)),codomain(X1)) ) ).
cnf(u574,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(g,g)) = compose(compose(domain(X0),g),g) ) ).
cnf(u6471,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(a)
| compose(compose(a,b),compose(codomain(X0),compose(a,b))) = compose(compose(compose(a,b),codomain(X0)),compose(a,b)) ) ).
cnf(u6472,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(codomain(X0),compose(a,b))) = compose(compose(compose(h,compose(a,b)),codomain(X0)),compose(a,b)) ) ).
cnf(u175,hypothesis,
compose(a,b) = compose(domain(a),compose(a,b)) ).
cnf(u11441,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(X1)
| compose(compose(a,b),compose(domain(X0),domain(X1))) = compose(compose(compose(a,b),domain(X0)),domain(X1)) ) ).
cnf(u2621,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(compose(g,a),compose(compose(a,b),X0)) = compose(compose(compose(g,a),compose(a,b)),X0) ) ).
cnf(u3654,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(X0,compose(a,compose(h,compose(a,b)))) = compose(compose(X0,a),compose(h,compose(a,b))) ) ).
cnf(u4444,axiom,
( domain(X0) != codomain(X2)
| domain(X0) != domain(X1)
| compose(codomain(X2),compose(domain(X0),domain(X1))) = compose(compose(codomain(X2),domain(X0)),domain(X1)) ) ).
cnf(u430,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,compose(a,b))) = compose(compose(compose(h,a),h),compose(a,b)) ) ).
cnf(u11325,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(g,a),compose(g,compose(h,compose(a,b)))) = compose(compose(compose(g,a),g),compose(h,compose(a,b))) ) ).
cnf(u56,hypothesis,
domain(h) = domain(compose(h,compose(a,b))) ).
cnf(u6844,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,a),compose(g,a))) = compose(compose(domain(X0),compose(h,a)),compose(g,a)) ) ).
cnf(u3514,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(X2)
| compose(X1,compose(codomain(X0),domain(X2))) = compose(compose(X1,codomain(X0)),domain(X2)) ) ).
cnf(u3660,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(X0,compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(X0,compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u16305,hypothesis,
( domain(b) != domain(h)
| compose(domain(b),compose(compose(h,a),compose(g,a))) = compose(compose(domain(b),compose(h,a)),compose(g,a)) ) ).
cnf(u6469,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != codomain(X1)
| compose(domain(X0),compose(codomain(X1),compose(a,b))) = compose(compose(domain(X0),codomain(X1)),compose(a,b)) ) ).
cnf(u7078,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) = codomain(compose(compose(a,b),domain(X0))) ) ).
cnf(u10588,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),codomain(X0)) = compose(domain(h),compose(compose(h,compose(a,b)),codomain(X0))) ) ).
cnf(u441,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(compose(compose(h,compose(a,b)),g),compose(a,b)) ) ).
cnf(u5101,hypothesis,
( codomain(b) != domain(h)
| domain(h) = domain(compose(compose(h,compose(a,b)),compose(g,a))) ) ).
cnf(u1493,hypothesis,
( domain(b) != domain(a)
| compose(a,compose(a,b)) = compose(domain(a),compose(a,compose(a,b))) ) ).
cnf(u552,hypothesis,
( domain(X0) != domain(h)
| domain(b) = codomain(compose(domain(X0),compose(g,a))) ) ).
cnf(u341,hypothesis,
( domain(b) != domain(a)
| domain(h) = domain(compose(compose(g,a),compose(a,b))) ) ).
cnf(u6849,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(compose(domain(X0),compose(h,a)),b) ) ).
cnf(u7343,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(a,b))) = compose(h,compose(domain(a),compose(h,compose(a,b)))) ) ).
cnf(u8037,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(domain(X0),compose(g,a))) = compose(compose(compose(g,a),domain(X0)),compose(g,a)) ) ).
cnf(u3780,axiom,
( codomain(X0) != domain(X2)
| codomain(X0) != domain(X1)
| compose(domain(X2),compose(codomain(X0),X1)) = compose(compose(domain(X2),codomain(X0)),X1) ) ).
cnf(u2511,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) = codomain(compose(compose(h,a),codomain(X0))) ) ).
cnf(u2642,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(g,compose(compose(a,b),compose(h,compose(a,b)))) ) ).
cnf(u1611,hypothesis,
( domain(b) != domain(a)
| compose(compose(g,a),compose(a,b)) = compose(compose(compose(g,a),domain(a)),compose(a,b)) ) ).
cnf(u342,hypothesis,
( domain(b) != domain(a)
| domain(h) = domain(compose(compose(h,a),compose(a,b))) ) ).
cnf(u2895,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),codomain(X0)) = compose(compose(compose(h,compose(a,b)),codomain(X0)),codomain(X0)) ) ).
cnf(u6474,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(a)
| compose(compose(g,a),compose(codomain(X0),compose(a,b))) = compose(compose(compose(g,a),codomain(X0)),compose(a,b)) ) ).
cnf(u1958,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != domain(a)
| compose(X1,compose(g,codomain(X0))) = compose(compose(X1,g),codomain(X0)) ) ).
cnf(u17408,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(codomain(X0),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(codomain(X0),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u14149,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(a,b),domain(a))) = compose(compose(compose(h,compose(a,b)),compose(a,b)),domain(a)) ) ).
cnf(u11331,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(g,compose(h,compose(a,b)))) = compose(compose(h,g),compose(h,compose(a,b))) ) ).
cnf(u8397,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) = codomain(compose(X1,codomain(X0))) ) ).
cnf(u848,hypothesis,
( domain(X1) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X1),compose(g,domain(X0))) = compose(compose(domain(X1),g),domain(X0)) ) ).
cnf(u8964,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(g,a)) = compose(codomain(X0),compose(codomain(X0),compose(g,a))) ) ).
cnf(u9108,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(a)
| compose(h,compose(codomain(X0),codomain(X1))) = compose(compose(h,codomain(X0)),codomain(X1)) ) ).
cnf(u6621,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(X2)
| compose(domain(X2),compose(X1,codomain(X0))) = compose(compose(domain(X2),X1),codomain(X0)) ) ).
cnf(u96,hypothesis,
( domain(X0) != domain(a)
| codomain(X0) = codomain(compose(h,X0)) ) ).
cnf(u8169,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(g,domain(X0))) = compose(compose(compose(h,compose(a,b)),g),domain(X0)) ) ).
cnf(u4439,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != domain(b)
| compose(codomain(X1),compose(compose(g,a),domain(X0))) = compose(compose(codomain(X1),compose(g,a)),domain(X0)) ) ).
cnf(u1578,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(a)
| compose(compose(h,a),compose(domain(X0),compose(a,b))) = compose(compose(compose(h,a),domain(X0)),compose(a,b)) ) ).
cnf(u1499,hypothesis,
( domain(b) != domain(h)
| compose(a,g) = compose(domain(a),compose(a,g)) ) ).
cnf(u4208,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(a,domain(a))) = compose(compose(compose(a,b),a),domain(a)) ) ).
cnf(u5129,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(compose(a,b),compose(g,codomain(X0))) = compose(compose(compose(a,b),g),codomain(X0)) ) ).
cnf(u5474,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != codomain(X1)
| compose(compose(h,compose(a,b)),compose(domain(X0),codomain(X1))) = compose(compose(compose(h,compose(a,b)),domain(X0)),codomain(X1)) ) ).
cnf(u481,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(a,b),compose(g,X0)) = compose(compose(compose(a,b),g),X0) ) ).
cnf(u170,hypothesis,
( domain(X1) != domain(b)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,X1)) = compose(compose(domain(X0),a),X1) ) ).
cnf(u1651,hypothesis,
( codomain(X0) != domain(b)
| domain(h) = domain(compose(compose(h,a),codomain(X0))) ) ).
cnf(u8965,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,a)) = compose(codomain(X0),compose(codomain(X0),compose(h,a))) ) ).
cnf(u5478,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(a)
| compose(h,compose(domain(X0),codomain(X1))) = compose(compose(h,domain(X0)),codomain(X1)) ) ).
cnf(u11324,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,a),compose(g,compose(h,compose(a,b)))) = compose(compose(compose(h,a),g),compose(h,compose(a,b))) ) ).
cnf(u8134,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(codomain(X0),compose(g,compose(h,a))) = compose(compose(codomain(X0),g),compose(h,a)) ) ).
cnf(u14591,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(a,b),compose(compose(g,a),compose(g,a))) = compose(compose(compose(a,b),compose(g,a)),compose(g,a)) ) ).
cnf(u10235,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(a)
| compose(codomain(X0),compose(compose(h,a),compose(a,b))) = compose(compose(codomain(X0),compose(h,a)),compose(a,b)) ) ).
cnf(u5217,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(a,compose(g,a))) = compose(compose(compose(a,b),a),compose(g,a)) ) ).
cnf(u5859,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(a,compose(a,compose(h,compose(a,b)))) = compose(compose(a,a),compose(h,compose(a,b))) ) ).
cnf(u125,hypothesis,
( domain(X0) != domain(a)
| domain(h) = domain(compose(g,X0)) ) ).
cnf(u6840,hypothesis,
( codomain(X0) != domain(b)
| domain(X1) != domain(h)
| compose(domain(X1),compose(compose(h,a),codomain(X0))) = compose(compose(domain(X1),compose(h,a)),codomain(X0)) ) ).
cnf(u5303,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) = domain(compose(codomain(X0),compose(g,a))) ) ).
cnf(u14447,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(g,a),compose(codomain(X0),domain(b))) = compose(compose(compose(g,a),codomain(X0)),domain(b)) ) ).
cnf(u8172,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(compose(h,compose(a,b)),compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u2281,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(compose(domain(X0),compose(a,b)),codomain(b)) ) ).
cnf(u5202,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(X0,compose(g,compose(g,a))) = compose(compose(X0,g),compose(g,a)) ) ).
cnf(u7166,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(h,a),codomain(X0)) = compose(compose(h,a),compose(domain(b),codomain(X0))) ) ).
cnf(u5765,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) != domain(X1)
| compose(h,compose(codomain(X0),domain(X1))) = compose(compose(h,codomain(X0)),domain(X1)) ) ).
cnf(u5606,hypothesis,
( domain(X0) != domain(b)
| compose(a,compose(domain(X0),domain(b))) = compose(compose(a,domain(X0)),domain(b)) ) ).
cnf(u639,hypothesis,
( domain(X0) != domain(h)
| codomain(b) = codomain(compose(domain(X0),compose(h,compose(a,b)))) ) ).
cnf(u1010,axiom,
( codomain(X0) != domain(X1)
| codomain(X0) = domain(compose(codomain(X0),X1)) ) ).
cnf(u4609,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(X0,compose(h,compose(h,a))) = compose(compose(X0,h),compose(h,a)) ) ).
cnf(u677,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(X1)
| compose(compose(h,compose(a,b)),compose(domain(X0),X1)) = compose(compose(compose(h,compose(a,b)),domain(X0)),X1) ) ).
cnf(u15762,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(compose(g,a),compose(h,a))) = compose(compose(a,compose(g,a)),compose(h,a)) ) ).
cnf(u8221,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(h,domain(b))) = compose(compose(compose(g,a),h),domain(b)) ) ).
cnf(u2686,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(h,compose(compose(a,b),compose(h,compose(a,b)))) ) ).
cnf(u8704,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(compose(g,a),compose(codomain(X0),domain(X1))) = compose(compose(compose(g,a),codomain(X0)),domain(X1)) ) ).
cnf(u271,hypothesis,
( codomain(X0) != domain(b)
| compose(h,compose(a,codomain(X0))) = compose(compose(h,a),codomain(X0)) ) ).
cnf(u7789,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,compose(a,b)),compose(h,compose(a,b)))) = compose(compose(domain(X0),compose(h,compose(a,b))),compose(h,compose(a,b))) ) ).
cnf(u3703,hypothesis,
( domain(X0) != codomain(b)
| domain(h) = domain(compose(compose(h,compose(a,b)),domain(X0))) ) ).
cnf(u2282,axiom,
( codomain(X0) != domain(X1)
| compose(domain(X1),codomain(X0)) = compose(compose(domain(X1),codomain(X0)),codomain(X0)) ) ).
cnf(u7940,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,a)) = compose(compose(compose(h,a),domain(h)),compose(h,a)) ) ).
cnf(u1795,hypothesis,
( codomain(b) != domain(h)
| domain(a) = domain(compose(compose(a,b),compose(h,a))) ) ).
cnf(u7445,axiom,
( domain(X0) != domain(X1)
| compose(domain(X1),domain(X0)) = compose(domain(X1),compose(domain(X1),domain(X0))) ) ).
cnf(u6416,hypothesis,
( codomain(b) != domain(h)
| domain(b) = codomain(compose(compose(a,b),compose(h,a))) ) ).
cnf(u3670,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(X0,compose(compose(a,b),compose(h,compose(a,b)))) = compose(compose(X0,compose(a,b)),compose(h,compose(a,b))) ) ).
cnf(u9341,hypothesis,
( codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),domain(a))) = compose(compose(g,codomain(X0)),domain(a)) ) ).
cnf(u9174,hypothesis,
( domain(X0) != domain(a)
| compose(h,compose(domain(X0),domain(a))) = compose(compose(h,domain(X0)),domain(a)) ) ).
cnf(u1801,hypothesis,
( domain(X0) != codomain(b)
| domain(a) = domain(compose(compose(a,b),domain(X0))) ) ).
cnf(u8138,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(g,a),compose(g,compose(h,a))) = compose(compose(compose(g,a),g),compose(h,a)) ) ).
cnf(u4126,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(a,compose(compose(h,a),domain(X0))) = compose(compose(a,compose(h,a)),domain(X0)) ) ).
cnf(u4220,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,codomain(X1))) = compose(compose(codomain(X0),h),codomain(X1)) ) ).
cnf(u5203,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(X0,compose(compose(g,a),compose(g,a))) = compose(compose(X0,compose(g,a)),compose(g,a)) ) ).
cnf(u269,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(X2)
| compose(X2,compose(X1,codomain(X0))) = compose(compose(X2,X1),codomain(X0)) ) ).
cnf(u7944,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,a)) = compose(compose(g,domain(h)),compose(h,a)) ) ).
cnf(u14600,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(compose(g,a),compose(g,a))) = compose(compose(compose(g,a),compose(g,a)),compose(g,a)) ) ).
cnf(u10352,hypothesis,
( domain(b) != domain(h)
| codomain(b) = codomain(compose(compose(g,a),compose(h,compose(a,b)))) ) ).
cnf(u2990,hypothesis,
( codomain(X1) != codomain(b)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),codomain(X1))) = compose(compose(domain(X0),compose(a,b)),codomain(X1)) ) ).
cnf(u14385,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(g,compose(compose(h,a),compose(h,a))) = compose(compose(g,compose(h,a)),compose(h,a)) ) ).
cnf(u3585,hypothesis,
( domain(b) != domain(a)
| compose(a,compose(a,b)) = compose(a,compose(domain(b),compose(a,b))) ) ).
cnf(u8068,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(g,a)) = compose(compose(compose(h,a),domain(h)),compose(g,a)) ) ).
cnf(u16150,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(g,a),compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(compose(g,a),codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u4632,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(a,compose(a,compose(h,a))) = compose(compose(a,a),compose(h,a)) ) ).
cnf(u7165,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),domain(X0)) = compose(compose(h,a),compose(domain(b),domain(X0))) ) ).
cnf(u2296,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),g) = compose(compose(domain(X0),g),domain(a)) ) ).
cnf(u679,axiom,
( domain(X1) != domain(X2)
| domain(X0) != domain(X1)
| compose(domain(X0),compose(domain(X1),X2)) = compose(compose(domain(X0),domain(X1)),X2) ) ).
cnf(u12909,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(codomain(X0),compose(compose(h,a),compose(g,a))) = compose(compose(codomain(X0),compose(h,a)),compose(g,a)) ) ).
cnf(u266,axiom,
codomain(X0) = codomain(codomain(X0)) ).
cnf(u17608,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(a,compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u2069,hypothesis,
( domain(X0) != domain(a)
| compose(g,X0) = compose(compose(g,X0),codomain(X0)) ) ).
cnf(u2064,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),X0) = compose(compose(compose(h,compose(a,b)),X0),codomain(X0)) ) ).
cnf(u2,axiom,
domain(X0) = codomain(domain(X0)) ).
cnf(u9369,hypothesis,
( domain(X0) != domain(a)
| compose(g,compose(domain(X0),domain(a))) = compose(compose(g,domain(X0)),domain(a)) ) ).
cnf(u4139,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(a,compose(compose(a,b),domain(X0))) = compose(compose(a,compose(a,b)),domain(X0)) ) ).
cnf(u4225,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(a,compose(h,codomain(X0))) = compose(compose(a,h),codomain(X0)) ) ).
cnf(u5270,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(g,a),compose(h,compose(h,a))) = compose(compose(compose(g,a),h),compose(h,a)) ) ).
cnf(u2944,hypothesis,
( domain(a) != domain(h)
| domain(a) = codomain(compose(h,g)) ) ).
cnf(u8001,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(h,compose(a,b)))) = compose(compose(g,h),compose(h,compose(a,b))) ) ).
cnf(u25,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != domain(b)
| compose(X1,compose(a,X0)) = compose(compose(X1,a),X0) ) ).
cnf(u4619,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(h)
| compose(X1,compose(domain(X0),compose(h,a))) = compose(compose(X1,domain(X0)),compose(h,a)) ) ).
cnf(u14378,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(codomain(X0),compose(compose(h,a),compose(h,a))) = compose(compose(codomain(X0),compose(h,a)),compose(h,a)) ) ).
cnf(u13030,hypothesis,
( codomain(X0) != domain(a)
| compose(domain(a),compose(codomain(X0),compose(a,b))) = compose(compose(domain(a),codomain(X0)),compose(a,b)) ) ).
cnf(u52,hypothesis,
( domain(b) != codomain(h)
| codomain(b) = codomain(compose(a,compose(a,b))) ) ).
cnf(u5182,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(g,compose(g,domain(b))) = compose(compose(g,g),domain(b)) ) ).
cnf(u5268,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(h,a))) = compose(compose(compose(h,compose(a,b)),h),compose(h,a)) ) ).
cnf(u1171,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),a) = compose(compose(domain(X0),a),domain(b)) ) ).
cnf(u10236,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(a,b),compose(compose(h,a),compose(a,b))) = compose(compose(compose(a,b),compose(h,a)),compose(a,b)) ) ).
cnf(u8187,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,a),compose(h,domain(X0))) = compose(compose(compose(h,a),h),domain(X0)) ) ).
cnf(u16152,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(a)
| compose(h,compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(h,codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u16149,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(h,a),compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(compose(h,a),codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u4488,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != codomain(b)
| compose(codomain(X1),compose(compose(a,b),domain(X0))) = compose(compose(codomain(X1),compose(a,b)),domain(X0)) ) ).
cnf(u31,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(a,compose(a,X0)) = compose(compose(a,a),X0) ) ).
cnf(u5766,hypothesis,
( domain(X0) != domain(a)
| domain(X0) != domain(X1)
| compose(h,compose(domain(X0),domain(X1))) = compose(compose(h,domain(X0)),domain(X1)) ) ).
cnf(u5995,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(g,a),compose(g,a))) = compose(compose(domain(X0),compose(g,a)),compose(g,a)) ) ).
cnf(u10636,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(g,domain(b))) = compose(compose(compose(h,a),g),domain(b)) ) ).
cnf(u10842,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(compose(h,a),domain(X0))) = compose(compose(compose(g,a),compose(h,a)),domain(X0)) ) ).
cnf(u2471,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(h,compose(compose(g,a),X0)) = compose(compose(h,compose(g,a)),X0) ) ).
cnf(u4644,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(a,compose(compose(a,b),compose(a,b))) = compose(compose(a,compose(a,b)),compose(a,b)) ) ).
cnf(u1315,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != domain(h)
| compose(domain(X0),compose(h,X1)) = compose(compose(domain(X0),h),X1) ) ).
cnf(u2994,hypothesis,
( codomain(X0) != codomain(b)
| domain(b) != domain(a)
| compose(compose(h,a),compose(compose(a,b),codomain(X0))) = compose(compose(compose(h,a),compose(a,b)),codomain(X0)) ) ).
cnf(u1575,hypothesis,
( codomain(X0) != domain(X1)
| domain(X1) != domain(a)
| compose(codomain(X0),compose(domain(X1),compose(a,b))) = compose(compose(codomain(X0),domain(X1)),compose(a,b)) ) ).
cnf(u1428,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(compose(codomain(X0),g),compose(a,b)) ) ).
cnf(u17606,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(g,compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(g,compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u427,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(compose(domain(X0),h),compose(a,b)) ) ).
cnf(u414,hypothesis,
( codomain(X0) != domain(h)
| compose(compose(X0,g),compose(a,b)) = compose(X0,compose(h,compose(a,b))) ) ).
cnf(u2469,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(compose(g,a),X0)) = compose(compose(compose(g,a),compose(g,a)),X0) ) ).
cnf(u1952,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != domain(a)
| compose(X1,compose(h,codomain(X0))) = compose(compose(X1,h),codomain(X0)) ) ).
cnf(u3498,axiom,
( codomain(X1) != domain(X2)
| codomain(X0) != domain(X1)
| compose(codomain(X0),compose(X1,domain(X2))) = compose(compose(codomain(X0),X1),domain(X2)) ) ).
cnf(u7993,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(a,b),compose(h,compose(h,compose(a,b)))) = compose(compose(compose(a,b),h),compose(h,compose(a,b))) ) ).
cnf(u10642,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),g) = compose(compose(compose(h,a),g),domain(a)) ) ).
cnf(u11690,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(h)
| compose(compose(a,b),compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(compose(a,b),domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u8072,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(g,a)) = compose(compose(g,domain(h)),compose(g,a)) ) ).
cnf(u17610,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(compose(h,a),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u6847,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,a),g)) = compose(compose(domain(X0),compose(h,a)),g) ) ).
cnf(u4282,hypothesis,
( domain(a) != domain(h)
| compose(h,h) = compose(compose(h,h),domain(a)) ) ).
cnf(u7210,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(X1)
| compose(compose(a,b),compose(codomain(X0),X1)) = compose(compose(compose(a,b),codomain(X0)),X1) ) ).
cnf(u425,hypothesis,
( codomain(X0) != domain(a)
| domain(a) != codomain(b)
| compose(X0,compose(compose(a,b),compose(a,b))) = compose(compose(X0,compose(a,b)),compose(a,b)) ) ).
cnf(u2108,hypothesis,
( codomain(X0) != domain(b)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,codomain(X0))) = compose(compose(compose(h,compose(a,b)),a),codomain(X0)) ) ).
cnf(u4563,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(a,b),codomain(X0)) = compose(domain(a),compose(compose(a,b),codomain(X0))) ) ).
cnf(u11790,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(a)
| compose(h,compose(codomain(X0),compose(g,a))) = compose(compose(h,codomain(X0)),compose(g,a)) ) ).
cnf(u168,axiom,
( domain(X0) != domain(X1)
| domain(domain(X0)) = domain(compose(domain(X0),X1)) ) ).
cnf(u1860,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(compose(h,a),X0)) = compose(compose(compose(g,a),compose(h,a)),X0) ) ).
cnf(u8205,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,a),compose(g,compose(g,a))) = compose(compose(compose(h,a),g),compose(g,a)) ) ).
cnf(u9677,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(a,compose(compose(a,b),X0)) = compose(compose(a,compose(a,b)),X0) ) ).
cnf(u9296,hypothesis,
( codomain(X0) != domain(b)
| domain(a) != domain(h)
| compose(g,compose(compose(h,a),codomain(X0))) = compose(compose(g,compose(h,a)),codomain(X0)) ) ).
cnf(u7453,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),g) = compose(domain(X0),compose(domain(X0),g)) ) ).
cnf(u12915,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(h,compose(compose(h,a),compose(g,a))) = compose(compose(h,compose(h,a)),compose(g,a)) ) ).
cnf(u2626,hypothesis,
( domain(X1) != codomain(b)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),X1)) = compose(compose(domain(X0),compose(a,b)),X1) ) ).
cnf(u1663,hypothesis,
( codomain(X0) != codomain(b)
| domain(a) = domain(compose(compose(a,b),codomain(X0))) ) ).
cnf(u2993,hypothesis,
( codomain(X0) != codomain(b)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(a,b),codomain(X0))) = compose(compose(compose(h,compose(a,b)),compose(a,b)),codomain(X0)) ) ).
cnf(u1295,hypothesis,
( codomain(X0) != domain(b)
| compose(a,codomain(X0)) = compose(domain(a),compose(a,codomain(X0))) ) ).
cnf(u10644,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(g,a),compose(g,domain(X0))) = compose(compose(compose(g,a),g),domain(X0)) ) ).
cnf(u7878,hypothesis,
( codomain(b) != domain(h)
| codomain(b) = codomain(compose(compose(h,compose(a,b)),compose(h,compose(a,b)))) ) ).
cnf(u11696,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(g,domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u7359,hypothesis,
( domain(a) != domain(h)
| compose(g,g) = compose(g,compose(domain(a),g)) ) ).
cnf(u954,hypothesis,
( domain(a) != codomain(b)
| codomain(b) = codomain(compose(compose(h,compose(a,b)),compose(a,b))) ) ).
cnf(u12074,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(compose(h,a),compose(compose(a,b),domain(X0))) = compose(compose(compose(h,a),compose(a,b)),domain(X0)) ) ).
cnf(u7996,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(g,a),compose(h,compose(h,compose(a,b)))) = compose(compose(compose(g,a),h),compose(h,compose(a,b))) ) ).
cnf(u5947,hypothesis,
( codomain(X0) != domain(a)
| compose(g,codomain(X0)) = compose(g,compose(domain(a),codomain(X0))) ) ).
cnf(u8039,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(domain(X0),compose(g,a))) = compose(compose(h,domain(X0)),compose(g,a)) ) ).
cnf(u69,hypothesis,
( domain(b) != domain(h)
| codomain(h) = codomain(compose(a,g)) ) ).
cnf(u3302,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(h,compose(g,a))) ) ).
cnf(u199,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,compose(g,a))) = compose(compose(domain(X0),a),compose(g,a)) ) ).
cnf(u2378,hypothesis,
( domain(X0) != domain(b)
| compose(a,domain(X0)) = compose(compose(a,domain(X0)),domain(X0)) ) ).
cnf(u11732,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(a,codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u7624,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),domain(X0)) = compose(compose(a,b),compose(codomain(b),domain(X0))) ) ).
cnf(u15767,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(h)
| compose(compose(h,compose(a,b)),compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u2371,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,compose(a,b))) = compose(compose(a,compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u853,axiom,
( domain(X0) != codomain(X1)
| domain(X0) = codomain(compose(X1,domain(X0))) ) ).
cnf(u80,hypothesis,
a = compose(a,domain(b)) ).
cnf(u851,axiom,
( domain(X0) != domain(X1)
| domain(X0) = codomain(compose(domain(X1),domain(X0))) ) ).
cnf(u2637,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,b)) = compose(g,compose(compose(a,b),compose(a,b))) ) ).
cnf(u5162,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(g,domain(X0))) = compose(compose(h,g),domain(X0)) ) ).
cnf(u343,hypothesis,
( domain(a) != codomain(b)
| domain(h) = domain(compose(compose(h,compose(a,b)),compose(a,b))) ) ).
cnf(u465,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(g,X0)) = compose(compose(h,g),X0) ) ).
cnf(u5857,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(a,compose(h,compose(a,b)))) = compose(compose(compose(h,a),a),compose(h,compose(a,b))) ) ).
cnf(u2635,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),domain(X0)) = compose(g,compose(compose(a,b),domain(X0))) ) ).
cnf(u86,hypothesis,
( domain(X0) != codomain(b)
| codomain(X0) = codomain(compose(compose(h,compose(a,b)),X0)) ) ).
cnf(u5855,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(a,compose(h,compose(a,b)))) = compose(compose(compose(a,b),a),compose(h,compose(a,b))) ) ).
cnf(u7665,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),domain(X1)) = compose(codomain(X0),compose(codomain(X0),domain(X1))) ) ).
cnf(u5198,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(X0,compose(h,compose(g,a))) = compose(compose(X0,h),compose(g,a)) ) ).
cnf(u5854,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(codomain(X0),compose(a,compose(h,compose(a,b)))) = compose(compose(codomain(X0),a),compose(h,compose(a,b))) ) ).
cnf(u109,hypothesis,
( domain(X0) != domain(b)
| domain(h) = domain(compose(compose(h,a),X0)) ) ).
cnf(u2935,hypothesis,
( domain(a) != domain(h)
| domain(b) = codomain(compose(h,compose(h,a))) ) ).
cnf(u5205,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(h)
| compose(X0,compose(compose(h,compose(a,b)),compose(g,a))) = compose(compose(X0,compose(h,compose(a,b))),compose(g,a)) ) ).
cnf(u11359,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(h)
| compose(a,compose(compose(g,a),codomain(X0))) = compose(compose(a,compose(g,a)),codomain(X0)) ) ).
cnf(u3425,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(g,a)) = compose(compose(h,compose(g,a)),domain(b)) ) ).
cnf(u6507,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(domain(X0),compose(domain(X0),compose(a,b))) ) ).
cnf(u1217,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),a) = compose(compose(codomain(X0),a),domain(b)) ) ).
cnf(u4221,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(compose(a,b),compose(h,codomain(X0))) = compose(compose(compose(a,b),h),codomain(X0)) ) ).
cnf(u8174,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(X1)
| compose(compose(h,compose(a,b)),compose(codomain(X0),domain(X1))) = compose(compose(compose(h,compose(a,b)),codomain(X0)),domain(X1)) ) ).
cnf(u3303,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(h,compose(h,a))) ) ).
cnf(u1386,hypothesis,
( domain(a) != domain(h)
| domain(X0) != codomain(b)
| compose(g,compose(compose(h,compose(a,b)),X0)) = compose(compose(g,compose(h,compose(a,b))),X0) ) ).
cnf(u1380,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(a,b),compose(compose(h,compose(a,b)),X0)) = compose(compose(compose(a,b),compose(h,compose(a,b))),X0) ) ).
cnf(u99,hypothesis,
( domain(X0) != domain(b)
| compose(h,compose(a,X0)) = compose(compose(h,a),X0) ) ).
cnf(u8046,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(g,a)) = compose(compose(X0,domain(h)),compose(g,a)) ) ).
cnf(u383,hypothesis,
( domain(b) != domain(h)
| domain(a) = domain(compose(a,compose(h,a))) ) ).
cnf(u17409,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(a,b),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(compose(a,b),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u354,hypothesis,
g = compose(domain(h),g) ).
cnf(u9295,hypothesis,
( codomain(X0) != domain(b)
| domain(a) != domain(h)
| compose(g,compose(compose(g,a),codomain(X0))) = compose(compose(g,compose(g,a)),codomain(X0)) ) ).
cnf(u126,hypothesis,
domain(h) = domain(compose(g,a)) ).
cnf(u5893,hypothesis,
( domain(a) != domain(h)
| domain(X0) != codomain(b)
| compose(g,compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(g,compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u3795,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(domain(X1),domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u7909,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(domain(X0),compose(h,a))) = compose(compose(compose(g,a),domain(X0)),compose(h,a)) ) ).
cnf(u1384,hypothesis,
( domain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(a,compose(compose(h,compose(a,b)),X0)) = compose(compose(a,compose(h,compose(a,b))),X0) ) ).
cnf(u626,hypothesis,
( codomain(X0) != domain(h)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(h,compose(a,b)))) = compose(compose(X1,X0),compose(h,compose(a,b))) ) ).
cnf(u8339,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,a)) = compose(compose(compose(a,b),compose(h,a)),domain(b)) ) ).
cnf(u7172,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,compose(a,b))) = compose(compose(h,a),compose(domain(b),compose(h,compose(a,b)))) ) ).
cnf(u678,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(X1)
| compose(compose(a,b),compose(domain(X0),X1)) = compose(compose(compose(a,b),domain(X0)),X1) ) ).
cnf(u10766,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,a)) = compose(compose(compose(g,a),compose(h,a)),domain(b)) ) ).
cnf(u7788,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,compose(a,b)),compose(h,a))) = compose(compose(domain(X0),compose(h,compose(a,b))),compose(h,a)) ) ).
cnf(u1142,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(g,compose(h,compose(a,b)))) ) ).
cnf(u381,hypothesis,
( codomain(X0) != domain(h)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(h,a))) = compose(compose(X1,X0),compose(h,a)) ) ).
cnf(u9781,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != codomain(b)
| compose(codomain(X1),compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(codomain(X1),compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u10239,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(compose(h,a),compose(a,b))) = compose(compose(compose(g,a),compose(h,a)),compose(a,b)) ) ).
cnf(u482,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != domain(h)
| compose(domain(X0),compose(g,X1)) = compose(compose(domain(X0),g),X1) ) ).
cnf(u12062,hypothesis,
( domain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(h,a),compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(compose(h,a),compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u124,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != domain(a)
| compose(X1,compose(g,X0)) = compose(compose(X1,g),X0) ) ).
cnf(u7667,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),domain(X0)) = compose(compose(h,compose(a,b)),compose(codomain(b),domain(X0))) ) ).
cnf(u7942,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,a)) = compose(compose(a,domain(h)),compose(h,a)) ) ).
cnf(u14379,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(a,b),compose(compose(h,a),compose(h,a))) = compose(compose(compose(a,b),compose(h,a)),compose(h,a)) ) ).
cnf(u3575,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(a)
| compose(a,compose(codomain(X0),compose(a,b))) = compose(compose(a,codomain(X0)),compose(a,b)) ) ).
cnf(u8193,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(h,domain(b))) = compose(compose(compose(h,a),h),domain(b)) ) ).
cnf(codomain_of_a_equals_domain_of_b,hypothesis,
codomain(a) = domain(b) ).
cnf(u371,hypothesis,
( domain(b) != domain(h)
| domain(a) = domain(compose(a,g)) ) ).
cnf(u3454,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(g,a)) = compose(compose(g,compose(g,a)),domain(b)) ) ).
cnf(u7292,hypothesis,
( domain(X0) != domain(a)
| compose(h,X0) = compose(h,compose(domain(a),X0)) ) ).
cnf(u3970,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),g) = compose(compose(domain(X0),domain(h)),g) ) ).
cnf(u480,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(g,X0)) = compose(compose(compose(h,compose(a,b)),g),X0) ) ).
cnf(u5103,hypothesis,
( codomain(b) != domain(h)
| domain(h) = domain(compose(compose(h,compose(a,b)),compose(h,compose(a,b)))) ) ).
cnf(u2681,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,b)) = compose(h,compose(compose(a,b),compose(a,b))) ) ).
cnf(u782,hypothesis,
( codomain(X0) != domain(h)
| domain(a) = codomain(compose(codomain(X0),g)) ) ).
cnf(u2110,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(a)
| compose(compose(g,a),compose(a,codomain(X0))) = compose(compose(compose(g,a),a),codomain(X0)) ) ).
cnf(u1144,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(g,compose(g,a))) ) ).
cnf(u14599,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(compose(g,a),compose(g,a))) = compose(compose(a,compose(g,a)),compose(g,a)) ) ).
cnf(u1274,hypothesis,
( domain(X0) != domain(b)
| compose(a,domain(X0)) = compose(domain(a),compose(a,domain(X0))) ) ).
cnf(codomain_domain2,axiom,
( codomain(X0) != domain(X1)
| codomain(compose(X0,X1)) = codomain(X1) ) ).
cnf(u2835,hypothesis,
( codomain(X0) != domain(a)
| compose(h,codomain(X0)) = compose(domain(h),compose(h,codomain(X0))) ) ).
cnf(u10808,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,a)) = compose(compose(compose(h,a),compose(h,a)),domain(b)) ) ).
cnf(u5731,hypothesis,
( domain(b) != domain(a)
| compose(domain(b),compose(a,compose(a,b))) = compose(compose(domain(b),a),compose(a,b)) ) ).
cnf(u12910,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(a,b),compose(compose(h,a),compose(g,a))) = compose(compose(compose(a,b),compose(h,a)),compose(g,a)) ) ).
cnf(u11146,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),g) = compose(codomain(X0),compose(codomain(X0),g)) ) ).
cnf(u14960,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(g,a),codomain(X0)) = compose(domain(h),compose(compose(g,a),codomain(X0))) ) ).
cnf(u36,hypothesis,
( domain(X0) != domain(b)
| codomain(X0) = codomain(compose(a,X0)) ) ).
cnf(u672,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(X2)
| compose(X1,compose(codomain(X0),X2)) = compose(compose(X1,codomain(X0)),X2) ) ).
cnf(u13324,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(compose(g,a),codomain(X0))) = compose(compose(compose(h,compose(a,b)),compose(g,a)),codomain(X0)) ) ).
cnf(u2077,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,b)) = compose(compose(X0,compose(a,b)),codomain(b)) ) ).
cnf(u1858,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,a),X0)) = compose(compose(compose(h,compose(a,b)),compose(h,a)),X0) ) ).
cnf(u477,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(a,compose(g,X0)) = compose(compose(a,g),X0) ) ).
cnf(u7296,axiom,
( codomain(X0) != codomain(X1)
| compose(X1,codomain(X0)) = compose(X1,compose(codomain(X1),codomain(X0))) ) ).
cnf(u8071,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(g,a)) = compose(compose(h,domain(h)),compose(g,a)) ) ).
cnf(u4226,hypothesis,
( codomain(X0) != domain(a)
| domain(a) != domain(h)
| compose(h,compose(h,codomain(X0))) = compose(compose(h,h),codomain(X0)) ) ).
cnf(u137,hypothesis,
( codomain(X0) != domain(h)
| domain(b) = codomain(compose(X0,compose(g,a))) ) ).
cnf(u916,hypothesis,
( compose(X0,b) != compose(h,compose(a,b))
| codomain(X0) != domain(a)
| compose(h,a) = X0 ) ).
cnf(u5267,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(a,b),compose(h,compose(h,a))) = compose(compose(compose(a,b),h),compose(h,a)) ) ).
cnf(u4902,axiom,
( domain(X0) != codomain(X1)
| domain(X0) = codomain(compose(codomain(X1),domain(X0))) ) ).
cnf(u270,hypothesis,
( codomain(X0) != domain(b)
| codomain(codomain(X0)) = codomain(compose(a,codomain(X0))) ) ).
cnf(u4127,hypothesis,
( domain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(a,compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(a,compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u26,hypothesis,
( codomain(X0) != codomain(h)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(a,b))) = compose(compose(X1,X0),compose(a,b)) ) ).
cnf(u12321,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(a,b),compose(compose(h,a),codomain(X0))) = compose(compose(compose(a,b),compose(h,a)),codomain(X0)) ) ).
cnf(u8934,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(g,a),compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(compose(g,a),compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u3969,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(compose(domain(X0),domain(h)),compose(h,compose(a,b))) ) ).
cnf(u16902,hypothesis,
( domain(b) != domain(h)
| compose(domain(b),compose(compose(h,a),compose(h,a))) = compose(compose(domain(b),compose(h,a)),compose(h,a)) ) ).
cnf(u8361,hypothesis,
( domain(b) != domain(a)
| compose(compose(g,a),compose(a,domain(a))) = compose(compose(compose(g,a),a),domain(a)) ) ).
cnf(u143,hypothesis,
( domain(X0) != domain(b)
| codomain(X0) = codomain(compose(compose(g,a),X0)) ) ).
cnf(u6418,hypothesis,
( domain(b) != domain(h)
| domain(b) = codomain(compose(compose(h,a),compose(h,a))) ) ).
cnf(u98,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != domain(a)
| compose(X1,compose(h,X0)) = compose(compose(X1,h),X0) ) ).
cnf(u5275,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(h,compose(h,a))) = compose(compose(g,h),compose(h,a)) ) ).
cnf(u8933,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(h,a),compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(compose(h,a),compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u5168,hypothesis,
( domain(b) != domain(a)
| domain(a) != domain(h)
| compose(h,compose(g,domain(b))) = compose(compose(h,g),domain(b)) ) ).
cnf(u3459,hypothesis,
( domain(X0) != domain(a)
| compose(g,domain(X0)) = compose(compose(g,domain(X0)),domain(X0)) ) ).
cnf(u1319,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(g,a),compose(h,X0)) = compose(compose(compose(g,a),h),X0) ) ).
cnf(u10826,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(compose(g,a),domain(X0))) = compose(compose(compose(h,a),compose(g,a)),domain(X0)) ) ).
cnf(u11702,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,compose(a,b))) = compose(compose(X0,domain(h)),compose(h,compose(a,b))) ) ).
cnf(u1427,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(compose(codomain(X0),h),compose(a,b)) ) ).
cnf(u7326,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(g,a)) = compose(a,compose(domain(b),compose(g,a))) ) ).
cnf(u6926,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(compose(compose(h,compose(a,b)),compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u5928,hypothesis,
( domain(X0) != domain(a)
| compose(g,domain(X0)) = compose(g,compose(domain(a),domain(X0))) ) ).
cnf(u55,hypothesis,
domain(a) = domain(compose(a,b)) ).
cnf(u11323,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),g),compose(h,compose(a,b))) ) ).
cnf(u676,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(compose(h,a),compose(domain(X0),X1)) = compose(compose(compose(h,a),domain(X0)),X1) ) ).
cnf(u1579,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(a)
| compose(compose(g,a),compose(domain(X0),compose(a,b))) = compose(compose(compose(g,a),domain(X0)),compose(a,b)) ) ).
cnf(u4615,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(X0,compose(compose(h,a),compose(h,a))) = compose(compose(X0,compose(h,a)),compose(h,a)) ) ).
cnf(u12920,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(compose(h,a),compose(g,a))) = compose(compose(compose(h,a),compose(h,a)),compose(g,a)) ) ).
cnf(u5296,hypothesis,
( domain(X0) != domain(a)
| domain(a) = domain(compose(domain(a),X0)) ) ).
cnf(u4896,hypothesis,
( codomain(X0) != domain(h)
| domain(b) = codomain(compose(codomain(X0),compose(h,a))) ) ).
cnf(u1447,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(a)
| compose(codomain(X0),compose(g,X1)) = compose(compose(codomain(X0),g),X1) ) ).
cnf(u2466,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(a,b),compose(compose(g,a),X0)) = compose(compose(compose(a,b),compose(g,a)),X0) ) ).
cnf(u1585,hypothesis,
( domain(X0) != domain(a)
| compose(h,compose(domain(X0),compose(a,b))) = compose(compose(h,domain(X0)),compose(a,b)) ) ).
cnf(u2107,hypothesis,
( codomain(X0) != domain(b)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(a,codomain(X0))) = compose(compose(compose(a,b),a),codomain(X0)) ) ).
cnf(u4388,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(h,a),compose(h,a))) ) ).
cnf(u5678,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(a)
| compose(X0,compose(a,compose(a,b))) = compose(compose(X0,a),compose(a,b)) ) ).
cnf(u7341,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(g,a)) = compose(h,compose(domain(a),compose(g,a))) ) ).
cnf(u3510,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(b)
| compose(X0,compose(compose(g,a),domain(X1))) = compose(compose(X0,compose(g,a)),domain(X1)) ) ).
cnf(u4618,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(h)
| compose(X1,compose(codomain(X0),compose(h,a))) = compose(compose(X1,codomain(X0)),compose(h,a)) ) ).
cnf(u11326,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(a,compose(g,compose(h,compose(a,b)))) = compose(compose(a,g),compose(h,compose(a,b))) ) ).
cnf(u10562,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),domain(X0)) = compose(domain(h),compose(compose(h,compose(a,b)),domain(X0))) ) ).
cnf(u6470,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != codomain(X1)
| compose(codomain(X0),compose(codomain(X1),compose(a,b))) = compose(compose(codomain(X0),codomain(X1)),compose(a,b)) ) ).
cnf(u2991,hypothesis,
( codomain(X1) != codomain(b)
| codomain(X0) != domain(a)
| compose(codomain(X0),compose(compose(a,b),codomain(X1))) = compose(compose(codomain(X0),compose(a,b)),codomain(X1)) ) ).
cnf(u10807,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,compose(a,b))) = compose(compose(compose(h,a),compose(h,compose(a,b))),codomain(b)) ) ).
cnf(u9892,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != codomain(b)
| compose(compose(a,b),compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(compose(a,b),compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u8345,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),domain(X0)) = compose(compose(compose(a,b),domain(X0)),domain(X0)) ) ).
cnf(u3509,hypothesis,
( codomain(X0) != domain(h)
| domain(X1) != domain(b)
| compose(X0,compose(compose(h,a),domain(X1))) = compose(compose(X0,compose(h,a)),domain(X1)) ) ).
cnf(u12121,hypothesis,
( domain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(g,a),compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(compose(g,a),compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u13730,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != codomain(X1)
| compose(domain(X0),compose(codomain(X1),compose(g,a))) = compose(compose(domain(X0),codomain(X1)),compose(g,a)) ) ).
cnf(u3252,hypothesis,
( codomain(X0) != domain(a)
| compose(g,codomain(X0)) = compose(domain(h),compose(g,codomain(X0))) ) ).
cnf(u2619,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),X0) = compose(g,compose(compose(a,b),X0)) ) ).
cnf(u7493,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(b)
| compose(h,compose(domain(b),X0)) = compose(compose(h,domain(b)),X0) ) ).
cnf(u6933,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),domain(X0)) = compose(compose(compose(h,compose(a,b)),domain(X0)),domain(X0)) ) ).
cnf(u11693,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(compose(g,a),domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u8137,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,a),compose(g,compose(h,a))) = compose(compose(compose(h,a),g),compose(h,a)) ) ).
cnf(u2111,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(a)
| compose(a,compose(a,codomain(X0))) = compose(compose(a,a),codomain(X0)) ) ).
cnf(u3513,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != codomain(b)
| compose(X0,compose(compose(a,b),domain(X1))) = compose(compose(X0,compose(a,b)),domain(X1)) ) ).
cnf(u2894,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(a,b),codomain(X0)) = compose(compose(compose(a,b),codomain(X0)),codomain(X0)) ) ).
cnf(u1002,hypothesis,
( domain(X0) != domain(h)
| domain(X0) = domain(compose(domain(X0),compose(g,a))) ) ).
cnf(u9040,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,a)) = compose(compose(h,compose(a,b)),compose(codomain(b),compose(g,a))) ) ).
cnf(u2900,hypothesis,
( codomain(X0) != domain(a)
| compose(g,codomain(X0)) = compose(compose(g,codomain(X0)),codomain(X0)) ) ).
cnf(u7356,hypothesis,
( domain(a) != domain(h)
| compose(g,compose(g,a)) = compose(g,compose(domain(a),compose(g,a))) ) ).
cnf(u13153,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(h)
| compose(compose(h,compose(a,b)),compose(codomain(X0),compose(h,a))) = compose(compose(compose(h,compose(a,b)),codomain(X0)),compose(h,a)) ) ).
cnf(u2376,hypothesis,
( domain(b) != domain(a)
| compose(a,compose(a,b)) = compose(compose(a,compose(a,b)),codomain(b)) ) ).
cnf(u1857,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(a,b),compose(compose(h,a),X0)) = compose(compose(compose(a,b),compose(h,a)),X0) ) ).
cnf(u379,hypothesis,
( codomain(X0) != domain(h)
| domain(X0) = domain(compose(X0,compose(h,a))) ) ).
cnf(u93,hypothesis,
compose(h,compose(a,b)) = compose(compose(h,a),b) ).
cnf(u576,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(g,a)) = compose(compose(domain(X0),g),a) ) ).
cnf(u7625,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(a,b),codomain(X0)) = compose(compose(a,b),compose(codomain(b),codomain(X0))) ) ).
cnf(u12124,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(compose(g,a),compose(domain(X0),domain(X1))) = compose(compose(compose(g,a),domain(X0)),domain(X1)) ) ).
cnf(u4163,hypothesis,
( codomain(X0) != domain(b)
| compose(a,codomain(X0)) = compose(a,compose(domain(b),codomain(X0))) ) ).
cnf(u11321,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(codomain(X0),compose(g,compose(h,compose(a,b)))) = compose(compose(codomain(X0),g),compose(h,compose(a,b))) ) ).
cnf(u1109,hypothesis,
( domain(a) != domain(h)
| domain(b) = codomain(compose(g,compose(g,a))) ) ).
cnf(u5858,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(a,compose(h,compose(a,b)))) = compose(compose(compose(g,a),a),compose(h,compose(a,b))) ) ).
cnf(u1644,hypothesis,
( codomain(X0) != domain(a)
| domain(h) = domain(compose(h,codomain(X0))) ) ).
cnf(u5476,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(domain(X0),codomain(X1))) = compose(compose(compose(g,a),domain(X0)),codomain(X1)) ) ).
cnf(u5750,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(a)
| compose(h,compose(X1,codomain(X0))) = compose(compose(h,X1),codomain(X0)) ) ).
cnf(u83,hypothesis,
g = compose(g,domain(a)) ).
cnf(u4310,hypothesis,
( domain(b) != domain(h)
| compose(a,h) = compose(compose(a,h),domain(a)) ) ).
cnf(u5221,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(a,compose(a,compose(g,a))) = compose(compose(a,a),compose(g,a)) ) ).
cnf(u367,hypothesis,
( domain(b) != domain(a)
| domain(a) = domain(compose(a,compose(a,b))) ) ).
cnf(u2893,axiom,
( codomain(X0) != codomain(X1)
| compose(codomain(X0),codomain(X1)) = compose(compose(codomain(X0),codomain(X1)),codomain(X1)) ) ).
cnf(u721,hypothesis,
( domain(X0) != domain(b)
| compose(compose(h,a),domain(X0)) = compose(h,compose(a,domain(X0))) ) ).
cnf(u476,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(g,X0)) = compose(compose(g,g),X0) ) ).
cnf(u12387,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(h,a),codomain(X0)) = compose(domain(h),compose(compose(h,a),codomain(X0))) ) ).
cnf(u8340,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(g,a)) = compose(compose(compose(a,b),compose(g,a)),domain(b)) ) ).
cnf(u196,hypothesis,
( domain(b) != domain(a)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,compose(a,b))) = compose(compose(domain(X0),a),compose(a,b)) ) ).
cnf(u6512,hypothesis,
( domain(b) != domain(a)
| compose(compose(g,a),compose(a,b)) = compose(compose(g,a),compose(domain(b),compose(a,b))) ) ).
cnf(u2510,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) = codomain(compose(compose(g,a),codomain(X0))) ) ).
cnf(u136,hypothesis,
( codomain(X0) != domain(h)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(g,a))) = compose(compose(X1,X0),compose(g,a)) ) ).
cnf(u7783,hypothesis,
( codomain(X0) != codomain(b)
| domain(X1) != domain(h)
| compose(domain(X1),compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(domain(X1),compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u1498,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,compose(a,b))) = compose(domain(a),compose(a,compose(h,compose(a,b)))) ) ).
cnf(u9779,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != domain(b)
| compose(codomain(X1),compose(compose(g,a),codomain(X0))) = compose(compose(codomain(X1),compose(g,a)),codomain(X0)) ) ).
cnf(u4222,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(h,codomain(X0))) = compose(compose(compose(h,compose(a,b)),h),codomain(X0)) ) ).
cnf(u10859,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(a,b))) = compose(compose(h,compose(a,b)),compose(codomain(b),compose(h,compose(a,b)))) ) ).
cnf(u8040,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(a)
| compose(g,compose(domain(X0),compose(g,a))) = compose(compose(g,domain(X0)),compose(g,a)) ) ).
cnf(u8144,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(g,compose(h,a))) = compose(compose(h,g),compose(h,a)) ) ).
cnf(u3954,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),X1) = compose(compose(codomain(X0),domain(X1)),X1) ) ).
cnf(u3664,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(h)
| compose(X1,compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(X1,codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u13151,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != codomain(X1)
| compose(codomain(X0),compose(codomain(X1),compose(h,a))) = compose(compose(codomain(X0),codomain(X1)),compose(h,a)) ) ).
cnf(u10311,hypothesis,
( domain(b) != domain(h)
| codomain(b) = codomain(compose(compose(h,a),compose(h,compose(a,b)))) ) ).
cnf(u8206,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(g,a),compose(g,compose(g,a))) = compose(compose(compose(g,a),g),compose(g,a)) ) ).
cnf(u108,hypothesis,
( codomain(X1) != domain(h)
| domain(X0) != domain(b)
| compose(X1,compose(compose(h,a),X0)) = compose(compose(X1,compose(h,a)),X0) ) ).
cnf(u10656,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),g) = compose(compose(compose(g,a),g),domain(a)) ) ).
cnf(u238,hypothesis,
( domain(b) != domain(h)
| compose(g,compose(a,compose(g,a))) = compose(compose(g,a),compose(g,a)) ) ).
cnf(u3788,axiom,
( domain(X1) != domain(X2)
| domain(X0) != domain(X1)
| compose(domain(X2),compose(domain(X1),domain(X0))) = compose(compose(domain(X2),domain(X1)),domain(X0)) ) ).
cnf(u9299,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),codomain(X1))) = compose(compose(g,codomain(X0)),codomain(X1)) ) ).
cnf(u5895,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) != domain(X1)
| compose(g,compose(codomain(X0),domain(X1))) = compose(compose(g,codomain(X0)),domain(X1)) ) ).
cnf(u7133,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),g) = compose(compose(g,a),compose(domain(b),g)) ) ).
cnf(u1496,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(g,a)) = compose(domain(a),compose(a,compose(g,a))) ) ).
cnf(u7911,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(a)
| compose(h,compose(domain(X0),compose(h,a))) = compose(compose(h,domain(X0)),compose(h,a)) ) ).
cnf(u6633,hypothesis,
( domain(X1) != domain(h)
| domain(X0) != domain(b)
| compose(domain(X1),compose(compose(h,a),domain(X0))) = compose(compose(domain(X1),compose(h,a)),domain(X0)) ) ).
cnf(u2684,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,a)) = compose(h,compose(compose(a,b),compose(g,a))) ) ).
cnf(u123,hypothesis,
( domain(X0) != domain(b)
| compose(g,compose(a,X0)) = compose(compose(g,a),X0) ) ).
cnf(u13325,hypothesis,
( codomain(X0) != domain(b)
| domain(b) != domain(h)
| compose(compose(h,a),compose(compose(g,a),codomain(X0))) = compose(compose(compose(h,a),compose(g,a)),codomain(X0)) ) ).
cnf(u355,axiom,
codomain(X0) = compose(codomain(X0),codomain(X0)) ).
cnf(u12006,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(g,a),compose(compose(g,a),compose(a,b))) = compose(compose(compose(g,a),compose(g,a)),compose(a,b)) ) ).
cnf(u1107,hypothesis,
( domain(a) != domain(h)
| codomain(b) = codomain(compose(g,compose(h,compose(a,b)))) ) ).
cnf(u2160,hypothesis,
( domain(b) != domain(a)
| compose(a,a) = compose(compose(a,a),domain(b)) ) ).
cnf(u5589,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),codomain(X1))) = compose(compose(a,codomain(X0)),codomain(X1)) ) ).
cnf(u6846,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(domain(X0),compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u443,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,compose(a,b))) = compose(compose(compose(g,a),g),compose(a,b)) ) ).
cnf(u1385,hypothesis,
( domain(a) != domain(h)
| domain(X0) != codomain(b)
| compose(h,compose(compose(h,compose(a,b)),X0)) = compose(compose(h,compose(h,compose(a,b))),X0) ) ).
cnf(u6246,hypothesis,
( domain(b) != domain(h)
| domain(h) = domain(compose(compose(h,a),compose(g,a))) ) ).
cnf(u2679,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),domain(X0)) = compose(h,compose(compose(a,b),domain(X0))) ) ).
cnf(u12529,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != codomain(X1)
| compose(compose(h,compose(a,b)),compose(codomain(X0),codomain(X1))) = compose(compose(compose(h,compose(a,b)),codomain(X0)),codomain(X1)) ) ).
cnf(u14596,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(h,compose(compose(g,a),compose(g,a))) = compose(compose(h,compose(g,a)),compose(g,a)) ) ).
cnf(u6873,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(compose(codomain(X0),compose(h,a)),b) ) ).
cnf(u12004,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,compose(a,b)),compose(compose(g,a),compose(a,b))) = compose(compose(compose(h,compose(a,b)),compose(g,a)),compose(a,b)) ) ).
cnf(u5392,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(a,b),compose(h,compose(g,a))) = compose(compose(compose(a,b),h),compose(g,a)) ) ).
cnf(u7918,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,a)) = compose(compose(X0,domain(h)),compose(h,a)) ) ).
cnf(u5707,hypothesis,
( domain(b) != domain(a)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,compose(a,b))) = compose(compose(compose(h,compose(a,b)),a),compose(a,b)) ) ).
cnf(u3424,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,a)) = compose(compose(h,compose(h,a)),domain(b)) ) ).
cnf(prove_h_equals_g,negated_conjecture,
h != g ).
cnf(u226,hypothesis,
( domain(b) != domain(a)
| compose(h,compose(a,compose(a,b))) = compose(compose(h,a),compose(a,b)) ) ).
cnf(u635,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(g,compose(h,compose(a,b)))) = compose(compose(domain(X0),g),compose(h,compose(a,b))) ) ).
cnf(u8966,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,compose(a,b))) = compose(codomain(X0),compose(codomain(X0),compose(h,compose(a,b)))) ) ).
cnf(u2061,axiom,
( domain(X0) != domain(X1)
| compose(domain(X0),X1) = compose(compose(domain(X0),X1),codomain(X1)) ) ).
cnf(u8155,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(h,domain(X0))) = compose(compose(compose(h,compose(a,b)),h),domain(X0)) ) ).
cnf(u4077,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),g) = compose(compose(codomain(X0),domain(h)),g) ) ).
cnf(u1584,hypothesis,
( domain(X0) != domain(a)
| compose(g,compose(domain(X0),compose(a,b))) = compose(compose(g,domain(X0)),compose(a,b)) ) ).
cnf(u127,hypothesis,
domain(b) = codomain(compose(g,a)) ).
cnf(u12530,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(b)
| compose(compose(h,a),compose(codomain(X0),codomain(X1))) = compose(compose(compose(h,a),codomain(X0)),codomain(X1)) ) ).
cnf(u7937,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,a)) = compose(compose(codomain(X0),domain(h)),compose(h,a)) ) ).
cnf(u267,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) = domain(compose(X1,codomain(X0))) ) ).
cnf(u7446,axiom,
( codomain(X0) != domain(X1)
| compose(domain(X1),codomain(X0)) = compose(domain(X1),compose(domain(X1),codomain(X0))) ) ).
cnf(u748,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),domain(X0)) = compose(g,compose(a,domain(X0))) ) ).
cnf(u10765,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,compose(a,b))) = compose(compose(compose(g,a),compose(h,compose(a,b))),codomain(b)) ) ).
cnf(star_property,axiom,
( codomain(X1) != domain(X2)
| codomain(X0) != domain(X1)
| compose(X0,compose(X1,X2)) = compose(compose(X0,X1),X2) ) ).
cnf(u8175,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(X1)
| compose(compose(h,compose(a,b)),compose(domain(X0),domain(X1))) = compose(compose(compose(h,compose(a,b)),domain(X0)),domain(X1)) ) ).
cnf(u3462,hypothesis,
( domain(a) != domain(h)
| compose(g,g) = compose(compose(g,g),domain(a)) ) ).
cnf(u4629,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(a,compose(h,a))) = compose(compose(compose(h,compose(a,b)),a),compose(h,a)) ) ).
cnf(u1654,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) = domain(compose(codomain(X0),codomain(X1))) ) ).
cnf(u919,hypothesis,
( b != compose(h,compose(a,b))
| domain(b) != domain(a)
| domain(b) = compose(h,a) ) ).
cnf(u7450,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(g,a)) = compose(domain(X0),compose(domain(X0),compose(g,a))) ) ).
cnf(u33,hypothesis,
codomain(b) = codomain(compose(a,b)) ).
cnf(u8199,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),h) = compose(compose(compose(h,a),h),domain(a)) ) ).
cnf(u8065,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(g,a)) = compose(compose(codomain(X0),domain(h)),compose(g,a)) ) ).
cnf(u4346,axiom,
( domain(X0) != codomain(X1)
| compose(codomain(X1),domain(X0)) = compose(compose(codomain(X1),domain(X0)),domain(X0)) ) ).
cnf(u2067,hypothesis,
( domain(X0) != domain(b)
| compose(a,X0) = compose(compose(a,X0),codomain(X0)) ) ).
cnf(u4638,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),compose(a,b))) = compose(compose(domain(X0),compose(a,b)),compose(a,b)) ) ).
cnf(u549,axiom,
( codomain(X0) != domain(X1)
| codomain(X0) = codomain(compose(domain(X1),codomain(X0))) ) ).
cnf(u10238,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(compose(h,a),compose(compose(h,a),compose(a,b))) = compose(compose(compose(h,a),compose(h,a)),compose(a,b)) ) ).
cnf(u8,axiom,
( codomain(X0) != domain(X1)
| domain(X0) = domain(compose(X0,X1)) ) ).
cnf(u138,hypothesis,
( domain(b) != domain(h)
| domain(b) = codomain(compose(a,compose(g,a))) ) ).
cnf(u5879,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(a)
| compose(g,compose(X1,codomain(X0))) = compose(compose(g,X1),codomain(X0)) ) ).
cnf(u15760,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(g,compose(compose(g,a),compose(h,a))) = compose(compose(g,compose(g,a)),compose(h,a)) ) ).
cnf(u39,hypothesis,
( codomain(X0) != codomain(h)
| codomain(compose(a,b)) = codomain(compose(X0,compose(a,b))) ) ).
cnf(u12322,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,a),codomain(X0))) = compose(compose(compose(h,compose(a,b)),compose(h,a)),codomain(X0)) ) ).
cnf(u7209,axiom,
( codomain(X1) != domain(X2)
| codomain(X0) != codomain(X1)
| compose(codomain(X0),compose(codomain(X1),X2)) = compose(compose(codomain(X0),codomain(X1)),X2) ) ).
cnf(u6927,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,a)) = compose(compose(compose(h,compose(a,b)),compose(h,a)),domain(b)) ) ).
cnf(u7452,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(domain(X0),compose(domain(X0),compose(h,compose(a,b)))) ) ).
cnf(u2106,hypothesis,
( codomain(X1) != domain(b)
| codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,codomain(X1))) = compose(compose(codomain(X0),a),codomain(X1)) ) ).
cnf(u7302,hypothesis,
( codomain(X0) != domain(h)
| compose(X0,compose(h,compose(a,b))) = compose(X0,compose(codomain(X0),compose(h,compose(a,b)))) ) ).
cnf(u7560,hypothesis,
( domain(X0) != domain(a)
| domain(X0) != domain(X1)
| compose(g,compose(domain(X0),X1)) = compose(compose(g,domain(X0)),X1) ) ).
cnf(u1431,axiom,
( codomain(X0) != domain(X1)
| domain(X1) != domain(X2)
| compose(codomain(X0),compose(domain(X1),X2)) = compose(compose(codomain(X0),domain(X1)),X2) ) ).
cnf(u1956,axiom,
( domain(X0) != codomain(X1)
| compose(X1,X0) = compose(compose(X1,X0),codomain(X0)) ) ).
cnf(u675,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(compose(g,a),compose(domain(X0),X1)) = compose(compose(compose(g,a),domain(X0)),X1) ) ).
cnf(u12919,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(compose(h,a),compose(g,a))) = compose(compose(compose(g,a),compose(h,a)),compose(g,a)) ) ).
cnf(u37,hypothesis,
( domain(X0) != codomain(h)
| codomain(X0) = codomain(compose(g,X0)) ) ).
cnf(u167,axiom,
domain(X0) = compose(domain(X0),domain(X0)) ).
cnf(u4341,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(g,a)) = compose(compose(codomain(X0),compose(g,a)),domain(b)) ) ).
cnf(u572,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(g,compose(g,a))) = compose(compose(domain(X0),g),compose(g,a)) ) ).
cnf(u5394,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,a),compose(h,compose(g,a))) = compose(compose(compose(h,a),h),compose(g,a)) ) ).
cnf(u11724,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(h,compose(a,b))) = compose(compose(compose(h,a),domain(h)),compose(h,compose(a,b))) ) ).
cnf(u431,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(h,compose(a,b))) = compose(compose(compose(g,a),h),compose(a,b)) ) ).
cnf(u48,hypothesis,
( codomain(X1) != codomain(h)
| domain(X0) != codomain(b)
| compose(X1,compose(compose(a,b),X0)) = compose(compose(X1,compose(a,b)),X0) ) ).
cnf(u4650,hypothesis,
( domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(a,b),compose(a,b))) = compose(compose(compose(h,compose(a,b)),compose(a,b)),compose(a,b)) ) ).
cnf(u1680,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(h,a))) = compose(compose(domain(X0),h),compose(h,a)) ) ).
cnf(u7327,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,a)) = compose(a,compose(domain(b),compose(h,a))) ) ).
cnf(u7073,hypothesis,
( codomain(b) != domain(h)
| domain(b) = codomain(compose(compose(a,b),compose(g,a))) ) ).
cnf(u3500,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),compose(X0,domain(X1))) = compose(compose(compose(h,compose(a,b)),X0),domain(X1)) ) ).
cnf(u4534,hypothesis,
( domain(X1) != codomain(b)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,b),domain(X1))) = compose(compose(domain(X0),compose(a,b)),domain(X1)) ) ).
cnf(u7126,hypothesis,
( codomain(X0) != domain(b)
| compose(compose(g,a),codomain(X0)) = compose(compose(g,a),compose(domain(b),codomain(X0))) ) ).
cnf(u9107,hypothesis,
( codomain(X0) != codomain(b)
| domain(a) != domain(h)
| compose(h,compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(h,compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u9893,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,compose(a,b)),codomain(X0))) = compose(compose(compose(h,compose(a,b)),compose(h,compose(a,b))),codomain(X0)) ) ).
cnf(u9783,axiom,
( codomain(X0) != codomain(X2)
| codomain(X0) != codomain(X1)
| compose(codomain(X2),compose(codomain(X0),codomain(X1))) = compose(compose(codomain(X2),codomain(X0)),codomain(X1)) ) ).
cnf(u433,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(a,b))) = compose(compose(h,h),compose(a,b)) ) ).
cnf(u420,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(a)
| compose(X1,compose(domain(X0),compose(a,b))) = compose(compose(X1,domain(X0)),compose(a,b)) ) ).
cnf(u2467,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(compose(g,a),X0)) = compose(compose(compose(h,compose(a,b)),compose(g,a)),X0) ) ).
cnf(u11438,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != codomain(b)
| compose(compose(a,b),compose(compose(h,compose(a,b)),domain(X0))) = compose(compose(compose(a,b),compose(h,compose(a,b))),domain(X0)) ) ).
cnf(u176,hypothesis,
compose(h,compose(a,b)) = compose(domain(h),compose(h,compose(a,b))) ).
cnf(u3967,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(g,a)) = compose(compose(domain(X0),domain(h)),compose(g,a)) ) ).
cnf(u3497,axiom,
( codomain(X1) != domain(X2)
| domain(X0) != domain(X1)
| compose(domain(X0),compose(X1,domain(X2))) = compose(compose(domain(X0),X1),domain(X2)) ) ).
cnf(u1716,hypothesis,
( codomain(X0) != domain(h)
| compose(codomain(X0),compose(h,a)) = compose(compose(codomain(X0),h),a) ) ).
cnf(u947,hypothesis,
( domain(a) != codomain(b)
| codomain(b) = codomain(compose(compose(a,b),compose(a,b))) ) ).
cnf(u560,hypothesis,
( domain(X0) != domain(h)
| domain(a) = codomain(compose(domain(X0),g)) ) ).
cnf(u439,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,compose(a,b))) = compose(compose(domain(X0),g),compose(a,b)) ) ).
cnf(u7994,hypothesis,
( codomain(b) != domain(h)
| domain(a) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),h),compose(h,compose(a,b))) ) ).
cnf(u4012,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(X1)
| compose(domain(X1),compose(codomain(X0),g)) = compose(compose(domain(X1),codomain(X0)),g) ) ).
cnf(u11435,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(a)
| compose(compose(a,b),compose(g,domain(X0))) = compose(compose(compose(a,b),g),domain(X0)) ) ).
cnf(u6845,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,a),compose(h,a))) = compose(compose(domain(X0),compose(h,a)),compose(h,a)) ) ).
cnf(u11821,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),compose(h,a))) = compose(compose(g,codomain(X0)),compose(h,a)) ) ).
cnf(u7735,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(h,compose(a,b)),codomain(X0)) = compose(compose(h,compose(a,b)),compose(codomain(b),codomain(X0))) ) ).
cnf(u4540,hypothesis,
( domain(b) != domain(a)
| domain(X0) != codomain(b)
| compose(domain(b),compose(compose(a,b),domain(X0))) = compose(compose(domain(b),compose(a,b)),domain(X0)) ) ).
cnf(u8379,hypothesis,
( domain(b) != domain(a)
| compose(compose(h,a),compose(a,domain(a))) = compose(compose(compose(h,a),a),domain(a)) ) ).
cnf(u77,hypothesis,
( codomain(X0) != domain(a)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(a,b))) = compose(compose(X1,X0),compose(a,b)) ) ).
cnf(u840,hypothesis,
( domain(X0) != domain(b)
| domain(a) = domain(compose(a,domain(X0))) ) ).
cnf(u4443,axiom,
( codomain(X0) != codomain(X2)
| codomain(X0) != domain(X1)
| compose(codomain(X2),compose(codomain(X0),domain(X1))) = compose(compose(codomain(X2),codomain(X0)),domain(X1)) ) ).
cnf(u10827,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(g,a),compose(compose(g,a),domain(X0))) = compose(compose(compose(g,a),compose(g,a)),domain(X0)) ) ).
cnf(u5130,hypothesis,
( codomain(b) != domain(h)
| codomain(X0) != domain(a)
| compose(compose(h,compose(a,b)),compose(g,codomain(X0))) = compose(compose(compose(h,compose(a,b)),g),codomain(X0)) ) ).
cnf(u17601,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(compose(h,compose(a,b)),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u7629,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(g,a)) = compose(compose(a,b),compose(codomain(b),compose(g,a))) ) ).
cnf(u8036,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(domain(X0),compose(g,a))) = compose(compose(compose(h,a),domain(X0)),compose(g,a)) ) ).
cnf(u6509,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),compose(a,b)) = compose(compose(a,b),compose(codomain(b),compose(a,b))) ) ).
cnf(u1960,hypothesis,
( codomain(X1) != domain(h)
| codomain(X0) != domain(b)
| compose(X1,compose(compose(h,a),codomain(X0))) = compose(compose(X1,compose(h,a)),codomain(X0)) ) ).
cnf(u5305,hypothesis,
( codomain(X0) != domain(h)
| codomain(X0) = domain(compose(codomain(X0),compose(h,compose(a,b)))) ) ).
cnf(u67,hypothesis,
domain(g) = domain(h) ).
cnf(u1478,hypothesis,
( domain(X0) != domain(b)
| compose(a,X0) = compose(domain(a),compose(a,X0)) ) ).
cnf(u3655,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(X0,compose(h,compose(h,compose(a,b)))) = compose(compose(X0,h),compose(h,compose(a,b))) ) ).
cnf(u2377,hypothesis,
( codomain(X0) != domain(b)
| compose(a,codomain(X0)) = compose(compose(a,codomain(X0)),codomain(X0)) ) ).
cnf(u7372,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(a,compose(domain(X0),X1)) = compose(compose(a,domain(X0)),X1) ) ).
cnf(u94,hypothesis,
h = compose(h,domain(a)) ).
cnf(u5128,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != domain(h)
| compose(codomain(X0),compose(g,codomain(X1))) = compose(compose(codomain(X0),g),codomain(X1)) ) ).
cnf(u7867,hypothesis,
( domain(a) != domain(h)
| compose(domain(a),compose(h,compose(g,a))) = compose(compose(domain(a),h),compose(g,a)) ) ).
cnf(u838,axiom,
( domain(X1) != codomain(X2)
| domain(X0) != codomain(X1)
| compose(X2,compose(X1,domain(X0))) = compose(compose(X2,X1),domain(X0)) ) ).
cnf(u3661,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(X0,compose(compose(h,a),compose(h,compose(a,b)))) = compose(compose(X0,compose(h,a)),compose(h,compose(a,b))) ) ).
cnf(u361,hypothesis,
( b != compose(X0,b)
| codomain(X0) != domain(a)
| domain(b) = X0 ) ).
cnf(u3659,hypothesis,
( codomain(X0) != domain(h)
| domain(a) != domain(h)
| compose(X0,compose(g,compose(h,compose(a,b)))) = compose(compose(X0,g),compose(h,compose(a,b))) ) ).
cnf(u14934,hypothesis,
( domain(X0) != domain(b)
| compose(compose(g,a),domain(X0)) = compose(domain(h),compose(compose(g,a),domain(X0))) ) ).
cnf(u349,hypothesis,
( domain(a) != codomain(b)
| domain(a) = domain(compose(compose(a,b),compose(a,b))) ) ).
cnf(u16147,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(h)
| compose(compose(a,b),compose(codomain(X0),compose(h,compose(a,b)))) = compose(compose(compose(a,b),codomain(X0)),compose(h,compose(a,b))) ) ).
cnf(u3665,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(h)
| compose(X1,compose(domain(X0),compose(h,compose(a,b)))) = compose(compose(X1,domain(X0)),compose(h,compose(a,b))) ) ).
cnf(u5997,hypothesis,
( domain(b) != domain(h)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(domain(X0),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u1963,axiom,
( codomain(X0) != codomain(X2)
| codomain(X0) != codomain(X1)
| compose(X2,compose(codomain(X0),codomain(X1))) = compose(compose(X2,codomain(X0)),codomain(X1)) ) ).
cnf(u3789,axiom,
( codomain(X0) != domain(X1)
| domain(X1) != domain(X2)
| compose(domain(X2),compose(domain(X1),codomain(X0))) = compose(compose(domain(X2),domain(X1)),codomain(X0)) ) ).
cnf(u11425,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(b)
| compose(compose(a,b),compose(X1,codomain(X0))) = compose(compose(compose(a,b),X1),codomain(X0)) ) ).
cnf(u7885,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) = codomain(compose(compose(h,compose(a,b)),domain(X0))) ) ).
cnf(u13857,hypothesis,
( domain(a) != domain(h)
| compose(domain(a),compose(g,compose(g,a))) = compose(compose(domain(a),g),compose(g,a)) ) ).
cnf(u1108,hypothesis,
( domain(a) != domain(h)
| domain(b) = codomain(compose(g,compose(h,a))) ) ).
cnf(u5477,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(b)
| compose(a,compose(domain(X0),codomain(X1))) = compose(compose(a,domain(X0)),codomain(X1)) ) ).
cnf(u728,hypothesis,
( domain(b) != domain(a)
| compose(h,compose(a,domain(a))) = compose(compose(h,a),domain(a)) ) ).
cnf(u12007,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(a,compose(compose(g,a),compose(a,b))) = compose(compose(a,compose(g,a)),compose(a,b)) ) ).
cnf(u362,hypothesis,
( a != compose(X0,a)
| codomain(X0) != domain(b)
| domain(a) = X0 ) ).
cnf(u11727,hypothesis,
( domain(a) != domain(h)
| compose(h,compose(h,compose(a,b))) = compose(compose(h,domain(h)),compose(h,compose(a,b))) ) ).
cnf(u82,hypothesis,
compose(a,b) = compose(compose(a,b),codomain(b)) ).
cnf(u3793,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),compose(g,a))) = compose(compose(domain(X1),domain(X0)),compose(g,a)) ) ).
cnf(u5990,hypothesis,
( domain(X1) != domain(h)
| domain(X0) != domain(b)
| compose(domain(X1),compose(compose(g,a),domain(X0))) = compose(compose(domain(X1),compose(g,a)),domain(X0)) ) ).
cnf(u7630,hypothesis,
( codomain(b) != domain(h)
| compose(compose(a,b),compose(h,a)) = compose(compose(a,b),compose(codomain(b),compose(h,a))) ) ).
cnf(u388,hypothesis,
( domain(b) != domain(h)
| domain(b) = codomain(compose(a,compose(h,a))) ) ).
cnf(u1112,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) = codomain(compose(g,codomain(X0))) ) ).
cnf(u7130,hypothesis,
( domain(b) != domain(h)
| compose(compose(g,a),compose(g,a)) = compose(compose(g,a),compose(domain(b),compose(g,a))) ) ).
cnf(u105,hypothesis,
( domain(X0) != domain(b)
| codomain(X0) = codomain(compose(compose(h,a),X0)) ) ).
cnf(u235,hypothesis,
( domain(b) != domain(a)
| compose(g,compose(a,compose(a,b))) = compose(compose(g,a),compose(a,b)) ) ).
cnf(u10742,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),compose(a,b)) = compose(domain(a),compose(compose(a,b),compose(a,b))) ) ).
cnf(u10240,hypothesis,
( domain(b) != domain(h)
| domain(b) != domain(a)
| compose(a,compose(compose(h,a),compose(a,b))) = compose(compose(a,compose(h,a)),compose(a,b)) ) ).
cnf(u2277,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,a)) = compose(compose(domain(X0),compose(h,a)),domain(b)) ) ).
cnf(u360,hypothesis,
( b != compose(X0,b)
| domain(b) != domain(a)
| codomain(X0) != domain(b)
| domain(b) = X0 ) ).
cnf(u1143,hypothesis,
( domain(a) != domain(h)
| domain(h) = domain(compose(g,compose(h,a))) ) ).
cnf(u4,axiom,
codomain(X0) = domain(codomain(X0)) ).
cnf(u1497,hypothesis,
( domain(b) != domain(h)
| compose(a,compose(h,a)) = compose(domain(a),compose(a,compose(h,a))) ) ).
cnf(u7908,hypothesis,
( domain(X0) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,a),compose(domain(X0),compose(h,a))) = compose(compose(compose(h,a),domain(X0)),compose(h,a)) ) ).
cnf(u8931,hypothesis,
( codomain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(compose(a,b),compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u1006,axiom,
( codomain(X0) != domain(X1)
| domain(X1) = domain(compose(domain(X1),codomain(X0))) ) ).
cnf(u14590,hypothesis,
( codomain(X0) != domain(h)
| domain(b) != domain(h)
| compose(codomain(X0),compose(compose(g,a),compose(g,a))) = compose(compose(codomain(X0),compose(g,a)),compose(g,a)) ) ).
cnf(u15755,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(compose(g,a),compose(h,a))) = compose(compose(compose(h,compose(a,b)),compose(g,a)),compose(h,a)) ) ).
cnf(u17600,hypothesis,
( codomain(b) != domain(h)
| domain(b) != domain(h)
| compose(compose(a,b),compose(compose(g,a),compose(h,compose(a,b)))) = compose(compose(compose(a,b),compose(g,a)),compose(h,compose(a,b))) ) ).
cnf(u1148,hypothesis,
( domain(X0) != domain(a)
| domain(h) = domain(compose(g,domain(X0))) ) ).
cnf(u3059,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),h) = compose(compose(domain(X0),h),domain(a)) ) ).
cnf(u8667,hypothesis,
( domain(a) != domain(h)
| compose(domain(a),compose(h,compose(h,a))) = compose(compose(domain(a),h),compose(h,a)) ) ).
cnf(u2278,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(g,a)) = compose(compose(domain(X0),compose(g,a)),domain(b)) ) ).
cnf(u7285,axiom,
( domain(X0) != domain(X1)
| compose(domain(X0),X1) = compose(domain(X0),compose(domain(X0),X1)) ) ).
cnf(u5716,hypothesis,
( domain(b) != domain(a)
| compose(a,compose(a,compose(a,b))) = compose(compose(a,a),compose(a,b)) ) ).
cnf(u4223,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(compose(h,a),compose(h,codomain(X0))) = compose(compose(compose(h,a),h),codomain(X0)) ) ).
cnf(u4114,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(b)
| compose(a,compose(X1,codomain(X0))) = compose(compose(a,X1),codomain(X0)) ) ).
cnf(u5132,hypothesis,
( codomain(X0) != domain(a)
| domain(b) != domain(h)
| compose(compose(g,a),compose(g,codomain(X0))) = compose(compose(compose(g,a),g),codomain(X0)) ) ).
cnf(u12916,hypothesis,
( domain(b) != domain(h)
| domain(a) != domain(h)
| compose(g,compose(compose(h,a),compose(g,a))) = compose(compose(g,compose(h,a)),compose(g,a)) ) ).
cnf(u8171,hypothesis,
( codomain(b) != domain(h)
| domain(X0) != domain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,a),domain(X0))) = compose(compose(compose(h,compose(a,b)),compose(h,a)),domain(X0)) ) ).
cnf(u4200,hypothesis,
( domain(a) != codomain(b)
| domain(X0) != domain(b)
| compose(compose(a,b),compose(a,domain(X0))) = compose(compose(compose(a,b),a),domain(X0)) ) ).
cnf(u239,hypothesis,
( domain(b) != domain(h)
| compose(g,compose(a,g)) = compose(compose(g,a),g) ) ).
cnf(u5892,hypothesis,
( domain(a) != domain(h)
| domain(X0) != domain(b)
| compose(g,compose(compose(h,a),domain(X0))) = compose(compose(g,compose(h,a)),domain(X0)) ) ).
cnf(u7939,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(h,a)) = compose(compose(compose(h,compose(a,b)),domain(h)),compose(h,a)) ) ).
cnf(u8932,hypothesis,
( codomain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(h,compose(a,b)),compose(compose(h,compose(a,b)),compose(a,b))) = compose(compose(compose(h,compose(a,b)),compose(h,compose(a,b))),compose(a,b)) ) ).
cnf(u272,hypothesis,
( codomain(X0) != domain(b)
| compose(g,compose(a,codomain(X0))) = compose(compose(g,a),codomain(X0)) ) ).
cnf(u2934,hypothesis,
( domain(a) != domain(h)
| codomain(b) = codomain(compose(h,compose(h,compose(a,b)))) ) ).
cnf(u120,hypothesis,
( domain(X0) != domain(a)
| codomain(X0) = codomain(compose(g,X0)) ) ).
cnf(u7170,hypothesis,
( domain(b) != domain(h)
| compose(compose(h,a),compose(g,a)) = compose(compose(h,a),compose(domain(b),compose(g,a))) ) ).
cnf(u8408,hypothesis,
( domain(X0) != domain(b)
| domain(X0) = codomain(compose(compose(h,a),domain(X0))) ) ).
cnf(u4628,hypothesis,
( domain(b) != domain(h)
| domain(a) != codomain(b)
| compose(compose(a,b),compose(a,compose(h,a))) = compose(compose(compose(a,b),a),compose(h,a)) ) ).
cnf(u2078,axiom,
( codomain(X0) != codomain(X1)
| compose(X1,codomain(X0)) = compose(compose(X1,codomain(X0)),codomain(X0)) ) ).
cnf(u5896,hypothesis,
( domain(X0) != domain(a)
| domain(X0) != domain(X1)
| compose(g,compose(domain(X0),domain(X1))) = compose(compose(g,domain(X0)),domain(X1)) ) ).
cnf(u1608,hypothesis,
( domain(a) != codomain(b)
| compose(compose(a,b),compose(a,b)) = compose(compose(compose(a,b),domain(a)),compose(a,b)) ) ).
cnf(u1855,hypothesis,
( domain(X1) != domain(b)
| domain(X0) != domain(h)
| compose(domain(X0),compose(compose(h,a),X1)) = compose(compose(domain(X0),compose(h,a)),X1) ) ).
cnf(u1000,hypothesis,
( domain(X0) != domain(h)
| domain(X0) = domain(compose(domain(X0),compose(h,compose(a,b)))) ) ).
cnf(u5623,hypothesis,
( codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),domain(b))) = compose(compose(a,codomain(X0)),domain(b)) ) ).
cnf(u3297,hypothesis,
( domain(X0) != domain(a)
| domain(h) = domain(compose(h,domain(X0))) ) ).
cnf(u7451,hypothesis,
( domain(X0) != domain(h)
| compose(domain(X0),compose(h,a)) = compose(domain(X0),compose(domain(X0),compose(h,a))) ) ).
cnf(u8067,hypothesis,
( codomain(b) != domain(h)
| compose(compose(h,compose(a,b)),compose(g,a)) = compose(compose(compose(h,compose(a,b)),domain(h)),compose(g,a)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CAT002-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.24 % Computer : n018.cluster.edu
% 0.12/0.24 % Model : x86_64 x86_64
% 0.12/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.24 % Memory : 8046.5625MB
% 0.12/0.24 % OS : Linux 6.8.0-71-generic
% 0.12/0.24 % CPULimit : 300
% 0.12/0.24 % WCLimit : 300
% 0.12/0.24 % DateTime : Mon Sep 28 21:13:55 UTC 2026
% 0.12/0.24 % CPUTime :
% 0.12/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.29 Running first-order theorem proving
% 0.23/0.29 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.75/2.50 % (3793575)Input is clausal, will run a generic CNF schedule.
% 10.75/2.50 % (3793581)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2620536066:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.75/2.50 % (3793586)dis-21_1_sil=8000:lcm=predicate:random_seed=14018278:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.75/2.50 % (3793586)Refutation not found, incomplete strategy
% 10.75/2.50 % (3793586)------------------------------
% 10.75/2.50 % (3793586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793586)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793586)Termination reason: Refutation not found, incomplete strategy
% 10.75/2.50 % (3793586)Time elapsed: 0.004 s
% 10.75/2.50 % (3793586)Peak memory usage: 88 MB
% 10.75/2.50 % (3793586)Instructions burned: 1 (million)
% 10.75/2.50 % (3793584)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4110894641:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.75/2.50 % (3793585)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2154892825:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.75/2.50 % (3793583)lrs+10_1_sil=8000:sp=occurrence:random_seed=3192398020:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.75/2.50 % (3793580)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3837830216:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.75/2.50 % (3793582)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=996306706:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.75/2.50 % (3793584)Instruction limit reached!
% 10.75/2.50 % (3793584)------------------------------
% 10.75/2.50 % (3793584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793584)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793584)Termination reason: Instruction limit
% 10.75/2.50 % (3793584)Termination phase: Saturation
% 10.75/2.50 % (3793584)Time elapsed: 0.098 s
% 10.75/2.50 % (3793584)Peak memory usage: 88 MB
% 10.75/2.50 % (3793584)Instructions burned: 115 (million)
% 10.75/2.50 % (3793583)Instruction limit reached!
% 10.75/2.50 % (3793583)------------------------------
% 10.75/2.50 % (3793583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793583)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793583)Termination reason: Instruction limit
% 10.75/2.50 % (3793583)Termination phase: Saturation
% 10.75/2.50 % (3793583)Time elapsed: 0.100 s
% 10.75/2.50 % (3793583)Peak memory usage: 89 MB
% 10.75/2.50 % (3793583)Instructions burned: 108 (million)
% 10.75/2.50 % (3793585)Instruction limit reached!
% 10.75/2.50 % (3793585)------------------------------
% 10.75/2.50 % (3793585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793585)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793585)Termination reason: Instruction limit
% 10.75/2.50 % (3793585)Termination phase: Saturation
% 10.75/2.50 % (3793585)Time elapsed: 0.163 s
% 10.75/2.50 % (3793585)Peak memory usage: 89 MB
% 10.75/2.50 % (3793585)Instructions burned: 180 (million)
% 10.75/2.50 % (3793586)------------------------------
% 10.75/2.50 % (3793586)------------------------------
% 10.75/2.50 % (3793594)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1339215166:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 10.75/2.50 % (3793595)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1313974281:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 10.75/2.50 % (3793596)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3819356606:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 10.75/2.50 % (3793594)Instruction limit reached!
% 10.75/2.50 % (3793594)------------------------------
% 10.75/2.50 % (3793594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793594)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793594)Termination reason: Instruction limit
% 10.75/2.50 % (3793594)Termination phase: Saturation
% 10.75/2.50 % (3793594)Time elapsed: 0.132 s
% 10.75/2.50 % (3793594)Peak memory usage: 89 MB
% 10.75/2.50 % (3793594)Instructions burned: 144 (million)
% 10.75/2.50 % (3793597)lrs+10_64_to=lpo:sil=8000:random_seed=3415540763:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 10.75/2.50 % (3793595)Instruction limit reached!
% 10.75/2.50 % (3793595)------------------------------
% 10.75/2.50 % (3793595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793595)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793595)Termination reason: Instruction limit
% 10.75/2.50 % (3793595)Termination phase: Saturation
% 10.75/2.50 % (3793595)Time elapsed: 0.182 s
% 10.75/2.50 % (3793595)Peak memory usage: 89 MB
% 10.75/2.50 % (3793595)Instructions burned: 189 (million)
% 10.75/2.50 % (3793596)Instruction limit reached!
% 10.75/2.50 % (3793596)------------------------------
% 10.75/2.50 % (3793596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793596)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793596)Termination reason: Instruction limit
% 10.75/2.50 % (3793596)Termination phase: Saturation
% 10.75/2.50 % (3793596)Time elapsed: 0.178 s
% 10.75/2.50 % (3793596)Peak memory usage: 89 MB
% 10.75/2.50 % (3793596)Instructions burned: 219 (million)
% 10.75/2.50 % (3793597)Instruction limit reached!
% 10.75/2.50 % (3793597)------------------------------
% 10.75/2.50 % (3793597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793597)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793597)Termination reason: Instruction limit
% 10.75/2.50 % (3793597)Termination phase: Saturation
% 10.75/2.50 % (3793597)Time elapsed: 0.118 s
% 10.75/2.50 % (3793597)Peak memory usage: 89 MB
% 10.75/2.50 % (3793597)Instructions burned: 126 (million)
% 10.75/2.50 % (3793601)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=51745411:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 10.75/2.50 % (3793603)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=894437730:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 10.75/2.50 % (3793604)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1033715937:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 10.75/2.50 % (3793605)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3416831981:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 10.75/2.50 % (3793601)Instruction limit reached!
% 10.75/2.50 % (3793601)------------------------------
% 10.75/2.50 % (3793601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793601)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793601)Termination reason: Instruction limit
% 10.75/2.50 % (3793601)Termination phase: Saturation
% 10.75/2.50 % (3793601)Time elapsed: 0.176 s
% 10.75/2.50 % (3793601)Peak memory usage: 90 MB
% 10.75/2.50 % (3793601)Instructions burned: 194 (million)
% 10.75/2.50 % (3793603)Instruction limit reached!
% 10.75/2.50 % (3793603)------------------------------
% 10.75/2.50 % (3793603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793603)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793603)Termination reason: Instruction limit
% 10.75/2.50 % (3793603)Termination phase: Saturation
% 10.75/2.50 % (3793603)Time elapsed: 0.144 s
% 10.75/2.50 % (3793603)Peak memory usage: 89 MB
% 10.75/2.50 % (3793603)Instructions burned: 157 (million)
% 10.75/2.50 % (3793605)Instruction limit reached!
% 10.75/2.50 % (3793605)------------------------------
% 10.75/2.50 % (3793605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793605)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793605)Termination reason: Instruction limit
% 10.75/2.50 % (3793605)Termination phase: Saturation
% 10.75/2.50 % (3793605)Time elapsed: 0.112 s
% 10.75/2.50 % (3793605)Peak memory usage: 89 MB
% 10.75/2.50 % (3793605)Instructions burned: 106 (million)
% 10.75/2.50 % (3793581)First to succeed.
% 10.75/2.50 % (3793581)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3793575"
% 10.75/2.50 % (3793610)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1513707914:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 10.75/2.50 % (3793611)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3965089748:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 10.75/2.50 % (3793612)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=585686247:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 10.75/2.50 % (3793610)Instruction limit reached!
% 10.75/2.50 % (3793610)------------------------------
% 10.75/2.50 % (3793610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.50 % (3793610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.50 % (3793610)CaDiCaL version: 2.1.3
% 10.75/2.50 % (3793610)Termination reason: Instruction limit
% 10.75/2.50 % (3793610)Termination phase: Saturation
% 10.75/2.50 % (3793610)Time elapsed: 0.100 s
% 10.75/2.50 % (3793610)Peak memory usage: 88 MB
% 10.75/2.50 % (3793610)Instructions burned: 107 (million)
% 10.75/2.50 % SZS status Satisfiable for theBenchmark
% 10.75/2.50 % SZS output start Saturation.
% See solution above
% 12.56/2.71 % SZS output start Definitions and Model Updates.
% 12.56/2.71 % SZS output end Definitions and Model Updates.
% 12.56/2.71 % (3793581)------------------------------
% 12.56/2.71 % (3793581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.56/2.71 % (3793581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.56/2.72 % (3793581)CaDiCaL version: 2.1.3
% 12.56/2.72 % (3793581)Termination reason: Satisfiable
% 12.56/2.72 % (3793581)Time elapsed: 1.243 s
% 12.56/2.72 % (3793581)Peak memory usage: 137 MB
% 12.56/2.72 % (3793581)Instructions burned: 2229 (million)
% 12.56/2.72 % (3793581)------------------------------
% 12.56/2.72 % (3793581)------------------------------
% 12.56/2.72 % (3793575)Success in time 1.664 s
% 12.56/2.72 % Vampire exiting
%------------------------------------------------------------------------------