%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO011+1 : 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 : 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 01:59:24 PM UTC 2026
% Result : Theorem 0.11s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO011+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 03:44:16 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 0.11/0.38 % Refutation found
% 0.11/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.38 fof(f3,axiom,(
% 0.11/0.38 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f22,axiom,(
% 0.11/0.38 (! [X56,X57] :( leaf(X56,X57)<=> ( ( root(X56,X57)| (? [X58] : min_precedes(X58,X56,X57) ))& ~ (? [X59] : min_precedes(X56,X59,X57) )) ) )),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f35,axiom,(
% 0.11/0.38 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f36,axiom,(
% 0.11/0.38 (! [X105] :( occurrence_of(X105,tptp0)=> (? [X106,X107,X108] :( occurrence_of(X106,tptp3)& root_occ(X106,X105)& occurrence_of(X107,tptp4)& next_subocc(X106,X107,tptp0)& ( occurrence_of(X108,tptp1)| occurrence_of(X108,tptp2) )& next_subocc(X107,X108,tptp0)& leaf_occ(X108,X105) ) )) )),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f49,conjecture,(
% 0.11/0.38 (! [X109] :( occurrence_of(X109,tptp0)=> (? [X110,X111] :( leaf_occ(X111,X109)& ( occurrence_of(X111,tptp1)=> ~ (? [X112] :( occurrence_of(X112,tptp2)& subactivity_occurrence(X112,X109)& min_precedes(X110,X112,tptp0) ) ))& ( occurrence_of(X111,tptp2)=> ~ (? [X113] :( occurrence_of(X113,tptp1)& subactivity_occurrence(X113,X109)& min_precedes(X110,X113,tptp0) ) )) ) )) )),
% 0.11/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.38 fof(f50,negated_conjecture,(
% 0.11/0.38 ~((! [X109] :( occurrence_of(X109,tptp0)=> (? [X110,X111] :( leaf_occ(X111,X109)& ( occurrence_of(X111,tptp1)=> ~ (? [X112] :( occurrence_of(X112,tptp2)& subactivity_occurrence(X112,X109)& min_precedes(X110,X112,tptp0) ) ))& ( occurrence_of(X111,tptp2)=> ~ (? [X113] :( occurrence_of(X113,tptp1)& subactivity_occurrence(X113,X109)& min_precedes(X110,X113,tptp0) ) )) ) )) ))),
% 0.11/0.38 inference(negated_conjecture,[status(cth)],[f49])).
% 0.11/0.38 fof(f58,plain,(
% 0.11/0.38 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 0.11/0.38 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.11/0.38 fof(f59,plain,(
% 0.11/0.38 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 0.11/0.38 inference(miniscoping,[status(thm)],[f58])).
% 0.11/0.38 fof(f60,plain,(
% 0.11/0.38 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f59])).
% 0.11/0.38 fof(f121,plain,(
% 0.11/0.38 ![X56,X57]: (leaf(X56,X57)<=>((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57))))),
% 0.11/0.38 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.11/0.38 fof(f122,plain,(
% 0.11/0.38 ![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.11/0.38 inference(NNF_transformation,[status(thm)],[f121])).
% 0.11/0.38 fof(f123,plain,(
% 0.11/0.38 (![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.11/0.38 inference(miniscoping,[status(thm)],[f122])).
% 0.11/0.38 fof(f124,plain,(
% 0.11/0.38 (![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.11/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(X58,sK5_skl(X57,X56)),skolemize(X59,sK6_skl(X57,X56))],[f123])).
% 0.11/0.38 fof(f126,plain,(
% 0.11/0.38 ![X0,X1,X2]: (~leaf(X0,X1)|~min_precedes(X0,X2,X1))),
% 0.11/0.38 inference(cnf_transformation,[status(thm)],[f124])).
% 0.11/0.38 fof(f184,plain,(
% 0.11/0.38 ![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.11/0.38 inference(NNF_transformation,[status(thm)],[f35])).
% 0.11/0.39 fof(f185,plain,(
% 0.11/0.39 (![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.11/0.39 inference(miniscoping,[status(thm)],[f184])).
% 0.11/0.39 fof(f186,plain,(
% 0.11/0.39 (![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.11/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f185])).
% 0.11/0.39 fof(f187,plain,(
% 0.11/0.39 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK14_skl(X1,X0)))),
% 0.11/0.39 inference(cnf_transformation,[status(thm)],[f186])).
% 0.11/0.39 fof(f189,plain,(
% 0.11/0.39 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK14_skl(X1,X0)))),
% 0.11/0.39 inference(cnf_transformation,[status(thm)],[f186])).
% 0.11/0.39 fof(f191,plain,(
% 0.11/0.39 ![X105]: (~occurrence_of(X105,tptp0)|(?[X106,X107,X108]: ((((((occurrence_of(X106,tptp3)&root_occ(X106,X105))&occurrence_of(X107,tptp4))&next_subocc(X106,X107,tptp0))&(occurrence_of(X108,tptp1)|occurrence_of(X108,tptp2)))&next_subocc(X107,X108,tptp0))&leaf_occ(X108,X105))))),
% 0.11/0.39 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.11/0.39 fof(f192,plain,(
% 0.11/0.39 ![X105]: (~occurrence_of(X105,tptp0)|(?[X108]: ((?[X107]: (((?[X106]: (((occurrence_of(X106,tptp3)&root_occ(X106,X105))&occurrence_of(X107,tptp4))&next_subocc(X106,X107,tptp0)))&(occurrence_of(X108,tptp1)|occurrence_of(X108,tptp2)))&next_subocc(X107,X108,tptp0)))&leaf_occ(X108,X105))))),
% 0.11/0.39 inference(miniscoping,[status(thm)],[f191])).
% 0.11/0.39 fof(f193,plain,(
% 0.11/0.39 ![X105]: (~occurrence_of(X105,tptp0)|((((((occurrence_of(sK17_skl(X105),tptp3)&root_occ(sK17_skl(X105),X105))&occurrence_of(sK16_skl(X105),tptp4))&next_subocc(sK17_skl(X105),sK16_skl(X105),tptp0))&(occurrence_of(sK15_skl(X105),tptp1)|occurrence_of(sK15_skl(X105),tptp2)))&next_subocc(sK16_skl(X105),sK15_skl(X105),tptp0))&leaf_occ(sK15_skl(X105),X105)))),
% 0.11/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X108,sK15_skl(X105)),skolemize(X107,sK16_skl(X105)),skolemize(X106,sK17_skl(X105))],[f192])).
% 0.11/0.39 fof(f200,plain,(
% 0.11/0.39 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK15_skl(X0),X0))),
% 0.11/0.39 inference(cnf_transformation,[status(thm)],[f193])).
% 0.11/0.39 fof(f213,plain,(
% 0.11/0.39 (?[X109]: (occurrence_of(X109,tptp0)&(![X110,X111]: ((~leaf_occ(X111,X109)|(occurrence_of(X111,tptp1)&(?[X112]: ((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0)))))|(occurrence_of(X111,tptp2)&(?[X113]: ((occurrence_of(X113,tptp1)&subactivity_occurrence(X113,X109))&min_precedes(X110,X113,tptp0))))))))),
% 0.11/0.39 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.11/0.39 fof(f214,definition,(
% 0.11/0.39 ![X109,X110,X111]: (sP0_prd(X111,X110,X109)<=>(occurrence_of(X111,tptp1)&(?[X112]: ((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0)))))),
% 0.11/0.39 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.11/0.39 fof(f215,plain,(
% 0.11/0.39 ?[X109]: (occurrence_of(X109,tptp0)&(![X110,X111]: ((~leaf_occ(X111,X109)|sP0_prd(X111,X110,X109))|(occurrence_of(X111,tptp2)&(?[X113]: ((occurrence_of(X113,tptp1)&subactivity_occurrence(X113,X109))&min_precedes(X110,X113,tptp0)))))))),
% 0.11/0.39 inference(formula_renaming,[status(thm)],[f213,f214])).
% 0.11/0.39 fof(f216,plain,(
% 0.11/0.39 (occurrence_of(sK18_skl,tptp0)&(![X110,X111]: ((~leaf_occ(X111,sK18_skl)|sP0_prd(X111,X110,sK18_skl))|(occurrence_of(X111,tptp2)&((occurrence_of(sK19_skl(X111,X110),tptp1)&subactivity_occurrence(sK19_skl(X111,X110),sK18_skl))&min_precedes(X110,sK19_skl(X111,X110),tptp0))))))),
% 0.11/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl]),skolemize(X109,sK18_skl),skolemize(X113,sK19_skl(X111,X110))],[f215])).
% 0.11/0.39 fof(f217,plain,(
% 0.11/0.39 occurrence_of(sK18_skl,tptp0)),
% 0.11/0.39 inference(cnf_transformation,[status(thm)],[f216])).
% 0.11/0.39 fof(f221,plain,(
% 0.11/0.39 ![X0,X1]: (~leaf_occ(X0,sK18_skl)|sP0_prd(X0,X1,sK18_skl)|min_precedes(X1,sK19_skl(X0,X1),tptp0))),
% 0.11/0.39 inference(cnf_transformation,[status(thm)],[f216])).
% 0.11/0.39 fof(f222,plain,(
% 0.11/0.39 ![X109,X110,X111]: ((~sP0_prd(X111,X110,X109)|(occurrence_of(X111,tptp1)&(?[X112]: ((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0)))))&(sP0_prd(X111,X110,X109)|(~occurrence_of(X111,tptp1)|(![X112]: ((~occurrence_of(X112,tptp2)|~subactivity_occurrence(X112,X109))|~min_precedes(X110,X112,tptp0))))))),
% 0.11/0.39 inference(NNF_transformation,[status(thm)],[f214])).
% 0.11/0.39 fof(f223,plain,(
% 0.11/0.39 (![X109,X110,X111]: (~sP0_prd(X111,X110,X109)|(occurrence_of(X111,tptp1)&(?[X112]: ((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0))))))&(![X109,X110,X111]: (sP0_prd(X111,X110,X109)|(~occurrence_of(X111,tptp1)|(![X112]: ((~occurrence_of(X112,tptp2)|~subactivity_occurrence(X112,X109))|~min_precedes(X110,X112,tptp0))))))),
% 0.11/0.39 inference(miniscoping,[status(thm)],[f222])).
% 0.11/0.39 fof(f224,plain,(
% 0.11/0.39 (![X109,X110,X111]: (~sP0_prd(X111,X110,X109)|(occurrence_of(X111,tptp1)&((occurrence_of(sK20_skl(X111,X110,X109),tptp2)&subactivity_occurrence(sK20_skl(X111,X110,X109),X109))&min_precedes(X110,sK20_skl(X111,X110,X109),tptp0)))))&(![X109,X110,X111]: (sP0_prd(X111,X110,X109)|(~occurrence_of(X111,tptp1)|(![X112]: ((~occurrence_of(X112,tptp2)|~subactivity_occurrence(X112,X109))|~min_precedes(X110,X112,tptp0))))))),
% 0.11/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X112,sK20_skl(X111,X110,X109))],[f223])).
% 0.11/0.39 fof(f228,plain,(
% 0.11/0.39 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|min_precedes(X1,sK20_skl(X0,X1,X2),tptp0))),
% 0.11/0.39 inference(cnf_transformation,[status(thm)],[f224])).
% 0.11/0.39 fof(f231,plain,(
% 0.11/0.39 ![X0]: (~occurrence_of(sK18_skl,X0)|X0=tptp0)),
% 0.11/0.39 inference(resolution,[status(thm)],[f60,f217])).
% 0.11/0.39 fof(f271,plain,(
% 0.11/0.39 leaf_occ(sK15_skl(sK18_skl),sK18_skl)),
% 0.11/0.39 inference(resolution,[status(thm)],[f200,f217])).
% 0.11/0.39 fof(f273,plain,(
% 0.11/0.39 ![X0]: (sP0_prd(sK15_skl(sK18_skl),X0,sK18_skl)|min_precedes(X0,sK19_skl(sK15_skl(sK18_skl),X0),tptp0))),
% 0.11/0.39 inference(resolution,[status(thm)],[f271,f221])).
% 0.11/0.39 fof(f276,plain,(
% 0.11/0.39 leaf(sK15_skl(sK18_skl),sK14_skl(sK18_skl,sK15_skl(sK18_skl)))),
% 0.11/0.39 inference(resolution,[status(thm)],[f271,f189])).
% 0.11/0.39 fof(f277,plain,(
% 0.11/0.39 occurrence_of(sK18_skl,sK14_skl(sK18_skl,sK15_skl(sK18_skl)))),
% 0.11/0.39 inference(resolution,[status(thm)],[f271,f187])).
% 0.11/0.39 fof(f333,plain,(
% 0.11/0.39 sK14_skl(sK18_skl,sK15_skl(sK18_skl))=tptp0),
% 0.11/0.39 inference(resolution,[status(thm)],[f277,f231])).
% 0.11/0.39 fof(f339,plain,(
% 0.11/0.39 leaf(sK15_skl(sK18_skl),tptp0)),
% 0.11/0.39 inference(backward_demodulation,[status(thm)],[f333,f276])).
% 0.11/0.39 fof(f343,plain,(
% 0.11/0.39 ![X0]: (~min_precedes(sK15_skl(sK18_skl),X0,tptp0))),
% 0.11/0.39 inference(resolution,[status(thm)],[f339,f126])).
% 0.11/0.39 fof(f344,plain,(
% 0.11/0.39 ![X0,X1]: (~sP0_prd(X0,sK15_skl(sK18_skl),X1))),
% 0.11/0.39 inference(resolution,[status(thm)],[f343,f228])).
% 0.11/0.39 fof(f361,plain,(
% 0.11/0.39 sP0_prd(sK15_skl(sK18_skl),sK15_skl(sK18_skl),sK18_skl)),
% 0.11/0.39 inference(resolution,[status(thm)],[f273,f343])).
% 0.11/0.39 fof(f367,plain,(
% 0.11/0.39 $false),
% 0.11/0.39 inference(forward_subsumption_resolution,[status(thm)],[f361,f344])).
% 0.11/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.42 % Elapsed time: 0.062472 seconds
% 0.11/0.42 % CPU time: 0.166273 seconds
% 0.11/0.42 % Total memory used: 83.902 MB
% 0.11/0.42 % Net memory used: 83.781 MB
%------------------------------------------------------------------------------