%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO009+3 : 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 : 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 01:59:23 PM UTC 2026
% Result : Theorem 0.18s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO009+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.38 % Computer : n015.cluster.edu
% 0.14/0.38 % Model : x86_64 x86_64
% 0.14/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.38 % Memory : 8046.5625MB
% 0.14/0.38 % OS : Linux 6.8.0-71-generic
% 0.14/0.38 % CPULimit : 300
% 0.14/0.38 % WCLimit : 300
% 0.14/0.38 % DateTime : Mon Sep 21 03:45:36 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.43 % Drodi V4.1.1
% 0.18/0.59 % Refutation found
% 0.18/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.59 fof(f23,axiom,(
% 0.18/0.59 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f39,axiom,(
% 0.18/0.59 (! [X117,X118,X119] :( ( occurrence_of(X117,X119)& root_occ(X118,X117) )=> ~ (? [X120] : min_precedes(X120,X118,X119) )) )),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f42,axiom,(
% 0.18/0.59 (! [X130,X131,X132,X133] :( ( occurrence_of(X130,X133)& leaf_occ(X131,X130)& root_occ(X132,X130)& X131 != X132 )=> min_precedes(X132,X131,X133) ) )),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f50,axiom,(
% 0.18/0.59 (! [X161] :( occurrence_of(X161,tptp0)=> (? [X162,X163,X164] :( occurrence_of(X162,tptp3)& root_occ(X162,X161)& occurrence_of(X163,tptp4)& next_subocc(X162,X163,tptp0)& ( occurrence_of(X164,tptp2)| occurrence_of(X164,tptp1) )& next_subocc(X163,X164,tptp0)& leaf_occ(X164,X161) ) )) )),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f63,conjecture,(
% 0.18/0.59 (! [X165] :( occurrence_of(X165,tptp0)=> (? [X166,X167] :( occurrence_of(X166,tptp3)& root_occ(X166,X165)& ( occurrence_of(X167,tptp2)| occurrence_of(X167,tptp1) )& min_precedes(X166,X167,tptp0)& leaf_occ(X167,X165) ) )) )),
% 0.18/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.59 fof(f64,negated_conjecture,(
% 0.18/0.59 ~((! [X165] :( occurrence_of(X165,tptp0)=> (? [X166,X167] :( occurrence_of(X166,tptp3)& root_occ(X166,X165)& ( occurrence_of(X167,tptp2)| occurrence_of(X167,tptp1) )& min_precedes(X166,X167,tptp0)& leaf_occ(X167,X165) ) )) ))),
% 0.18/0.59 inference(negated_conjecture,[status(cth)],[f63])).
% 0.18/0.59 fof(f143,plain,(
% 0.18/0.59 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 0.18/0.59 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.18/0.59 fof(f144,plain,(
% 0.18/0.59 ![X60,X61,X62]: ((~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))&(next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 0.18/0.59 inference(NNF_transformation,[status(thm)],[f143])).
% 0.18/0.59 fof(f145,plain,(
% 0.18/0.59 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 0.18/0.59 inference(miniscoping,[status(thm)],[f144])).
% 0.18/0.59 fof(f146,plain,(
% 0.18/0.59 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(min_precedes(X60,sK7_skl(X62,X61,X60),X62)&min_precedes(sK7_skl(X62,X61,X60),X61,X62)))))),
% 0.18/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f145])).
% 0.18/0.59 fof(f147,plain,(
% 0.18/0.59 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f146])).
% 0.18/0.59 fof(f214,plain,(
% 0.18/0.59 ![X117,X118,X119]: ((~occurrence_of(X117,X119)|~root_occ(X118,X117))|(![X120]: ~min_precedes(X120,X118,X119)))),
% 0.18/0.59 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.18/0.59 fof(f215,plain,(
% 0.18/0.59 ![X118,X119]: ((![X117]: (~occurrence_of(X117,X119)|~root_occ(X118,X117)))|(![X120]: ~min_precedes(X120,X118,X119)))),
% 0.18/0.59 inference(miniscoping,[status(thm)],[f214])).
% 0.18/0.59 fof(f216,plain,(
% 0.18/0.59 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~min_precedes(X3,X2,X1))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f215])).
% 0.18/0.59 fof(f223,plain,(
% 0.18/0.59 ![X130,X131,X132,X133]: ((((~occurrence_of(X130,X133)|~leaf_occ(X131,X130))|~root_occ(X132,X130))|X131=X132)|min_precedes(X132,X131,X133))),
% 0.18/0.59 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.18/0.59 fof(f224,plain,(
% 0.18/0.59 ![X131,X132,X133]: (((![X130]: ((~occurrence_of(X130,X133)|~leaf_occ(X131,X130))|~root_occ(X132,X130)))|X131=X132)|min_precedes(X132,X131,X133))),
% 0.18/0.59 inference(miniscoping,[status(thm)],[f223])).
% 0.18/0.59 fof(f225,plain,(
% 0.18/0.59 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~root_occ(X3,X0)|X2=X3|min_precedes(X3,X2,X1))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f224])).
% 0.18/0.59 fof(f249,plain,(
% 0.18/0.59 ![X161]: (~occurrence_of(X161,tptp0)|(?[X162,X163,X164]: ((((((occurrence_of(X162,tptp3)&root_occ(X162,X161))&occurrence_of(X163,tptp4))&next_subocc(X162,X163,tptp0))&(occurrence_of(X164,tptp2)|occurrence_of(X164,tptp1)))&next_subocc(X163,X164,tptp0))&leaf_occ(X164,X161))))),
% 0.18/0.59 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.18/0.59 fof(f250,plain,(
% 0.18/0.59 ![X161]: (~occurrence_of(X161,tptp0)|(?[X164]: ((?[X163]: (((?[X162]: (((occurrence_of(X162,tptp3)&root_occ(X162,X161))&occurrence_of(X163,tptp4))&next_subocc(X162,X163,tptp0)))&(occurrence_of(X164,tptp2)|occurrence_of(X164,tptp1)))&next_subocc(X163,X164,tptp0)))&leaf_occ(X164,X161))))),
% 0.18/0.59 inference(miniscoping,[status(thm)],[f249])).
% 0.18/0.59 fof(f251,plain,(
% 0.18/0.59 ![X161]: (~occurrence_of(X161,tptp0)|((((((occurrence_of(sK18_skl(X161),tptp3)&root_occ(sK18_skl(X161),X161))&occurrence_of(sK17_skl(X161),tptp4))&next_subocc(sK18_skl(X161),sK17_skl(X161),tptp0))&(occurrence_of(sK16_skl(X161),tptp2)|occurrence_of(sK16_skl(X161),tptp1)))&next_subocc(sK17_skl(X161),sK16_skl(X161),tptp0))&leaf_occ(sK16_skl(X161),X161)))),
% 0.18/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X164,sK16_skl(X161)),skolemize(X163,sK17_skl(X161)),skolemize(X162,sK18_skl(X161))],[f250])).
% 0.18/0.59 fof(f252,plain,(
% 0.18/0.59 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK18_skl(X0),tptp3))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f251])).
% 0.18/0.59 fof(f253,plain,(
% 0.18/0.59 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK18_skl(X0),X0))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f251])).
% 0.18/0.59 fof(f256,plain,(
% 0.18/0.59 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK16_skl(X0),tptp2)|occurrence_of(sK16_skl(X0),tptp1))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f251])).
% 0.18/0.59 fof(f257,plain,(
% 0.18/0.59 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK17_skl(X0),sK16_skl(X0),tptp0))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f251])).
% 0.18/0.59 fof(f258,plain,(
% 0.18/0.59 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK16_skl(X0),X0))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f251])).
% 0.18/0.59 fof(f271,plain,(
% 0.18/0.59 (?[X165]: (occurrence_of(X165,tptp0)&(![X166,X167]: ((((~occurrence_of(X166,tptp3)|~root_occ(X166,X165))|(~occurrence_of(X167,tptp2)&~occurrence_of(X167,tptp1)))|~min_precedes(X166,X167,tptp0))|~leaf_occ(X167,X165)))))),
% 0.18/0.59 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.18/0.59 fof(f272,plain,(
% 0.18/0.59 ?[X165]: (occurrence_of(X165,tptp0)&(![X167]: ((![X166]: (((~occurrence_of(X166,tptp3)|~root_occ(X166,X165))|(~occurrence_of(X167,tptp2)&~occurrence_of(X167,tptp1)))|~min_precedes(X166,X167,tptp0)))|~leaf_occ(X167,X165))))),
% 0.18/0.59 inference(miniscoping,[status(thm)],[f271])).
% 0.18/0.59 fof(f273,plain,(
% 0.18/0.59 (occurrence_of(sK19_skl,tptp0)&(![X167]: ((![X166]: (((~occurrence_of(X166,tptp3)|~root_occ(X166,sK19_skl))|(~occurrence_of(X167,tptp2)&~occurrence_of(X167,tptp1)))|~min_precedes(X166,X167,tptp0)))|~leaf_occ(X167,sK19_skl))))),
% 0.18/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(X165,sK19_skl)],[f272])).
% 0.18/0.59 fof(f274,plain,(
% 0.18/0.59 occurrence_of(sK19_skl,tptp0)),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f273])).
% 0.18/0.59 fof(f275,plain,(
% 0.18/0.59 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK19_skl)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0)|~leaf_occ(X1,sK19_skl))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f273])).
% 0.18/0.59 fof(f276,plain,(
% 0.18/0.59 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK19_skl)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0)|~leaf_occ(X1,sK19_skl))),
% 0.18/0.59 inference(cnf_transformation,[status(thm)],[f273])).
% 0.18/0.59 fof(f281,plain,(
% 0.18/0.59 root_occ(sK18_skl(sK19_skl),sK19_skl)),
% 0.18/0.59 inference(resolution,[status(thm)],[f253,f274])).
% 0.18/0.59 fof(f283,plain,(
% 0.18/0.59 ![X0,X1]: (~occurrence_of(sK19_skl,X0)|~min_precedes(X1,sK18_skl(sK19_skl),X0))),
% 0.18/0.59 inference(resolution,[status(thm)],[f281,f216])).
% 0.18/0.59 fof(f284,plain,(
% 0.18/0.59 leaf_occ(sK16_skl(sK19_skl),sK19_skl)),
% 0.18/0.61 inference(resolution,[status(thm)],[f258,f274])).
% 0.18/0.61 fof(f288,plain,(
% 0.18/0.61 ![X0,X1]: (~occurrence_of(sK19_skl,X0)|~root_occ(X1,sK19_skl)|sK16_skl(sK19_skl)=X1|min_precedes(X1,sK16_skl(sK19_skl),X0))),
% 0.18/0.61 inference(resolution,[status(thm)],[f284,f225])).
% 0.18/0.61 fof(f295,plain,(
% 0.18/0.61 ![X0]: (~root_occ(X0,sK19_skl)|sK16_skl(sK19_skl)=X0|min_precedes(X0,sK16_skl(sK19_skl),tptp0))),
% 0.18/0.61 inference(resolution,[status(thm)],[f288,f274])).
% 0.18/0.61 fof(f296,plain,(
% 0.18/0.61 sK16_skl(sK19_skl)=sK18_skl(sK19_skl)|min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 0.18/0.61 inference(resolution,[status(thm)],[f295,f281])).
% 0.18/0.61 fof(f318,plain,(
% 0.18/0.61 occurrence_of(sK18_skl(sK19_skl),tptp3)),
% 0.18/0.61 inference(resolution,[status(thm)],[f252,f274])).
% 0.18/0.61 fof(f319,plain,(
% 0.18/0.61 ![X0]: (~root_occ(sK18_skl(sK19_skl),sK19_skl)|~occurrence_of(X0,tptp1)|~min_precedes(sK18_skl(sK19_skl),X0,tptp0)|~leaf_occ(X0,sK19_skl))),
% 0.18/0.61 inference(resolution,[status(thm)],[f318,f276])).
% 0.18/0.61 fof(f320,plain,(
% 0.18/0.61 ![X0]: (~root_occ(sK18_skl(sK19_skl),sK19_skl)|~occurrence_of(X0,tptp2)|~min_precedes(sK18_skl(sK19_skl),X0,tptp0)|~leaf_occ(X0,sK19_skl))),
% 0.18/0.61 inference(resolution,[status(thm)],[f318,f275])).
% 0.18/0.61 fof(f324,plain,(
% 0.18/0.61 ![X0]: (~occurrence_of(X0,tptp1)|~min_precedes(sK18_skl(sK19_skl),X0,tptp0)|~leaf_occ(X0,sK19_skl))),
% 0.18/0.61 inference(forward_subsumption_resolution,[status(thm)],[f319,f281])).
% 0.18/0.61 fof(f325,plain,(
% 0.18/0.61 ![X0]: (~occurrence_of(X0,tptp2)|~min_precedes(sK18_skl(sK19_skl),X0,tptp0)|~leaf_occ(X0,sK19_skl))),
% 0.18/0.61 inference(forward_subsumption_resolution,[status(thm)],[f320,f281])).
% 0.18/0.61 fof(f328,plain,(
% 0.18/0.61 ![X0]: (~occurrence_of(X0,tptp0)|min_precedes(sK17_skl(X0),sK16_skl(X0),tptp0))),
% 0.18/0.61 inference(resolution,[status(thm)],[f257,f147])).
% 0.18/0.61 fof(f330,plain,(
% 0.18/0.61 min_precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 0.18/0.61 inference(resolution,[status(thm)],[f328,f274])).
% 0.18/0.61 fof(f377,plain,(
% 0.18/0.61 occurrence_of(sK16_skl(sK19_skl),tptp2)|occurrence_of(sK16_skl(sK19_skl),tptp1)),
% 0.18/0.61 inference(resolution,[status(thm)],[f256,f274])).
% 0.18/0.61 fof(f397,plain,(
% 0.18/0.61 occurrence_of(sK16_skl(sK19_skl),tptp2)|~min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)|~leaf_occ(sK16_skl(sK19_skl),sK19_skl)),
% 0.18/0.61 inference(resolution,[status(thm)],[f377,f324])).
% 0.18/0.61 fof(f402,plain,(
% 0.18/0.61 ~min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)|~leaf_occ(sK16_skl(sK19_skl),sK19_skl)),
% 0.18/0.61 inference(forward_subsumption_resolution,[status(thm)],[f397,f325])).
% 0.18/0.61 fof(f405,plain,(
% 0.18/0.61 sK16_skl(sK19_skl)=sK18_skl(sK19_skl)),
% 0.18/0.61 inference(backward_subsumption_resolution,[status(thm)],[f296,f406])).
% 0.18/0.61 fof(f406,plain,(
% 0.18/0.61 ~min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 0.18/0.61 inference(forward_subsumption_resolution,[status(thm)],[f402,f284])).
% 0.18/0.61 fof(f437,plain,(
% 0.18/0.61 min_precedes(sK17_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)),
% 0.18/0.61 inference(forward_demodulation,[status(thm)],[f405,f330])).
% 0.18/0.61 fof(f438,plain,(
% 0.18/0.61 ~occurrence_of(sK19_skl,tptp0)),
% 0.18/0.61 inference(resolution,[status(thm)],[f437,f283])).
% 0.18/0.61 fof(f443,plain,(
% 0.18/0.61 $false),
% 0.18/0.61 inference(forward_subsumption_resolution,[status(thm)],[f438,f274])).
% 0.18/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.65 % Elapsed time: 0.230429 seconds
% 0.18/0.65 % CPU time: 1.257720 seconds
% 0.18/0.65 % Total memory used: 96.464 MB
% 0.18/0.65 % Net memory used: 95.788 MB
%------------------------------------------------------------------------------