%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CAT020-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 : Thu Sep 24 12:07:45 PM UTC 2026
% Result : Satisfiable 0.14s 0.42s
% Output : Saturation 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( product(X,Y,compose(X,Y))
| ~ defined(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( defined(X,Y)
| ~ product(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Xy,Z] :
( defined(Y,Z)
| ~ defined(Xy,Z)
| ~ product(X,Y,Xy) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,Xy,Z,Yz] :
( defined(X,Yz)
| ~ defined(Xy,Z)
| ~ product(Y,Z,Yz)
| ~ product(X,Y,Xy) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Xy,Z,Xyz,Yz] :
( product(X,Yz,Xyz)
| ~ product(Y,Z,Yz)
| ~ product(Xy,Z,Xyz)
| ~ product(X,Y,Xy) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Y,Z,Yz,X] :
( defined(X,Y)
| ~ defined(X,Yz)
| ~ product(Y,Z,Yz) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Y,Z,Yz,X,Xy] :
( defined(Xy,Z)
| ~ defined(X,Yz)
| ~ product(X,Y,Xy)
| ~ product(Y,Z,Yz) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [Y,Z,Yz,X,Xyz,Xy] :
( product(Xy,Z,Xyz)
| ~ product(X,Y,Xy)
| ~ product(X,Yz,Xyz)
| ~ product(Y,Z,Yz) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z] :
( defined(X,Z)
| ~ identity_map(Y)
| ~ defined(Y,Z)
| ~ defined(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] : identity_map(domain(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] : identity_map(codomain(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : defined(X,domain(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] : defined(codomain(X),X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] : product(X,domain(X),X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X] : product(codomain(X),X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X,Y] :
( product(X,Y,Y)
| ~ identity_map(X)
| ~ defined(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X,Y] :
( product(X,Y,X)
| ~ identity_map(Y)
| ~ defined(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X,Y,Z,W] :
( Z = W
| ~ product(X,Y,W)
| ~ product(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,plain,
! [X0,X1] :
( product(X0,X1,compose(X0,X1))
| ~ defined(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [X,Y] :
( defined(X,Y)
| ! [Z] : ~ product(X,Y,Z) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f21,plain,
! [X0,X1,X2] :
( defined(X0,X1)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [Y,Z] :
( defined(Y,Z)
| ! [Xy] :
( ~ defined(Xy,Z)
| ! [X] : ~ product(X,Y,Xy) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( defined(X1,X3)
| ~ defined(X2,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X,Yz] :
( defined(X,Yz)
| ! [Xy,Z] :
( ~ defined(Xy,Z)
| ! [Y] :
( ~ product(Y,Z,Yz)
| ~ product(X,Y,Xy) ) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f25,plain,
! [X0,X1,X2,X3,X4] :
( defined(X0,X4)
| ~ defined(X2,X3)
| ~ product(X1,X3,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
! [X,Xyz,Yz] :
( product(X,Yz,Xyz)
| ! [Y,Z] :
( ~ product(Y,Z,Yz)
| ! [Xy] :
( ~ product(Xy,Z,Xyz)
| ~ product(X,Y,Xy) ) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f27,plain,
! [X0,X1,X2,X3,X4,X5] :
( product(X0,X5,X4)
| ~ product(X1,X3,X5)
| ~ product(X2,X3,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f28,plain,
! [Y,X] :
( defined(X,Y)
| ! [Yz] :
( ~ defined(X,Yz)
| ! [Z] : ~ product(Y,Z,Yz) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f29,plain,
! [X0,X1,X2,X3] :
( defined(X3,X0)
| ~ defined(X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [Z,Xy] :
( defined(Xy,Z)
| ! [Yz,X] :
( ~ defined(X,Yz)
| ! [Y] :
( ~ product(X,Y,Xy)
| ~ product(Y,Z,Yz) ) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f31,plain,
! [X0,X1,X2,X3,X4] :
( defined(X4,X1)
| ~ defined(X3,X2)
| ~ product(X3,X0,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
! [Z,Xyz,Xy] :
( product(Xy,Z,Xyz)
| ! [Y,X] :
( ~ product(X,Y,Xy)
| ! [Yz] :
( ~ product(X,Yz,Xyz)
| ~ product(Y,Z,Yz) ) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f33,plain,
! [X0,X1,X2,X3,X4,X5] :
( product(X5,X1,X4)
| ~ product(X3,X0,X5)
| ~ product(X3,X2,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [X,Z] :
( defined(X,Z)
| ! [Y] :
( ~ identity_map(Y)
| ~ defined(Y,Z)
| ~ defined(X,Y) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f35,plain,
! [X0,X1,X2] :
( defined(X0,X2)
| ~ identity_map(X1)
| ~ defined(X1,X2)
| ~ defined(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
! [X0] : identity_map(domain(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f37,plain,
! [X0] : identity_map(codomain(X0)),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f38,plain,
! [X0] : defined(X0,domain(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f39,plain,
! [X0] : defined(codomain(X0),X0),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f40,plain,
! [X0] : product(X0,domain(X0),X0),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f41,plain,
! [X0] : product(codomain(X0),X0,X0),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f42,plain,
! [X0,X1] :
( product(X0,X1,X1)
| ~ identity_map(X0)
| ~ defined(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f43,plain,
! [X0,X1] :
( product(X0,X1,X0)
| ~ identity_map(X1)
| ~ defined(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f44,plain,
! [Z,W] :
( Z = W
| ! [X,Y] :
( ~ product(X,Y,W)
| ~ product(X,Y,Z) ) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0] : product(X0,domain(X0),compose(X0,domain(X0))),
inference(resolution,[status(thm)],[f38,f19]) ).
fof(f47,plain,
! [X0] : product(codomain(X0),X0,compose(codomain(X0),X0)),
inference(resolution,[status(thm)],[f39,f19]) ).
fof(f51,plain,
! [X0,X1] :
( defined(domain(X0),X1)
| ~ defined(X0,X1) ),
inference(resolution,[status(thm)],[f23,f40]) ).
fof(f53,plain,
! [X0] : defined(domain(X0),domain(X0)),
inference(resolution,[status(thm)],[f51,f38]) ).
fof(f56,plain,
! [X0,X1,X2] :
( defined(codomain(X0),X2)
| ~ defined(X0,X1)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f25,f41]) ).
fof(f57,plain,
! [X0,X1,X2] :
( defined(X0,X2)
| ~ defined(X0,X1)
| ~ product(domain(X0),X1,X2) ),
inference(resolution,[status(thm)],[f25,f40]) ).
fof(f58,plain,
! [X0,X1,X2] :
( defined(codomain(X0),X2)
| ~ product(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f56,f21]) ).
fof(f63,plain,
! [X0,X1,X2,X3] :
( product(codomain(X0),X3,X2)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f27,f41]) ).
fof(f64,plain,
! [X0,X1,X2,X3] :
( product(X0,X3,X2)
| ~ product(domain(X0),X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f27,f40]) ).
fof(f69,plain,
! [X0,X1] :
( defined(X0,codomain(X1))
| ~ defined(X0,X1) ),
inference(resolution,[status(thm)],[f29,f41]) ).
fof(f78,plain,
! [X0] : defined(codomain(X0),codomain(X0)),
inference(resolution,[status(thm)],[f69,f39]) ).
fof(f80,plain,
! [X0,X1,X2] :
( defined(X2,X1)
| ~ defined(X0,X1)
| ~ product(X0,codomain(X1),X2) ),
inference(resolution,[status(thm)],[f31,f41]) ).
fof(f81,plain,
! [X0,X1,X2] :
( defined(X2,domain(X1))
| ~ defined(X0,X1)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f31,f40]) ).
fof(f82,plain,
! [X0,X1,X2] :
( defined(X2,domain(X1))
| ~ product(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f81,f21]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( product(X3,X1,X2)
| ~ product(X0,codomain(X1),X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f33,f41]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( product(X3,domain(X1),X2)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(resolution,[status(thm)],[f33,f40]) ).
fof(f105,plain,
! [X0,X1] :
( defined(codomain(X0),X1)
| ~ identity_map(X0)
| ~ defined(X0,X1) ),
inference(resolution,[status(thm)],[f35,f39]) ).
fof(f107,plain,
! [X0,X1] :
( defined(X0,X1)
| ~ identity_map(domain(X0))
| ~ defined(domain(X0),X1) ),
inference(resolution,[status(thm)],[f35,f38]) ).
fof(f109,plain,
! [X0,X1] :
( defined(X0,X1)
| ~ defined(domain(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f107,f36]) ).
fof(f126,plain,
! [X0] :
( product(domain(X0),domain(X0),domain(X0))
| ~ identity_map(domain(X0)) ),
inference(resolution,[status(thm)],[f42,f53]) ).
fof(f129,plain,
! [X0] :
( product(codomain(X0),codomain(X0),codomain(X0))
| ~ identity_map(codomain(X0)) ),
inference(resolution,[status(thm)],[f42,f78]) ).
fof(f132,plain,
! [X0] :
( product(X0,domain(X0),domain(X0))
| ~ identity_map(X0) ),
inference(resolution,[status(thm)],[f42,f38]) ).
fof(f139,plain,
! [X0] : product(domain(X0),domain(X0),domain(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f126,f36]) ).
fof(f142,plain,
! [X0] : product(codomain(X0),codomain(X0),codomain(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f129,f37]) ).
fof(f171,plain,
! [X0] :
( product(codomain(X0),X0,codomain(X0))
| ~ identity_map(X0) ),
inference(resolution,[status(thm)],[f43,f39]) ).
fof(f192,plain,
! [X0,X1] :
( X0 = X1
| ~ product(codomain(X0),X0,X1) ),
inference(resolution,[status(thm)],[f45,f41]) ).
fof(f194,plain,
! [X0,X1] :
( X0 = X1
| ~ product(X0,domain(X0),X1) ),
inference(resolution,[status(thm)],[f45,f40]) ).
fof(f197,plain,
! [X0] : X0 = compose(X0,domain(X0)),
inference(resolution,[status(thm)],[f46,f194]) ).
fof(f216,plain,
! [X0] : X0 = compose(codomain(X0),X0),
inference(resolution,[status(thm)],[f47,f192]) ).
fof(f253,plain,
! [X0,X1] :
( product(codomain(X0),X1,X0)
| ~ product(X0,domain(X0),X1) ),
inference(resolution,[status(thm)],[f63,f40]) ).
fof(f275,plain,
! [X0,X1] :
( product(codomain(X0),X1,X0)
| ~ product(domain(codomain(X0)),X0,X1) ),
inference(resolution,[status(thm)],[f64,f41]) ).
fof(f278,plain,
! [X0,X1] :
( product(X0,X1,X0)
| ~ product(domain(X0),domain(X0),X1) ),
inference(resolution,[status(thm)],[f64,f40]) ).
fof(f341,plain,
! [X0,X1] :
( product(X1,X0,X0)
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(resolution,[status(thm)],[f89,f41]) ).
fof(f366,plain,
! [X0,X1] :
( domain(X0) = X1
| ~ product(domain(X0),domain(X0),X1) ),
inference(resolution,[status(thm)],[f139,f45]) ).
fof(f368,plain,
! [X0,X1,X2] :
( defined(X2,domain(X1))
| ~ defined(X0,domain(X1))
| ~ product(X0,domain(X1),X2) ),
inference(resolution,[status(thm)],[f139,f31]) ).
fof(f372,plain,
! [X0,X1,X2] :
( defined(domain(X0),X2)
| ~ defined(domain(X0),X1)
| ~ product(domain(X0),X1,X2) ),
inference(resolution,[status(thm)],[f139,f25]) ).
fof(f375,plain,
! [X0,X1,X2] :
( defined(X2,domain(X1))
| ~ product(X0,domain(X1),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f21]) ).
fof(f376,plain,
! [X0,X1,X2] :
( defined(domain(X0),X2)
| ~ product(domain(X0),X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f21]) ).
fof(f382,plain,
! [X0,X1] :
( product(X1,domain(X0),X0)
| ~ product(codomain(X0),X0,X1) ),
inference(resolution,[status(thm)],[f90,f41]) ).
fof(f385,plain,
! [X0,X1] :
( product(X1,domain(domain(X0)),X0)
| ~ product(X0,domain(X0),X1) ),
inference(resolution,[status(thm)],[f90,f40]) ).
fof(f392,plain,
! [X0,X1] :
( codomain(X0) = X1
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(resolution,[status(thm)],[f142,f45]) ).
fof(f394,plain,
! [X0,X1,X2] :
( defined(X2,codomain(X1))
| ~ defined(X0,codomain(X1))
| ~ product(X0,codomain(X1),X2) ),
inference(resolution,[status(thm)],[f142,f31]) ).
fof(f398,plain,
! [X0,X1,X2] :
( defined(codomain(X0),X2)
| ~ defined(codomain(X0),X1)
| ~ product(codomain(X0),X1,X2) ),
inference(resolution,[status(thm)],[f142,f25]) ).
fof(f401,plain,
! [X0,X1,X2] :
( defined(X2,codomain(X1))
| ~ product(X0,codomain(X1),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f394,f21]) ).
fof(f402,plain,
! [X0,X1,X2] :
( defined(codomain(X0),X2)
| ~ product(codomain(X0),X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f398,f21]) ).
fof(f422,plain,
! [X0] :
( defined(codomain(X0),domain(X0))
| ~ identity_map(X0) ),
inference(resolution,[status(thm)],[f105,f38]) ).
fof(f430,plain,
! [X0] : product(codomain(X0),domain(codomain(X0)),domain(codomain(X0))),
inference(resolution,[status(thm)],[f132,f37]) ).
fof(f431,plain,
! [X0] : product(domain(X0),domain(domain(X0)),domain(domain(X0))),
inference(resolution,[status(thm)],[f132,f36]) ).
fof(f434,plain,
! [X0] : product(codomain(codomain(X0)),codomain(X0),codomain(codomain(X0))),
inference(resolution,[status(thm)],[f171,f37]) ).
fof(f435,plain,
! [X0] : product(codomain(domain(X0)),domain(X0),codomain(domain(X0))),
inference(resolution,[status(thm)],[f171,f36]) ).
fof(f1001,plain,
! [X0] : codomain(X0) = domain(codomain(X0)),
inference(resolution,[status(thm)],[f430,f194]) ).
fof(f1002,plain,
! [X0,X1] :
( product(X1,domain(domain(codomain(X0))),domain(codomain(X0)))
| ~ product(codomain(X0),domain(codomain(X0)),X1) ),
inference(resolution,[status(thm)],[f430,f90]) ).
fof(f1005,plain,
! [X0,X1] :
( product(codomain(X0),X1,domain(codomain(X0)))
| ~ product(domain(codomain(X0)),domain(codomain(X0)),X1) ),
inference(resolution,[status(thm)],[f430,f64]) ).
fof(f1008,plain,
! [X0,X1,X2,X3] :
( product(X3,domain(codomain(X1)),X2)
| ~ product(X0,codomain(X1),X3)
| ~ product(X0,domain(codomain(X1)),X2) ),
inference(resolution,[status(thm)],[f430,f33]) ).
fof(f1012,plain,
! [X0,X1,X2,X3] :
( product(codomain(X0),X3,X2)
| ~ product(domain(codomain(X0)),X1,X3)
| ~ product(domain(codomain(X0)),X1,X2) ),
inference(resolution,[status(thm)],[f430,f27]) ).
fof(f1031,plain,
! [X0,X1] :
( product(codomain(X0),X1,X0)
| ~ product(codomain(X0),X0,X1) ),
inference(backward_demodulation,[status(thm)],[f1001,f275]) ).
fof(f1079,plain,
! [X0] : codomain(X0) = compose(codomain(X0),codomain(X0)),
inference(paramodulation,[status(thm)],[f1001,f197]) ).
fof(f1155,plain,
! [X0] : domain(X0) = domain(domain(X0)),
inference(resolution,[status(thm)],[f431,f194]) ).
fof(f1156,plain,
! [X0,X1] :
( product(X1,domain(domain(domain(X0))),domain(domain(X0)))
| ~ product(domain(X0),domain(domain(X0)),X1) ),
inference(resolution,[status(thm)],[f431,f90]) ).
fof(f1159,plain,
! [X0,X1] :
( product(domain(X0),X1,domain(domain(X0)))
| ~ product(domain(domain(X0)),domain(domain(X0)),X1) ),
inference(resolution,[status(thm)],[f431,f64]) ).
fof(f1162,plain,
! [X0,X1,X2,X3] :
( product(X3,domain(domain(X1)),X2)
| ~ product(X0,domain(X1),X3)
| ~ product(X0,domain(domain(X1)),X2) ),
inference(resolution,[status(thm)],[f431,f33]) ).
fof(f1166,plain,
! [X0,X1,X2,X3] :
( product(domain(X0),X3,X2)
| ~ product(domain(domain(X0)),X1,X3)
| ~ product(domain(domain(X0)),X1,X2) ),
inference(resolution,[status(thm)],[f431,f27]) ).
fof(f1192,plain,
! [X0,X1] :
( product(X1,domain(X0),X0)
| ~ product(X0,domain(X0),X1) ),
inference(backward_demodulation,[status(thm)],[f1155,f385]) ).
fof(f1222,plain,
! [X0] : domain(X0) = compose(domain(X0),domain(X0)),
inference(paramodulation,[status(thm)],[f1155,f197]) ).
fof(f1268,plain,
! [X0] : codomain(X0) = codomain(codomain(X0)),
inference(resolution,[status(thm)],[f434,f192]) ).
fof(f1346,plain,
! [X0] : domain(X0) = codomain(domain(X0)),
inference(resolution,[status(thm)],[f435,f192]) ).
fof(f1602,plain,
! [X0,X1] :
( product(X1,domain(domain(codomain(X0))),domain(codomain(X0)))
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1001,f1002]) ).
fof(f1603,plain,
! [X0,X1] :
( product(X1,domain(codomain(X0)),domain(codomain(X0)))
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1602]) ).
fof(f1604,plain,
! [X0,X1] :
( product(X1,codomain(X0),domain(codomain(X0)))
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1001,f1603]) ).
fof(f1605,plain,
! [X0,X1] :
( product(X1,codomain(X0),codomain(X0))
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1001,f1604]) ).
fof(f1644,plain,
! [X0,X1] :
( product(codomain(X0),X1,domain(codomain(X0)))
| ~ product(codomain(X0),domain(codomain(X0)),X1) ),
inference(forward_demodulation,[status(thm)],[f1001,f1005]) ).
fof(f1645,plain,
! [X0,X1] :
( product(codomain(X0),X1,domain(codomain(X0)))
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1001,f1644]) ).
fof(f1646,plain,
! [X0,X1] :
( product(codomain(X0),X1,codomain(X0))
| ~ product(codomain(X0),codomain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1001,f1645]) ).
fof(f1683,plain,
! [X0,X1,X2,X3] :
( product(X3,domain(codomain(X1)),X2)
| ~ product(X0,codomain(X1),X3)
| ~ product(X0,codomain(X1),X2) ),
inference(forward_demodulation,[status(thm)],[f1001,f1008]) ).
fof(f1684,plain,
! [X0,X1,X2,X3] :
( product(X3,codomain(X1),X2)
| ~ product(X0,codomain(X1),X3)
| ~ product(X0,codomain(X1),X2) ),
inference(forward_demodulation,[status(thm)],[f1001,f1683]) ).
fof(f1706,plain,
! [X0,X1,X2,X3] :
( product(codomain(X0),X3,X2)
| ~ product(domain(codomain(X0)),X1,X3)
| ~ product(codomain(X0),X1,X2) ),
inference(forward_demodulation,[status(thm)],[f1001,f1012]) ).
fof(f1707,plain,
! [X0,X1,X2,X3] :
( product(codomain(X0),X3,X2)
| ~ product(codomain(X0),X1,X3)
| ~ product(codomain(X0),X1,X2) ),
inference(forward_demodulation,[status(thm)],[f1001,f1706]) ).
fof(f1746,plain,
! [X0,X1] :
( product(X1,domain(domain(domain(X0))),domain(domain(X0)))
| ~ product(domain(X0),domain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1156]) ).
fof(f1747,plain,
! [X0,X1] :
( product(X1,domain(domain(X0)),domain(domain(X0)))
| ~ product(domain(X0),domain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1746]) ).
fof(f1748,plain,
! [X0,X1] :
( product(X1,domain(X0),domain(domain(X0)))
| ~ product(domain(X0),domain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1747]) ).
fof(f1749,plain,
! [X0,X1] :
( product(X1,domain(X0),domain(X0))
| ~ product(domain(X0),domain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1748]) ).
fof(f1772,plain,
! [X0,X1] :
( product(domain(X0),X1,domain(domain(X0)))
| ~ product(domain(X0),domain(domain(X0)),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1159]) ).
fof(f1773,plain,
! [X0,X1] :
( product(domain(X0),X1,domain(domain(X0)))
| ~ product(domain(X0),domain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1772]) ).
fof(f1774,plain,
! [X0,X1] :
( product(domain(X0),X1,domain(X0))
| ~ product(domain(X0),domain(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f1155,f1773]) ).
fof(f1798,plain,
! [X0,X1,X2,X3] :
( product(X3,domain(domain(X1)),X2)
| ~ product(X0,domain(X1),X3)
| ~ product(X0,domain(X1),X2) ),
inference(forward_demodulation,[status(thm)],[f1155,f1162]) ).
fof(f1799,plain,
! [X0,X1,X2,X3] :
( product(X3,domain(X1),X2)
| ~ product(X0,domain(X1),X3)
| ~ product(X0,domain(X1),X2) ),
inference(forward_demodulation,[status(thm)],[f1155,f1798]) ).
fof(f1810,plain,
! [X0,X1,X2,X3] :
( product(domain(X0),X3,X2)
| ~ product(domain(domain(X0)),X1,X3)
| ~ product(domain(X0),X1,X2) ),
inference(forward_demodulation,[status(thm)],[f1155,f1166]) ).
fof(f1811,plain,
! [X0,X1,X2,X3] :
( product(domain(X0),X3,X2)
| ~ product(domain(X0),X1,X3)
| ~ product(domain(X0),X1,X2) ),
inference(forward_demodulation,[status(thm)],[f1155,f1810]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT020-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 14:02:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.14/0.42 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.14/0.42 % SZS output start Saturation for theBenchmark
% See solution above
% 0.14/0.45 % Elapsed time: 0.086767 seconds
% 0.14/0.45 % CPU time: 0.483004 seconds
% 0.14/0.45 % Total memory used: 6.696 MB
% 0.14/0.45 % Net memory used: 5.860 MB
%------------------------------------------------------------------------------