%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO010+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 : n013.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.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO010+1 : 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/0.36 % Computer : n013.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 03:41:37 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 0.11/0.40 % Refutation found
% 0.11/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.40 fof(f3,axiom,(
% 0.11/0.40 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 0.11/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f22,axiom,(
% 0.11/0.40 (! [X56,X57] :( leaf(X56,X57)<=> ( ( root(X56,X57)| (? [X58] : min_precedes(X58,X56,X57) ))& ~ (? [X59] : min_precedes(X56,X59,X57) )) ) )),
% 0.11/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f35,axiom,(
% 0.11/0.40 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 0.11/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f36,axiom,(
% 0.11/0.40 (! [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.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f49,conjecture,(
% 0.11/0.40 (! [X109] :( occurrence_of(X109,tptp0)=> (? [X110,X111] :( leaf_occ(X111,X109)& ( occurrence_of(X111,tptp1)=> ~ (? [X112] :( occurrence_of(X112,tptp2)& min_precedes(X110,X112,tptp0) ) ))& ( occurrence_of(X111,tptp2)=> ~ (? [X113] :( occurrence_of(X113,tptp1)& min_precedes(X110,X113,tptp0) ) )) ) )) )),
% 0.11/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f50,negated_conjecture,(
% 0.11/0.40 ~((! [X109] :( occurrence_of(X109,tptp0)=> (? [X110,X111] :( leaf_occ(X111,X109)& ( occurrence_of(X111,tptp1)=> ~ (? [X112] :( occurrence_of(X112,tptp2)& min_precedes(X110,X112,tptp0) ) ))& ( occurrence_of(X111,tptp2)=> ~ (? [X113] :( occurrence_of(X113,tptp1)& min_precedes(X110,X113,tptp0) ) )) ) )) ))),
% 0.11/0.40 inference(negated_conjecture,[status(cth)],[f49])).
% 0.11/0.40 fof(f58,plain,(
% 0.11/0.40 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 0.11/0.40 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.11/0.40 fof(f59,plain,(
% 0.11/0.40 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 0.11/0.40 inference(miniscoping,[status(thm)],[f58])).
% 0.11/0.40 fof(f60,plain,(
% 0.11/0.40 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f59])).
% 0.11/0.40 fof(f121,plain,(
% 0.11/0.40 ![X56,X57]: (leaf(X56,X57)<=>((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57))))),
% 0.11/0.40 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.11/0.40 fof(f122,plain,(
% 0.11/0.40 ![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.40 inference(NNF_transformation,[status(thm)],[f121])).
% 0.11/0.40 fof(f123,plain,(
% 0.11/0.40 (![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.40 inference(miniscoping,[status(thm)],[f122])).
% 0.11/0.40 fof(f124,plain,(
% 0.11/0.40 (![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.40 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.40 fof(f126,plain,(
% 0.11/0.40 ![X0,X1,X2]: (~leaf(X0,X1)|~min_precedes(X0,X2,X1))),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f124])).
% 0.11/0.40 fof(f184,plain,(
% 0.11/0.40 ![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.40 inference(NNF_transformation,[status(thm)],[f35])).
% 0.11/0.40 fof(f185,plain,(
% 0.11/0.40 (![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.40 inference(miniscoping,[status(thm)],[f184])).
% 0.11/0.40 fof(f186,plain,(
% 0.11/0.40 (![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.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f185])).
% 0.11/0.40 fof(f187,plain,(
% 0.11/0.40 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK14_skl(X1,X0)))),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f186])).
% 0.11/0.40 fof(f189,plain,(
% 0.11/0.40 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK14_skl(X1,X0)))),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f186])).
% 0.11/0.40 fof(f191,plain,(
% 0.11/0.40 ![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.40 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.11/0.40 fof(f192,plain,(
% 0.11/0.40 ![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.40 inference(miniscoping,[status(thm)],[f191])).
% 0.11/0.40 fof(f193,plain,(
% 0.11/0.40 ![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.40 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.40 fof(f200,plain,(
% 0.11/0.40 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK15_skl(X0),X0))),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f193])).
% 0.11/0.40 fof(f213,plain,(
% 0.11/0.40 (?[X109]: (occurrence_of(X109,tptp0)&(![X110,X111]: ((~leaf_occ(X111,X109)|(occurrence_of(X111,tptp1)&(?[X112]: (occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0)))))|(occurrence_of(X111,tptp2)&(?[X113]: (occurrence_of(X113,tptp1)&min_precedes(X110,X113,tptp0))))))))),
% 0.11/0.40 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.11/0.40 fof(f214,definition,(
% 0.11/0.40 ![X110,X111]: (sP0_prd(X111,X110)<=>(occurrence_of(X111,tptp1)&(?[X112]: (occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0)))))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.11/0.40 fof(f215,plain,(
% 0.11/0.40 ?[X109]: (occurrence_of(X109,tptp0)&(![X110,X111]: ((~leaf_occ(X111,X109)|sP0_prd(X111,X110))|(occurrence_of(X111,tptp2)&(?[X113]: (occurrence_of(X113,tptp1)&min_precedes(X110,X113,tptp0)))))))),
% 0.11/0.40 inference(formula_renaming,[status(thm)],[f213,f214])).
% 0.11/0.40 fof(f216,plain,(
% 0.11/0.40 (occurrence_of(sK18_skl,tptp0)&(![X110,X111]: ((~leaf_occ(X111,sK18_skl)|sP0_prd(X111,X110))|(occurrence_of(X111,tptp2)&(occurrence_of(sK19_skl(X111,X110),tptp1)&min_precedes(X110,sK19_skl(X111,X110),tptp0))))))),
% 0.11/0.40 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.40 fof(f217,plain,(
% 0.11/0.40 occurrence_of(sK18_skl,tptp0)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f216])).
% 0.11/0.40 fof(f220,plain,(
% 0.11/0.40 ![X0,X1]: (~leaf_occ(X0,sK18_skl)|sP0_prd(X0,X1)|min_precedes(X1,sK19_skl(X0,X1),tptp0))),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f216])).
% 0.11/0.40 fof(f221,plain,(
% 0.11/0.40 ![X110,X111]: ((~sP0_prd(X111,X110)|(occurrence_of(X111,tptp1)&(?[X112]: (occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0)))))&(sP0_prd(X111,X110)|(~occurrence_of(X111,tptp1)|(![X112]: (~occurrence_of(X112,tptp2)|~min_precedes(X110,X112,tptp0))))))),
% 0.11/0.40 inference(NNF_transformation,[status(thm)],[f214])).
% 0.11/0.40 fof(f222,plain,(
% 0.11/0.40 (![X110,X111]: (~sP0_prd(X111,X110)|(occurrence_of(X111,tptp1)&(?[X112]: (occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0))))))&(![X110,X111]: (sP0_prd(X111,X110)|(~occurrence_of(X111,tptp1)|(![X112]: (~occurrence_of(X112,tptp2)|~min_precedes(X110,X112,tptp0))))))),
% 0.11/0.40 inference(miniscoping,[status(thm)],[f221])).
% 0.11/0.40 fof(f223,plain,(
% 0.11/0.40 (![X110,X111]: (~sP0_prd(X111,X110)|(occurrence_of(X111,tptp1)&(occurrence_of(sK20_skl(X111,X110),tptp2)&min_precedes(X110,sK20_skl(X111,X110),tptp0)))))&(![X110,X111]: (sP0_prd(X111,X110)|(~occurrence_of(X111,tptp1)|(![X112]: (~occurrence_of(X112,tptp2)|~min_precedes(X110,X112,tptp0))))))),
% 0.11/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X112,sK20_skl(X111,X110))],[f222])).
% 0.11/0.40 fof(f226,plain,(
% 0.11/0.40 ![X0,X1]: (~sP0_prd(X0,X1)|min_precedes(X1,sK20_skl(X0,X1),tptp0))),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f223])).
% 0.11/0.40 fof(f229,plain,(
% 0.11/0.40 ![X0]: (~occurrence_of(sK18_skl,X0)|X0=tptp0)),
% 0.11/0.40 inference(resolution,[status(thm)],[f60,f217])).
% 0.11/0.40 fof(f268,plain,(
% 0.11/0.40 leaf_occ(sK15_skl(sK18_skl),sK18_skl)),
% 0.11/0.40 inference(resolution,[status(thm)],[f200,f217])).
% 0.11/0.40 fof(f269,plain,(
% 0.11/0.40 ![X0]: (sP0_prd(sK15_skl(sK18_skl),X0)|min_precedes(X0,sK19_skl(sK15_skl(sK18_skl),X0),tptp0))),
% 0.11/0.40 inference(resolution,[status(thm)],[f268,f220])).
% 0.11/0.40 fof(f272,plain,(
% 0.11/0.40 leaf(sK15_skl(sK18_skl),sK14_skl(sK18_skl,sK15_skl(sK18_skl)))),
% 0.11/0.40 inference(resolution,[status(thm)],[f268,f189])).
% 0.11/0.40 fof(f273,plain,(
% 0.11/0.40 occurrence_of(sK18_skl,sK14_skl(sK18_skl,sK15_skl(sK18_skl)))),
% 0.11/0.40 inference(resolution,[status(thm)],[f268,f187])).
% 0.11/0.40 fof(f340,plain,(
% 0.11/0.40 sK14_skl(sK18_skl,sK15_skl(sK18_skl))=tptp0),
% 0.11/0.40 inference(resolution,[status(thm)],[f273,f229])).
% 0.11/0.40 fof(f346,plain,(
% 0.11/0.40 leaf(sK15_skl(sK18_skl),tptp0)),
% 0.11/0.40 inference(backward_demodulation,[status(thm)],[f340,f272])).
% 0.11/0.40 fof(f350,plain,(
% 0.11/0.40 ![X0]: (~min_precedes(sK15_skl(sK18_skl),X0,tptp0))),
% 0.11/0.40 inference(resolution,[status(thm)],[f346,f126])).
% 0.11/0.40 fof(f353,plain,(
% 0.11/0.40 ![X0]: (~sP0_prd(X0,sK15_skl(sK18_skl)))),
% 0.11/0.40 inference(resolution,[status(thm)],[f350,f226])).
% 0.11/0.40 fof(f358,plain,(
% 0.11/0.40 sP0_prd(sK15_skl(sK18_skl),sK15_skl(sK18_skl))),
% 0.11/0.40 inference(resolution,[status(thm)],[f269,f350])).
% 0.11/0.40 fof(f363,plain,(
% 0.11/0.40 $false),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f358,f353])).
% 0.11/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.43 % Elapsed time: 0.050675 seconds
% 0.11/0.43 % CPU time: 0.168760 seconds
% 0.11/0.43 % Total memory used: 84.138 MB
% 0.11/0.43 % Net memory used: 84.014 MB
%------------------------------------------------------------------------------