%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET563-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.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 02:43:27 PM UTC 2026
% Result : Unsatisfiable 2.66s 2.20s
% Output : Proof 2.66s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t110,axiom,
sF0 = compatible(xh1,xf1,xf2),
introduced(definition) ).
cnf(f112,negated_conjecture,
compatible(xh1,xf1,xf2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_compatible_function_property3_1) ).
fof(f112_nnf,plain,
compatible(xh1,xf1,xf2),
inference(nnf_transformation,[status(thm)],[f112]) ).
cnf(c112,plain,
compatible(xh1,xf1,xf2),
inference(cnf_transformation,[status(esa)],[f112_nnf]) ).
cnf(t11,plain,
compatible(xh1,xf1,xf2) = true,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t132,plain,
compatible(xh1,xf1,xf2) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1174,plain,
sF0 = true,
inference(step,[status(thm)],[t110,t132]) ).
cnf(t134,plain,
true = sF0,
inference(orient,[status(thm)],[t1174]) ).
cnf(t117,axiom,
sF7 = subclass(domain_of(domain_of(flip(cross_product(xh1,universal_class)))),domain_of(xh2)),
introduced(definition) ).
cnf(t112,axiom,
sF2 = cross_product(xh1,universal_class),
introduced(definition) ).
cnf(t131,plain,
cross_product(xh1,universal_class) = sF2,
inference(orient,[status(thm)],[t112]) ).
cnf(t1254,plain,
sF7 = subclass(domain_of(domain_of(flip(sF2))),domain_of(xh2)),
inference(step,[status(thm)],[t117,t131]) ).
cnf(t113,axiom,
sF3 = flip(cross_product(xh1,universal_class)),
introduced(definition) ).
cnf(t1195,plain,
sF3 = flip(sF2),
inference(step,[status(thm)],[t113,t131]) ).
cnf(t158,plain,
flip(sF2) = sF3,
inference(orient,[status(thm)],[t1195]) ).
cnf(t1255,plain,
sF7 = subclass(domain_of(domain_of(sF3)),domain_of(xh2)),
inference(step,[status(thm)],[t1254,t158]) ).
cnf(t114,axiom,
sF4 = domain_of(flip(cross_product(xh1,universal_class))),
introduced(definition) ).
cnf(t1200,plain,
sF4 = domain_of(flip(sF2)),
inference(step,[status(thm)],[t114,t131]) ).
cnf(t1201,plain,
sF4 = domain_of(sF3),
inference(step,[status(thm)],[t1200,t158]) ).
cnf(t164,plain,
domain_of(sF3) = sF4,
inference(orient,[status(thm)],[t1201]) ).
cnf(t1256,plain,
sF7 = subclass(domain_of(sF4),domain_of(xh2)),
inference(step,[status(thm)],[t1255,t164]) ).
cnf(t115,axiom,
sF5 = domain_of(domain_of(flip(cross_product(xh1,universal_class)))),
introduced(definition) ).
cnf(t1204,plain,
sF5 = domain_of(domain_of(flip(sF2))),
inference(step,[status(thm)],[t115,t131]) ).
cnf(t1205,plain,
sF5 = domain_of(domain_of(sF3)),
inference(step,[status(thm)],[t1204,t158]) ).
cnf(t1206,plain,
sF5 = domain_of(sF4),
inference(step,[status(thm)],[t1205,t164]) ).
cnf(t169,plain,
domain_of(sF4) = sF5,
inference(orient,[status(thm)],[t1206]) ).
cnf(t1257,plain,
sF7 = subclass(sF5,domain_of(xh2)),
inference(step,[status(thm)],[t1256,t169]) ).
cnf(t116,axiom,
sF6 = domain_of(xh2),
introduced(definition) ).
cnf(t123,plain,
domain_of(xh2) = sF6,
inference(orient,[status(thm)],[t116]) ).
cnf(t1258,plain,
sF7 = subclass(sF5,sF6),
inference(step,[status(thm)],[t1257,t123]) ).
cnf(f114,negated_conjecture,
~ subclass(range_of(xh1),domain_of(xh2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_compatible_function_property3_3) ).
fof(f114_nnf,plain,
~ subclass(range_of(xh1),domain_of(xh2)),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
~ subclass(range_of(xh1),domain_of(xh2)),
inference(skolemisation,[status(esa)],[f114_nnf]) ).
cnf(c114,plain,
~ subclass(range_of(xh1),domain_of(xh2)),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(u57,axiom,
subclass(range_of(xh1),domain_of(xh2)) = false,
inference(equality_encoding,[status(esa)],[c114]) ).
cnf(f38,axiom,
domain_of(inverse(Z)) = range_of(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_of) ).
fof(f38_nnf,plain,
! [Z] : domain_of(inverse(Z)) = range_of(Z),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [Z] : domain_of(inverse(Z)) = range_of(Z),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
domain_of(inverse(X0)) = range_of(X0),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(u38,axiom,
domain_of(inverse(X0)) = range_of(X0),
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(f37,axiom,
domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
fof(f37_nnf,plain,
! [Y] : domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [Y] : domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(d5,axiom,
domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(d6,axiom,
domain_of(domain_of(flip(cross_product(X0,universal_class)))) = range_of(X0),
inference(definition_unfolding,[status(thm)],[u38,d5]) ).
cnf(t42,plain,
subclass(domain_of(domain_of(flip(cross_product(xh1,universal_class)))),domain_of(xh2)) = false,
inference(definition_unfolding,[status(thm)],[u57,d6]) ).
cnf(t1247,plain,
subclass(domain_of(domain_of(flip(sF2))),domain_of(xh2)) = false,
inference(step,[status(thm)],[t42,t131]) ).
cnf(t1248,plain,
subclass(domain_of(domain_of(sF3)),domain_of(xh2)) = false,
inference(step,[status(thm)],[t1247,t158]) ).
cnf(t1249,plain,
subclass(domain_of(sF4),domain_of(xh2)) = false,
inference(step,[status(thm)],[t1248,t164]) ).
cnf(t1250,plain,
subclass(sF5,domain_of(xh2)) = false,
inference(step,[status(thm)],[t1249,t169]) ).
cnf(t1251,plain,
subclass(sF5,sF6) = false,
inference(step,[status(thm)],[t1250,t123]) ).
cnf(t265,plain,
subclass(sF5,sF6) = false,
inference(orient,[status(thm)],[t1251]) ).
cnf(t1259,plain,
sF7 = false,
inference(step,[status(thm)],[t1258,t265]) ).
cnf(t275,plain,
false = sF7,
inference(orient,[status(thm)],[t1259]) ).
cnf(f83,axiom,
( subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| ~ compatible(Xh,Xf1,Xf2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible3) ).
fof(f83_nnf,plain,
! [Xh,Xf1,Xf2] :
( subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| ~ compatible(Xh,Xf1,Xf2) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [Xh,Xf1,Xf2] :
( subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| ~ compatible(Xh,Xf1,Xf2) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
( subclass(range_of(X0),domain_of(domain_of(X2)))
| ~ compatible(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(u52,axiom,
ifeq(compatible(X0,X1,X2),true,subclass(range_of(X0),domain_of(domain_of(X2))),true) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(t71,plain,
ifeq(compatible(X1,X2,X3),true,subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3))),true) = true,
inference(definition_unfolding,[status(thm)],[u52,d6]) ).
cnf(t1564,plain,
ifeq(compatible(X1,X2,X3),sF0,subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3))),true) = true,
inference(step,[status(thm)],[t71,t134]) ).
cnf(t1565,plain,
ifeq(compatible(X1,X2,X3),sF0,subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3))),sF0) = true,
inference(step,[status(thm)],[t1564,t134]) ).
cnf(t1566,plain,
ifeq(compatible(X1,X2,X3),sF0,subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3))),sF0) = sF0,
inference(step,[status(thm)],[t1565,t134]) ).
cnf(t1098,plain,
ifeq(compatible(X1,X2,X3),sF0,subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3))),sF0) = sF0,
inference(orient,[status(thm)],[t1566]) ).
cnf(t1188,plain,
compatible(xh1,xf1,xf2) = sF0,
inference(step,[status(thm)],[t132,t134]) ).
cnf(t150,plain,
compatible(xh1,xf1,xf2) = sF0,
inference(orient,[status(thm)],[t1188]) ).
cnf(t1101,plain,
sF0 = ifeq(sF0,sF0,subclass(domain_of(domain_of(flip(cross_product(xh1,universal_class)))),domain_of(domain_of(xf2))),sF0),
inference(cp,[status(thm)],[t1098,t150]) ).
cnf(t13,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t159,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t1567,plain,
sF0 = subclass(domain_of(domain_of(flip(cross_product(xh1,universal_class)))),domain_of(domain_of(xf2))),
inference(step,[status(thm)],[t1101,t159]) ).
cnf(t1568,plain,
sF0 = subclass(domain_of(domain_of(flip(sF2))),domain_of(domain_of(xf2))),
inference(step,[status(thm)],[t1567,t131]) ).
cnf(t1569,plain,
sF0 = subclass(domain_of(domain_of(sF3)),domain_of(domain_of(xf2))),
inference(step,[status(thm)],[t1568,t158]) ).
cnf(t1570,plain,
sF0 = subclass(domain_of(sF4),domain_of(domain_of(xf2))),
inference(step,[status(thm)],[t1569,t164]) ).
cnf(t1571,plain,
sF0 = subclass(sF5,domain_of(domain_of(xf2))),
inference(step,[status(thm)],[t1570,t169]) ).
cnf(f82,axiom,
( domain_of(domain_of(Xf1)) = domain_of(Xh)
| ~ compatible(Xh,Xf1,Xf2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compatible2) ).
fof(f82_nnf,plain,
! [Xh,Xf1,Xf2] :
( domain_of(domain_of(Xf1)) = domain_of(Xh)
| ~ compatible(Xh,Xf1,Xf2) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [Xh,Xf1,Xf2] :
( domain_of(domain_of(Xf1)) = domain_of(Xh)
| ~ compatible(Xh,Xf1,Xf2) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
( domain_of(domain_of(X1)) = domain_of(X0)
| ~ compatible(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(t53,plain,
ifeq(compatible(X1,X2,X3),true,domain_of(domain_of(X2)),domain_of(X1)) = domain_of(X1),
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(t1328,plain,
ifeq(compatible(X1,X2,X3),sF0,domain_of(domain_of(X2)),domain_of(X1)) = domain_of(X1),
inference(step,[status(thm)],[t53,t134]) ).
cnf(t470,plain,
ifeq(compatible(X1,X2,X3),sF0,domain_of(domain_of(X2)),domain_of(X1)) = domain_of(X1),
inference(orient,[status(thm)],[t1328]) ).
cnf(f113,negated_conjecture,
compatible(xh2,xf2,xf3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_compatible_function_property3_2) ).
fof(f113_nnf,plain,
compatible(xh2,xf2,xf3),
inference(nnf_transformation,[status(thm)],[f113]) ).
cnf(c113,plain,
compatible(xh2,xf2,xf3),
inference(cnf_transformation,[status(esa)],[f113_nnf]) ).
cnf(t12,plain,
compatible(xh2,xf2,xf3) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(t133,plain,
compatible(xh2,xf2,xf3) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t1190,plain,
compatible(xh2,xf2,xf3) = sF0,
inference(step,[status(thm)],[t133,t134]) ).
cnf(t152,plain,
compatible(xh2,xf2,xf3) = sF0,
inference(orient,[status(thm)],[t1190]) ).
cnf(t474,plain,
domain_of(xh2) = ifeq(sF0,sF0,domain_of(domain_of(xf2)),domain_of(xh2)),
inference(cp,[status(thm)],[t470,t152]) ).
cnf(t1330,plain,
sF6 = ifeq(sF0,sF0,domain_of(domain_of(xf2)),domain_of(xh2)),
inference(step,[status(thm)],[t474,t123]) ).
cnf(t1331,plain,
sF6 = domain_of(domain_of(xf2)),
inference(step,[status(thm)],[t1330,t159]) ).
cnf(t484,plain,
domain_of(domain_of(xf2)) = sF6,
inference(orient,[status(thm)],[t1331]) ).
cnf(t1572,plain,
sF0 = subclass(sF5,sF6),
inference(step,[status(thm)],[t1571,t484]) ).
cnf(t1265,plain,
subclass(sF5,sF6) = sF7,
inference(step,[status(thm)],[t265,t275]) ).
cnf(t283,plain,
subclass(sF5,sF6) = sF7,
inference(orient,[status(thm)],[t1265]) ).
cnf(t1573,plain,
sF0 = sF7,
inference(step,[status(thm)],[t1572,t283]) ).
cnf(t1110,plain,
sF7 = sF0,
inference(orient,[status(thm)],[t1573]) ).
cnf(t1578,plain,
false = sF0,
inference(step,[status(thm)],[t275,t1110]) ).
cnf(t1115,plain,
false = sF0,
inference(orient,[status(thm)],[t1578]) ).
cnf(f23,axiom,
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f23_nnf,plain,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(f29,axiom,
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f29_nnf,plain,
! [X,Z] :
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X,Z] :
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ member(X1,domain_of(X0))
| restrict(X0,singleton(X1),universal_class) != null_class ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c23,c29,c114]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t134]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1115]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET563-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.40 % Computer : n014.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Thu Sep 24 11:18:32 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 2.66/2.20 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.66/2.20 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------