%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO578+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 03:44:31 PM UTC 2026
% Result : Theorem 0.09s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO578+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 11:57:32 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.38 % Refutation found
% 0.09/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.38 fof(f21,axiom,(
% 0.09/0.38 ( (! [X61] :( k04_buttercup10100(X61)=> b48_buttercup10098(X61) ))& (? [X62] :( b48_buttercup10098(X62)& ~ k04_buttercup10100(X62) ) )) ),
% 0.09/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f86,conjecture,(
% 0.09/0.38 ( ( (! [X142] :( b48_buttercup10098(X142)=> k04_buttercup10100(X142) ))& (? [X143] :( k04_buttercup10100(X143)& ~ b48_buttercup10098(X143) ) ))| ( (! [X144] :( k04_buttercup10100(X144)=> b48_buttercup10098(X144) ))& (? [X145] :( b48_buttercup10098(X145)& ~ k04_buttercup10100(X145) ) ))| (? [X146,X147,X148] :( k04_buttercup10100(X146)& b48_buttercup10098(X146)& k04_buttercup10100(X147)& ~ b48_buttercup10098(X147)& ~ k04_buttercup10100(X148)& b48_buttercup10098(X148) ))| (! [X149] :( k04_buttercup10100(X149)=> ~ b48_buttercup10098(X149) ) )) ),
% 0.09/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f87,negated_conjecture,(
% 0.09/0.38 ~(( ( (! [X142] :( b48_buttercup10098(X142)=> k04_buttercup10100(X142) ))& (? [X143] :( k04_buttercup10100(X143)& ~ b48_buttercup10098(X143) ) ))| ( (! [X144] :( k04_buttercup10100(X144)=> b48_buttercup10098(X144) ))& (? [X145] :( b48_buttercup10098(X145)& ~ k04_buttercup10100(X145) ) ))| (? [X146,X147,X148] :( k04_buttercup10100(X146)& b48_buttercup10098(X146)& k04_buttercup10100(X147)& ~ b48_buttercup10098(X147)& ~ k04_buttercup10100(X148)& b48_buttercup10098(X148) ))| (! [X149] :( k04_buttercup10100(X149)=> ~ b48_buttercup10098(X149) ) )) )),
% 0.09/0.38 inference(negated_conjecture,[status(cth)],[f86])).
% 0.09/0.38 fof(f171,plain,(
% 0.09/0.38 (![X61]: (~k04_buttercup10100(X61)|b48_buttercup10098(X61)))&(?[X62]: (b48_buttercup10098(X62)&~k04_buttercup10100(X62)))),
% 0.09/0.38 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.09/0.38 fof(f172,plain,(
% 0.09/0.38 (![X61]: (~k04_buttercup10100(X61)|b48_buttercup10098(X61)))&(b48_buttercup10098(sK11_skl)&~k04_buttercup10100(sK11_skl))),
% 0.09/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X62,sK11_skl)],[f171])).
% 0.09/0.38 fof(f174,plain,(
% 0.09/0.38 b48_buttercup10098(sK11_skl)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f172])).
% 0.09/0.38 fof(f175,plain,(
% 0.09/0.38 ~k04_buttercup10100(sK11_skl)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f172])).
% 0.09/0.38 fof(f319,plain,(
% 0.09/0.38 (((((?[X142]: (b48_buttercup10098(X142)&~k04_buttercup10100(X142)))|(![X143]: (~k04_buttercup10100(X143)|b48_buttercup10098(X143))))&((?[X144]: (k04_buttercup10100(X144)&~b48_buttercup10098(X144)))|(![X145]: (~b48_buttercup10098(X145)|k04_buttercup10100(X145)))))&(![X146,X147,X148]: (((((~k04_buttercup10100(X146)|~b48_buttercup10098(X146))|~k04_buttercup10100(X147))|b48_buttercup10098(X147))|k04_buttercup10100(X148))|~b48_buttercup10098(X148))))&(?[X149]: (k04_buttercup10100(X149)&b48_buttercup10098(X149))))),
% 0.09/0.38 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 0.09/0.38 fof(f320,plain,(
% 0.09/0.38 ((((?[X142]: (b48_buttercup10098(X142)&~k04_buttercup10100(X142)))|(![X143]: (~k04_buttercup10100(X143)|b48_buttercup10098(X143))))&((?[X144]: (k04_buttercup10100(X144)&~b48_buttercup10098(X144)))|(![X145]: (~b48_buttercup10098(X145)|k04_buttercup10100(X145)))))&(![X148]: (((![X147]: (((![X146]: (~k04_buttercup10100(X146)|~b48_buttercup10098(X146)))|~k04_buttercup10100(X147))|b48_buttercup10098(X147)))|k04_buttercup10100(X148))|~b48_buttercup10098(X148))))&(?[X149]: (k04_buttercup10100(X149)&b48_buttercup10098(X149)))),
% 0.09/0.38 inference(miniscoping,[status(thm)],[f319])).
% 0.09/0.38 fof(f321,plain,(
% 0.09/0.38 ((((b48_buttercup10098(sK27_skl)&~k04_buttercup10100(sK27_skl))|(![X143]: (~k04_buttercup10100(X143)|b48_buttercup10098(X143))))&((k04_buttercup10100(sK28_skl)&~b48_buttercup10098(sK28_skl))|(![X145]: (~b48_buttercup10098(X145)|k04_buttercup10100(X145)))))&(![X148]: (((![X147]: (((![X146]: (~k04_buttercup10100(X146)|~b48_buttercup10098(X146)))|~k04_buttercup10100(X147))|b48_buttercup10098(X147)))|k04_buttercup10100(X148))|~b48_buttercup10098(X148))))&(k04_buttercup10100(sK29_skl)&b48_buttercup10098(sK29_skl))),
% 0.09/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl,sK29_skl]),skolemize(X142,sK27_skl),skolemize(X144,sK28_skl),skolemize(X149,sK29_skl)],[f320])).
% 0.09/0.38 fof(f324,plain,(
% 0.09/0.38 ![X0]: (k04_buttercup10100(sK28_skl)|~b48_buttercup10098(X0)|k04_buttercup10100(X0))),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f321])).
% 0.09/0.38 fof(f325,plain,(
% 0.09/0.38 ![X0]: (~b48_buttercup10098(sK28_skl)|~b48_buttercup10098(X0)|k04_buttercup10100(X0))),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f321])).
% 0.09/0.38 fof(f326,plain,(
% 0.09/0.38 ![X0,X1,X2]: (~k04_buttercup10100(X0)|~b48_buttercup10098(X0)|~k04_buttercup10100(X1)|b48_buttercup10098(X1)|k04_buttercup10100(X2)|~b48_buttercup10098(X2))),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f321])).
% 0.09/0.38 fof(f327,plain,(
% 0.09/0.38 k04_buttercup10100(sK29_skl)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f321])).
% 0.09/0.38 fof(f328,plain,(
% 0.09/0.38 b48_buttercup10098(sK29_skl)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f321])).
% 0.09/0.38 fof(f591,definition,(
% 0.09/0.38 ![X0]: (sQ36_spl <=> (~k04_buttercup10100(X0)|b48_buttercup10098(X0)))),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.09/0.38 fof(f592,plain,(
% 0.09/0.38 ![X0]: (~k04_buttercup10100(X0)|b48_buttercup10098(X0)|~sQ36_spl)),
% 0.09/0.38 inference(component_clause,[status(thm)],[f591])).
% 0.09/0.38 fof(f599,definition,(
% 0.09/0.38 sQ38_spl <=> (k04_buttercup10100(sK28_skl))),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.09/0.38 fof(f600,plain,(
% 0.09/0.38 k04_buttercup10100(sK28_skl)|~sQ38_spl),
% 0.09/0.38 inference(component_clause,[status(thm)],[f599])).
% 0.09/0.38 fof(f602,definition,(
% 0.09/0.38 ![X0]: (sQ39_spl <=> (~b48_buttercup10098(X0)|k04_buttercup10100(X0)))),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.09/0.38 fof(f603,plain,(
% 0.09/0.38 ![X0]: (~b48_buttercup10098(X0)|k04_buttercup10100(X0)|~sQ39_spl)),
% 0.09/0.38 inference(component_clause,[status(thm)],[f602])).
% 0.09/0.38 fof(f605,plain,(
% 0.09/0.38 sQ38_spl|sQ39_spl),
% 0.09/0.38 inference(split_clause,[status(thm)],[f324,f599,f602])).
% 0.09/0.38 fof(f606,definition,(
% 0.09/0.38 sQ40_spl <=> (b48_buttercup10098(sK28_skl))),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.09/0.38 fof(f608,plain,(
% 0.09/0.38 ~b48_buttercup10098(sK28_skl)|sQ40_spl),
% 0.09/0.38 inference(component_clause,[status(thm)],[f606])).
% 0.09/0.38 fof(f609,plain,(
% 0.09/0.38 ~sQ40_spl|sQ39_spl),
% 0.09/0.38 inference(split_clause,[status(thm)],[f325,f606,f602])).
% 0.09/0.38 fof(f610,definition,(
% 0.09/0.38 ![X0]: (sQ41_spl <=> (~k04_buttercup10100(X0)|~b48_buttercup10098(X0)))),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.09/0.38 fof(f611,plain,(
% 0.09/0.38 ![X0]: (~k04_buttercup10100(X0)|~b48_buttercup10098(X0)|~sQ41_spl)),
% 0.09/0.38 inference(component_clause,[status(thm)],[f610])).
% 0.09/0.38 fof(f613,plain,(
% 0.09/0.38 sQ41_spl|sQ36_spl|sQ39_spl),
% 0.09/0.38 inference(split_clause,[status(thm)],[f326,f610,f591,f602])).
% 0.09/0.38 fof(f838,plain,(
% 0.09/0.38 ~b48_buttercup10098(sK11_skl)|~sQ39_spl),
% 0.09/0.38 inference(resolution,[status(thm)],[f175,f603])).
% 0.09/0.38 fof(f839,plain,(
% 0.09/0.38 $false|~sQ39_spl),
% 0.09/0.38 inference(forward_subsumption_resolution,[status(thm)],[f838,f174])).
% 0.09/0.38 fof(f840,plain,(
% 0.09/0.38 ~sQ39_spl),
% 0.09/0.38 inference(contradiction_clause,[status(thm)],[f839])).
% 0.09/0.38 fof(f843,plain,(
% 0.09/0.38 b48_buttercup10098(sK28_skl)|~sQ38_spl|~sQ36_spl),
% 0.09/0.38 inference(resolution,[status(thm)],[f600,f592])).
% 0.09/0.38 fof(f846,plain,(
% 0.09/0.38 $false|sQ40_spl|~sQ38_spl|~sQ36_spl),
% 0.09/0.38 inference(forward_subsumption_resolution,[status(thm)],[f843,f608])).
% 0.09/0.38 fof(f847,plain,(
% 0.09/0.38 sQ40_spl|~sQ38_spl|~sQ36_spl),
% 0.09/0.38 inference(contradiction_clause,[status(thm)],[f846])).
% 0.09/0.38 fof(f854,plain,(
% 0.09/0.38 ~b48_buttercup10098(sK29_skl)|~sQ41_spl),
% 0.09/0.38 inference(resolution,[status(thm)],[f611,f327])).
% 0.09/0.38 fof(f858,plain,(
% 0.09/0.38 $false|~sQ41_spl),
% 0.09/0.38 inference(forward_subsumption_resolution,[status(thm)],[f854,f328])).
% 0.09/0.38 fof(f859,plain,(
% 0.09/0.38 ~sQ41_spl),
% 0.09/0.38 inference(contradiction_clause,[status(thm)],[f858])).
% 0.09/0.38 fof(f860,plain,(
% 0.09/0.38 $false),
% 0.09/0.38 inference(sat_refutation,[status(thm)],[f605,f609,f613,f840,f847,f859])).
% 0.09/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.41 % Elapsed time: 0.040458 seconds
% 0.09/0.41 % CPU time: 0.090960 seconds
% 0.09/0.41 % Total memory used: 13.201 MB
% 0.09/0.41 % Net memory used: 13.115 MB
%------------------------------------------------------------------------------