%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CAT018-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:44 PM UTC 2026
% Result : Unsatisfiable 0.20s 15.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT018-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.20/15.30 % CPULimit : 300
% 0.20/15.30 % WCLimit : 300
% 0.20/15.30 % DateTime : Mon Sep 21 13:51:44 UTC 2026
% 0.20/15.30 % CPUTime :
% 0.20/15.31 % Drodi V4.1.1
% 0.20/15.34 % Refutation found
% 0.20/15.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.20/15.34 % SZS output start CNFRefutation for theBenchmark
% 0.20/15.34 fof(f1,axiom,(
% 0.20/15.34 (![X,Y]: (( ~ defined(X,Y)| product(X,Y,compose(X,Y)) ) ))),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f4,axiom,(
% 0.20/15.34 (![X,Y,Xy,Z,Yz]: (( ~ product(X,Y,Xy)| ~ product(Y,Z,Yz)| ~ defined(Xy,Z)| defined(X,Yz) ) ))),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f6,axiom,(
% 0.20/15.34 (![Y,Z,Yz,X]: (( ~ product(Y,Z,Yz)| ~ defined(X,Yz)| defined(X,Y) ) ))),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f9,axiom,(
% 0.20/15.34 (![X,Y,Z]: (( ~ defined(X,Y)| ~ defined(Y,Z)| ~ identity_map(Y)| defined(X,Z) ) ))),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f11,axiom,(
% 0.20/15.34 (![X]: (identity_map(codomain(X)) ))),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f15,axiom,(
% 0.20/15.34 (![X]: (product(codomain(X),X,X) ))),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f19,hypothesis,(
% 0.20/15.34 defined(a,b) ),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f20,hypothesis,(
% 0.20/15.34 defined(b,c) ),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f21,negated_conjecture,(
% 0.20/15.34 ~ defined(a,compose(b,c)) ),
% 0.20/15.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/15.34 fof(f22,plain,(
% 0.20/15.34 ![X0,X1]: (~defined(X0,X1)|product(X0,X1,compose(X0,X1)))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f1])).
% 0.20/15.34 fof(f27,plain,(
% 0.20/15.34 ![X,Yz]: ((![Xy,Z]: ((![Y]: (~product(X,Y,Xy)|~product(Y,Z,Yz)))|~defined(Xy,Z)))|defined(X,Yz))),
% 0.20/15.34 inference(miniscoping,[status(thm)],[f4])).
% 0.20/15.34 fof(f28,plain,(
% 0.20/15.34 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~defined(X2,X3)|defined(X0,X4))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f27])).
% 0.20/15.34 fof(f31,plain,(
% 0.20/15.34 ![Y,X]: ((![Yz]: ((![Z]: ~product(Y,Z,Yz))|~defined(X,Yz)))|defined(X,Y))),
% 0.20/15.34 inference(miniscoping,[status(thm)],[f6])).
% 0.20/15.34 fof(f32,plain,(
% 0.20/15.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~defined(X3,X2)|defined(X3,X0))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f31])).
% 0.20/15.34 fof(f37,plain,(
% 0.20/15.34 ![X,Z]: ((![Y]: ((~defined(X,Y)|~defined(Y,Z))|~identity_map(Y)))|defined(X,Z))),
% 0.20/15.34 inference(miniscoping,[status(thm)],[f9])).
% 0.20/15.34 fof(f38,plain,(
% 0.20/15.34 ![X0,X1,X2]: (~defined(X0,X1)|~defined(X1,X2)|~identity_map(X1)|defined(X0,X2))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f37])).
% 0.20/15.34 fof(f40,plain,(
% 0.20/15.34 ![X0]: (identity_map(codomain(X0)))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f11])).
% 0.20/15.34 fof(f44,plain,(
% 0.20/15.34 ![X0]: (product(codomain(X0),X0,X0))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f15])).
% 0.20/15.34 fof(f49,plain,(
% 0.20/15.34 defined(a,b)),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f19])).
% 0.20/15.34 fof(f50,plain,(
% 0.20/15.34 defined(b,c)),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f20])).
% 0.20/15.34 fof(f51,plain,(
% 0.20/15.34 ~defined(a,compose(b,c))),
% 0.20/15.34 inference(cnf_transformation,[status(thm)],[f21])).
% 0.20/15.34 fof(f53,plain,(
% 0.20/15.34 product(b,c,compose(b,c))),
% 0.20/15.34 inference(resolution,[status(thm)],[f50,f22])).
% 0.20/15.34 fof(f70,plain,(
% 0.20/15.34 ![X0,X1]: (~product(X0,b,X1)|~defined(X1,c)|defined(X0,compose(b,c)))),
% 0.20/15.34 inference(resolution,[status(thm)],[f53,f28])).
% 0.20/15.34 fof(f95,plain,(
% 0.20/15.34 ![X0,X1]: (~defined(X0,X1)|defined(X0,codomain(X1)))),
% 0.20/15.34 inference(resolution,[status(thm)],[f44,f32])).
% 0.20/15.34 fof(f118,plain,(
% 0.20/15.34 ![X0,X1,X2]: (~defined(X0,codomain(X1))|~defined(codomain(X1),X2)|defined(X0,X2))),
% 0.20/15.34 inference(resolution,[status(thm)],[f38,f40])).
% 0.20/15.34 fof(f362,plain,(
% 0.20/15.34 ![X0]: (~defined(a,codomain(X0))|~defined(codomain(X0),compose(b,c)))),
% 0.20/15.34 inference(resolution,[status(thm)],[f118,f51])).
% 0.20/15.34 fof(f386,plain,(
% 0.20/15.34 ![X0]: (~defined(codomain(X0),compose(b,c))|~defined(a,X0))),
% 0.20/15.34 inference(resolution,[status(thm)],[f362,f95])).
% 0.20/15.34 fof(f399,plain,(
% 0.20/15.34 ~defined(b,c)|defined(codomain(b),compose(b,c))),
% 0.20/15.34 inference(resolution,[status(thm)],[f70,f44])).
% 0.20/15.34 fof(f403,plain,(
% 0.20/15.34 defined(codomain(b),compose(b,c))),
% 0.20/15.34 inference(forward_subsumption_resolution,[status(thm)],[f399,f50])).
% 0.20/15.34 fof(f456,plain,(
% 0.20/15.34 ~defined(a,b)),
% 0.20/15.34 inference(resolution,[status(thm)],[f386,f403])).
% 0.20/15.34 fof(f463,plain,(
% 0.20/15.34 $false),
% 0.20/15.34 inference(forward_subsumption_resolution,[status(thm)],[f456,f49])).
% 0.20/15.34 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/15.37 % Elapsed time: 0.052497 seconds
% 0.20/15.37 % CPU time: 0.214156 seconds
% 0.20/15.37 % Total memory used: 46.203 MB
% 0.20/15.37 % Net memory used: 45.624 MB
%------------------------------------------------------------------------------