%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO011+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO011+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/10.39 % Computer : n019.cluster.edu
% 0.11/10.39 % Model : x86_64 x86_64
% 0.11/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.39 % Memory : 8046.5625MB
% 0.11/10.39 % OS : Linux 6.8.0-71-generic
% 0.11/10.39 % CPULimit : 300
% 0.11/10.39 % WCLimit : 300
% 0.11/10.39 % DateTime : Mon Sep 21 03:43:01 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.14/10.40 % Drodi V4.1.1
% 0.14/10.44 % Refutation found
% 0.14/10.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/10.44 % SZS output start CNFRefutation for theBenchmark
% 0.14/10.44 fof(f3,axiom,(
% 0.14/10.44 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 0.14/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.44 fof(f22,axiom,(
% 0.14/10.44 (! [X56,X57] :( leaf(X56,X57)<=> ( ( root(X56,X57)| (? [X58] : min_precedes(X58,X56,X57) ))& ~ (? [X59] : min_precedes(X56,X59,X57) )) ) )),
% 0.14/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.44 fof(f35,axiom,(
% 0.14/10.44 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 0.14/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.44 fof(f50,axiom,(
% 0.14/10.44 (! [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.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.44 fof(f63,conjecture,(
% 0.14/10.44 (! [X165] :( occurrence_of(X165,tptp0)=> (? [X166,X167] :( leaf_occ(X167,X165)& ( occurrence_of(X167,tptp1)=> ~ (? [X168] :( occurrence_of(X168,tptp2)& subactivity_occurrence(X168,X165)& min_precedes(X166,X168,tptp0) ) ))& ( occurrence_of(X167,tptp2)=> ~ (? [X169] :( occurrence_of(X169,tptp1)& subactivity_occurrence(X169,X165)& min_precedes(X166,X169,tptp0) ) )) ) )) )),
% 0.14/10.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.44 fof(f64,negated_conjecture,(
% 0.14/10.44 ~((! [X165] :( occurrence_of(X165,tptp0)=> (? [X166,X167] :( leaf_occ(X167,X165)& ( occurrence_of(X167,tptp1)=> ~ (? [X168] :( occurrence_of(X168,tptp2)& subactivity_occurrence(X168,X165)& min_precedes(X166,X168,tptp0) ) ))& ( occurrence_of(X167,tptp2)=> ~ (? [X169] :( occurrence_of(X169,tptp1)& subactivity_occurrence(X169,X165)& min_precedes(X166,X169,tptp0) ) )) ) )) ))),
% 0.14/10.44 inference(negated_conjecture,[status(cth)],[f63])).
% 0.14/10.44 fof(f72,plain,(
% 0.14/10.44 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 0.14/10.44 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/10.44 fof(f73,plain,(
% 0.14/10.44 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 0.14/10.44 inference(miniscoping,[status(thm)],[f72])).
% 0.14/10.44 fof(f74,plain,(
% 0.14/10.44 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/10.44 fof(f135,plain,(
% 0.14/10.44 ![X56,X57]: (leaf(X56,X57)<=>((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57))))),
% 0.14/10.44 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.14/10.44 fof(f136,plain,(
% 0.14/10.44 ![X56,X57]: ((~leaf(X56,X57)|((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57))))&(leaf(X56,X57)|((~root(X56,X57)&(![X58]: ~min_precedes(X58,X56,X57)))|(?[X59]: min_precedes(X56,X59,X57)))))),
% 0.14/10.44 inference(NNF_transformation,[status(thm)],[f135])).
% 0.14/10.44 fof(f137,plain,(
% 0.14/10.44 (![X56,X57]: (~leaf(X56,X57)|((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57)))))&(![X56,X57]: (leaf(X56,X57)|((~root(X56,X57)&(![X58]: ~min_precedes(X58,X56,X57)))|(?[X59]: min_precedes(X56,X59,X57)))))),
% 0.14/10.44 inference(miniscoping,[status(thm)],[f136])).
% 0.14/10.44 fof(f138,plain,(
% 0.14/10.44 (![X56,X57]: (~leaf(X56,X57)|((root(X56,X57)|min_precedes(sK5_skl(X57,X56),X56,X57))&(![X59]: ~min_precedes(X56,X59,X57)))))&(![X56,X57]: (leaf(X56,X57)|((~root(X56,X57)&(![X58]: ~min_precedes(X58,X56,X57)))|min_precedes(X56,sK6_skl(X57,X56),X57))))),
% 0.14/10.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(X58,sK5_skl(X57,X56)),skolemize(X59,sK6_skl(X57,X56))],[f137])).
% 0.14/10.44 fof(f140,plain,(
% 0.14/10.44 ![X0,X1,X2]: (~leaf(X0,X1)|~min_precedes(X0,X2,X1))),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f138])).
% 0.14/10.44 fof(f198,plain,(
% 0.14/10.44 ![X102,X103]: ((~leaf_occ(X102,X103)|(?[X104]: ((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104))))&(leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 0.14/10.44 inference(NNF_transformation,[status(thm)],[f35])).
% 0.14/10.44 fof(f199,plain,(
% 0.14/10.44 (![X102,X103]: (~leaf_occ(X102,X103)|(?[X104]: ((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104)))))&(![X102,X103]: (leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 0.14/10.44 inference(miniscoping,[status(thm)],[f198])).
% 0.14/10.44 fof(f200,plain,(
% 0.14/10.44 (![X102,X103]: (~leaf_occ(X102,X103)|((occurrence_of(X103,sK14_skl(X103,X102))&subactivity_occurrence(X102,X103))&leaf(X102,sK14_skl(X103,X102)))))&(![X102,X103]: (leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 0.14/10.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f199])).
% 0.14/10.44 fof(f201,plain,(
% 0.14/10.44 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK14_skl(X1,X0)))),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/10.44 fof(f203,plain,(
% 0.14/10.44 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK14_skl(X1,X0)))),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/10.44 fof(f249,plain,(
% 0.14/10.44 ![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.44 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.14/10.44 fof(f250,plain,(
% 0.14/10.44 ![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.44 inference(miniscoping,[status(thm)],[f249])).
% 0.14/10.44 fof(f251,plain,(
% 0.14/10.44 ![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.44 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.44 fof(f258,plain,(
% 0.14/10.44 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK16_skl(X0),X0))),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f251])).
% 0.14/10.44 fof(f271,plain,(
% 0.14/10.44 (?[X165]: (occurrence_of(X165,tptp0)&(![X166,X167]: ((~leaf_occ(X167,X165)|(occurrence_of(X167,tptp1)&(?[X168]: ((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0)))))|(occurrence_of(X167,tptp2)&(?[X169]: ((occurrence_of(X169,tptp1)&subactivity_occurrence(X169,X165))&min_precedes(X166,X169,tptp0))))))))),
% 0.14/10.44 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.14/10.44 fof(f272,definition,(
% 0.14/10.44 ![X165,X166,X167]: (sP0_prd(X167,X166,X165)<=>(occurrence_of(X167,tptp1)&(?[X168]: ((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0)))))),
% 0.14/10.44 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/10.44 fof(f273,plain,(
% 0.14/10.44 ?[X165]: (occurrence_of(X165,tptp0)&(![X166,X167]: ((~leaf_occ(X167,X165)|sP0_prd(X167,X166,X165))|(occurrence_of(X167,tptp2)&(?[X169]: ((occurrence_of(X169,tptp1)&subactivity_occurrence(X169,X165))&min_precedes(X166,X169,tptp0)))))))),
% 0.14/10.44 inference(formula_renaming,[status(thm)],[f271,f272])).
% 0.14/10.44 fof(f274,plain,(
% 0.14/10.44 (occurrence_of(sK19_skl,tptp0)&(![X166,X167]: ((~leaf_occ(X167,sK19_skl)|sP0_prd(X167,X166,sK19_skl))|(occurrence_of(X167,tptp2)&((occurrence_of(sK20_skl(X167,X166),tptp1)&subactivity_occurrence(sK20_skl(X167,X166),sK19_skl))&min_precedes(X166,sK20_skl(X167,X166),tptp0))))))),
% 0.14/10.44 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.44 fof(f275,plain,(
% 0.14/10.44 occurrence_of(sK19_skl,tptp0)),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/10.44 fof(f279,plain,(
% 0.14/10.44 ![X0,X1]: (~leaf_occ(X0,sK19_skl)|sP0_prd(X0,X1,sK19_skl)|min_precedes(X1,sK20_skl(X0,X1),tptp0))),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/10.44 fof(f280,plain,(
% 0.14/10.44 ![X165,X166,X167]: ((~sP0_prd(X167,X166,X165)|(occurrence_of(X167,tptp1)&(?[X168]: ((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0)))))&(sP0_prd(X167,X166,X165)|(~occurrence_of(X167,tptp1)|(![X168]: ((~occurrence_of(X168,tptp2)|~subactivity_occurrence(X168,X165))|~min_precedes(X166,X168,tptp0))))))),
% 0.14/10.44 inference(NNF_transformation,[status(thm)],[f272])).
% 0.14/10.44 fof(f281,plain,(
% 0.14/10.44 (![X165,X166,X167]: (~sP0_prd(X167,X166,X165)|(occurrence_of(X167,tptp1)&(?[X168]: ((occurrence_of(X168,tptp2)&subactivity_occurrence(X168,X165))&min_precedes(X166,X168,tptp0))))))&(![X165,X166,X167]: (sP0_prd(X167,X166,X165)|(~occurrence_of(X167,tptp1)|(![X168]: ((~occurrence_of(X168,tptp2)|~subactivity_occurrence(X168,X165))|~min_precedes(X166,X168,tptp0))))))),
% 0.14/10.44 inference(miniscoping,[status(thm)],[f280])).
% 0.14/10.44 fof(f282,plain,(
% 0.14/10.44 (![X165,X166,X167]: (~sP0_prd(X167,X166,X165)|(occurrence_of(X167,tptp1)&((occurrence_of(sK21_skl(X167,X166,X165),tptp2)&subactivity_occurrence(sK21_skl(X167,X166,X165),X165))&min_precedes(X166,sK21_skl(X167,X166,X165),tptp0)))))&(![X165,X166,X167]: (sP0_prd(X167,X166,X165)|(~occurrence_of(X167,tptp1)|(![X168]: ((~occurrence_of(X168,tptp2)|~subactivity_occurrence(X168,X165))|~min_precedes(X166,X168,tptp0))))))),
% 0.14/10.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(X168,sK21_skl(X167,X166,X165))],[f281])).
% 0.14/10.44 fof(f286,plain,(
% 0.14/10.44 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|min_precedes(X1,sK21_skl(X0,X1,X2),tptp0))),
% 0.14/10.44 inference(cnf_transformation,[status(thm)],[f282])).
% 0.14/10.44 fof(f289,plain,(
% 0.14/10.44 ![X0]: (~occurrence_of(sK19_skl,X0)|X0=tptp0)),
% 0.14/10.44 inference(resolution,[status(thm)],[f74,f275])).
% 0.14/10.44 fof(f359,plain,(
% 0.14/10.44 leaf_occ(sK16_skl(sK19_skl),sK19_skl)),
% 0.14/10.44 inference(resolution,[status(thm)],[f258,f275])).
% 0.14/10.44 fof(f361,plain,(
% 0.14/10.44 ![X0]: (sP0_prd(sK16_skl(sK19_skl),X0,sK19_skl)|min_precedes(X0,sK20_skl(sK16_skl(sK19_skl),X0),tptp0))),
% 0.14/10.44 inference(resolution,[status(thm)],[f359,f279])).
% 0.14/10.44 fof(f364,plain,(
% 0.14/10.44 leaf(sK16_skl(sK19_skl),sK14_skl(sK19_skl,sK16_skl(sK19_skl)))),
% 0.14/10.44 inference(resolution,[status(thm)],[f359,f203])).
% 0.14/10.44 fof(f365,plain,(
% 0.14/10.44 occurrence_of(sK19_skl,sK14_skl(sK19_skl,sK16_skl(sK19_skl)))),
% 0.14/10.44 inference(resolution,[status(thm)],[f359,f201])).
% 0.14/10.44 fof(f395,plain,(
% 0.14/10.44 sK14_skl(sK19_skl,sK16_skl(sK19_skl))=tptp0),
% 0.14/10.44 inference(resolution,[status(thm)],[f365,f289])).
% 0.14/10.44 fof(f401,plain,(
% 0.14/10.44 leaf(sK16_skl(sK19_skl),tptp0)),
% 0.14/10.44 inference(backward_demodulation,[status(thm)],[f395,f364])).
% 0.14/10.44 fof(f405,plain,(
% 0.14/10.44 ![X0]: (~min_precedes(sK16_skl(sK19_skl),X0,tptp0))),
% 0.14/10.44 inference(resolution,[status(thm)],[f401,f140])).
% 0.14/10.44 fof(f406,plain,(
% 0.14/10.44 ![X0,X1]: (~sP0_prd(X0,sK16_skl(sK19_skl),X1))),
% 0.14/10.44 inference(resolution,[status(thm)],[f405,f286])).
% 0.14/10.44 fof(f423,plain,(
% 0.14/10.44 sP0_prd(sK16_skl(sK19_skl),sK16_skl(sK19_skl),sK19_skl)),
% 0.14/10.44 inference(resolution,[status(thm)],[f361,f405])).
% 0.14/10.44 fof(f430,plain,(
% 0.14/10.44 $false),
% 0.14/10.44 inference(forward_subsumption_resolution,[status(thm)],[f423,f406])).
% 0.14/10.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/10.46 % Elapsed time: 0.068802 seconds
% 0.14/10.46 % CPU time: 0.221233 seconds
% 0.14/10.46 % Total memory used: 85.148 MB
% 0.14/10.46 % Net memory used: 84.998 MB
%------------------------------------------------------------------------------