%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO010+2 : 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 : n004.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.16s 5.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO010+2 : 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.10/5.57 % Computer : n004.cluster.edu
% 0.10/5.57 % Model : x86_64 x86_64
% 0.10/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.57 % Memory : 8046.5625MB
% 0.10/5.57 % OS : Linux 6.8.0-71-generic
% 0.10/5.57 % CPULimit : 300
% 0.10/5.57 % WCLimit : 300
% 0.10/5.57 % DateTime : Mon Sep 21 03:42:25 UTC 2026
% 0.10/5.57 % CPUTime :
% 0.10/5.59 % Drodi V4.1.1
% 0.16/5.63 % Refutation found
% 0.16/5.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/5.63 % SZS output start CNFRefutation for theBenchmark
% 0.16/5.63 fof(f12,axiom,(
% 0.16/5.63 (! [X35,X36] :( leaf_occ(X35,X36)<=> (? [X37] :( occurrence_of(X36,X37)& subactivity_occurrence(X35,X36)& leaf(X35,X37) ) )) )),
% 0.16/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.63 fof(f15,axiom,(
% 0.16/5.63 (! [X42,X43] :( leaf(X42,X43)<=> ( ( root(X42,X43)| (? [X44] : min_precedes(X44,X42,X43) ))& ~ (? [X45] : min_precedes(X42,X45,X43) )) ) )),
% 0.16/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.63 fof(f23,axiom,(
% 0.16/5.63 (! [X64,X65,X66] :( ( occurrence_of(X64,X65)& occurrence_of(X64,X66) )=> X65 = X66 ) )),
% 0.16/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.63 fof(f33,axiom,(
% 0.16/5.63 (! [X95] :( occurrence_of(X95,tptp0)=> (? [X96,X97,X98] :( occurrence_of(X96,tptp3)& root_occ(X96,X95)& occurrence_of(X97,tptp4)& next_subocc(X96,X97,tptp0)& ( occurrence_of(X98,tptp1)| occurrence_of(X98,tptp2) )& next_subocc(X97,X98,tptp0)& leaf_occ(X98,X95) ) )) )),
% 0.16/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.63 fof(f46,conjecture,(
% 0.16/5.63 (! [X99] :( occurrence_of(X99,tptp0)=> (? [X100,X101] :( leaf_occ(X101,X99)& ( occurrence_of(X101,tptp1)=> ~ (? [X102] :( occurrence_of(X102,tptp2)& min_precedes(X100,X102,tptp0) ) ))& ( occurrence_of(X101,tptp2)=> ~ (? [X103] :( occurrence_of(X103,tptp1)& min_precedes(X100,X103,tptp0) ) )) ) )) )),
% 0.16/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.63 fof(f47,negated_conjecture,(
% 0.16/5.63 ~((! [X99] :( occurrence_of(X99,tptp0)=> (? [X100,X101] :( leaf_occ(X101,X99)& ( occurrence_of(X101,tptp1)=> ~ (? [X102] :( occurrence_of(X102,tptp2)& min_precedes(X100,X102,tptp0) ) ))& ( occurrence_of(X101,tptp2)=> ~ (? [X103] :( occurrence_of(X103,tptp1)& min_precedes(X100,X103,tptp0) ) )) ) )) ))),
% 0.16/5.63 inference(negated_conjecture,[status(cth)],[f46])).
% 0.16/5.63 fof(f92,plain,(
% 0.16/5.63 ![X35,X36]: ((~leaf_occ(X35,X36)|(?[X37]: ((occurrence_of(X36,X37)&subactivity_occurrence(X35,X36))&leaf(X35,X37))))&(leaf_occ(X35,X36)|(![X37]: ((~occurrence_of(X36,X37)|~subactivity_occurrence(X35,X36))|~leaf(X35,X37)))))),
% 0.16/5.63 inference(NNF_transformation,[status(thm)],[f12])).
% 0.16/5.63 fof(f93,plain,(
% 0.16/5.63 (![X35,X36]: (~leaf_occ(X35,X36)|(?[X37]: ((occurrence_of(X36,X37)&subactivity_occurrence(X35,X36))&leaf(X35,X37)))))&(![X35,X36]: (leaf_occ(X35,X36)|(![X37]: ((~occurrence_of(X36,X37)|~subactivity_occurrence(X35,X36))|~leaf(X35,X37)))))),
% 0.16/5.63 inference(miniscoping,[status(thm)],[f92])).
% 0.16/5.63 fof(f94,plain,(
% 0.16/5.63 (![X35,X36]: (~leaf_occ(X35,X36)|((occurrence_of(X36,sK2_skl(X36,X35))&subactivity_occurrence(X35,X36))&leaf(X35,sK2_skl(X36,X35)))))&(![X35,X36]: (leaf_occ(X35,X36)|(![X37]: ((~occurrence_of(X36,X37)|~subactivity_occurrence(X35,X36))|~leaf(X35,X37)))))),
% 0.16/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X37,sK2_skl(X36,X35))],[f93])).
% 0.16/5.63 fof(f95,plain,(
% 0.16/5.63 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK2_skl(X1,X0)))),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f94])).
% 0.16/5.63 fof(f97,plain,(
% 0.16/5.63 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK2_skl(X1,X0)))),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f94])).
% 0.16/5.63 fof(f106,plain,(
% 0.16/5.63 ![X42,X43]: (leaf(X42,X43)<=>((root(X42,X43)|(?[X44]: min_precedes(X44,X42,X43)))&(![X45]: ~min_precedes(X42,X45,X43))))),
% 0.16/5.63 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.16/5.63 fof(f107,plain,(
% 0.16/5.63 ![X42,X43]: ((~leaf(X42,X43)|((root(X42,X43)|(?[X44]: min_precedes(X44,X42,X43)))&(![X45]: ~min_precedes(X42,X45,X43))))&(leaf(X42,X43)|((~root(X42,X43)&(![X44]: ~min_precedes(X44,X42,X43)))|(?[X45]: min_precedes(X42,X45,X43)))))),
% 0.16/5.63 inference(NNF_transformation,[status(thm)],[f106])).
% 0.16/5.63 fof(f108,plain,(
% 0.16/5.63 (![X42,X43]: (~leaf(X42,X43)|((root(X42,X43)|(?[X44]: min_precedes(X44,X42,X43)))&(![X45]: ~min_precedes(X42,X45,X43)))))&(![X42,X43]: (leaf(X42,X43)|((~root(X42,X43)&(![X44]: ~min_precedes(X44,X42,X43)))|(?[X45]: min_precedes(X42,X45,X43)))))),
% 0.16/5.63 inference(miniscoping,[status(thm)],[f107])).
% 0.16/5.63 fof(f109,plain,(
% 0.16/5.63 (![X42,X43]: (~leaf(X42,X43)|((root(X42,X43)|min_precedes(sK3_skl(X43,X42),X42,X43))&(![X45]: ~min_precedes(X42,X45,X43)))))&(![X42,X43]: (leaf(X42,X43)|((~root(X42,X43)&(![X44]: ~min_precedes(X44,X42,X43)))|min_precedes(X42,sK4_skl(X43,X42),X43))))),
% 0.16/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(X44,sK3_skl(X43,X42)),skolemize(X45,sK4_skl(X43,X42))],[f108])).
% 0.16/5.63 fof(f111,plain,(
% 0.16/5.63 ![X0,X1,X2]: (~leaf(X0,X1)|~min_precedes(X0,X2,X1))),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f109])).
% 0.16/5.63 fof(f138,plain,(
% 0.16/5.63 ![X64,X65,X66]: ((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)),
% 0.16/5.63 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.16/5.63 fof(f139,plain,(
% 0.16/5.63 ![X65,X66]: ((![X64]: (~occurrence_of(X64,X65)|~occurrence_of(X64,X66)))|X65=X66)),
% 0.16/5.63 inference(miniscoping,[status(thm)],[f138])).
% 0.16/5.63 fof(f140,plain,(
% 0.16/5.63 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f139])).
% 0.16/5.63 fof(f177,plain,(
% 0.16/5.63 ![X95]: (~occurrence_of(X95,tptp0)|(?[X96,X97,X98]: ((((((occurrence_of(X96,tptp3)&root_occ(X96,X95))&occurrence_of(X97,tptp4))&next_subocc(X96,X97,tptp0))&(occurrence_of(X98,tptp1)|occurrence_of(X98,tptp2)))&next_subocc(X97,X98,tptp0))&leaf_occ(X98,X95))))),
% 0.16/5.63 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.16/5.63 fof(f178,plain,(
% 0.16/5.63 ![X95]: (~occurrence_of(X95,tptp0)|(?[X98]: ((?[X97]: (((?[X96]: (((occurrence_of(X96,tptp3)&root_occ(X96,X95))&occurrence_of(X97,tptp4))&next_subocc(X96,X97,tptp0)))&(occurrence_of(X98,tptp1)|occurrence_of(X98,tptp2)))&next_subocc(X97,X98,tptp0)))&leaf_occ(X98,X95))))),
% 0.16/5.63 inference(miniscoping,[status(thm)],[f177])).
% 0.16/5.63 fof(f179,plain,(
% 0.16/5.63 ![X95]: (~occurrence_of(X95,tptp0)|((((((occurrence_of(sK16_skl(X95),tptp3)&root_occ(sK16_skl(X95),X95))&occurrence_of(sK15_skl(X95),tptp4))&next_subocc(sK16_skl(X95),sK15_skl(X95),tptp0))&(occurrence_of(sK14_skl(X95),tptp1)|occurrence_of(sK14_skl(X95),tptp2)))&next_subocc(sK15_skl(X95),sK14_skl(X95),tptp0))&leaf_occ(sK14_skl(X95),X95)))),
% 0.16/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X98,sK14_skl(X95)),skolemize(X97,sK15_skl(X95)),skolemize(X96,sK16_skl(X95))],[f178])).
% 0.16/5.63 fof(f186,plain,(
% 0.16/5.63 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK14_skl(X0),X0))),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f179])).
% 0.16/5.63 fof(f199,plain,(
% 0.16/5.63 (?[X99]: (occurrence_of(X99,tptp0)&(![X100,X101]: ((~leaf_occ(X101,X99)|(occurrence_of(X101,tptp1)&(?[X102]: (occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0)))))|(occurrence_of(X101,tptp2)&(?[X103]: (occurrence_of(X103,tptp1)&min_precedes(X100,X103,tptp0))))))))),
% 0.16/5.63 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.16/5.63 fof(f200,definition,(
% 0.16/5.63 ![X100,X101]: (sP0_prd(X101,X100)<=>(occurrence_of(X101,tptp1)&(?[X102]: (occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0)))))),
% 0.16/5.63 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.16/5.63 fof(f201,plain,(
% 0.16/5.63 ?[X99]: (occurrence_of(X99,tptp0)&(![X100,X101]: ((~leaf_occ(X101,X99)|sP0_prd(X101,X100))|(occurrence_of(X101,tptp2)&(?[X103]: (occurrence_of(X103,tptp1)&min_precedes(X100,X103,tptp0)))))))),
% 0.16/5.63 inference(formula_renaming,[status(thm)],[f199,f200])).
% 0.16/5.63 fof(f202,plain,(
% 0.16/5.63 (occurrence_of(sK17_skl,tptp0)&(![X100,X101]: ((~leaf_occ(X101,sK17_skl)|sP0_prd(X101,X100))|(occurrence_of(X101,tptp2)&(occurrence_of(sK18_skl(X101,X100),tptp1)&min_precedes(X100,sK18_skl(X101,X100),tptp0))))))),
% 0.16/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(X99,sK17_skl),skolemize(X103,sK18_skl(X101,X100))],[f201])).
% 0.16/5.63 fof(f203,plain,(
% 0.16/5.63 occurrence_of(sK17_skl,tptp0)),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f202])).
% 0.16/5.63 fof(f206,plain,(
% 0.16/5.63 ![X0,X1]: (~leaf_occ(X0,sK17_skl)|sP0_prd(X0,X1)|min_precedes(X1,sK18_skl(X0,X1),tptp0))),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f202])).
% 0.16/5.63 fof(f207,plain,(
% 0.16/5.63 ![X100,X101]: ((~sP0_prd(X101,X100)|(occurrence_of(X101,tptp1)&(?[X102]: (occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0)))))&(sP0_prd(X101,X100)|(~occurrence_of(X101,tptp1)|(![X102]: (~occurrence_of(X102,tptp2)|~min_precedes(X100,X102,tptp0))))))),
% 0.16/5.63 inference(NNF_transformation,[status(thm)],[f200])).
% 0.16/5.63 fof(f208,plain,(
% 0.16/5.63 (![X100,X101]: (~sP0_prd(X101,X100)|(occurrence_of(X101,tptp1)&(?[X102]: (occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0))))))&(![X100,X101]: (sP0_prd(X101,X100)|(~occurrence_of(X101,tptp1)|(![X102]: (~occurrence_of(X102,tptp2)|~min_precedes(X100,X102,tptp0))))))),
% 0.16/5.63 inference(miniscoping,[status(thm)],[f207])).
% 0.16/5.63 fof(f209,plain,(
% 0.16/5.63 (![X100,X101]: (~sP0_prd(X101,X100)|(occurrence_of(X101,tptp1)&(occurrence_of(sK19_skl(X101,X100),tptp2)&min_precedes(X100,sK19_skl(X101,X100),tptp0)))))&(![X100,X101]: (sP0_prd(X101,X100)|(~occurrence_of(X101,tptp1)|(![X102]: (~occurrence_of(X102,tptp2)|~min_precedes(X100,X102,tptp0))))))),
% 0.16/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(X102,sK19_skl(X101,X100))],[f208])).
% 0.16/5.63 fof(f212,plain,(
% 0.16/5.63 ![X0,X1]: (~sP0_prd(X0,X1)|min_precedes(X1,sK19_skl(X0,X1),tptp0))),
% 0.16/5.63 inference(cnf_transformation,[status(thm)],[f209])).
% 0.16/5.63 fof(f215,plain,(
% 0.16/5.63 ![X0]: (~occurrence_of(sK17_skl,X0)|X0=tptp0)),
% 0.16/5.63 inference(resolution,[status(thm)],[f140,f203])).
% 0.16/5.63 fof(f348,plain,(
% 0.16/5.63 leaf_occ(sK14_skl(sK17_skl),sK17_skl)),
% 0.16/5.63 inference(resolution,[status(thm)],[f186,f203])).
% 0.16/5.63 fof(f349,plain,(
% 0.16/5.63 ![X0]: (sP0_prd(sK14_skl(sK17_skl),X0)|min_precedes(X0,sK18_skl(sK14_skl(sK17_skl),X0),tptp0))),
% 0.16/5.63 inference(resolution,[status(thm)],[f348,f206])).
% 0.16/5.63 fof(f352,plain,(
% 0.16/5.63 leaf(sK14_skl(sK17_skl),sK2_skl(sK17_skl,sK14_skl(sK17_skl)))),
% 0.16/5.63 inference(resolution,[status(thm)],[f348,f97])).
% 0.16/5.63 fof(f353,plain,(
% 0.16/5.63 occurrence_of(sK17_skl,sK2_skl(sK17_skl,sK14_skl(sK17_skl)))),
% 0.16/5.63 inference(resolution,[status(thm)],[f348,f95])).
% 0.16/5.63 fof(f447,plain,(
% 0.16/5.63 sK2_skl(sK17_skl,sK14_skl(sK17_skl))=tptp0),
% 0.16/5.63 inference(resolution,[status(thm)],[f353,f215])).
% 0.16/5.63 fof(f453,plain,(
% 0.16/5.63 leaf(sK14_skl(sK17_skl),tptp0)),
% 0.16/5.63 inference(backward_demodulation,[status(thm)],[f447,f352])).
% 0.16/5.63 fof(f459,plain,(
% 0.16/5.63 ![X0]: (~min_precedes(sK14_skl(sK17_skl),X0,tptp0))),
% 0.16/5.63 inference(resolution,[status(thm)],[f453,f111])).
% 0.16/5.63 fof(f460,plain,(
% 0.16/5.63 sP0_prd(sK14_skl(sK17_skl),sK14_skl(sK17_skl))),
% 0.16/5.63 inference(resolution,[status(thm)],[f459,f349])).
% 0.16/5.63 fof(f462,plain,(
% 0.16/5.63 ![X0]: (~sP0_prd(X0,sK14_skl(sK17_skl)))),
% 0.16/5.63 inference(resolution,[status(thm)],[f459,f212])).
% 0.16/5.63 fof(f466,plain,(
% 0.16/5.63 $false),
% 0.16/5.63 inference(backward_subsumption_resolution,[status(thm)],[f460,f462])).
% 0.16/5.63 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/5.64 % Elapsed time: 0.056992 seconds
% 0.16/5.64 % CPU time: 0.201253 seconds
% 0.16/5.64 % Total memory used: 71.482 MB
% 0.16/5.64 % Net memory used: 71.361 MB
%------------------------------------------------------------------------------