%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CAT003-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:00:35 PM UTC 2026
% Result : Unsatisfiable 27.40s 3.92s
% Output : Proof 27.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 9
% Syntax : Number of formulae : 81 ( 69 unt; 0 def)
% Number of atoms : 109 ( 108 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 62 ( 34 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 80 ( 2 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f7,hypothesis,
( X = Z
| compose(compose(a,b),Z) != Y
| codomain(compose(a,b)) != domain(Z)
| compose(compose(a,b),X) != Y
| codomain(compose(a,b)) != domain(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',endomorphism) ).
fof(f7_nnf,plain,
! [X,Y,Z] :
( X = Z
| compose(compose(a,b),Z) != Y
| codomain(compose(a,b)) != domain(Z)
| compose(compose(a,b),X) != Y
| codomain(compose(a,b)) != domain(X) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] :
( X = Z
| compose(compose(a,b),Z) != Y
| codomain(compose(a,b)) != domain(Z)
| compose(compose(a,b),X) != Y
| codomain(compose(a,b)) != domain(X) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( X0 = X2
| compose(compose(a,b),X2) != X1
| codomain(compose(a,b)) != domain(X2)
| compose(compose(a,b),X0) != X1
| codomain(compose(a,b)) != domain(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t12,plain,
ifeq(codomain(compose(a,b)),domain(X1),ifeq(compose(compose(a,b),X1),X2,ifeq(codomain(compose(a,b)),domain(X3),ifeq(compose(compose(a,b),X3),X2,X1,X3),X3),X3),X3) = X3,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f5,axiom,
( codomain(compose(X,Y)) = codomain(Y)
| codomain(X) != domain(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain_domain2) ).
fof(f5_nnf,plain,
! [X,Y] :
( codomain(compose(X,Y)) = codomain(Y)
| codomain(X) != domain(Y) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] :
( codomain(compose(X,Y)) = codomain(Y)
| codomain(X) != domain(Y) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( codomain(compose(X0,X1)) = codomain(X1)
| codomain(X0) != domain(X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t9,plain,
ifeq(codomain(X1),domain(X2),codomain(compose(X1,X2)),codomain(X2)) = codomain(X2),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t44,plain,
ifeq(codomain(X1),domain(X2),codomain(compose(X1,X2)),codomain(X2)) = codomain(X2),
inference(orient,[status(thm)],[t9]) ).
cnf(f8,hypothesis,
codomain(a) = domain(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain_of_a_equals_domain_of_b) ).
fof(f8_nnf,plain,
codomain(a) = domain(b),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
codomain(a) = domain(b),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t0,plain,
domain(b) = codomain(a),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t13,plain,
codomain(a) = domain(b),
inference(orient,[status(thm)],[t0]) ).
cnf(t45,plain,
codomain(X1) = ifeq(domain(b),domain(X1),codomain(compose(a,X1)),codomain(X1)),
inference(cp,[status(thm)],[t44,t13]) ).
cnf(t86,plain,
ifeq(domain(b),domain(X1),codomain(compose(a,X1)),codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t45]) ).
cnf(f10,hypothesis,
codomain(b) = domain(g),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain_of_b_equals_domain_of_g) ).
fof(f10_nnf,plain,
codomain(b) = domain(g),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
codomain(b) = domain(g),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t1,plain,
domain(g) = codomain(b),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t14,plain,
codomain(b) = domain(g),
inference(orient,[status(thm)],[t1]) ).
cnf(f9,hypothesis,
codomain(b) = domain(h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain_of_b_equals_domain_of_h) ).
fof(f9_nnf,plain,
codomain(b) = domain(h),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
codomain(b) = domain(h),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t2,plain,
domain(h) = codomain(b),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t1569,plain,
domain(h) = domain(g),
inference(step,[status(thm)],[t2,t14]) ).
cnf(t15,plain,
domain(g) = domain(h),
inference(orient,[status(thm)],[t1569]) ).
cnf(t1570,plain,
codomain(b) = domain(h),
inference(step,[status(thm)],[t14,t15]) ).
cnf(t16,plain,
codomain(b) = domain(h),
inference(orient,[status(thm)],[t1570]) ).
cnf(t88,plain,
codomain(b) = ifeq(domain(b),domain(b),codomain(compose(a,b)),domain(h)),
inference(cp,[status(thm)],[t86,t16]) ).
cnf(t1589,plain,
domain(h) = ifeq(domain(b),domain(b),codomain(compose(a,b)),domain(h)),
inference(step,[status(thm)],[t88,t16]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t41,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t1590,plain,
domain(h) = codomain(compose(a,b)),
inference(step,[status(thm)],[t1589,t41]) ).
cnf(t93,plain,
codomain(compose(a,b)) = domain(h),
inference(orient,[status(thm)],[t1590]) ).
cnf(t1600,plain,
ifeq(domain(h),domain(X1),ifeq(compose(compose(a,b),X1),X2,ifeq(codomain(compose(a,b)),domain(X3),ifeq(compose(compose(a,b),X3),X2,X1,X3),X3),X3),X3) = X3,
inference(step,[status(thm)],[t12,t93]) ).
cnf(t1601,plain,
ifeq(domain(h),domain(X1),ifeq(compose(compose(a,b),X1),X2,ifeq(domain(h),domain(X3),ifeq(compose(compose(a,b),X3),X2,X1,X3),X3),X3),X3) = X3,
inference(step,[status(thm)],[t1600,t93]) ).
cnf(t226,plain,
ifeq(domain(h),domain(X1),ifeq(compose(compose(a,b),X1),X2,ifeq(domain(h),domain(X3),ifeq(compose(compose(a,b),X3),X2,X1,X3),X3),X3),X3) = X3,
inference(orient,[status(thm)],[t1601]) ).
cnf(t227,plain,
X1 = ifeq(domain(h),domain(h),ifeq(compose(compose(a,b),g),X2,ifeq(domain(h),domain(X1),ifeq(compose(compose(a,b),X1),X2,g,X1),X1),X1),X1),
inference(cp,[status(thm)],[t226,t15]) ).
cnf(t2055,plain,
X1 = ifeq(compose(compose(a,b),g),X2,ifeq(domain(h),domain(X1),ifeq(compose(compose(a,b),X1),X2,g,X1),X1),X1),
inference(step,[status(thm)],[t227,t41]) ).
cnf(f6,axiom,
( compose(X,compose(Y,Z)) = compose(compose(X,Y),Z)
| codomain(Y) != domain(Z)
| codomain(X) != domain(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_property) ).
fof(f6_nnf,plain,
! [X,Y,Z] :
( compose(X,compose(Y,Z)) = compose(compose(X,Y),Z)
| codomain(Y) != domain(Z)
| codomain(X) != domain(Y) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] :
( compose(X,compose(Y,Z)) = compose(compose(X,Y),Z)
| codomain(Y) != domain(Z)
| codomain(X) != domain(Y) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( compose(X0,compose(X1,X2)) = compose(compose(X0,X1),X2)
| codomain(X1) != domain(X2)
| codomain(X0) != domain(X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t11,plain,
ifeq(codomain(X1),domain(X2),ifeq(codomain(X2),domain(X3),compose(X1,compose(X2,X3)),compose(compose(X1,X2),X3)),compose(compose(X1,X2),X3)) = compose(compose(X1,X2),X3),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t106,plain,
ifeq(codomain(X1),domain(X2),ifeq(codomain(X2),domain(X3),compose(X1,compose(X2,X3)),compose(compose(X1,X2),X3)),compose(compose(X1,X2),X3)) = compose(compose(X1,X2),X3),
inference(orient,[status(thm)],[t11]) ).
cnf(t107,plain,
compose(compose(a,X1),X2) = ifeq(domain(b),domain(X1),ifeq(codomain(X1),domain(X2),compose(a,compose(X1,X2)),compose(compose(a,X1),X2)),compose(compose(a,X1),X2)),
inference(cp,[status(thm)],[t106,t13]) ).
cnf(t719,plain,
ifeq(domain(b),domain(X1),ifeq(codomain(X1),domain(X2),compose(a,compose(X1,X2)),compose(compose(a,X1),X2)),compose(compose(a,X1),X2)) = compose(compose(a,X1),X2),
inference(orient,[status(thm)],[t107]) ).
cnf(f11,hypothesis,
compose(b,h) = compose(b,g),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bh_equals_bg) ).
fof(f11_nnf,plain,
compose(b,h) = compose(b,g),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
compose(b,h) = compose(b,g),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t7,plain,
compose(b,h) = compose(b,g),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t24,plain,
compose(b,g) = compose(b,h),
inference(orient,[status(thm)],[t7]) ).
cnf(t727,plain,
compose(compose(a,b),g) = ifeq(domain(b),domain(b),ifeq(codomain(b),domain(g),compose(a,compose(b,h)),compose(compose(a,b),g)),compose(compose(a,b),g)),
inference(cp,[status(thm)],[t719,t24]) ).
cnf(t1732,plain,
compose(compose(a,b),g) = ifeq(codomain(b),domain(g),compose(a,compose(b,h)),compose(compose(a,b),g)),
inference(step,[status(thm)],[t727,t41]) ).
cnf(t1733,plain,
compose(compose(a,b),g) = ifeq(domain(h),domain(g),compose(a,compose(b,h)),compose(compose(a,b),g)),
inference(step,[status(thm)],[t1732,t16]) ).
cnf(t1734,plain,
compose(compose(a,b),g) = ifeq(domain(h),domain(h),compose(a,compose(b,h)),compose(compose(a,b),g)),
inference(step,[status(thm)],[t1733,t15]) ).
cnf(t1735,plain,
compose(compose(a,b),g) = compose(a,compose(b,h)),
inference(step,[status(thm)],[t1734,t41]) ).
cnf(t740,plain,
compose(compose(a,b),g) = compose(a,compose(b,h)),
inference(orient,[status(thm)],[t1735]) ).
cnf(t2056,plain,
X1 = ifeq(compose(a,compose(b,h)),X2,ifeq(domain(h),domain(X1),ifeq(compose(compose(a,b),X1),X2,g,X1),X1),X1),
inference(step,[status(thm)],[t2055,t740]) ).
cnf(t1431,plain,
ifeq(compose(a,compose(b,h)),X1,ifeq(domain(h),domain(X2),ifeq(compose(compose(a,b),X2),X1,g,X2),X2),X2) = X2,
inference(orient,[status(thm)],[t2056]) ).
cnf(t1437,plain,
h = ifeq(compose(a,compose(b,h)),X1,ifeq(compose(compose(a,b),h),X1,g,h),h),
inference(cp,[status(thm)],[t1431,t41]) ).
cnf(t721,plain,
compose(compose(a,b),X1) = ifeq(domain(b),domain(b),ifeq(domain(h),domain(X1),compose(a,compose(b,X1)),compose(compose(a,b),X1)),compose(compose(a,b),X1)),
inference(cp,[status(thm)],[t719,t16]) ).
cnf(t1775,plain,
compose(compose(a,b),X1) = ifeq(domain(h),domain(X1),compose(a,compose(b,X1)),compose(compose(a,b),X1)),
inference(step,[status(thm)],[t721,t41]) ).
cnf(t873,plain,
ifeq(domain(h),domain(X1),compose(a,compose(b,X1)),compose(compose(a,b),X1)) = compose(compose(a,b),X1),
inference(orient,[status(thm)],[t1775]) ).
cnf(t876,plain,
compose(compose(a,b),h) = compose(a,compose(b,h)),
inference(cp,[status(thm)],[t873,t41]) ).
cnf(t881,plain,
compose(compose(a,b),h) = compose(a,compose(b,h)),
inference(orient,[status(thm)],[t876]) ).
cnf(t2065,plain,
h = ifeq(compose(a,compose(b,h)),X1,ifeq(compose(a,compose(b,h)),X1,g,h),h),
inference(step,[status(thm)],[t1437,t881]) ).
cnf(t1448,plain,
ifeq(compose(a,compose(b,h)),X1,ifeq(compose(a,compose(b,h)),X1,g,h),h) = h,
inference(orient,[status(thm)],[t2065]) ).
cnf(t1449,plain,
h = ifeq(compose(a,compose(b,h)),compose(a,compose(b,h)),g,h),
inference(cp,[status(thm)],[t1448,t41]) ).
cnf(t2066,plain,
h = g,
inference(step,[status(thm)],[t1449,t41]) ).
cnf(t1450,plain,
g = h,
inference(orient,[status(thm)],[t2066]) ).
cnf(f12,negated_conjecture,
g != h,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_g_equals_h) ).
fof(f12_nnf,plain,
g != h,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
g != h,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
g != h,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(goal_0,negated_conjecture,
h != g,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(g0_0,plain,
h != h,
inference(rw,[status(thm)],[goal_0,t1450]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT003-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 06:51:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 27.40/3.92 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.40/3.92 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------