%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CAT004-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:26 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.39s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 27
% Syntax : Number of formulae : 107 ( 24 unt; 14 def)
% Number of atoms : 259 ( 151 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 287 ( 135 ~; 138 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 15 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 55 ( 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : codomain(domain(X)) = domain(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : domain(codomain(X)) = codomain(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : compose(X,codomain(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] :
( domain(compose(X,Y)) = domain(X)
| codomain(X) != domain(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( codomain(compose(X,Y)) = codomain(Y)
| codomain(X) != domain(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] :
( compose(X,compose(Y,Z)) = compose(compose(X,Y),Z)
| codomain(Y) != domain(Z)
| codomain(X) != domain(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
! [X,Y,Z] :
( X = Z
| compose(a,Z) != Y
| codomain(a) != domain(Z)
| compose(a,X) != Y
| codomain(a) != domain(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
! [X,Y,Z] :
( X = Z
| compose(b,Z) != Y
| codomain(b) != domain(Z)
| compose(b,X) != Y
| codomain(b) != domain(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
codomain(a) = domain(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
codomain(compose(a,b)) = domain(h),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
codomain(compose(a,b)) = domain(g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
compose(compose(a,b),h) = compose(compose(a,b),g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
h != g,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,plain,
! [X0] : codomain(domain(X0)) = domain(X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f16,plain,
! [X0] : domain(codomain(X0)) = codomain(X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [X0] : compose(X0,codomain(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f19,plain,
! [X0,X1] :
( domain(compose(X0,X1)) = domain(X0)
| codomain(X0) != domain(X1) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f20,plain,
! [X0,X1] :
( codomain(compose(X0,X1)) = codomain(X1)
| codomain(X0) != domain(X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f21,plain,
! [X0,X1,X2] :
( compose(X0,compose(X1,X2)) = compose(compose(X0,X1),X2)
| codomain(X1) != domain(X2)
| codomain(X0) != domain(X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f22,plain,
! [X,Z] :
( X = Z
| ! [Y] :
( compose(a,Z) != Y
| codomain(a) != domain(Z)
| compose(a,X) != Y
| codomain(a) != domain(X) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f23,plain,
! [X0,X1,X2] :
( X0 = X2
| compose(a,X2) != X1
| codomain(a) != domain(X2)
| compose(a,X0) != X1
| codomain(a) != domain(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X,Z] :
( X = Z
| ! [Y] :
( compose(b,Z) != Y
| codomain(b) != domain(Z)
| compose(b,X) != Y
| codomain(b) != domain(X) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f25,plain,
! [X0,X1,X2] :
( X0 = X2
| compose(b,X2) != X1
| codomain(b) != domain(X2)
| compose(b,X0) != X1
| codomain(b) != domain(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
codomain(a) = domain(b),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f27,plain,
codomain(compose(a,b)) = domain(h),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f28,plain,
codomain(compose(a,b)) = domain(g),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f29,plain,
compose(compose(a,b),h) = compose(compose(a,b),g),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f30,plain,
h != g,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f31,plain,
! [X0,X1] :
( X0 = X1
| compose(a,X1) != compose(a,X0)
| codomain(a) != domain(X1)
| codomain(a) != domain(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f23]) ).
fof(f32,plain,
! [X0,X1] :
( X0 = X1
| compose(b,X1) != compose(b,X0)
| codomain(b) != domain(X1)
| codomain(b) != domain(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f25]) ).
fof(f34,plain,
! [X0] : domain(domain(X0)) = codomain(domain(X0)),
inference(paramodulation,[status(thm)],[f15,f16]) ).
fof(f37,plain,
! [X0] : domain(domain(X0)) = domain(X0),
inference(forward_demodulation,[status(thm)],[f15,f34]) ).
fof(f110,plain,
( domain(h) = codomain(b)
| codomain(a) != domain(b) ),
inference(paramodulation,[status(thm)],[f27,f20]) ).
fof(f116,definition,
( sQ3_spl
<=> codomain(a) = domain(b) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f118,plain,
( sQ3_spl
| codomain(a) != domain(b) ),
inference(component_clause,[status(thm)],[f116]) ).
fof(f119,definition,
( sQ4_spl
<=> domain(h) = codomain(b) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f120,plain,
( ~ sQ4_spl
| domain(h) = codomain(b) ),
inference(component_clause,[status(thm)],[f119]) ).
fof(f122,plain,
( sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f110,f116,f119]) ).
fof(f129,plain,
( sQ3_spl
| domain(b) != domain(b) ),
inference(forward_demodulation,[status(thm)],[f26,f118]) ).
fof(f130,plain,
( sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f129]) ).
fof(f131,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f130]) ).
fof(f136,plain,
( ~ sQ4_spl
| compose(b,domain(h)) = b ),
inference(paramodulation,[status(thm)],[f120,f18]) ).
fof(f194,plain,
domain(h) = domain(g),
inference(forward_demodulation,[status(thm)],[f27,f28]) ).
fof(f317,plain,
! [X0,X1] :
( X0 = X1
| compose(a,X1) != compose(a,X0)
| codomain(a) != domain(X1)
| domain(b) != domain(X0) ),
inference(forward_demodulation,[status(thm)],[f26,f31]) ).
fof(f318,plain,
! [X0,X1] :
( X0 = X1
| compose(a,X1) != compose(a,X0)
| domain(b) != domain(X1)
| domain(b) != domain(X0) ),
inference(forward_demodulation,[status(thm)],[f26,f317]) ).
fof(f378,plain,
( compose(a,compose(b,g)) = compose(compose(a,b),h)
| codomain(b) != domain(g)
| codomain(a) != domain(b) ),
inference(paramodulation,[status(thm)],[f29,f21]) ).
fof(f383,definition,
( sQ28_spl
<=> codomain(b) = domain(g) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( sQ28_spl
| codomain(b) != domain(g) ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f386,definition,
( sQ29_spl
<=> compose(a,compose(b,g)) = compose(compose(a,b),h) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( ~ sQ29_spl
| compose(a,compose(b,g)) = compose(compose(a,b),h) ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f389,plain,
( sQ29_spl
| ~ sQ28_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f378,f116,f383,f386]) ).
fof(f413,plain,
( sQ28_spl
| ~ sQ4_spl
| domain(h) != domain(g) ),
inference(forward_demodulation,[status(thm)],[f120,f385]) ).
fof(f414,plain,
( sQ28_spl
| ~ sQ4_spl
| domain(h) != domain(h) ),
inference(forward_demodulation,[status(thm)],[f194,f413]) ).
fof(f415,plain,
( sQ28_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f414]) ).
fof(f416,plain,
( sQ28_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f415]) ).
fof(f458,plain,
! [X0,X1] :
( ~ sQ4_spl
| X0 = X1
| compose(b,X1) != compose(b,X0)
| codomain(b) != domain(X1)
| domain(h) != domain(X0) ),
inference(forward_demodulation,[status(thm)],[f120,f32]) ).
fof(f459,plain,
! [X0,X1] :
( ~ sQ4_spl
| X0 = X1
| compose(b,X1) != compose(b,X0)
| domain(h) != domain(X1)
| domain(h) != domain(X0) ),
inference(forward_demodulation,[status(thm)],[f120,f458]) ).
fof(f462,plain,
! [X0] :
( ~ sQ4_spl
| X0 = domain(h)
| b != compose(b,X0)
| domain(h) != domain(domain(h))
| domain(h) != domain(X0) ),
inference(paramodulation,[status(thm)],[f136,f459]) ).
fof(f475,definition,
! [X0] :
( sQ37_spl
<=> ( X0 = domain(h)
| b != compose(b,X0)
| domain(h) != domain(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f476,plain,
! [X0] :
( ~ sQ37_spl
| X0 = domain(h)
| b != compose(b,X0)
| domain(h) != domain(X0) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ38_spl
<=> domain(h) = domain(domain(h)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f480,plain,
( sQ38_spl
| domain(h) != domain(domain(h)) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( ~ sQ4_spl
| ~ sQ38_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f462,f475,f478,f119]) ).
fof(f541,plain,
( ~ sQ4_spl
| ~ sQ37_spl
| domain(h) = domain(h)
| domain(h) != domain(domain(h)) ),
inference(resolution,[status(thm)],[f476,f136]) ).
fof(f545,definition,
( sQ47_spl
<=> domain(h) = domain(h) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( ~ sQ4_spl
| ~ sQ37_spl
| sQ47_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f541,f478,f545,f475,f119]) ).
fof(f555,plain,
( sQ38_spl
| domain(h) != domain(h) ),
inference(forward_demodulation,[status(thm)],[f37,f480]) ).
fof(f556,plain,
( sQ38_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f555]) ).
fof(f557,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f556]) ).
fof(f653,plain,
( ~ sQ29_spl
| compose(a,compose(b,h)) = compose(a,compose(b,g))
| codomain(b) != domain(h)
| codomain(a) != domain(b) ),
inference(paramodulation,[status(thm)],[f387,f21]) ).
fof(f659,definition,
( sQ56_spl
<=> compose(a,compose(b,h)) = compose(a,compose(b,g)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( ~ sQ56_spl
| compose(a,compose(b,h)) = compose(a,compose(b,g)) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f662,plain,
( ~ sQ29_spl
| sQ56_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f653,f116,f119,f659,f386]) ).
fof(f693,definition,
( sQ62_spl
<=> codomain(a) = domain(compose(b,g)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f694,plain,
( ~ sQ62_spl
| codomain(a) = domain(compose(b,g)) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f695,plain,
( sQ62_spl
| codomain(a) != domain(compose(b,g)) ),
inference(component_clause,[status(thm)],[f693]) ).
fof(f711,plain,
( sQ62_spl
| domain(b) != domain(compose(b,g)) ),
inference(forward_demodulation,[status(thm)],[f26,f695]) ).
fof(f712,plain,
( sQ62_spl
| codomain(b) != domain(g) ),
inference(resolution,[status(thm)],[f711,f19]) ).
fof(f713,plain,
( sQ62_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f712,f383,f693]) ).
fof(f714,plain,
( ~ sQ62_spl
| domain(b) = domain(compose(b,g)) ),
inference(forward_demodulation,[status(thm)],[f26,f694]) ).
fof(f971,plain,
( ~ sQ56_spl
| compose(b,g) = compose(b,h)
| domain(b) != domain(compose(b,h))
| domain(b) != domain(compose(b,g)) ),
inference(resolution,[status(thm)],[f660,f318]) ).
fof(f981,definition,
( sQ94_spl
<=> domain(b) = domain(compose(b,g)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f983,plain,
( sQ94_spl
| domain(b) != domain(compose(b,g)) ),
inference(component_clause,[status(thm)],[f981]) ).
fof(f984,definition,
( sQ95_spl
<=> domain(b) = domain(compose(b,h)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f986,plain,
( sQ95_spl
| domain(b) != domain(compose(b,h)) ),
inference(component_clause,[status(thm)],[f984]) ).
fof(f987,definition,
( sQ96_spl
<=> compose(b,g) = compose(b,h) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f988,plain,
( ~ sQ96_spl
| compose(b,g) = compose(b,h) ),
inference(component_clause,[status(thm)],[f987]) ).
fof(f990,plain,
( ~ sQ56_spl
| sQ96_spl
| ~ sQ95_spl
| ~ sQ94_spl ),
inference(split_clause,[status(thm)],[f971,f981,f984,f987,f659]) ).
fof(f1024,plain,
( sQ94_spl
| ~ sQ62_spl
| domain(b) != domain(b) ),
inference(forward_demodulation,[status(thm)],[f714,f983]) ).
fof(f1025,plain,
( sQ94_spl
| ~ sQ62_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1024]) ).
fof(f1026,plain,
( sQ94_spl
| ~ sQ62_spl ),
inference(contradiction_clause,[status(thm)],[f1025]) ).
fof(f1031,plain,
( sQ95_spl
| codomain(b) != domain(h) ),
inference(resolution,[status(thm)],[f986,f19]) ).
fof(f1032,plain,
( sQ95_spl
| ~ sQ4_spl
| domain(h) != domain(h) ),
inference(forward_demodulation,[status(thm)],[f120,f1031]) ).
fof(f1033,plain,
( sQ95_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1032]) ).
fof(f1034,plain,
( sQ95_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1033]) ).
fof(f1040,plain,
( ~ sQ4_spl
| ~ sQ96_spl
| h = g
| domain(h) != domain(g)
| domain(h) != domain(h) ),
inference(resolution,[status(thm)],[f988,f459]) ).
fof(f1052,definition,
( sQ105_spl
<=> domain(h) = domain(g) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( sQ105_spl
| domain(h) != domain(g) ),
inference(component_clause,[status(thm)],[f1052]) ).
fof(f1055,definition,
( sQ106_spl
<=> h = g ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1056,plain,
( ~ sQ106_spl
| h = g ),
inference(component_clause,[status(thm)],[f1055]) ).
fof(f1058,plain,
( ~ sQ4_spl
| ~ sQ96_spl
| sQ106_spl
| ~ sQ105_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f1040,f545,f1052,f1055,f987,f119]) ).
fof(f1089,plain,
( sQ105_spl
| domain(h) != domain(h) ),
inference(forward_demodulation,[status(thm)],[f194,f1054]) ).
fof(f1090,plain,
( sQ105_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1089]) ).
fof(f1091,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f1090]) ).
fof(f1096,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1056,f30]) ).
fof(f1097,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1096]) ).
fof(f1098,plain,
$false,
inference(sat_refutation,[status(thm)],[f122,f131,f389,f416,f481,f548,f557,f662,f713,f990,f1026,f1034,f1058,f1091,f1097]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CAT004-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 13:56:18 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.42 % Elapsed time: 0.052817 seconds
% 0.12/0.42 % CPU time: 0.209823 seconds
% 0.12/0.42 % Total memory used: 69.506 MB
% 0.12/0.42 % Net memory used: 69.061 MB
%------------------------------------------------------------------------------