%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO017+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 : n016.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:26 PM UTC 2026
% Result : Theorem 45.26s 6.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO017+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.08/0.36 % Computer : n016.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 03:48:37 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 45.26/6.20 % Refutation found
% 45.26/6.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 45.26/6.20 % SZS output start CNFRefutation for theBenchmark
% 45.26/6.20 fof(f1,axiom,(
% 45.26/6.20 (! [X0,X1] :( occurrence_of(X1,X0)=> ( activity(X0)& activity_occurrence(X1) ) ) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f2,axiom,(
% 45.26/6.20 (! [X2] :( activity_occurrence(X2)=> (? [X3] :( activity(X3)& occurrence_of(X2,X3) ) )) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f3,axiom,(
% 45.26/6.20 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f8,axiom,(
% 45.26/6.20 (! [X16,X17] :( occurrence_of(X16,X17)=> ( arboreal(X16)<=> atomic(X17) ) ) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f22,axiom,(
% 45.26/6.20 (! [X56,X57] :( leaf(X56,X57)<=> ( ( root(X56,X57)| (? [X58] : min_precedes(X58,X56,X57) ))& ~ (? [X59] : min_precedes(X56,X59,X57) )) ) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f23,axiom,(
% 45.26/6.20 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f26,axiom,(
% 45.26/6.20 (! [X69,X70,X71] :( min_precedes(X70,X71,X69)=> (? [X72] :( occurrence_of(X72,X69)& subactivity_occurrence(X70,X72)& subactivity_occurrence(X71,X72) ) )) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f38,axiom,(
% 45.26/6.20 (! [X113,X114,X115] :( ( occurrence_of(X113,X115)& leaf_occ(X114,X113) )=> ~ (? [X116] : min_precedes(X114,X116,X115) )) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f50,axiom,(
% 45.26/6.20 (! [X161,X162] :( ( occurrence_of(X162,tptp0)& subactivity_occurrence(X161,X162)& arboreal(X161)& ~ leaf_occ(X161,X162) )=> (? [X163,X164,X165] :( occurrence_of(X163,tptp3)& next_subocc(X161,X163,tptp0)& occurrence_of(X164,tptp4)& min_precedes(X163,X164,tptp0)& ( occurrence_of(X165,tptp2)| occurrence_of(X165,tptp1) )& min_precedes(X164,X165,tptp0)& (! [X166] :( min_precedes(X163,X166,tptp0)=> ( X166 = X164| X166 = X165 ) ) )) )) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f56,axiom,(
% 45.26/6.20 atomic(tptp3) ),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f57,axiom,(
% 45.26/6.20 tptp4 != tptp3 ),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f63,conjecture,(
% 45.26/6.20 (! [X167,X168] :( ( occurrence_of(X168,tptp0)& subactivity_occurrence(X167,X168)& arboreal(X167)& ~ leaf_occ(X167,X168) )=> (? [X169,X170] :( occurrence_of(X169,tptp3)& next_subocc(X167,X169,tptp0)& ( occurrence_of(X170,tptp2)| occurrence_of(X170,tptp1) )& min_precedes(X169,X170,tptp0)& leaf(X170,tptp0) ) )) )),
% 45.26/6.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 45.26/6.20 fof(f64,negated_conjecture,(
% 45.26/6.20 ~((! [X167,X168] :( ( occurrence_of(X168,tptp0)& subactivity_occurrence(X167,X168)& arboreal(X167)& ~ leaf_occ(X167,X168) )=> (? [X169,X170] :( occurrence_of(X169,tptp3)& next_subocc(X167,X169,tptp0)& ( occurrence_of(X170,tptp2)| occurrence_of(X170,tptp1) )& min_precedes(X169,X170,tptp0)& leaf(X170,tptp0) ) )) ))),
% 45.26/6.20 inference(negated_conjecture,[status(cth)],[f63])).
% 45.26/6.20 fof(f65,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X1,X0)|(activity(X0)&activity_occurrence(X1)))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 45.26/6.20 fof(f67,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f65])).
% 45.26/6.20 fof(f68,plain,(
% 45.26/6.20 ![X2]: (~activity_occurrence(X2)|(?[X3]: (activity(X3)&occurrence_of(X2,X3))))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 45.26/6.20 fof(f69,plain,(
% 45.26/6.20 ![X2]: (~activity_occurrence(X2)|(activity(sK0_skl(X2))&occurrence_of(X2,sK0_skl(X2))))),
% 45.26/6.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X3,sK0_skl(X2))],[f68])).
% 45.26/6.20 fof(f71,plain,(
% 45.26/6.20 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK0_skl(X0)))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f69])).
% 45.26/6.20 fof(f72,plain,(
% 45.26/6.20 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 45.26/6.20 fof(f73,plain,(
% 45.26/6.20 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 45.26/6.20 inference(miniscoping,[status(thm)],[f72])).
% 45.26/6.20 fof(f74,plain,(
% 45.26/6.20 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f73])).
% 45.26/6.20 fof(f85,plain,(
% 45.26/6.20 ![X16,X17]: (~occurrence_of(X16,X17)|(arboreal(X16)<=>atomic(X17)))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 45.26/6.20 fof(f86,plain,(
% 45.26/6.20 ![X16,X17]: (~occurrence_of(X16,X17)|((~arboreal(X16)|atomic(X17))&(arboreal(X16)|~atomic(X17))))),
% 45.26/6.20 inference(NNF_transformation,[status(thm)],[f85])).
% 45.26/6.20 fof(f88,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f86])).
% 45.26/6.20 fof(f135,plain,(
% 45.26/6.20 ![X56,X57]: (leaf(X56,X57)<=>((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57))))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 45.26/6.20 fof(f136,plain,(
% 45.26/6.20 ![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)))))),
% 45.26/6.20 inference(NNF_transformation,[status(thm)],[f135])).
% 45.26/6.20 fof(f137,plain,(
% 45.26/6.20 (![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)))))),
% 45.26/6.20 inference(miniscoping,[status(thm)],[f136])).
% 45.26/6.20 fof(f138,plain,(
% 45.26/6.20 (![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))))),
% 45.26/6.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(X58,sK5_skl(X57,X56)),skolemize(X59,sK6_skl(X57,X56))],[f137])).
% 45.26/6.20 fof(f140,plain,(
% 45.26/6.20 ![X0,X1,X2]: (~leaf(X0,X1)|~min_precedes(X0,X2,X1))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f138])).
% 45.26/6.20 fof(f142,plain,(
% 45.26/6.20 ![X0,X1,X2]: (leaf(X0,X1)|~min_precedes(X2,X0,X1)|min_precedes(X0,sK6_skl(X1,X0),X1))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f138])).
% 45.26/6.20 fof(f143,plain,(
% 45.26/6.20 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 45.26/6.20 fof(f144,plain,(
% 45.26/6.20 ![X60,X61,X62]: ((~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))&(next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 45.26/6.20 inference(NNF_transformation,[status(thm)],[f143])).
% 45.26/6.20 fof(f145,plain,(
% 45.26/6.20 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 45.26/6.20 inference(miniscoping,[status(thm)],[f144])).
% 45.26/6.20 fof(f146,plain,(
% 45.26/6.20 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(min_precedes(X60,sK7_skl(X62,X61,X60),X62)&min_precedes(sK7_skl(X62,X61,X60),X61,X62)))))),
% 45.26/6.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f145])).
% 45.26/6.20 fof(f147,plain,(
% 45.26/6.20 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f146])).
% 45.26/6.20 fof(f148,plain,(
% 45.26/6.20 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f146])).
% 45.26/6.20 fof(f161,plain,(
% 45.26/6.20 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|(?[X72]: ((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 45.26/6.20 fof(f162,plain,(
% 45.26/6.20 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|((occurrence_of(sK9_skl(X71,X70,X69),X69)&subactivity_occurrence(X70,sK9_skl(X71,X70,X69)))&subactivity_occurrence(X71,sK9_skl(X71,X70,X69))))),
% 45.26/6.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f161])).
% 45.26/6.20 fof(f163,plain,(
% 45.26/6.20 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK9_skl(X1,X0,X2),X2))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f162])).
% 45.26/6.20 fof(f164,plain,(
% 45.26/6.20 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK9_skl(X1,X0,X2)))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f162])).
% 45.26/6.20 fof(f211,plain,(
% 45.26/6.20 ![X113,X114,X115]: ((~occurrence_of(X113,X115)|~leaf_occ(X114,X113))|(![X116]: ~min_precedes(X114,X116,X115)))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 45.26/6.20 fof(f212,plain,(
% 45.26/6.20 ![X114,X115]: ((![X113]: (~occurrence_of(X113,X115)|~leaf_occ(X114,X113)))|(![X116]: ~min_precedes(X114,X116,X115)))),
% 45.26/6.20 inference(miniscoping,[status(thm)],[f211])).
% 45.26/6.20 fof(f213,plain,(
% 45.26/6.20 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f212])).
% 45.26/6.20 fof(f249,plain,(
% 45.26/6.20 ![X161,X162]: ((((~occurrence_of(X162,tptp0)|~subactivity_occurrence(X161,X162))|~arboreal(X161))|leaf_occ(X161,X162))|(?[X163,X164,X165]: ((((((occurrence_of(X163,tptp3)&next_subocc(X161,X163,tptp0))&occurrence_of(X164,tptp4))&min_precedes(X163,X164,tptp0))&(occurrence_of(X165,tptp2)|occurrence_of(X165,tptp1)))&min_precedes(X164,X165,tptp0))&(![X166]: (~min_precedes(X163,X166,tptp0)|(X166=X164|X166=X165))))))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 45.26/6.20 fof(f250,plain,(
% 45.26/6.20 ![X161]: ((![X162]: (((~occurrence_of(X162,tptp0)|~subactivity_occurrence(X161,X162))|~arboreal(X161))|leaf_occ(X161,X162)))|(?[X163,X164,X165]: ((((((occurrence_of(X163,tptp3)&next_subocc(X161,X163,tptp0))&occurrence_of(X164,tptp4))&min_precedes(X163,X164,tptp0))&(occurrence_of(X165,tptp2)|occurrence_of(X165,tptp1)))&min_precedes(X164,X165,tptp0))&(![X166]: (~min_precedes(X163,X166,tptp0)|(X166=X164|X166=X165))))))),
% 45.26/6.20 inference(miniscoping,[status(thm)],[f249])).
% 45.26/6.20 fof(f251,plain,(
% 45.26/6.20 ![X161]: ((![X162]: (((~occurrence_of(X162,tptp0)|~subactivity_occurrence(X161,X162))|~arboreal(X161))|leaf_occ(X161,X162)))|((((((occurrence_of(sK16_skl(X161),tptp3)&next_subocc(X161,sK16_skl(X161),tptp0))&occurrence_of(sK17_skl(X161),tptp4))&min_precedes(sK16_skl(X161),sK17_skl(X161),tptp0))&(occurrence_of(sK18_skl(X161),tptp2)|occurrence_of(sK18_skl(X161),tptp1)))&min_precedes(sK17_skl(X161),sK18_skl(X161),tptp0))&(![X166]: (~min_precedes(sK16_skl(X161),X166,tptp0)|(X166=sK17_skl(X161)|X166=sK18_skl(X161))))))),
% 45.26/6.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X163,sK16_skl(X161)),skolemize(X164,sK17_skl(X161)),skolemize(X165,sK18_skl(X161))],[f250])).
% 45.26/6.20 fof(f252,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp3))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f251])).
% 45.26/6.20 fof(f253,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK16_skl(X1),tptp0))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f251])).
% 45.26/6.20 fof(f254,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK17_skl(X1),tptp4))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f251])).
% 45.26/6.20 fof(f255,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK16_skl(X1),sK17_skl(X1),tptp0))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f251])).
% 45.26/6.20 fof(f257,plain,(
% 45.26/6.20 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK17_skl(X1),sK18_skl(X1),tptp0))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f251])).
% 45.26/6.20 fof(f258,plain,(
% 45.26/6.20 ![X0,X1,X2]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|~min_precedes(sK16_skl(X1),X2,tptp0)|X2=sK17_skl(X1)|X2=sK18_skl(X1))),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f251])).
% 45.26/6.20 fof(f264,plain,(
% 45.26/6.20 atomic(tptp3)),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f56])).
% 45.26/6.20 fof(f265,plain,(
% 45.26/6.20 ~tptp4=tptp3),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f57])).
% 45.26/6.20 fof(f271,plain,(
% 45.26/6.20 (?[X167,X168]: ((((occurrence_of(X168,tptp0)&subactivity_occurrence(X167,X168))&arboreal(X167))&~leaf_occ(X167,X168))&(![X169,X170]: ((((~occurrence_of(X169,tptp3)|~next_subocc(X167,X169,tptp0))|(~occurrence_of(X170,tptp2)&~occurrence_of(X170,tptp1)))|~min_precedes(X169,X170,tptp0))|~leaf(X170,tptp0)))))),
% 45.26/6.20 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 45.26/6.20 fof(f272,plain,(
% 45.26/6.20 ?[X167]: ((?[X168]: (((occurrence_of(X168,tptp0)&subactivity_occurrence(X167,X168))&arboreal(X167))&~leaf_occ(X167,X168)))&(![X170]: ((![X169]: (((~occurrence_of(X169,tptp3)|~next_subocc(X167,X169,tptp0))|(~occurrence_of(X170,tptp2)&~occurrence_of(X170,tptp1)))|~min_precedes(X169,X170,tptp0)))|~leaf(X170,tptp0))))),
% 45.26/6.20 inference(miniscoping,[status(thm)],[f271])).
% 45.26/6.20 fof(f273,plain,(
% 45.26/6.20 ((((occurrence_of(sK20_skl,tptp0)&subactivity_occurrence(sK19_skl,sK20_skl))&arboreal(sK19_skl))&~leaf_occ(sK19_skl,sK20_skl))&(![X170]: ((![X169]: (((~occurrence_of(X169,tptp3)|~next_subocc(sK19_skl,X169,tptp0))|(~occurrence_of(X170,tptp2)&~occurrence_of(X170,tptp1)))|~min_precedes(X169,X170,tptp0)))|~leaf(X170,tptp0))))),
% 45.26/6.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X167,sK19_skl),skolemize(X168,sK20_skl)],[f272])).
% 45.26/6.20 fof(f274,plain,(
% 45.26/6.20 occurrence_of(sK20_skl,tptp0)),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f273])).
% 45.26/6.20 fof(f275,plain,(
% 45.26/6.20 subactivity_occurrence(sK19_skl,sK20_skl)),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f273])).
% 45.26/6.20 fof(f276,plain,(
% 45.26/6.20 arboreal(sK19_skl)),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f273])).
% 45.26/6.20 fof(f277,plain,(
% 45.26/6.20 ~leaf_occ(sK19_skl,sK20_skl)),
% 45.26/6.20 inference(cnf_transformation,[status(thm)],[f273])).
% 45.26/6.20 fof(f792,plain,(
% 45.26/6.20 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 45.26/6.20 inference(resolution,[status(thm)],[f252,f275])).
% 45.26/6.20 fof(f795,plain,(
% 45.26/6.20 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f792,f274])).
% 45.26/6.20 fof(f929,plain,(
% 45.26/6.20 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f253,f275])).
% 45.26/6.20 fof(f933,plain,(
% 45.26/6.20 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f929,f274])).
% 45.26/6.20 fof(f940,plain,(
% 45.26/6.20 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK17_skl(sK19_skl),tptp4)),
% 45.26/6.20 inference(resolution,[status(thm)],[f254,f275])).
% 45.26/6.20 fof(f944,plain,(
% 45.26/6.20 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK17_skl(sK19_skl),tptp4)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f940,f274])).
% 45.26/6.20 fof(f951,plain,(
% 45.26/6.20 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f255,f275])).
% 45.26/6.20 fof(f955,plain,(
% 45.26/6.20 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f951,f274])).
% 45.26/6.20 fof(f984,plain,(
% 45.26/6.20 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK17_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f257,f275])).
% 45.26/6.20 fof(f988,plain,(
% 45.26/6.20 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK17_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f984,f274])).
% 45.26/6.20 fof(f995,plain,(
% 45.26/6.20 ![X0]: (~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|~min_precedes(sK16_skl(sK19_skl),X0,tptp0)|X0=sK17_skl(sK19_skl)|X0=sK18_skl(sK19_skl))),
% 45.26/6.20 inference(resolution,[status(thm)],[f258,f275])).
% 45.26/6.20 fof(f999,plain,(
% 45.26/6.20 ![X0]: (~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|~min_precedes(sK16_skl(sK19_skl),X0,tptp0)|X0=sK17_skl(sK19_skl)|X0=sK18_skl(sK19_skl))),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f995,f274])).
% 45.26/6.20 fof(f1013,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f795,f276])).
% 45.26/6.20 fof(f1049,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|arboreal(sK16_skl(sK19_skl))|~atomic(tptp3)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1013,f88])).
% 45.26/6.20 fof(f1085,plain,(
% 45.26/6.20 arboreal(sK16_skl(sK19_skl))|~atomic(tptp3)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1049,f277])).
% 45.26/6.20 fof(f1099,plain,(
% 45.26/6.20 arboreal(sK16_skl(sK19_skl))),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1085,f264])).
% 45.26/6.20 fof(f1105,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f933,f276])).
% 45.26/6.20 fof(f1120,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1105,f147])).
% 45.26/6.20 fof(f1131,plain,(
% 45.26/6.20 min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1120,f277])).
% 45.26/6.20 fof(f1138,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK17_skl(sK19_skl),tptp4)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f944,f276])).
% 45.26/6.20 fof(f1175,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|activity_occurrence(sK17_skl(sK19_skl))),
% 45.26/6.20 inference(resolution,[status(thm)],[f1138,f67])).
% 45.26/6.20 fof(f1179,plain,(
% 45.26/6.20 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~occurrence_of(sK17_skl(sK19_skl),X0)|X0=tptp4)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1138,f74])).
% 45.26/6.20 fof(f1211,plain,(
% 45.26/6.20 activity_occurrence(sK17_skl(sK19_skl))),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1175,f277])).
% 45.26/6.20 fof(f1213,plain,(
% 45.26/6.20 ![X0]: (~occurrence_of(sK17_skl(sK19_skl),X0)|X0=tptp4)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1179,f277])).
% 45.26/6.20 fof(f1216,plain,(
% 45.26/6.20 occurrence_of(sK17_skl(sK19_skl),sK0_skl(sK17_skl(sK19_skl)))),
% 45.26/6.20 inference(resolution,[status(thm)],[f1211,f71])).
% 45.26/6.20 fof(f1228,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f955,f276])).
% 45.26/6.20 fof(f1244,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))),
% 45.26/6.20 inference(resolution,[status(thm)],[f1228,f164])).
% 45.26/6.20 fof(f1253,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1228,f163])).
% 45.26/6.20 fof(f1266,plain,(
% 45.26/6.20 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~next_subocc(sK16_skl(sK19_skl),X0,tptp0)|~min_precedes(sK17_skl(sK19_skl),X0,tptp0))),
% 45.26/6.20 inference(resolution,[status(thm)],[f1228,f148])).
% 45.26/6.20 fof(f1268,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1228,f140])).
% 45.26/6.20 fof(f1283,plain,(
% 45.26/6.20 subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1244,f277])).
% 45.26/6.20 fof(f1292,plain,(
% 45.26/6.20 occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1253,f277])).
% 45.26/6.20 fof(f1304,plain,(
% 45.26/6.20 ![X0]: (~next_subocc(sK16_skl(sK19_skl),X0,tptp0)|~min_precedes(sK17_skl(sK19_skl),X0,tptp0))),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1266,f277])).
% 45.26/6.20 fof(f1305,plain,(
% 45.26/6.20 ~leaf(sK16_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1268,f277])).
% 45.26/6.20 fof(f1410,plain,(
% 45.26/6.20 leaf(sK16_skl(sK19_skl),tptp0)|min_precedes(sK16_skl(sK19_skl),sK6_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1131,f142])).
% 45.26/6.20 fof(f1438,plain,(
% 45.26/6.20 min_precedes(sK16_skl(sK19_skl),sK6_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f1410,f1305])).
% 45.26/6.20 fof(f1439,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK17_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f988,f276])).
% 45.26/6.20 fof(f1522,plain,(
% 45.26/6.20 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~min_precedes(sK16_skl(sK19_skl),X0,tptp0)|X0=sK17_skl(sK19_skl)|X0=sK18_skl(sK19_skl))),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f999,f276])).
% 45.26/6.20 fof(f1795,plain,(
% 45.26/6.20 sK0_skl(sK17_skl(sK19_skl))=tptp4),
% 45.26/6.20 inference(resolution,[status(thm)],[f1216,f1213])).
% 45.26/6.20 fof(f2936,plain,(
% 45.26/6.20 ![X0,X1]: (~leaf_occ(X0,sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|~min_precedes(X0,X1,tptp0))),
% 45.26/6.20 inference(resolution,[status(thm)],[f1292,f213])).
% 45.26/6.20 fof(f3640,plain,(
% 45.26/6.20 ~occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)|~arboreal(sK16_skl(sK19_skl))|leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1283,f253])).
% 45.26/6.20 fof(f3641,plain,(
% 45.26/6.20 ~occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)|~arboreal(sK16_skl(sK19_skl))|leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1283,f252])).
% 45.26/6.20 fof(f3668,plain,(
% 45.26/6.20 ~arboreal(sK16_skl(sK19_skl))|leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f3640,f1292])).
% 45.26/6.20 fof(f3669,plain,(
% 45.26/6.20 ~arboreal(sK16_skl(sK19_skl))|leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f3641,f1292])).
% 45.26/6.20 fof(f3891,plain,(
% 45.26/6.20 ~next_subocc(sK16_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)|leaf_occ(sK19_skl,sK20_skl)),
% 45.26/6.20 inference(resolution,[status(thm)],[f1304,f1439])).
% 45.26/6.20 fof(f3892,plain,(
% 45.26/6.20 ~next_subocc(sK16_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f3891,f277])).
% 45.26/6.20 fof(f11732,plain,(
% 45.26/6.20 ~leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))),
% 45.26/6.20 inference(resolution,[status(thm)],[f2936,f1438])).
% 45.26/6.20 fof(f22956,plain,(
% 45.26/6.20 leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f3668,f1099])).
% 45.26/6.20 fof(f22957,plain,(
% 45.26/6.20 next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f22956,f11732])).
% 45.26/6.20 fof(f22989,plain,(
% 45.26/6.20 leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f3669,f1099])).
% 45.26/6.20 fof(f22990,plain,(
% 45.26/6.20 occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3)),
% 45.26/6.20 inference(resolution,[status(thm)],[f22989,f11732])).
% 45.26/6.20 fof(f23135,plain,(
% 45.26/6.20 activity_occurrence(sK16_skl(sK16_skl(sK19_skl)))),
% 45.26/6.20 inference(resolution,[status(thm)],[f22990,f67])).
% 45.26/6.20 fof(f23139,plain,(
% 45.26/6.20 ![X0]: (~occurrence_of(sK16_skl(sK16_skl(sK19_skl)),X0)|X0=tptp3)),
% 45.26/6.20 inference(resolution,[status(thm)],[f22990,f74])).
% 45.26/6.20 fof(f23171,plain,(
% 45.26/6.20 occurrence_of(sK16_skl(sK16_skl(sK19_skl)),sK0_skl(sK16_skl(sK16_skl(sK19_skl))))),
% 45.26/6.20 inference(resolution,[status(thm)],[f23135,f71])).
% 45.26/6.20 fof(f23389,plain,(
% 45.26/6.20 min_precedes(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 45.26/6.20 inference(resolution,[status(thm)],[f22957,f147])).
% 45.26/6.20 fof(f23479,plain,(
% 45.26/6.20 leaf_occ(sK19_skl,sK20_skl)|sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)|sK16_skl(sK16_skl(sK19_skl))=sK18_skl(sK19_skl)),
% 45.26/6.20 inference(resolution,[status(thm)],[f23389,f1522])).
% 45.26/6.20 fof(f23549,plain,(
% 45.26/6.20 sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)|sK16_skl(sK16_skl(sK19_skl))=sK18_skl(sK19_skl)),
% 45.26/6.20 inference(forward_subsumption_resolution,[status(thm)],[f23479,f277])).
% 43.12/6.25 fof(f25841,plain,(
% 43.12/6.25 sK0_skl(sK16_skl(sK16_skl(sK19_skl)))=tptp3),
% 43.12/6.25 inference(resolution,[status(thm)],[f23171,f23139])).
% 43.12/6.25 fof(f32563,plain,(
% 43.12/6.25 next_subocc(sK16_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)|sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)),
% 43.12/6.25 inference(paramodulation,[status(thm)],[f23549,f22957])).
% 43.12/6.25 fof(f32576,plain,(
% 43.12/6.25 sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)),
% 43.12/6.25 inference(forward_subsumption_resolution,[status(thm)],[f32563,f3892])).
% 43.12/6.25 fof(f32635,plain,(
% 43.12/6.25 sK0_skl(sK17_skl(sK19_skl))=tptp3),
% 43.12/6.25 inference(backward_demodulation,[status(thm)],[f32576,f25841])).
% 43.12/6.25 fof(f32680,plain,(
% 43.12/6.25 tptp4=tptp3),
% 43.12/6.25 inference(forward_demodulation,[status(thm)],[f1795,f32635])).
% 43.12/6.25 fof(f32681,plain,(
% 43.12/6.25 $false),
% 43.12/6.25 inference(forward_subsumption_resolution,[status(thm)],[f32680,f265])).
% 43.12/6.25 % SZS output end CNFRefutation for theBenchmark.p
% 43.12/6.28 % Elapsed time: 5.900805 seconds
% 43.12/6.28 % CPU time: 46.492744 seconds
% 43.12/6.28 % Total memory used: 327.083 MB
% 43.12/6.28 % Net memory used: 309.664 MB
%------------------------------------------------------------------------------