%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO010+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 : 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 01:59:24 PM UTC 2026
% Result : Theorem 0.14s 10.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO010+3 : 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.11/10.68 % Computer : n002.cluster.edu
% 0.11/10.68 % Model : x86_64 x86_64
% 0.11/10.68 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.68 % Memory : 8046.5625MB
% 0.11/10.68 % OS : Linux 6.8.0-71-generic
% 0.11/10.68 % CPULimit : 300
% 0.11/10.68 % WCLimit : 300
% 0.11/10.68 % DateTime : Mon Sep 21 03:44:59 UTC 2026
% 0.11/10.69 % CPUTime :
% 0.14/10.70 % Drodi V4.1.1
% 0.14/10.73 % Refutation found
% 0.14/10.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/10.73 % SZS output start CNFRefutation for theBenchmark
% 0.14/10.73 fof(f8,axiom,(
% 0.14/10.73 (! [X16,X17] :( occurrence_of(X16,X17)=> ( arboreal(X16)<=> atomic(X17) ) ) )),
% 0.14/10.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/10.73 fof(f47,axiom,(
% 0.14/10.73 (! [X148,X149,X150] :( min_precedes(X148,X149,X150)=> arboreal(X148) ) )),
% 0.14/10.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/10.73 fof(f50,axiom,(
% 0.14/10.73 (! [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,tptp1)| occurrence_of(X164,tptp2) )& next_subocc(X163,X164,tptp0)& leaf_occ(X164,X161) ) )) )),
% 0.14/10.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/10.73 fof(f52,axiom,(
% 0.14/10.73 ~ atomic(tptp0) ),
% 0.14/10.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/10.73 fof(f63,conjecture,(
% 0.14/10.73 (! [X165] :( occurrence_of(X165,tptp0)=> (? [X166,X167] :( leaf_occ(X167,X165)& ( occurrence_of(X167,tptp1)=> ~ (? [X168] :( occurrence_of(X168,tptp2)& min_precedes(X166,X168,tptp0) ) ))& ( occurrence_of(X167,tptp2)=> ~ (? [X169] :( occurrence_of(X169,tptp1)& min_precedes(X166,X169,tptp0) ) )) ) )) )),
% 0.14/10.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/10.73 fof(f64,negated_conjecture,(
% 0.14/10.73 ~((! [X165] :( occurrence_of(X165,tptp0)=> (? [X166,X167] :( leaf_occ(X167,X165)& ( occurrence_of(X167,tptp1)=> ~ (? [X168] :( occurrence_of(X168,tptp2)& min_precedes(X166,X168,tptp0) ) ))& ( occurrence_of(X167,tptp2)=> ~ (? [X169] :( occurrence_of(X169,tptp1)& min_precedes(X166,X169,tptp0) ) )) ) )) ))),
% 0.14/10.73 inference(negated_conjecture,[status(cth)],[f63])).
% 0.14/10.73 fof(f85,plain,(
% 0.14/10.73 ![X16,X17]: (~occurrence_of(X16,X17)|(arboreal(X16)<=>atomic(X17)))),
% 0.14/10.73 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.14/10.73 fof(f86,plain,(
% 0.14/10.73 ![X16,X17]: (~occurrence_of(X16,X17)|((~arboreal(X16)|atomic(X17))&(arboreal(X16)|~atomic(X17))))),
% 0.14/10.73 inference(NNF_transformation,[status(thm)],[f85])).
% 0.14/10.73 fof(f87,plain,(
% 0.14/10.73 ![X0,X1]: (~occurrence_of(X0,X1)|~arboreal(X0)|atomic(X1))),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f86])).
% 0.14/10.73 fof(f240,plain,(
% 0.14/10.73 ![X148,X149,X150]: (~min_precedes(X148,X149,X150)|arboreal(X148))),
% 0.14/10.73 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.14/10.73 fof(f241,plain,(
% 0.14/10.73 ![X148]: ((![X149,X150]: ~min_precedes(X148,X149,X150))|arboreal(X148))),
% 0.14/10.73 inference(miniscoping,[status(thm)],[f240])).
% 0.14/10.73 fof(f242,plain,(
% 0.14/10.73 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|arboreal(X0))),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f241])).
% 0.14/10.73 fof(f249,plain,(
% 0.14/10.73 ![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,tptp1)|occurrence_of(X164,tptp2)))&next_subocc(X163,X164,tptp0))&leaf_occ(X164,X161))))),
% 0.14/10.73 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.14/10.73 fof(f250,plain,(
% 0.14/10.73 ![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,tptp1)|occurrence_of(X164,tptp2)))&next_subocc(X163,X164,tptp0)))&leaf_occ(X164,X161))))),
% 0.14/10.73 inference(miniscoping,[status(thm)],[f249])).
% 0.14/10.73 fof(f251,plain,(
% 0.14/10.73 ![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),tptp1)|occurrence_of(sK16_skl(X161),tptp2)))&next_subocc(sK17_skl(X161),sK16_skl(X161),tptp0))&leaf_occ(sK16_skl(X161),X161)))),
% 0.14/10.73 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.14/10.73 fof(f258,plain,(
% 0.14/10.73 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK16_skl(X0),X0))),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f251])).
% 0.14/10.73 fof(f260,plain,(
% 0.14/10.73 ~atomic(tptp0)),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/10.73 fof(f271,plain,(
% 0.14/10.73 (?[X165]: (occurrence_of(X165,tptp0)&(![X166,X167]: ((~leaf_occ(X167,X165)|(occurrence_of(X167,tptp1)&(?[X168]: (occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0)))))|(occurrence_of(X167,tptp2)&(?[X169]: (occurrence_of(X169,tptp1)&min_precedes(X166,X169,tptp0))))))))),
% 0.14/10.73 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.14/10.73 fof(f272,definition,(
% 0.14/10.73 ![X166,X167]: (sP0_prd(X167,X166)<=>(occurrence_of(X167,tptp1)&(?[X168]: (occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0)))))),
% 0.14/10.73 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/10.73 fof(f273,plain,(
% 0.14/10.73 ?[X165]: (occurrence_of(X165,tptp0)&(![X166,X167]: ((~leaf_occ(X167,X165)|sP0_prd(X167,X166))|(occurrence_of(X167,tptp2)&(?[X169]: (occurrence_of(X169,tptp1)&min_precedes(X166,X169,tptp0)))))))),
% 0.14/10.73 inference(formula_renaming,[status(thm)],[f271,f272])).
% 0.14/10.73 fof(f274,plain,(
% 0.14/10.73 (occurrence_of(sK19_skl,tptp0)&(![X166,X167]: ((~leaf_occ(X167,sK19_skl)|sP0_prd(X167,X166))|(occurrence_of(X167,tptp2)&(occurrence_of(sK20_skl(X167,X166),tptp1)&min_precedes(X166,sK20_skl(X167,X166),tptp0))))))),
% 0.14/10.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X165,sK19_skl),skolemize(X169,sK20_skl(X167,X166))],[f273])).
% 0.14/10.73 fof(f275,plain,(
% 0.14/10.73 occurrence_of(sK19_skl,tptp0)),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/10.73 fof(f278,plain,(
% 0.14/10.73 ![X0,X1]: (~leaf_occ(X0,sK19_skl)|sP0_prd(X0,X1)|min_precedes(X1,sK20_skl(X0,X1),tptp0))),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/10.73 fof(f279,plain,(
% 0.14/10.73 ![X166,X167]: ((~sP0_prd(X167,X166)|(occurrence_of(X167,tptp1)&(?[X168]: (occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0)))))&(sP0_prd(X167,X166)|(~occurrence_of(X167,tptp1)|(![X168]: (~occurrence_of(X168,tptp2)|~min_precedes(X166,X168,tptp0))))))),
% 0.14/10.73 inference(NNF_transformation,[status(thm)],[f272])).
% 0.14/10.73 fof(f280,plain,(
% 0.14/10.73 (![X166,X167]: (~sP0_prd(X167,X166)|(occurrence_of(X167,tptp1)&(?[X168]: (occurrence_of(X168,tptp2)&min_precedes(X166,X168,tptp0))))))&(![X166,X167]: (sP0_prd(X167,X166)|(~occurrence_of(X167,tptp1)|(![X168]: (~occurrence_of(X168,tptp2)|~min_precedes(X166,X168,tptp0))))))),
% 0.14/10.73 inference(miniscoping,[status(thm)],[f279])).
% 0.14/10.73 fof(f281,plain,(
% 0.14/10.73 (![X166,X167]: (~sP0_prd(X167,X166)|(occurrence_of(X167,tptp1)&(occurrence_of(sK21_skl(X167,X166),tptp2)&min_precedes(X166,sK21_skl(X167,X166),tptp0)))))&(![X166,X167]: (sP0_prd(X167,X166)|(~occurrence_of(X167,tptp1)|(![X168]: (~occurrence_of(X168,tptp2)|~min_precedes(X166,X168,tptp0))))))),
% 0.14/10.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(X168,sK21_skl(X167,X166))],[f280])).
% 0.14/10.73 fof(f284,plain,(
% 0.14/10.73 ![X0,X1]: (~sP0_prd(X0,X1)|min_precedes(X1,sK21_skl(X0,X1),tptp0))),
% 0.14/10.73 inference(cnf_transformation,[status(thm)],[f281])).
% 0.14/10.73 fof(f310,plain,(
% 0.14/10.73 ![X0,X1]: (arboreal(X0)|~sP0_prd(X1,X0))),
% 0.14/10.73 inference(resolution,[status(thm)],[f242,f284])).
% 0.14/10.73 fof(f326,plain,(
% 0.14/10.73 leaf_occ(sK16_skl(sK19_skl),sK19_skl)),
% 0.14/10.73 inference(resolution,[status(thm)],[f258,f275])).
% 0.14/10.73 fof(f330,plain,(
% 0.14/10.73 ![X0]: (sP0_prd(sK16_skl(sK19_skl),X0)|min_precedes(X0,sK20_skl(sK16_skl(sK19_skl),X0),tptp0))),
% 0.14/10.73 inference(resolution,[status(thm)],[f326,f278])).
% 0.14/10.73 fof(f366,plain,(
% 0.14/10.73 ![X0]: (sP0_prd(sK16_skl(sK19_skl),X0)|arboreal(X0))),
% 0.14/10.73 inference(resolution,[status(thm)],[f330,f242])).
% 0.14/10.73 fof(f368,plain,(
% 0.14/10.73 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1))),
% 0.14/10.73 inference(backward_subsumption_resolution,[status(thm)],[f87,f372])).
% 0.14/10.73 fof(f372,plain,(
% 0.14/10.73 ![X0]: (arboreal(X0))),
% 0.14/10.73 inference(forward_subsumption_resolution,[status(thm)],[f366,f310])).
% 0.14/10.73 fof(f379,plain,(
% 0.14/10.73 atomic(tptp0)),
% 0.14/10.73 inference(resolution,[status(thm)],[f368,f275])).
% 0.14/10.73 fof(f381,plain,(
% 0.14/10.73 $false),
% 0.14/10.73 inference(forward_subsumption_resolution,[status(thm)],[f379,f260])).
% 0.14/10.73 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/10.75 % Elapsed time: 0.061549 seconds
% 0.14/10.75 % CPU time: 0.180112 seconds
% 0.14/10.75 % Total memory used: 84.751 MB
% 0.14/10.75 % Net memory used: 84.607 MB
%------------------------------------------------------------------------------