%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CAT001-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 : n008.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:32 AM UTC 2026
% Result : Satisfiable 4.92s 1.47s
% Output : Saturation 6.18s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u22,negated_conjecture,
h != g ).
cnf(u27,hypothesis,
compose(a,h) = compose(a,g) ).
cnf(u32,hypothesis,
codomain(a) = domain(g) ).
cnf(u37,hypothesis,
codomain(a) = domain(h) ).
cnf(u42,hypothesis,
codomain(a) = domain(b) ).
cnf(u49,hypothesis,
domain(h) = domain(g) ).
cnf(u58,hypothesis,
domain(b) = domain(g) ).
cnf(u63,hypothesis,
domain(b) = domain(h) ).
cnf(u82,hypothesis,
h = compose(domain(b),h) ).
cnf(u88,hypothesis,
g = compose(domain(b),g) ).
cnf(u100,hypothesis,
a = compose(a,domain(b)) ).
cnf(u182,hypothesis,
domain(compose(a,b)) = domain(a) ).
cnf(u189,hypothesis,
domain(a) = domain(compose(a,h)) ).
cnf(u209,hypothesis,
domain(b) != domain(a) ).
cnf(u214,hypothesis,
compose(a,b) = compose(domain(a),compose(a,b)) ).
cnf(u228,hypothesis,
codomain(compose(a,b)) = codomain(b) ).
cnf(u235,hypothesis,
codomain(h) = codomain(compose(a,h)) ).
cnf(u243,hypothesis,
codomain(compose(a,h)) = codomain(g) ).
cnf(u250,hypothesis,
codomain(h) = codomain(g) ).
cnf(u264,hypothesis,
g = compose(g,codomain(h)) ).
cnf(u339,hypothesis,
compose(a,h) = compose(domain(a),compose(a,h)) ).
cnf(u374,hypothesis,
compose(a,b) = compose(compose(a,b),codomain(b)) ).
cnf(u389,hypothesis,
domain(a) != codomain(h) ).
cnf(u399,hypothesis,
domain(a) != codomain(b) ).
cnf(u447,hypothesis,
compose(a,h) = compose(compose(a,h),codomain(h)) ).
cnf(u1548,hypothesis,
domain(b) != codomain(h) ).
cnf(u1563,hypothesis,
domain(b) != codomain(b) ).
cnf(u1646,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(h)
| compose(g,compose(X1,codomain(X0))) = compose(compose(g,X1),codomain(X0)) ) ).
cnf(u812,axiom,
( codomain(X0) != codomain(X1)
| compose(X1,codomain(X0)) = compose(compose(X1,codomain(X0)),codomain(X0)) ) ).
cnf(u367,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) = codomain(compose(compose(a,b),codomain(X0))) ) ).
cnf(u819,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != domain(b)
| compose(domain(X1),compose(a,domain(X0))) = compose(compose(domain(X1),a),domain(X0)) ) ).
cnf(u3247,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),domain(X0)) = compose(domain(a),compose(compose(a,b),domain(X0))) ) ).
cnf(u3230,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),domain(X0)) = compose(domain(a),compose(compose(a,h),domain(X0))) ) ).
cnf(u810,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,h)) = compose(compose(X0,compose(a,h)),codomain(h)) ) ).
cnf(u988,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(u923,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(X2)
| compose(X1,compose(codomain(X0),domain(X2))) = compose(compose(X1,codomain(X0)),domain(X2)) ) ).
cnf(u813,axiom,
( domain(X0) != codomain(X1)
| compose(X1,domain(X0)) = compose(compose(X1,domain(X0)),domain(X0)) ) ).
cnf(u521,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) = codomain(compose(g,domain(X0))) ) ).
cnf(u3073,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) != domain(a)
| compose(compose(a,b),compose(domain(X0),compose(a,h))) = compose(compose(compose(a,b),domain(X0)),compose(a,h)) ) ).
cnf(u986,axiom,
( domain(X1) != codomain(X2)
| domain(X0) != domain(X1)
| compose(domain(X0),compose(domain(X1),codomain(X2))) = compose(compose(domain(X0),domain(X1)),codomain(X2)) ) ).
cnf(u138,axiom,
( codomain(X0) != domain(X1)
| codomain(X1) = codomain(compose(codomain(X0),X1)) ) ).
cnf(u442,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != codomain(h)
| compose(X1,compose(compose(a,h),X0)) = compose(compose(X1,compose(a,h)),X0) ) ).
cnf(u109,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) = domain(compose(X1,codomain(X0))) ) ).
cnf(u1585,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),domain(X0)) = compose(a,compose(g,domain(X0))) ) ).
cnf(u2710,hypothesis,
( domain(X0) != codomain(h)
| compose(g,domain(X0)) = compose(domain(b),compose(g,domain(X0))) ) ).
cnf(u1234,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,b)) = compose(X0,compose(codomain(X0),compose(a,b))) ) ).
cnf(u1693,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(codomain(X0),compose(codomain(X0),compose(a,b))) ) ).
cnf(u3047,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(a)
| compose(a,compose(codomain(X0),compose(a,h))) = compose(compose(a,codomain(X0)),compose(a,h)) ) ).
cnf(u913,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(u172,hypothesis,
( codomain(X0) != domain(b)
| domain(a) = domain(compose(a,codomain(X0))) ) ).
cnf(u624,hypothesis,
( codomain(X0) != domain(a)
| codomain(b) = codomain(compose(codomain(X0),compose(a,b))) ) ).
cnf(u1235,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,h)) = compose(X0,compose(codomain(X0),compose(a,h))) ) ).
cnf(u1694,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,h)) = compose(codomain(X0),compose(codomain(X0),compose(a,h))) ) ).
cnf(u1715,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),domain(X0)) = compose(compose(a,h),compose(codomain(h),domain(X0))) ) ).
cnf(u940,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(u3083,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,h)) = compose(compose(X0,domain(a)),compose(a,h)) ) ).
cnf(u1358,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),X1) = compose(compose(codomain(X0),domain(X1)),X1) ) ).
cnf(u638,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) = domain(compose(codomain(X0),compose(a,h))) ) ).
cnf(u1335,axiom,
( codomain(X0) != codomain(X1)
| compose(codomain(X0),codomain(X1)) = compose(codomain(X0),compose(codomain(X0),codomain(X1))) ) ).
cnf(u1705,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(u591,hypothesis,
( domain(X0) != codomain(b)
| domain(a) = domain(compose(compose(a,b),domain(X0))) ) ).
cnf(star_property,axiom,
( codomain(X1) != domain(X2)
| codomain(X0) != domain(X1)
| compose(X0,compose(X1,X2)) = compose(compose(X0,X1),X2) ) ).
cnf(u918,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != codomain(h)
| compose(g,compose(X0,domain(X1))) = compose(compose(g,X0),domain(X1)) ) ).
cnf(u317,hypothesis,
( domain(X0) != domain(a)
| codomain(b) = codomain(compose(domain(X0),compose(a,b))) ) ).
cnf(u990,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(b)
| compose(a,compose(domain(X0),codomain(X1))) = compose(compose(a,domain(X0)),codomain(X1)) ) ).
cnf(u142,axiom,
( codomain(X0) != domain(X1)
| codomain(X0) = domain(compose(codomain(X0),X1)) ) ).
cnf(u1618,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(b)
| compose(a,compose(X1,codomain(X0))) = compose(compose(a,X1),codomain(X0)) ) ).
cnf(u421,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(u1227,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),X0) = compose(compose(a,h),compose(codomain(h),X0)) ) ).
cnf(u129,axiom,
( domain(X0) != codomain(X1)
| domain(X0) = codomain(compose(X1,domain(X0))) ) ).
cnf(u914,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != codomain(h)
| compose(compose(a,h),compose(X0,domain(X1))) = compose(compose(compose(a,h),X0),domain(X1)) ) ).
cnf(u1297,axiom,
( domain(X0) != codomain(X1)
| compose(codomain(X1),domain(X0)) = compose(compose(codomain(X1),domain(X0)),domain(X0)) ) ).
cnf(u2041,hypothesis,
( codomain(X1) != domain(b)
| domain(X0) != codomain(h)
| compose(codomain(X1),compose(g,domain(X0))) = compose(compose(codomain(X1),g),domain(X0)) ) ).
cnf(u1795,hypothesis,
( domain(X0) != domain(b)
| compose(a,domain(X0)) = compose(domain(a),compose(a,domain(X0))) ) ).
cnf(u1737,hypothesis,
( domain(X0) != codomain(X1)
| domain(X0) != domain(a)
| compose(X1,compose(domain(X0),compose(a,h))) = compose(compose(X1,domain(X0)),compose(a,h)) ) ).
cnf(u148,axiom,
( domain(X1) != codomain(X2)
| domain(X0) != codomain(X1)
| compose(X2,compose(X1,domain(X0))) = compose(compose(X2,X1),domain(X0)) ) ).
cnf(u3021,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(u1786,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != domain(b)
| compose(codomain(X0),compose(a,domain(X1))) = compose(compose(codomain(X0),a),domain(X1)) ) ).
cnf(u804,hypothesis,
( domain(X0) != domain(b)
| compose(a,X0) = compose(compose(a,X0),codomain(X0)) ) ).
cnf(u989,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != codomain(X1)
| compose(compose(a,h),compose(domain(X0),codomain(X1))) = compose(compose(compose(a,h),domain(X0)),codomain(X1)) ) ).
cnf(u1691,axiom,
( domain(X0) != codomain(X1)
| compose(codomain(X1),domain(X0)) = compose(codomain(X1),compose(codomain(X1),domain(X0))) ) ).
cnf(u1917,hypothesis,
( domain(X0) != domain(b)
| compose(a,compose(domain(X0),domain(b))) = compose(compose(a,domain(X0)),domain(b)) ) ).
cnf(u1024,axiom,
( domain(X0) != domain(X1)
| compose(domain(X0),X1) = compose(compose(domain(X0),domain(X1)),X1) ) ).
cnf(u1653,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(X1)
| compose(g,compose(domain(X0),domain(X1))) = compose(compose(g,domain(X0)),domain(X1)) ) ).
cnf(u802,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),X0) = compose(compose(compose(a,b),X0),codomain(X0)) ) ).
cnf(u1534,hypothesis,
( codomain(X0) != domain(b)
| domain(X1) != codomain(h)
| compose(codomain(X0),compose(g,X1)) = compose(compose(codomain(X0),g),X1) ) ).
cnf(u915,hypothesis,
( codomain(X0) != domain(X1)
| domain(X0) != domain(b)
| compose(a,compose(X0,domain(X1))) = compose(compose(a,X0),domain(X1)) ) ).
cnf(u1326,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),domain(X0)) = compose(compose(compose(a,h),domain(X0)),domain(X0)) ) ).
cnf(u2232,hypothesis,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(h)
| compose(compose(a,h),compose(X1,codomain(X0))) = compose(compose(compose(a,h),X1),codomain(X0)) ) ).
cnf(u1213,hypothesis,
( domain(X0) != domain(b)
| compose(a,domain(X0)) = compose(a,compose(domain(b),domain(X0))) ) ).
cnf(u2090,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(u966,axiom,
( codomain(X1) != codomain(X2)
| codomain(X0) != codomain(X1)
| compose(codomain(X0),compose(codomain(X1),codomain(X2))) = compose(compose(codomain(X0),codomain(X1)),codomain(X2)) ) ).
cnf(u1279,axiom,
( codomain(X0) != domain(X1)
| compose(domain(X1),codomain(X0)) = compose(compose(domain(X1),codomain(X0)),codomain(X0)) ) ).
cnf(u422,axiom,
( codomain(X0) != codomain(X2)
| codomain(X0) != codomain(X1)
| compose(X2,compose(codomain(X0),codomain(X1))) = compose(compose(X2,codomain(X0)),codomain(X1)) ) ).
cnf(u2039,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(u1666,hypothesis,
( domain(X0) != domain(b)
| compose(domain(X0),h) = compose(domain(X0),compose(domain(X0),h)) ) ).
cnf(u73,axiom,
codomain(X0) = codomain(codomain(X0)) ).
cnf(u1231,hypothesis,
( domain(X0) != codomain(h)
| compose(g,X0) = compose(g,compose(codomain(h),X0)) ) ).
cnf(u1276,hypothesis,
( domain(X0) != domain(b)
| compose(domain(X0),g) = compose(compose(domain(X0),g),codomain(h)) ) ).
cnf(u3078,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(a)
| compose(g,compose(domain(X0),compose(a,h))) = compose(compose(g,domain(X0)),compose(a,h)) ) ).
cnf(u1628,hypothesis,
( codomain(X0) != domain(b)
| compose(codomain(X0),g) = compose(compose(codomain(X0),domain(b)),g) ) ).
cnf(u1226,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),X0) = compose(compose(a,b),compose(codomain(b),X0)) ) ).
cnf(u3045,hypothesis,
( codomain(X0) != codomain(b)
| codomain(X0) != domain(a)
| compose(compose(a,b),compose(codomain(X0),compose(a,h))) = compose(compose(compose(a,b),codomain(X0)),compose(a,h)) ) ).
cnf(u440,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != codomain(h)
| compose(X1,compose(compose(a,h),codomain(X0))) = compose(compose(X1,compose(a,h)),codomain(X0)) ) ).
cnf(u196,hypothesis,
( codomain(X0) != domain(a)
| domain(X0) = domain(compose(X0,compose(a,b))) ) ).
cnf(u335,hypothesis,
( codomain(X0) != domain(a)
| codomain(h) = codomain(compose(X0,compose(a,h))) ) ).
cnf(u159,hypothesis,
( compose(a,b) != compose(X0,compose(a,b))
| codomain(X0) != domain(compose(a,b))
| domain(compose(a,b)) = X0 ) ).
cnf(u602,hypothesis,
( domain(X0) != codomain(b)
| domain(X0) = codomain(compose(compose(a,b),domain(X0))) ) ).
cnf(u2037,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != codomain(h)
| compose(codomain(X1),compose(compose(a,h),domain(X0))) = compose(compose(codomain(X1),compose(a,h)),domain(X0)) ) ).
cnf(u1019,hypothesis,
( domain(X0) != domain(a)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),compose(a,h))) = compose(compose(domain(X1),domain(X0)),compose(a,h)) ) ).
cnf(u2132,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(a)
| compose(codomain(X1),compose(codomain(X0),compose(a,h))) = compose(compose(codomain(X1),codomain(X0)),compose(a,h)) ) ).
cnf(u294,axiom,
( domain(X0) != domain(X1)
| domain(X1) = domain(compose(domain(X1),domain(X0))) ) ).
cnf(u941,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(X1)
| compose(compose(a,h),compose(codomain(X0),X1)) = compose(compose(compose(a,h),codomain(X0)),X1) ) ).
cnf(u1750,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,h)) = compose(compose(codomain(X0),domain(a)),compose(a,h)) ) ).
cnf(u3006,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(a)
| compose(compose(a,h),compose(codomain(X0),compose(a,b))) = compose(compose(compose(a,h),codomain(X0)),compose(a,b)) ) ).
cnf(u423,axiom,
( domain(X0) != codomain(X2)
| domain(X0) != codomain(X1)
| compose(X2,compose(domain(X0),codomain(X1))) = compose(compose(X2,domain(X0)),codomain(X1)) ) ).
cnf(domain_composition,axiom,
compose(domain(X0),X0) = X0 ).
cnf(u969,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),codomain(X1))) = compose(compose(a,codomain(X0)),codomain(X1)) ) ).
cnf(u77,axiom,
codomain(X0) = compose(codomain(X0),codomain(X0)) ).
cnf(u457,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(a,compose(domain(X0),X1)) = compose(compose(a,domain(X0)),X1) ) ).
cnf(u3007,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(u8,axiom,
( codomain(X0) != domain(X1)
| domain(X0) = domain(compose(X0,X1)) ) ).
cnf(u319,axiom,
( domain(X0) != domain(X1)
| domain(X0) = codomain(compose(domain(X1),domain(X0))) ) ).
cnf(u1435,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,h)) = compose(compose(codomain(X0),a),g) ) ).
cnf(u370,hypothesis,
( domain(X0) != codomain(b)
| domain(a) = domain(compose(compose(a,b),X0)) ) ).
cnf(u1521,hypothesis,
( codomain(X0) != domain(b)
| compose(codomain(X0),g) = compose(compose(codomain(X0),g),codomain(h)) ) ).
cnf(u592,axiom,
( codomain(X0) != domain(X1)
| codomain(X0) = domain(compose(codomain(X0),domain(X1))) ) ).
cnf(u3027,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(a)
| compose(g,compose(domain(X0),compose(a,b))) = compose(compose(g,domain(X0)),compose(a,b)) ) ).
cnf(u2711,hypothesis,
( codomain(X0) != codomain(h)
| compose(g,codomain(X0)) = compose(domain(b),compose(g,codomain(X0))) ) ).
cnf(u1749,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(compose(codomain(X0),domain(a)),compose(a,b)) ) ).
cnf(u898,hypothesis,
( domain(X0) != domain(b)
| compose(a,X0) = compose(a,compose(domain(b),X0)) ) ).
cnf(u2112,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) != domain(X1)
| compose(domain(X1),compose(codomain(X0),compose(a,h))) = compose(compose(domain(X1),codomain(X0)),compose(a,h)) ) ).
cnf(u285,axiom,
( domain(X0) != codomain(X1)
| domain(X0) = domain(compose(domain(X0),codomain(X1))) ) ).
cnf(u238,hypothesis,
( domain(X0) != domain(b)
| domain(X0) = codomain(compose(a,domain(X0))) ) ).
cnf(u1714,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),domain(X0)) = compose(compose(a,b),compose(codomain(b),domain(X0))) ) ).
cnf(u2063,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(u1202,hypothesis,
( codomain(X0) != domain(b)
| compose(a,codomain(X0)) = compose(compose(a,codomain(X0)),codomain(X0)) ) ).
cnf(u3022,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(u1624,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(a,compose(codomain(X0),domain(X1))) = compose(compose(a,codomain(X0)),domain(X1)) ) ).
cnf(u316,hypothesis,
( domain(X0) != domain(b)
| codomain(h) = codomain(compose(domain(X0),g)) ) ).
cnf(u1411,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,h)) = compose(compose(codomain(X0),a),h) ) ).
cnf(u1203,hypothesis,
( domain(X0) != domain(b)
| compose(a,domain(X0)) = compose(compose(a,domain(X0)),domain(X0)) ) ).
cnf(u360,hypothesis,
( domain(X0) != codomain(b)
| codomain(X0) = codomain(compose(compose(a,b),X0)) ) ).
cnf(u828,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,h)) = compose(compose(domain(X0),a),h) ) ).
cnf(u1497,hypothesis,
( codomain(X0) != domain(b)
| compose(codomain(X0),h) = compose(compose(codomain(X0),h),codomain(h)) ) ).
cnf(u128,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) = codomain(compose(X1,codomain(X0))) ) ).
cnf(u867,hypothesis,
( codomain(X1) != domain(b)
| codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,codomain(X1))) = compose(compose(codomain(X0),a),codomain(X1)) ) ).
cnf(u348,axiom,
( codomain(X0) != codomain(X1)
| codomain(X1) = codomain(compose(codomain(X0),codomain(X1))) ) ).
cnf(u1325,hypothesis,
( domain(X0) != codomain(b)
| compose(compose(a,b),domain(X0)) = compose(compose(compose(a,b),domain(X0)),domain(X0)) ) ).
cnf(u826,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(compose(domain(X0),a),b) ) ).
cnf(u151,axiom,
( domain(X0) != codomain(X2)
| domain(X0) != domain(X1)
| compose(X2,compose(domain(X0),X1)) = compose(compose(X2,domain(X0)),X1) ) ).
cnf(u603,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) = codomain(compose(compose(a,h),domain(X0))) ) ).
cnf(u1224,axiom,
( domain(X0) != domain(X1)
| compose(domain(X0),X1) = compose(domain(X0),compose(domain(X0),X1)) ) ).
cnf(u2040,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(u110,axiom,
( domain(X0) != domain(X1)
| domain(X0) = domain(compose(domain(X0),X1)) ) ).
cnf(u1822,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),a) = compose(compose(codomain(X0),a),domain(b)) ) ).
cnf(u945,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(X1)
| compose(g,compose(codomain(X0),X1)) = compose(compose(g,codomain(X0)),X1) ) ).
cnf(u330,hypothesis,
( domain(X0) != domain(a)
| domain(X0) = domain(compose(domain(X0),compose(a,h))) ) ).
cnf(u2009,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != codomain(b)
| compose(domain(X1),compose(compose(a,b),domain(X0))) = compose(compose(domain(X1),compose(a,b)),domain(X0)) ) ).
cnf(u2131,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(a)
| compose(codomain(X1),compose(codomain(X0),compose(a,b))) = compose(compose(codomain(X1),codomain(X0)),compose(a,b)) ) ).
cnf(u125,axiom,
( domain(X0) != domain(X1)
| codomain(X1) = codomain(compose(domain(X0),X1)) ) ).
cnf(u1652,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(X1)
| compose(g,compose(codomain(X0),domain(X1))) = compose(compose(g,codomain(X0)),domain(X1)) ) ).
cnf(u2012,hypothesis,
( domain(X1) != domain(b)
| domain(X0) != codomain(h)
| compose(domain(X1),compose(g,domain(X0))) = compose(compose(domain(X1),g),domain(X0)) ) ).
cnf(u1369,hypothesis,
( domain(X0) != domain(b)
| compose(domain(X0),g) = compose(compose(domain(X0),domain(b)),g) ) ).
cnf(u1932,hypothesis,
( codomain(X0) != domain(b)
| compose(codomain(X0),h) = compose(codomain(X0),compose(codomain(X0),h)) ) ).
cnf(u540,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) = domain(compose(codomain(X0),g)) ) ).
cnf(u3046,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(a)
| compose(compose(a,h),compose(codomain(X0),compose(a,h))) = compose(compose(compose(a,h),codomain(X0)),compose(a,h)) ) ).
cnf(u590,hypothesis,
( domain(X0) != codomain(h)
| domain(a) = domain(compose(compose(a,h),domain(X0))) ) ).
cnf(u811,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,b)) = compose(compose(X0,compose(a,b)),codomain(b)) ) ).
cnf(u2210,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(u1736,hypothesis,
( codomain(X0) != codomain(X1)
| codomain(X0) != domain(a)
| compose(X1,compose(codomain(X0),compose(a,h))) = compose(compose(X1,codomain(X0)),compose(a,h)) ) ).
cnf(u535,hypothesis,
( domain(X0) != codomain(h)
| domain(b) = domain(compose(g,domain(X0))) ) ).
cnf(u830,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,h)) = compose(compose(domain(X0),a),g) ) ).
cnf(u1270,hypothesis,
( domain(X0) != domain(b)
| compose(domain(X0),h) = compose(compose(domain(X0),h),codomain(h)) ) ).
cnf(u318,axiom,
( codomain(X0) != domain(X1)
| codomain(X0) = codomain(compose(domain(X1),codomain(X0))) ) ).
cnf(u987,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(u889,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(a,compose(codomain(X0),X1)) = compose(compose(a,codomain(X0)),X1) ) ).
cnf(u553,hypothesis,
( codomain(X0) != domain(b)
| codomain(h) = codomain(compose(codomain(X0),h)) ) ).
cnf(u1752,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(u377,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != domain(b)
| compose(codomain(X0),compose(a,X1)) = compose(compose(codomain(X0),a),X1) ) ).
cnf(u2111,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) != domain(X1)
| compose(domain(X1),compose(codomain(X0),compose(a,b))) = compose(compose(domain(X1),codomain(X0)),compose(a,b)) ) ).
cnf(u800,axiom,
( domain(X0) != domain(X1)
| compose(domain(X0),X1) = compose(compose(domain(X0),X1),codomain(X1)) ) ).
cnf(u1278,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(compose(domain(X0),compose(a,b)),codomain(b)) ) ).
cnf(u3032,hypothesis,
( codomain(X0) != domain(a)
| compose(X0,compose(a,b)) = compose(compose(X0,domain(a)),compose(a,b)) ) ).
cnf(u2709,hypothesis,
( domain(X0) != codomain(h)
| compose(g,X0) = compose(domain(b),compose(g,X0)) ) ).
cnf(u2160,hypothesis,
( codomain(X1) != codomain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,h),codomain(X1))) = compose(compose(domain(X0),compose(a,h)),codomain(X1)) ) ).
cnf(u122,hypothesis,
( domain(X0) != domain(b)
| codomain(X0) = codomain(compose(a,X0)) ) ).
cnf(u3024,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(u523,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) = domain(compose(codomain(X0),h)) ) ).
cnf(u4,axiom,
codomain(X0) = domain(codomain(X0)) ).
cnf(u352,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) = codomain(compose(g,codomain(X0))) ) ).
cnf(u820,hypothesis,
( codomain(X0) != domain(b)
| domain(X1) != domain(a)
| compose(domain(X1),compose(a,codomain(X0))) = compose(compose(domain(X1),a),codomain(X0)) ) ).
cnf(u412,hypothesis,
( codomain(X1) != domain(a)
| codomain(X0) != domain(b)
| compose(X1,compose(a,codomain(X0))) = compose(compose(X1,a),codomain(X0)) ) ).
cnf(u456,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(X1)
| compose(compose(a,h),compose(domain(X0),X1)) = compose(compose(compose(a,h),domain(X0)),X1) ) ).
cnf(u924,axiom,
( domain(X0) != codomain(X1)
| domain(X0) != domain(X2)
| compose(X1,compose(domain(X0),domain(X2))) = compose(compose(X1,domain(X0)),domain(X2)) ) ).
cnf(u1214,hypothesis,
( codomain(X0) != domain(b)
| compose(a,codomain(X0)) = compose(a,compose(domain(b),codomain(X0))) ) ).
cnf(u1552,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),X0) = compose(a,compose(g,X0)) ) ).
cnf(u968,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != codomain(X1)
| compose(compose(a,h),compose(codomain(X0),codomain(X1))) = compose(compose(compose(a,h),codomain(X0)),codomain(X1)) ) ).
cnf(u939,axiom,
( codomain(X1) != domain(X2)
| codomain(X0) != codomain(X1)
| compose(codomain(X0),compose(codomain(X1),X2)) = compose(compose(codomain(X0),codomain(X1)),X2) ) ).
cnf(u2,axiom,
domain(X0) = codomain(domain(X0)) ).
cnf(u3251,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(a,b),codomain(X0)) = compose(domain(a),compose(compose(a,b),codomain(X0))) ) ).
cnf(u922,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(u3074,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(a)
| compose(compose(a,h),compose(domain(X0),compose(a,h))) = compose(compose(compose(a,h),domain(X0)),compose(a,h)) ) ).
cnf(u171,hypothesis,
( domain(X0) != domain(b)
| domain(a) = domain(compose(a,domain(X0))) ) ).
cnf(u1799,hypothesis,
( codomain(X0) != domain(b)
| compose(a,codomain(X0)) = compose(domain(a),compose(a,codomain(X0))) ) ).
cnf(u3072,hypothesis,
( codomain(X0) != domain(X1)
| domain(X1) != domain(a)
| compose(codomain(X0),compose(domain(X1),compose(a,h))) = compose(compose(codomain(X0),domain(X1)),compose(a,h)) ) ).
cnf(u1751,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(u149,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(X2)
| compose(X2,compose(X1,codomain(X0))) = compose(compose(X2,X1),codomain(X0)) ) ).
cnf(u1625,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(a,compose(domain(X0),domain(X1))) = compose(compose(a,domain(X0)),domain(X1)) ) ).
cnf(u1242,hypothesis,
( domain(X0) != codomain(h)
| compose(g,domain(X0)) = compose(g,compose(codomain(h),domain(X0))) ) ).
cnf(u993,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != codomain(X1)
| compose(g,compose(domain(X0),codomain(X1))) = compose(compose(g,domain(X0)),codomain(X1)) ) ).
cnf(u2142,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(u284,axiom,
( codomain(X0) != codomain(X1)
| codomain(X0) = domain(compose(codomain(X0),codomain(X1))) ) ).
cnf(u3023,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(a)
| compose(compose(a,h),compose(domain(X0),compose(a,b))) = compose(compose(compose(a,h),domain(X0)),compose(a,b)) ) ).
cnf(u1971,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(domain(X1),compose(codomain(X0),g)) = compose(compose(domain(X1),codomain(X0)),g) ) ).
cnf(u2038,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(u1766,hypothesis,
( domain(X1) != codomain(h)
| domain(X0) != domain(a)
| compose(domain(X0),compose(compose(a,h),X1)) = compose(compose(domain(X0),compose(a,h)),X1) ) ).
cnf(u323,hypothesis,
( codomain(X0) != domain(a)
| domain(X0) = domain(compose(X0,compose(a,h))) ) ).
cnf(u1294,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,h)) = compose(compose(codomain(X0),compose(a,h)),codomain(h)) ) ).
cnf(u803,hypothesis,
( domain(X0) != codomain(h)
| compose(compose(a,h),X0) = compose(compose(compose(a,h),X0),codomain(X0)) ) ).
cnf(u460,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(X1)
| compose(g,compose(domain(X0),X1)) = compose(compose(g,domain(X0)),X1) ) ).
cnf(u912,axiom,
( codomain(X1) != domain(X2)
| codomain(X0) != domain(X1)
| compose(codomain(X0),compose(X1,domain(X2))) = compose(compose(codomain(X0),X1),domain(X2)) ) ).
cnf(u1366,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(compose(domain(X0),domain(a)),compose(a,b)) ) ).
cnf(u1309,hypothesis,
( codomain(X0) != codomain(h)
| compose(compose(a,h),codomain(X0)) = compose(compose(compose(a,h),codomain(X0)),codomain(X0)) ) ).
cnf(u972,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != codomain(X1)
| compose(g,compose(codomain(X0),codomain(X1))) = compose(compose(g,codomain(X0)),codomain(X1)) ) ).
cnf(u1277,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,h)) = compose(compose(domain(X0),compose(a,h)),codomain(h)) ) ).
cnf(u1600,hypothesis,
( codomain(X0) != domain(b)
| compose(codomain(X0),h) = compose(compose(codomain(X0),domain(b)),h) ) ).
cnf(codomain_composition,axiom,
compose(X0,codomain(X0)) = X0 ).
cnf(u967,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(u297,hypothesis,
( domain(X0) != domain(b)
| domain(X0) = domain(compose(domain(X0),h)) ) ).
cnf(u2008,hypothesis,
( domain(X1) != domain(a)
| domain(X0) != codomain(h)
| compose(domain(X1),compose(compose(a,h),domain(X0))) = compose(compose(domain(X1),compose(a,h)),domain(X0)) ) ).
cnf(u198,hypothesis,
( codomain(X0) != domain(a)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(a,b))) = compose(compose(X1,X0),compose(a,b)) ) ).
cnf(u369,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != codomain(b)
| compose(X1,compose(compose(a,b),X0)) = compose(compose(X1,compose(a,b)),X0) ) ).
cnf(u3075,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(a)
| compose(a,compose(domain(X0),compose(a,h))) = compose(compose(a,domain(X0)),compose(a,h)) ) ).
cnf(u94,axiom,
domain(X0) = compose(domain(X0),domain(X0)) ).
cnf(u429,hypothesis,
( domain(X0) != codomain(h)
| codomain(X0) = codomain(compose(compose(a,h),X0)) ) ).
cnf(u1296,axiom,
( codomain(X0) != codomain(X1)
| compose(codomain(X1),codomain(X0)) = compose(compose(codomain(X1),codomain(X0)),codomain(X0)) ) ).
cnf(u197,hypothesis,
( codomain(X0) != domain(a)
| codomain(compose(X0,compose(a,b))) = codomain(compose(a,b)) ) ).
cnf(u2031,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) != codomain(X2)
| compose(codomain(X2),compose(X1,codomain(X0))) = compose(compose(codomain(X2),X1),codomain(X0)) ) ).
cnf(u1334,axiom,
( domain(X0) != codomain(X1)
| compose(domain(X0),codomain(X1)) = compose(domain(X0),compose(domain(X0),codomain(X1))) ) ).
cnf(u2161,hypothesis,
( codomain(X1) != codomain(h)
| codomain(X0) != domain(a)
| compose(codomain(X0),compose(compose(a,h),codomain(X1))) = compose(compose(codomain(X0),compose(a,h)),codomain(X1)) ) ).
cnf(u267,hypothesis,
( domain(X0) != codomain(h)
| domain(b) = domain(compose(g,X0)) ) ).
cnf(u119,axiom,
( domain(X0) != codomain(X1)
| domain(X1) = domain(compose(X1,domain(X0))) ) ).
cnf(u807,hypothesis,
( domain(X0) != codomain(h)
| compose(g,X0) = compose(compose(g,X0),codomain(X0)) ) ).
cnf(u1016,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(u1368,hypothesis,
( domain(X0) != domain(b)
| compose(domain(X0),h) = compose(compose(domain(X0),domain(b)),h) ) ).
cnf(u286,hypothesis,
( codomain(X0) != codomain(h)
| domain(b) = domain(compose(g,codomain(X0))) ) ).
cnf(u298,hypothesis,
( domain(X0) != domain(b)
| domain(X0) = domain(compose(domain(X0),g)) ) ).
cnf(u637,hypothesis,
( codomain(X0) != domain(a)
| codomain(X0) = domain(compose(codomain(X0),compose(a,b))) ) ).
cnf(u1567,hypothesis,
( codomain(X1) != codomain(h)
| domain(X0) != domain(b)
| compose(domain(X0),compose(g,codomain(X1))) = compose(compose(domain(X0),g),codomain(X1)) ) ).
cnf(u974,axiom,
( codomain(X0) != codomain(X1)
| compose(X0,compose(codomain(X0),codomain(X1))) = compose(X0,codomain(X1)) ) ).
cnf(codomain_domain2,axiom,
( codomain(X0) != domain(X1)
| codomain(compose(X0,X1)) = codomain(X1) ) ).
cnf(u2091,hypothesis,
( domain(X0) != codomain(h)
| domain(X0) != domain(X1)
| compose(compose(a,h),compose(domain(X0),domain(X1))) = compose(compose(compose(a,h),domain(X0)),domain(X1)) ) ).
cnf(u455,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(u1212,hypothesis,
( domain(X0) != codomain(h)
| compose(g,domain(X0)) = compose(compose(g,domain(X0)),domain(X0)) ) ).
cnf(u1337,hypothesis,
( codomain(X0) != codomain(h)
| compose(compose(a,h),codomain(X0)) = compose(compose(a,h),compose(codomain(h),codomain(X0))) ) ).
cnf(u2010,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(u1665,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,h)) = compose(domain(X0),compose(domain(X0),compose(a,h))) ) ).
cnf(u1336,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(a,b),codomain(X0)) = compose(compose(a,b),compose(codomain(b),codomain(X0))) ) ).
cnf(u72,axiom,
domain(X0) = domain(domain(X0)) ).
cnf(u376,hypothesis,
( domain(X1) != domain(b)
| domain(X0) != domain(a)
| compose(domain(X0),compose(a,X1)) = compose(compose(domain(X0),a),X1) ) ).
cnf(u921,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != codomain(h)
| compose(X0,compose(compose(a,h),domain(X1))) = compose(compose(X0,compose(a,h)),domain(X1)) ) ).
cnf(u436,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) = codomain(compose(compose(a,h),codomain(X0))) ) ).
cnf(u311,hypothesis,
( domain(X0) != domain(b)
| codomain(h) = codomain(compose(domain(X0),h)) ) ).
cnf(u1958,hypothesis,
( codomain(X0) != domain(b)
| compose(codomain(X0),g) = compose(codomain(X0),compose(codomain(X0),g)) ) ).
cnf(u443,hypothesis,
( domain(X0) != codomain(h)
| domain(a) = domain(compose(compose(a,h),X0)) ) ).
cnf(u1020,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),h)) = compose(compose(domain(X1),domain(X0)),h) ) ).
cnf(u1533,hypothesis,
( domain(X1) != codomain(h)
| domain(X0) != domain(b)
| compose(domain(X0),compose(g,X1)) = compose(compose(domain(X0),g),X1) ) ).
cnf(u1367,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,h)) = compose(compose(domain(X0),domain(a)),compose(a,h)) ) ).
cnf(u1018,hypothesis,
( domain(X0) != domain(a)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),compose(a,b))) = compose(compose(domain(X1),domain(X0)),compose(a,b)) ) ).
cnf(u334,hypothesis,
( domain(X0) != domain(a)
| codomain(h) = codomain(compose(domain(X0),compose(a,h))) ) ).
cnf(u1021,hypothesis,
( domain(X0) != domain(b)
| domain(X0) != domain(X1)
| compose(domain(X1),compose(domain(X0),g)) = compose(compose(domain(X1),domain(X0)),g) ) ).
cnf(u1706,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(u3010,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),compose(a,b))) = compose(compose(g,codomain(X0)),compose(a,b)) ) ).
cnf(u965,axiom,
( codomain(X1) != codomain(X2)
| domain(X0) != codomain(X1)
| compose(domain(X0),compose(codomain(X1),codomain(X2))) = compose(compose(domain(X0),codomain(X1)),codomain(X2)) ) ).
cnf(u453,axiom,
( domain(X1) != domain(X2)
| domain(X0) != domain(X1)
| compose(domain(X0),compose(domain(X1),X2)) = compose(compose(domain(X0),domain(X1)),X2) ) ).
cnf(u1385,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(compose(codomain(X0),a),b) ) ).
cnf(u1664,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),compose(a,b)) = compose(domain(X0),compose(domain(X0),compose(a,b))) ) ).
cnf(u3234,hypothesis,
( codomain(X0) != codomain(h)
| compose(compose(a,h),codomain(X0)) = compose(domain(a),compose(compose(a,h),codomain(X0))) ) ).
cnf(u3050,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(a)
| compose(g,compose(codomain(X0),compose(a,h))) = compose(compose(g,codomain(X0)),compose(a,h)) ) ).
cnf(u424,hypothesis,
( codomain(X1) != domain(b)
| codomain(X0) != codomain(h)
| compose(X1,compose(g,codomain(X0))) = compose(compose(X1,g),codomain(X0)) ) ).
cnf(u1662,axiom,
( domain(X0) != domain(X1)
| compose(domain(X1),domain(X0)) = compose(domain(X1),compose(domain(X1),domain(X0))) ) ).
cnf(u1225,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),X1) = compose(codomain(X0),compose(codomain(X0),X1)) ) ).
cnf(u563,hypothesis,
( codomain(X0) != domain(b)
| codomain(h) = codomain(compose(codomain(X0),g)) ) ).
cnf(u143,hypothesis,
( codomain(X1) != domain(a)
| domain(X0) != domain(b)
| compose(X1,compose(a,X0)) = compose(compose(X1,a),X0) ) ).
cnf(u3005,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(u623,hypothesis,
( codomain(X0) != domain(a)
| codomain(h) = codomain(compose(codomain(X0),compose(a,h))) ) ).
cnf(u2064,hypothesis,
( codomain(X0) != codomain(h)
| codomain(X0) != domain(X1)
| compose(compose(a,h),compose(codomain(X0),domain(X1))) = compose(compose(compose(a,h),codomain(X0)),domain(X1)) ) ).
cnf(u1578,hypothesis,
( codomain(X0) != codomain(h)
| compose(compose(a,h),codomain(X0)) = compose(a,compose(g,codomain(X0))) ) ).
cnf(u601,axiom,
( codomain(X0) != domain(X1)
| domain(X1) = codomain(compose(codomain(X0),domain(X1))) ) ).
cnf(u2141,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(u325,hypothesis,
( codomain(X0) != domain(a)
| domain(X0) != codomain(X1)
| compose(X1,compose(X0,compose(a,h))) = compose(compose(X1,X0),compose(a,h)) ) ).
cnf(u1308,hypothesis,
( codomain(X0) != codomain(b)
| compose(compose(a,b),codomain(X0)) = compose(compose(compose(a,b),codomain(X0)),codomain(X0)) ) ).
cnf(u454,axiom,
( codomain(X0) != domain(X1)
| domain(X1) != domain(X2)
| compose(codomain(X0),compose(domain(X1),X2)) = compose(compose(codomain(X0),domain(X1)),X2) ) ).
cnf(u1820,hypothesis,
( domain(X0) != domain(a)
| compose(domain(X0),a) = compose(compose(domain(X0),a),domain(b)) ) ).
cnf(u2002,axiom,
( codomain(X0) != codomain(X1)
| domain(X1) != domain(X2)
| compose(domain(X2),compose(X1,codomain(X0))) = compose(compose(domain(X2),X1),codomain(X0)) ) ).
cnf(u1945,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) != domain(X1)
| compose(domain(X1),compose(codomain(X0),h)) = compose(compose(domain(X1),codomain(X0)),h) ) ).
cnf(u266,hypothesis,
( codomain(X1) != domain(b)
| domain(X0) != codomain(h)
| compose(X1,compose(g,X0)) = compose(compose(X1,g),X0) ) ).
cnf(u296,hypothesis,
( domain(X0) != domain(a)
| domain(X0) = domain(compose(domain(X0),compose(a,b))) ) ).
cnf(u1211,hypothesis,
( codomain(X0) != codomain(h)
| compose(g,codomain(X0)) = compose(compose(g,codomain(X0)),codomain(X0)) ) ).
cnf(u368,hypothesis,
( codomain(X0) != codomain(b)
| domain(a) = domain(compose(compose(a,b),codomain(X0))) ) ).
cnf(u1243,hypothesis,
( codomain(X0) != codomain(h)
| compose(g,codomain(X0)) = compose(g,compose(codomain(h),codomain(X0))) ) ).
cnf(u417,axiom,
( domain(X0) != codomain(X1)
| compose(X1,X0) = compose(compose(X1,X0),codomain(X0)) ) ).
cnf(u911,axiom,
( codomain(X1) != domain(X2)
| domain(X0) != domain(X1)
| compose(domain(X0),compose(X1,domain(X2))) = compose(compose(domain(X0),X1),domain(X2)) ) ).
cnf(u472,hypothesis,
( compose(a,b) != compose(X0,compose(a,b))
| codomain(X0) != domain(a)
| domain(a) = X0 ) ).
cnf(u1667,hypothesis,
( domain(X0) != domain(b)
| compose(domain(X0),g) = compose(domain(X0),compose(domain(X0),g)) ) ).
cnf(u1568,hypothesis,
( codomain(X1) != codomain(h)
| codomain(X0) != domain(b)
| compose(codomain(X0),compose(g,codomain(X1))) = compose(compose(codomain(X0),g),codomain(X1)) ) ).
cnf(u1295,hypothesis,
( codomain(X0) != domain(a)
| compose(codomain(X0),compose(a,b)) = compose(compose(codomain(X0),compose(a,b)),codomain(b)) ) ).
cnf(u947,axiom,
( codomain(X0) != domain(X1)
| compose(X0,X1) = compose(X0,compose(codomain(X0),X1)) ) ).
cnf(u18,hypothesis,
( compose(X0,compose(a,b)) != compose(X2,compose(a,b))
| domain(compose(a,b)) != codomain(X2)
| codomain(X0) != domain(compose(a,b))
| X0 = X2 ) ).
cnf(u1232,axiom,
( domain(X0) != codomain(X1)
| compose(X1,domain(X0)) = compose(X1,compose(codomain(X1),domain(X0))) ) ).
cnf(u938,axiom,
( codomain(X1) != domain(X2)
| domain(X0) != codomain(X1)
| compose(domain(X0),compose(codomain(X1),X2)) = compose(compose(domain(X0),codomain(X1)),X2) ) ).
cnf(u801,axiom,
( codomain(X0) != domain(X1)
| compose(codomain(X0),X1) = compose(compose(codomain(X0),X1),codomain(X1)) ) ).
cnf(u150,axiom,
( codomain(X0) != codomain(X2)
| codomain(X0) != domain(X1)
| compose(X2,compose(codomain(X0),X1)) = compose(compose(X2,codomain(X0)),X1) ) ).
cnf(u1871,hypothesis,
( codomain(X0) != domain(b)
| compose(a,compose(codomain(X0),domain(b))) = compose(compose(a,codomain(X0)),domain(b)) ) ).
cnf(u441,hypothesis,
( codomain(X0) != codomain(h)
| domain(a) = domain(compose(compose(a,h),codomain(X0))) ) ).
cnf(u105,hypothesis,
( domain(X0) != domain(b)
| domain(a) = domain(compose(a,X0)) ) ).
cnf(u1767,hypothesis,
( codomain(X0) != domain(a)
| domain(X1) != codomain(h)
| compose(codomain(X0),compose(compose(a,h),X1)) = compose(compose(codomain(X0),compose(a,h)),X1) ) ).
cnf(u255,hypothesis,
( domain(X0) != codomain(h)
| codomain(X0) = codomain(compose(g,X0)) ) ).
cnf(u237,hypothesis,
( codomain(X0) != domain(b)
| codomain(X0) = codomain(compose(a,codomain(X0))) ) ).
cnf(u1280,axiom,
( domain(X0) != domain(X1)
| compose(domain(X1),domain(X0)) = compose(compose(domain(X1),domain(X0)),domain(X0)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT001-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 21:12:09 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 4.92/1.47 % (2657018)Input is clausal, will run a generic CNF schedule.
% 4.92/1.47 % (2657129)lrs+10_1_sil=8000:sp=occurrence:random_seed=2958703166:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.92/1.47 % (2657127)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1831455803:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.92/1.47 % (2657128)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3420194995:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.92/1.47 % (2657126)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=974550059:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.92/1.47 % (2657129)Instruction limit reached!
% 4.92/1.47 % (2657129)------------------------------
% 4.92/1.47 % (2657129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657129)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657129)Termination reason: Instruction limit
% 4.92/1.47 % (2657129)Termination phase: Saturation
% 4.92/1.47 % (2657129)Time elapsed: 0.032 s
% 4.92/1.47 % (2657129)Peak memory usage: 89 MB
% 4.92/1.47 % (2657129)Instructions burned: 108 (million)
% 4.92/1.47 % (2657131)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1230547221:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.92/1.47 % (2657134)dis-21_1_sil=8000:lcm=predicate:random_seed=668907968: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)
% 4.92/1.47 % (2657133)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2639625202:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.92/1.47 % (2657134)Refutation not found, incomplete strategy
% 4.92/1.47 % (2657134)------------------------------
% 4.92/1.47 % (2657134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657134)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657134)Termination reason: Refutation not found, incomplete strategy
% 4.92/1.47 % (2657134)Time elapsed: 0.002 s
% 4.92/1.47 % (2657134)Peak memory usage: 88 MB
% 4.92/1.47 % (2657134)Instructions burned: 1 (million)
% 4.92/1.47 % (2657131)Instruction limit reached!
% 4.92/1.47 % (2657131)------------------------------
% 4.92/1.47 % (2657131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657131)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657131)Termination reason: Instruction limit
% 4.92/1.47 % (2657131)Termination phase: Saturation
% 4.92/1.47 % (2657131)Time elapsed: 0.061 s
% 4.92/1.47 % (2657131)Peak memory usage: 88 MB
% 4.92/1.47 % (2657131)Instructions burned: 114 (million)
% 4.92/1.47 % (2657171)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=3625228929:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.92/1.47 % (2657133)Instruction limit reached!
% 4.92/1.47 % (2657133)------------------------------
% 4.92/1.47 % (2657133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657133)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657133)Termination reason: Instruction limit
% 4.92/1.47 % (2657133)Termination phase: Saturation
% 4.92/1.47 % (2657133)Time elapsed: 0.104 s
% 4.92/1.47 % (2657133)Peak memory usage: 89 MB
% 4.92/1.47 % (2657133)Instructions burned: 181 (million)
% 4.92/1.47 % (2657171)Instruction limit reached!
% 4.92/1.47 % (2657171)------------------------------
% 4.92/1.47 % (2657171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657171)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657171)Termination reason: Instruction limit
% 4.92/1.47 % (2657171)Termination phase: Saturation
% 4.92/1.47 % (2657171)Time elapsed: 0.046 s
% 4.92/1.47 % (2657171)Peak memory usage: 89 MB
% 4.92/1.47 % (2657171)Instructions burned: 146 (million)
% 4.92/1.47 % (2657183)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2756938199:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.92/1.47 % (2657134)------------------------------
% 4.92/1.47 % (2657134)------------------------------
% 4.92/1.47 % (2657187)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4224271017:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 4.92/1.47 % (2657206)lrs+10_64_to=lpo:sil=8000:random_seed=4172822823:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 4.92/1.47 % (2657206)Instruction limit reached!
% 4.92/1.47 % (2657206)------------------------------
% 4.92/1.47 % (2657206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657206)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657206)Termination reason: Instruction limit
% 4.92/1.47 % (2657206)Termination phase: Saturation
% 4.92/1.47 % (2657206)Time elapsed: 0.037 s
% 4.92/1.47 % (2657206)Peak memory usage: 89 MB
% 4.92/1.47 % (2657206)Instructions burned: 127 (million)
% 4.92/1.47 % (2657183)Instruction limit reached!
% 4.92/1.47 % (2657183)------------------------------
% 4.92/1.47 % (2657183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657183)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657183)Termination reason: Instruction limit
% 4.92/1.47 % (2657183)Termination phase: Saturation
% 4.92/1.47 % (2657183)Time elapsed: 0.113 s
% 4.92/1.47 % (2657183)Peak memory usage: 89 MB
% 4.92/1.47 % (2657183)Instructions burned: 190 (million)
% 4.92/1.47 % (2657187)Instruction limit reached!
% 4.92/1.47 % (2657187)------------------------------
% 4.92/1.47 % (2657187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657187)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657187)Termination reason: Instruction limit
% 4.92/1.47 % (2657187)Termination phase: Saturation
% 4.92/1.47 % (2657187)Time elapsed: 0.114 s
% 4.92/1.47 % (2657187)Peak memory usage: 89 MB
% 4.92/1.47 % (2657187)Instructions burned: 221 (million)
% 4.92/1.47 % (2657269)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1981907457:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 4.92/1.47 % (2657257)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1117390435:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 4.92/1.47 % (2657269)First to succeed.
% 4.92/1.47 % (2657269)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2657018"
% 4.92/1.47 % (2657277)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3035874051:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 4.92/1.47 % (2657257)Instruction limit reached!
% 4.92/1.47 % (2657257)------------------------------
% 4.92/1.47 % (2657257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657257)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657257)Termination reason: Instruction limit
% 4.92/1.47 % (2657257)Termination phase: Saturation
% 4.92/1.47 % (2657257)Time elapsed: 0.104 s
% 4.92/1.47 % (2657257)Peak memory usage: 89 MB
% 4.92/1.47 % (2657257)Instructions burned: 194 (million)
% 4.92/1.47 % (2657294)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=2081015618:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 4.92/1.47 % (2657294)Instruction limit reached!
% 4.92/1.47 % (2657294)------------------------------
% 4.92/1.47 % (2657294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.92/1.47 % (2657294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.92/1.47 % (2657294)CaDiCaL version: 2.1.3
% 4.92/1.47 % (2657294)Termination reason: Instruction limit
% 4.92/1.47 % (2657294)Termination phase: Saturation
% 4.92/1.47 % (2657294)Time elapsed: 0.068 s
% 4.92/1.47 % (2657294)Peak memory usage: 89 MB
% 4.92/1.47 % (2657294)Instructions burned: 107 (million)
% 4.92/1.47 % SZS status Satisfiable for theBenchmark
% 4.92/1.47 % SZS output start Saturation.
% See solution above
% 6.18/1.66 % SZS output start Definitions and Model Updates.
% 6.18/1.66 % SZS output end Definitions and Model Updates.
% 6.18/1.66 % (2657269)------------------------------
% 6.18/1.66 % (2657269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.18/1.66 % (2657269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.18/1.66 % (2657269)CaDiCaL version: 2.1.3
% 6.18/1.66 % (2657269)Termination reason: Satisfiable
% 6.18/1.66 % (2657269)Time elapsed: 0.044 s
% 6.18/1.66 % (2657269)Peak memory usage: 90 MB
% 6.18/1.66 % (2657269)Instructions burned: 151 (million)
% 6.18/1.66 % (2657269)------------------------------
% 6.18/1.66 % (2657269)------------------------------
% 6.18/1.66 % (2657018)Success in time 0.809 s
% 6.18/1.66 % Vampire exiting
%------------------------------------------------------------------------------