%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM016+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:10:43 PM UTC 2026
% Result : Theorem 0.13s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM016+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n002.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 14:17:04 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.38 % Refutation found
% 0.13/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.38 fof(f17,hypothesis,(
% 0.13/0.38 ( aElement0(xa)& aElement0(xb)& aElement0(xc) ) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f19,hypothesis,(
% 0.13/0.38 ( ( aReductOfIn0(xb,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xb) ) ))& sdtmndtplgtdt0(xa,xR,xb)& ( aReductOfIn0(xc,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xc) ) ))& sdtmndtplgtdt0(xa,xR,xc) ) ),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f20,conjecture,(
% 0.13/0.38 (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& ( W0 = xb| aReductOfIn0(xb,W0,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,W0,xR)& sdtmndtplgtdt0(W1,xR,xb) ))| sdtmndtplgtdt0(W0,xR,xb)| sdtmndtasgtdt0(W0,xR,xb) ) ) )),
% 0.13/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.38 fof(f21,negated_conjecture,(
% 0.13/0.38 ~((? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& ( W0 = xb| aReductOfIn0(xb,W0,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,W0,xR)& sdtmndtplgtdt0(W1,xR,xb) ))| sdtmndtplgtdt0(W0,xR,xb)| sdtmndtasgtdt0(W0,xR,xb) ) ) ))),
% 0.13/0.38 inference(negated_conjecture,[status(cth)],[f20])).
% 0.13/0.38 fof(f117,plain,(
% 0.13/0.38 aElement0(xb)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.38 fof(f178,plain,(
% 0.13/0.38 (((aReductOfIn0(xb,xa,xR)|((aElement0(sK19_skl)&aReductOfIn0(sK19_skl,xa,xR))&sdtmndtplgtdt0(sK19_skl,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb))&(aReductOfIn0(xc,xa,xR)|((aElement0(sK20_skl)&aReductOfIn0(sK20_skl,xa,xR))&sdtmndtplgtdt0(sK20_skl,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc)),
% 0.13/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W0,sK19_skl),skolemize(W0,sK20_skl)],[f19])).
% 0.13/0.38 fof(f179,plain,(
% 0.13/0.38 aReductOfIn0(xb,xa,xR)|aElement0(sK19_skl)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.38 fof(f180,plain,(
% 0.13/0.38 aReductOfIn0(xb,xa,xR)|aReductOfIn0(sK19_skl,xa,xR)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.38 fof(f181,plain,(
% 0.13/0.38 aReductOfIn0(xb,xa,xR)|sdtmndtplgtdt0(sK19_skl,xR,xb)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/0.38 fof(f187,plain,(
% 0.13/0.38 (![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|((((~W0=xb&~aReductOfIn0(xb,W0,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,W0,xR))|~sdtmndtplgtdt0(W1,xR,xb))))&~sdtmndtplgtdt0(W0,xR,xb))&~sdtmndtasgtdt0(W0,xR,xb))))),
% 0.13/0.38 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.13/0.38 fof(f188,plain,(
% 0.13/0.38 ![X0]: (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|~X0=xb)),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.38 fof(f191,plain,(
% 0.13/0.38 ![X0]: (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|~sdtmndtplgtdt0(X0,xR,xb))),
% 0.13/0.38 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.38 fof(f204,definition,(
% 0.13/0.38 sQ0_spl <=> (aReductOfIn0(xb,xa,xR))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f205,plain,(
% 0.13/0.38 aReductOfIn0(xb,xa,xR)|~sQ0_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f204])).
% 0.13/0.38 fof(f207,definition,(
% 0.13/0.38 sQ1_spl <=> (aElement0(sK19_skl))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f208,plain,(
% 0.13/0.38 aElement0(sK19_skl)|~sQ1_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f207])).
% 0.13/0.38 fof(f210,plain,(
% 0.13/0.38 sQ0_spl|sQ1_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f179,f204,f207])).
% 0.13/0.38 fof(f211,definition,(
% 0.13/0.38 sQ2_spl <=> (aReductOfIn0(sK19_skl,xa,xR))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f214,plain,(
% 0.13/0.38 sQ0_spl|sQ2_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f180,f204,f211])).
% 0.13/0.38 fof(f215,definition,(
% 0.13/0.38 sQ3_spl <=> (sdtmndtplgtdt0(sK19_skl,xR,xb))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f218,plain,(
% 0.13/0.38 sQ0_spl|sQ3_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f181,f204,f215])).
% 0.13/0.38 fof(f258,plain,(
% 0.13/0.38 ~aElement0(xb)|~aReductOfIn0(xb,xa,xR)),
% 0.13/0.38 inference(destructive_equality_resolution,[status(thm)],[f188])).
% 0.13/0.38 fof(f280,plain,(
% 0.13/0.38 ~aReductOfIn0(xb,xa,xR)),
% 0.13/0.38 inference(backward_subsumption_resolution,[status(thm)],[f258,f117])).
% 0.13/0.38 fof(f343,plain,(
% 0.13/0.38 $false|~sQ0_spl),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f205,f280])).
% 0.13/0.39 fof(f344,plain,(
% 0.13/0.39 ~sQ0_spl),
% 0.13/0.39 inference(contradiction_clause,[status(thm)],[f343])).
% 0.13/0.39 fof(f347,plain,(
% 0.13/0.39 ~aReductOfIn0(sK19_skl,xa,xR)|~sdtmndtplgtdt0(sK19_skl,xR,xb)|~sQ1_spl),
% 0.13/0.39 inference(resolution,[status(thm)],[f208,f191])).
% 0.13/0.39 fof(f357,plain,(
% 0.13/0.39 ~sQ2_spl|~sQ3_spl|~sQ1_spl),
% 0.13/0.39 inference(split_clause,[status(thm)],[f347,f211,f215,f207])).
% 0.13/0.39 fof(f362,plain,(
% 0.13/0.39 $false),
% 0.13/0.39 inference(sat_refutation,[status(thm)],[f210,f214,f218,f344,f357])).
% 0.13/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.41 % Elapsed time: 0.050743 seconds
% 0.13/0.41 % CPU time: 0.221933 seconds
% 0.13/0.41 % Total memory used: 53.202 MB
% 0.13/0.41 % Net memory used: 52.770 MB
%------------------------------------------------------------------------------