%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CAT004-2 : 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 : n015.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:41 PM UTC 2026
% Result : Unsatisfiable 0.15s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT004-2 : 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.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 13:58:36 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 0.15/0.46 % Refutation found
% 0.15/0.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.46 fof(f1,axiom,(
% 0.15/0.46 (![X]: (codomain(domain(X)) = domain(X) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f2,axiom,(
% 0.15/0.46 (![X]: (domain(codomain(X)) = codomain(X) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f3,axiom,(
% 0.15/0.46 (![X]: (compose(domain(X),X) = X ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f4,axiom,(
% 0.15/0.46 (![X]: (compose(X,codomain(X)) = X ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f5,axiom,(
% 0.15/0.46 (![X,Y]: (( codomain(X) != domain(Y)| domain(compose(X,Y)) = domain(X) ) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f6,axiom,(
% 0.15/0.46 (![X,Y]: (( codomain(X) != domain(Y)| codomain(compose(X,Y)) = codomain(Y) ) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f7,axiom,(
% 0.15/0.46 (![X,Y,Z]: (( codomain(X) != domain(Y)| codomain(Y) != domain(Z)| compose(X,compose(Y,Z)) = compose(compose(X,Y),Z) ) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f8,hypothesis,(
% 0.15/0.46 (![X,Y,Z]: (( codomain(a) != domain(X)| compose(a,X) != Y| codomain(a) != domain(Z)| compose(a,Z) != Y| X = Z ) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f9,hypothesis,(
% 0.15/0.46 (![X,Y,Z]: (( codomain(b) != domain(X)| compose(b,X) != Y| codomain(b) != domain(Z)| compose(b,Z) != Y| X = Z ) ))),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f10,hypothesis,(
% 0.15/0.46 codomain(a) = domain(b) ),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f11,hypothesis,(
% 0.15/0.46 codomain(compose(a,b)) = domain(h) ),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f12,hypothesis,(
% 0.15/0.46 codomain(compose(a,b)) = domain(g) ),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f13,hypothesis,(
% 0.15/0.46 compose(compose(a,b),h) = compose(compose(a,b),g) ),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f14,negated_conjecture,(
% 0.15/0.46 h != g ),
% 0.15/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f15,plain,(
% 0.15/0.46 ![X0]: (codomain(domain(X0))=domain(X0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f1])).
% 0.15/0.46 fof(f16,plain,(
% 0.15/0.46 ![X0]: (domain(codomain(X0))=codomain(X0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.46 fof(f17,plain,(
% 0.15/0.46 ![X0]: (compose(domain(X0),X0)=X0)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.46 fof(f18,plain,(
% 0.15/0.46 ![X0]: (compose(X0,codomain(X0))=X0)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.46 fof(f19,plain,(
% 0.15/0.46 ![X0,X1]: (~codomain(X0)=domain(X1)|domain(compose(X0,X1))=domain(X0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/0.46 fof(f20,plain,(
% 0.15/0.46 ![X0,X1]: (~codomain(X0)=domain(X1)|codomain(compose(X0,X1))=codomain(X1))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/0.46 fof(f21,plain,(
% 0.15/0.46 ![X0,X1,X2]: (~codomain(X0)=domain(X1)|~codomain(X1)=domain(X2)|compose(X0,compose(X1,X2))=compose(compose(X0,X1),X2))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f7])).
% 0.15/0.46 fof(f22,plain,(
% 0.15/0.46 ![X,Z]: ((![Y]: (((~codomain(a)=domain(X)|~compose(a,X)=Y)|~codomain(a)=domain(Z))|~compose(a,Z)=Y))|X=Z)),
% 0.15/0.46 inference(miniscoping,[status(thm)],[f8])).
% 0.15/0.46 fof(f23,plain,(
% 0.15/0.46 ![X0,X1,X2]: (~codomain(a)=domain(X0)|~compose(a,X0)=X1|~codomain(a)=domain(X2)|~compose(a,X2)=X1|X0=X2)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f22])).
% 0.15/0.46 fof(f24,plain,(
% 0.15/0.46 ![X,Z]: ((![Y]: (((~codomain(b)=domain(X)|~compose(b,X)=Y)|~codomain(b)=domain(Z))|~compose(b,Z)=Y))|X=Z)),
% 0.15/0.46 inference(miniscoping,[status(thm)],[f9])).
% 0.15/0.46 fof(f25,plain,(
% 0.15/0.46 ![X0,X1,X2]: (~codomain(b)=domain(X0)|~compose(b,X0)=X1|~codomain(b)=domain(X2)|~compose(b,X2)=X1|X0=X2)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f24])).
% 0.15/0.46 fof(f26,plain,(
% 0.15/0.46 codomain(a)=domain(b)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.15/0.46 fof(f27,plain,(
% 0.15/0.46 codomain(compose(a,b))=domain(h)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f11])).
% 0.15/0.46 fof(f28,plain,(
% 0.15/0.46 codomain(compose(a,b))=domain(g)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f12])).
% 0.15/0.46 fof(f29,plain,(
% 0.15/0.46 compose(compose(a,b),h)=compose(compose(a,b),g)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f13])).
% 0.15/0.46 fof(f30,plain,(
% 0.15/0.46 ~h=g),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f14])).
% 0.15/0.46 fof(f31,plain,(
% 0.15/0.46 ![X0,X1]: (~codomain(a)=domain(X0)|~codomain(a)=domain(X1)|~compose(a,X1)=compose(a,X0)|X0=X1)),
% 0.15/0.46 inference(destructive_equality_resolution,[status(thm)],[f23])).
% 0.15/0.46 fof(f32,plain,(
% 0.15/0.46 ![X0,X1]: (~codomain(b)=domain(X0)|~codomain(b)=domain(X1)|~compose(b,X1)=compose(b,X0)|X0=X1)),
% 0.15/0.46 inference(destructive_equality_resolution,[status(thm)],[f25])).
% 0.15/0.46 fof(f33,plain,(
% 0.15/0.46 domain(h)=domain(g)),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f27,f28])).
% 0.15/0.46 fof(f39,plain,(
% 0.15/0.46 ![X0]: (domain(domain(X0))=codomain(domain(X0)))),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f15,f16])).
% 0.15/0.46 fof(f43,plain,(
% 0.15/0.46 ![X0]: (domain(domain(X0))=domain(X0))),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f15,f39])).
% 0.15/0.46 fof(f196,plain,(
% 0.15/0.46 ~codomain(a)=domain(b)|domain(h)=codomain(b)),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f27,f20])).
% 0.15/0.46 fof(f205,definition,(
% 0.15/0.46 sQ11_spl <=> (codomain(a)=domain(b))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f207,plain,(
% 0.15/0.46 ~codomain(a)=domain(b)|sQ11_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f205])).
% 0.15/0.46 fof(f208,definition,(
% 0.15/0.46 sQ12_spl <=> (domain(h)=codomain(b))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f209,plain,(
% 0.15/0.46 domain(h)=codomain(b)|~sQ12_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f208])).
% 0.15/0.46 fof(f211,plain,(
% 0.15/0.46 ~sQ11_spl|sQ12_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f196,f205,f208])).
% 0.15/0.46 fof(f231,plain,(
% 0.15/0.46 ~domain(b)=domain(b)|sQ11_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f26,f207])).
% 0.15/0.46 fof(f232,plain,(
% 0.15/0.46 $false|sQ11_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f231])).
% 0.15/0.46 fof(f233,plain,(
% 0.15/0.46 sQ11_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f232])).
% 0.15/0.46 fof(f238,plain,(
% 0.15/0.46 compose(b,domain(h))=b|~sQ12_spl),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f209,f18])).
% 0.15/0.46 fof(f246,plain,(
% 0.15/0.46 ~codomain(a)=domain(b)|~codomain(b)=domain(g)|compose(a,compose(b,g))=compose(compose(a,b),h)),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f29,f21])).
% 0.15/0.46 fof(f252,plain,(
% 0.15/0.46 ![X0,X1]: (~codomain(domain(X0))=domain(X0)|~codomain(X0)=domain(X1)|compose(domain(X0),compose(X0,X1))=compose(X0,X1))),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f17,f21])).
% 0.15/0.46 fof(f263,definition,(
% 0.15/0.46 sQ19_spl <=> (codomain(b)=domain(g))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f265,plain,(
% 0.15/0.46 ~codomain(b)=domain(g)|sQ19_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f263])).
% 0.15/0.46 fof(f266,definition,(
% 0.15/0.46 sQ20_spl <=> (compose(a,compose(b,g))=compose(compose(a,b),h))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f267,plain,(
% 0.15/0.46 compose(a,compose(b,g))=compose(compose(a,b),h)|~sQ20_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f266])).
% 0.15/0.46 fof(f269,plain,(
% 0.15/0.46 ~sQ11_spl|~sQ19_spl|sQ20_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f246,f205,f263,f266])).
% 0.15/0.46 fof(f288,plain,(
% 0.15/0.46 ![X0,X1]: (~domain(X0)=domain(X0)|~codomain(X0)=domain(X1)|compose(domain(X0),compose(X0,X1))=compose(X0,X1))),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f15,f252])).
% 0.15/0.46 fof(f289,plain,(
% 0.15/0.46 ![X0,X1]: (~codomain(X0)=domain(X1)|compose(domain(X0),compose(X0,X1))=compose(X0,X1))),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f288])).
% 0.15/0.46 fof(f307,plain,(
% 0.15/0.46 ~domain(h)=domain(g)|~sQ12_spl|sQ19_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f209,f265])).
% 0.15/0.46 fof(f308,plain,(
% 0.15/0.46 ~domain(h)=domain(h)|~sQ12_spl|sQ19_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f33,f307])).
% 0.15/0.46 fof(f309,plain,(
% 0.15/0.46 $false|~sQ12_spl|sQ19_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f308])).
% 0.15/0.46 fof(f310,plain,(
% 0.15/0.46 ~sQ12_spl|sQ19_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f309])).
% 0.15/0.46 fof(f313,plain,(
% 0.15/0.46 ![X0,X1]: (~domain(b)=domain(X0)|~codomain(a)=domain(X1)|~compose(a,X1)=compose(a,X0)|X0=X1)),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f26,f31])).
% 0.15/0.46 fof(f314,plain,(
% 0.15/0.46 ![X0,X1]: (~domain(b)=domain(X0)|~domain(b)=domain(X1)|~compose(a,X1)=compose(a,X0)|X0=X1)),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f26,f313])).
% 0.15/0.46 fof(f337,plain,(
% 0.15/0.46 ![X0,X1]: (~domain(h)=domain(X0)|~codomain(b)=domain(X1)|~compose(b,X1)=compose(b,X0)|X0=X1|~sQ12_spl)),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f209,f32])).
% 0.15/0.46 fof(f338,plain,(
% 0.15/0.46 ![X0,X1]: (~domain(h)=domain(X0)|~domain(h)=domain(X1)|~compose(b,X1)=compose(b,X0)|X0=X1|~sQ12_spl)),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f209,f337])).
% 0.15/0.46 fof(f351,plain,(
% 0.15/0.46 ![X0]: (~domain(h)=domain(domain(h))|~domain(h)=domain(X0)|~compose(b,X0)=b|domain(h)=X0|~sQ12_spl)),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f238,f338])).
% 0.15/0.46 fof(f356,definition,(
% 0.15/0.46 sQ31_spl <=> (domain(h)=domain(domain(h)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f358,plain,(
% 0.15/0.46 ~domain(h)=domain(domain(h))|sQ31_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f356])).
% 0.15/0.46 fof(f359,definition,(
% 0.15/0.46 ![X0]: (sQ32_spl <=> (~domain(h)=domain(X0)|~compose(b,X0)=b|domain(h)=X0))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f360,plain,(
% 0.15/0.46 ![X0]: (~domain(h)=domain(X0)|~compose(b,X0)=b|domain(h)=X0|~sQ32_spl)),
% 0.15/0.46 inference(component_clause,[status(thm)],[f359])).
% 0.15/0.46 fof(f362,plain,(
% 0.15/0.46 ~sQ31_spl|sQ32_spl|~sQ12_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f351,f356,f359,f208])).
% 0.15/0.46 fof(f378,plain,(
% 0.15/0.46 ~domain(h)=domain(h)|sQ31_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f43,f358])).
% 0.15/0.46 fof(f379,plain,(
% 0.15/0.46 $false|sQ31_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f378])).
% 0.15/0.46 fof(f380,plain,(
% 0.15/0.46 sQ31_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f379])).
% 0.15/0.46 fof(f473,definition,(
% 0.15/0.46 sQ44_spl <=> (domain(h)=domain(h))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f488,plain,(
% 0.15/0.46 ~domain(h)=domain(domain(h))|domain(h)=domain(h)|~sQ32_spl|~sQ12_spl),
% 0.15/0.46 inference(resolution,[status(thm)],[f360,f238])).
% 0.15/0.46 fof(f492,plain,(
% 0.15/0.46 ~sQ31_spl|sQ44_spl|~sQ32_spl|~sQ12_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f488,f356,f473,f359,f208])).
% 0.15/0.46 fof(f500,plain,(
% 0.15/0.46 ~codomain(a)=domain(b)|~codomain(b)=domain(h)|compose(a,compose(b,h))=compose(a,compose(b,g))|~sQ20_spl),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f267,f21])).
% 0.15/0.46 fof(f504,definition,(
% 0.15/0.46 sQ46_spl <=> (compose(a,compose(b,h))=compose(a,compose(b,g)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f505,plain,(
% 0.15/0.46 compose(a,compose(b,h))=compose(a,compose(b,g))|~sQ46_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f504])).
% 0.15/0.46 fof(f507,plain,(
% 0.15/0.46 ~sQ11_spl|~sQ12_spl|sQ46_spl|~sQ20_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f500,f205,f208,f504,f266])).
% 0.15/0.46 fof(f526,definition,(
% 0.15/0.46 sQ50_spl <=> (codomain(a)=domain(compose(b,g)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f527,plain,(
% 0.15/0.46 codomain(a)=domain(compose(b,g))|~sQ50_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f526])).
% 0.15/0.46 fof(f528,plain,(
% 0.15/0.46 ~codomain(a)=domain(compose(b,g))|sQ50_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f526])).
% 0.15/0.46 fof(f539,plain,(
% 0.15/0.46 ~domain(b)=domain(compose(b,g))|sQ50_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f26,f528])).
% 0.15/0.46 fof(f574,plain,(
% 0.15/0.46 ~codomain(b)=domain(g)|sQ50_spl),
% 0.15/0.46 inference(resolution,[status(thm)],[f539,f19])).
% 0.15/0.46 fof(f575,plain,(
% 0.15/0.46 ~sQ19_spl|sQ50_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f574,f263,f526])).
% 0.15/0.46 fof(f576,plain,(
% 0.15/0.46 domain(b)=domain(compose(b,g))|~sQ50_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f26,f527])).
% 0.15/0.46 fof(f662,plain,(
% 0.15/0.46 compose(domain(b),compose(b,h))=compose(b,h)|~sQ12_spl),
% 0.15/0.46 inference(resolution,[status(thm)],[f289,f209])).
% 0.15/0.46 fof(f723,plain,(
% 0.15/0.46 ~codomain(domain(b))=domain(compose(b,h))|domain(compose(b,h))=domain(domain(b))|~sQ12_spl),
% 0.15/0.46 inference(paramodulation,[status(thm)],[f662,f19])).
% 0.15/0.46 fof(f724,definition,(
% 0.15/0.46 sQ70_spl <=> (codomain(domain(b))=domain(compose(b,h)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f726,plain,(
% 0.15/0.46 ~codomain(domain(b))=domain(compose(b,h))|sQ70_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f724])).
% 0.15/0.46 fof(f735,definition,(
% 0.15/0.46 sQ73_spl <=> (domain(compose(b,h))=domain(domain(b)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f736,plain,(
% 0.15/0.46 domain(compose(b,h))=domain(domain(b))|~sQ73_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f735])).
% 0.15/0.46 fof(f738,plain,(
% 0.15/0.46 ~sQ70_spl|sQ73_spl|~sQ12_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f723,f724,f735,f208])).
% 0.15/0.46 fof(f739,plain,(
% 0.15/0.46 ~domain(b)=domain(compose(b,h))|sQ70_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f15,f726])).
% 0.15/0.46 fof(f810,plain,(
% 0.15/0.46 ~codomain(b)=domain(h)|sQ70_spl),
% 0.15/0.46 inference(resolution,[status(thm)],[f739,f19])).
% 0.15/0.46 fof(f811,plain,(
% 0.15/0.46 ~domain(h)=domain(h)|~sQ12_spl|sQ70_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f209,f810])).
% 0.15/0.46 fof(f812,plain,(
% 0.15/0.46 $false|~sQ12_spl|sQ70_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f811])).
% 0.15/0.46 fof(f813,plain,(
% 0.15/0.46 ~sQ12_spl|sQ70_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f812])).
% 0.15/0.46 fof(f814,plain,(
% 0.15/0.46 domain(compose(b,h))=domain(b)|~sQ73_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f43,f736])).
% 0.15/0.46 fof(f854,plain,(
% 0.15/0.46 ~domain(b)=domain(compose(b,g))|~domain(b)=domain(compose(b,h))|compose(b,g)=compose(b,h)|~sQ46_spl),
% 0.15/0.46 inference(resolution,[status(thm)],[f505,f314])).
% 0.15/0.46 fof(f861,definition,(
% 0.15/0.46 sQ75_spl <=> (domain(b)=domain(compose(b,g)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f863,plain,(
% 0.15/0.46 ~domain(b)=domain(compose(b,g))|sQ75_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f861])).
% 0.15/0.46 fof(f864,definition,(
% 0.15/0.46 sQ76_spl <=> (domain(b)=domain(compose(b,h)))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f866,plain,(
% 0.15/0.46 ~domain(b)=domain(compose(b,h))|sQ76_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f864])).
% 0.15/0.46 fof(f867,definition,(
% 0.15/0.46 sQ77_spl <=> (compose(b,g)=compose(b,h))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f868,plain,(
% 0.15/0.46 compose(b,g)=compose(b,h)|~sQ77_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f867])).
% 0.15/0.46 fof(f870,plain,(
% 0.15/0.46 ~sQ75_spl|~sQ76_spl|sQ77_spl|~sQ46_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f854,f861,f864,f867,f504])).
% 0.15/0.46 fof(f889,plain,(
% 0.15/0.46 ~domain(b)=domain(b)|~sQ50_spl|sQ75_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f576,f863])).
% 0.15/0.46 fof(f890,plain,(
% 0.15/0.46 $false|~sQ50_spl|sQ75_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f889])).
% 0.15/0.46 fof(f891,plain,(
% 0.15/0.46 ~sQ50_spl|sQ75_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f890])).
% 0.15/0.46 fof(f894,plain,(
% 0.15/0.46 ~domain(b)=domain(b)|~sQ73_spl|sQ76_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f814,f866])).
% 0.15/0.46 fof(f895,plain,(
% 0.15/0.46 $false|~sQ73_spl|sQ76_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f894])).
% 0.15/0.46 fof(f896,plain,(
% 0.15/0.46 ~sQ73_spl|sQ76_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f895])).
% 0.15/0.46 fof(f902,plain,(
% 0.15/0.46 ~domain(h)=domain(h)|~domain(h)=domain(g)|h=g|~sQ77_spl|~sQ12_spl),
% 0.15/0.46 inference(resolution,[status(thm)],[f868,f338])).
% 0.15/0.46 fof(f912,definition,(
% 0.15/0.46 sQ82_spl <=> (domain(h)=domain(g))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f914,plain,(
% 0.15/0.46 ~domain(h)=domain(g)|sQ82_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f912])).
% 0.15/0.46 fof(f915,definition,(
% 0.15/0.46 sQ83_spl <=> (h=g)),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f916,plain,(
% 0.15/0.46 h=g|~sQ83_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f915])).
% 0.15/0.46 fof(f918,plain,(
% 0.15/0.46 ~sQ44_spl|~sQ82_spl|sQ83_spl|~sQ77_spl|~sQ12_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f902,f473,f912,f915,f867,f208])).
% 0.15/0.46 fof(f941,plain,(
% 0.15/0.46 ~domain(h)=domain(h)|sQ82_spl),
% 0.15/0.46 inference(forward_demodulation,[status(thm)],[f33,f914])).
% 0.15/0.46 fof(f942,plain,(
% 0.15/0.46 $false|sQ82_spl),
% 0.15/0.46 inference(trivial_equality_resolution,[status(thm)],[f941])).
% 0.15/0.46 fof(f943,plain,(
% 0.15/0.46 sQ82_spl),
% 0.15/0.46 inference(contradiction_clause,[status(thm)],[f942])).
% 0.15/0.46 fof(f946,plain,(
% 0.15/0.46 $false|~sQ83_spl),
% 0.15/0.46 inference(forward_subsumption_resolution,[status(thm)],[f916,f30])).
% 0.15/0.47 fof(f947,plain,(
% 0.15/0.47 ~sQ83_spl),
% 0.15/0.47 inference(contradiction_clause,[status(thm)],[f946])).
% 0.15/0.47 fof(f948,plain,(
% 0.15/0.47 $false),
% 0.15/0.47 inference(sat_refutation,[status(thm)],[f211,f233,f269,f310,f362,f380,f492,f507,f575,f738,f813,f870,f891,f896,f918,f943,f947])).
% 0.15/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.48 % Elapsed time: 0.104682 seconds
% 0.15/0.48 % CPU time: 0.505484 seconds
% 0.15/0.48 % Total memory used: 76.940 MB
% 0.15/0.48 % Net memory used: 75.994 MB
%------------------------------------------------------------------------------