%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO018+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 : n018.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 112.74s 19.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO018+3 : 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.09/5.37 % Computer : n018.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 03:46:03 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 112.74/19.63 % Refutation found
% 112.74/19.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 112.74/19.63 % SZS output start CNFRefutation for theBenchmark
% 112.74/19.63 fof(f1,axiom,(
% 112.74/19.63 (! [X0,X1] :( occurrence_of(X1,X0)=> ( activity(X0)& activity_occurrence(X1) ) ) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f2,axiom,(
% 112.74/19.63 (! [X2] :( activity_occurrence(X2)=> (? [X3] :( activity(X3)& occurrence_of(X2,X3) ) )) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f3,axiom,(
% 112.74/19.63 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f8,axiom,(
% 112.74/19.63 (! [X16,X17] :( occurrence_of(X16,X17)=> ( arboreal(X16)<=> atomic(X17) ) ) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f14,axiom,(
% 112.74/19.63 (! [X31,X32,X33] :( min_precedes(X31,X32,X33)=> (? [X34] :( root(X34,X33)& min_precedes(X34,X32,X33) ) )) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f22,axiom,(
% 112.74/19.63 (! [X56,X57] :( leaf(X56,X57)<=> ( ( root(X56,X57)| (? [X58] : min_precedes(X58,X56,X57) ))& ~ (? [X59] : min_precedes(X56,X59,X57) )) ) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f23,axiom,(
% 112.74/19.63 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f26,axiom,(
% 112.74/19.63 (! [X69,X70,X71] :( min_precedes(X70,X71,X69)=> (? [X72] :( occurrence_of(X72,X69)& subactivity_occurrence(X70,X72)& subactivity_occurrence(X71,X72) ) )) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f38,axiom,(
% 112.74/19.63 (! [X113,X114,X115] :( ( occurrence_of(X113,X115)& leaf_occ(X114,X113) )=> ~ (? [X116] : min_precedes(X114,X116,X115) )) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f50,axiom,(
% 112.74/19.63 (! [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,tptp1)| occurrence_of(X165,tptp2) )& min_precedes(X164,X165,tptp0)& (! [X166] :( min_precedes(X163,X166,tptp0)=> ( X166 = X164| X166 = X165 ) ) )) )) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f56,axiom,(
% 112.74/19.63 atomic(tptp3) ),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f57,axiom,(
% 112.74/19.63 tptp4 != tptp3 ),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f60,axiom,(
% 112.74/19.63 tptp3 != tptp1 ),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f61,axiom,(
% 112.74/19.63 tptp3 != tptp2 ),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f63,conjecture,(
% 112.74/19.63 (! [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,tptp1)| occurrence_of(X170,tptp2) )& min_precedes(X169,X170,tptp0)& leaf_occ(X170,X168)& ( occurrence_of(X170,tptp1)=> ~ (? [X171] :( occurrence_of(X171,tptp2)& min_precedes(X169,X171,tptp0) ) ))& ( occurrence_of(X170,tptp2)=> ~ (? [X172] :( occurrence_of(X172,tptp1)& min_precedes(X169,X172,tptp0) ) )) ) )) )),
% 112.74/19.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.74/19.63 fof(f64,negated_conjecture,(
% 112.74/19.63 ~((! [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,tptp1)| occurrence_of(X170,tptp2) )& min_precedes(X169,X170,tptp0)& leaf_occ(X170,X168)& ( occurrence_of(X170,tptp1)=> ~ (? [X171] :( occurrence_of(X171,tptp2)& min_precedes(X169,X171,tptp0) ) ))& ( occurrence_of(X170,tptp2)=> ~ (? [X172] :( occurrence_of(X172,tptp1)& min_precedes(X169,X172,tptp0) ) )) ) )) ))),
% 112.74/19.63 inference(negated_conjecture,[status(cth)],[f63])).
% 112.74/19.63 fof(f65,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X1,X0)|(activity(X0)&activity_occurrence(X1)))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 112.74/19.63 fof(f67,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f65])).
% 112.74/19.63 fof(f68,plain,(
% 112.74/19.63 ![X2]: (~activity_occurrence(X2)|(?[X3]: (activity(X3)&occurrence_of(X2,X3))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 112.74/19.63 fof(f69,plain,(
% 112.74/19.63 ![X2]: (~activity_occurrence(X2)|(activity(sK0_skl(X2))&occurrence_of(X2,sK0_skl(X2))))),
% 112.74/19.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X3,sK0_skl(X2))],[f68])).
% 112.74/19.63 fof(f71,plain,(
% 112.74/19.63 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK0_skl(X0)))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f69])).
% 112.74/19.63 fof(f72,plain,(
% 112.74/19.63 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 112.74/19.63 fof(f73,plain,(
% 112.74/19.63 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f72])).
% 112.74/19.63 fof(f74,plain,(
% 112.74/19.63 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f73])).
% 112.74/19.63 fof(f85,plain,(
% 112.74/19.63 ![X16,X17]: (~occurrence_of(X16,X17)|(arboreal(X16)<=>atomic(X17)))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 112.74/19.63 fof(f86,plain,(
% 112.74/19.63 ![X16,X17]: (~occurrence_of(X16,X17)|((~arboreal(X16)|atomic(X17))&(arboreal(X16)|~atomic(X17))))),
% 112.74/19.63 inference(NNF_transformation,[status(thm)],[f85])).
% 112.74/19.63 fof(f88,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f86])).
% 112.74/19.63 fof(f110,plain,(
% 112.74/19.63 ![X31,X32,X33]: (~min_precedes(X31,X32,X33)|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 112.74/19.63 fof(f111,plain,(
% 112.74/19.63 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f110])).
% 112.74/19.63 fof(f112,plain,(
% 112.74/19.63 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(root(sK4_skl(X33,X32),X33)&min_precedes(sK4_skl(X33,X32),X32,X33)))),
% 112.74/19.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X34,sK4_skl(X33,X32))],[f111])).
% 112.74/19.63 fof(f114,plain,(
% 112.74/19.63 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK4_skl(X2,X1),X1,X2))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f112])).
% 112.74/19.63 fof(f135,plain,(
% 112.74/19.63 ![X56,X57]: (leaf(X56,X57)<=>((root(X56,X57)|(?[X58]: min_precedes(X58,X56,X57)))&(![X59]: ~min_precedes(X56,X59,X57))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 112.74/19.63 fof(f136,plain,(
% 112.74/19.63 ![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)))))),
% 112.74/19.63 inference(NNF_transformation,[status(thm)],[f135])).
% 112.74/19.63 fof(f137,plain,(
% 112.74/19.63 (![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)))))),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f136])).
% 112.74/19.63 fof(f138,plain,(
% 112.74/19.63 (![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))))),
% 112.74/19.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(X58,sK5_skl(X57,X56)),skolemize(X59,sK6_skl(X57,X56))],[f137])).
% 112.74/19.63 fof(f140,plain,(
% 112.74/19.63 ![X0,X1,X2]: (~leaf(X0,X1)|~min_precedes(X0,X2,X1))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f138])).
% 112.74/19.63 fof(f142,plain,(
% 112.74/19.63 ![X0,X1,X2]: (leaf(X0,X1)|~min_precedes(X2,X0,X1)|min_precedes(X0,sK6_skl(X1,X0),X1))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f138])).
% 112.74/19.63 fof(f143,plain,(
% 112.74/19.63 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 112.74/19.63 fof(f144,plain,(
% 112.74/19.63 ![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))))))),
% 112.74/19.63 inference(NNF_transformation,[status(thm)],[f143])).
% 112.74/19.63 fof(f145,plain,(
% 112.74/19.63 (![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))))))),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f144])).
% 112.74/19.63 fof(f146,plain,(
% 112.74/19.63 (![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)))))),
% 112.74/19.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f145])).
% 112.74/19.63 fof(f147,plain,(
% 112.74/19.63 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f146])).
% 112.74/19.63 fof(f161,plain,(
% 112.74/19.63 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|(?[X72]: ((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 112.74/19.63 fof(f162,plain,(
% 112.74/19.63 ![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))))),
% 112.74/19.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f161])).
% 112.74/19.63 fof(f163,plain,(
% 112.74/19.63 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK9_skl(X1,X0,X2),X2))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f162])).
% 112.74/19.63 fof(f164,plain,(
% 112.74/19.63 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK9_skl(X1,X0,X2)))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f162])).
% 112.74/19.63 fof(f211,plain,(
% 112.74/19.63 ![X113,X114,X115]: ((~occurrence_of(X113,X115)|~leaf_occ(X114,X113))|(![X116]: ~min_precedes(X114,X116,X115)))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 112.74/19.63 fof(f212,plain,(
% 112.74/19.63 ![X114,X115]: ((![X113]: (~occurrence_of(X113,X115)|~leaf_occ(X114,X113)))|(![X116]: ~min_precedes(X114,X116,X115)))),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f211])).
% 112.74/19.63 fof(f213,plain,(
% 112.74/19.63 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f212])).
% 112.74/19.63 fof(f249,plain,(
% 112.74/19.63 ![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,tptp1)|occurrence_of(X165,tptp2)))&min_precedes(X164,X165,tptp0))&(![X166]: (~min_precedes(X163,X166,tptp0)|(X166=X164|X166=X165))))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 112.74/19.63 fof(f250,plain,(
% 112.74/19.63 ![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,tptp1)|occurrence_of(X165,tptp2)))&min_precedes(X164,X165,tptp0))&(![X166]: (~min_precedes(X163,X166,tptp0)|(X166=X164|X166=X165))))))),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f249])).
% 112.74/19.63 fof(f251,plain,(
% 112.74/19.63 ![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),tptp1)|occurrence_of(sK18_skl(X161),tptp2)))&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))))))),
% 112.74/19.63 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])).
% 112.74/19.63 fof(f252,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp3))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f251])).
% 112.74/19.63 fof(f253,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK16_skl(X1),tptp0))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f251])).
% 112.74/19.63 fof(f254,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK17_skl(X1),tptp4))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f251])).
% 112.74/19.63 fof(f255,plain,(
% 112.74/19.63 ![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))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f251])).
% 112.74/19.63 fof(f256,plain,(
% 112.74/19.63 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK18_skl(X1),tptp1)|occurrence_of(sK18_skl(X1),tptp2))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f251])).
% 112.74/19.63 fof(f258,plain,(
% 112.74/19.63 ![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))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f251])).
% 112.74/19.63 fof(f264,plain,(
% 112.74/19.63 atomic(tptp3)),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f56])).
% 112.74/19.63 fof(f265,plain,(
% 112.74/19.63 ~tptp4=tptp3),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f57])).
% 112.74/19.63 fof(f268,plain,(
% 112.74/19.63 ~tptp3=tptp1),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f60])).
% 112.74/19.63 fof(f269,plain,(
% 112.74/19.63 ~tptp3=tptp2),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f61])).
% 112.74/19.63 fof(f271,plain,(
% 112.74/19.63 (?[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,tptp1)&~occurrence_of(X170,tptp2)))|~min_precedes(X169,X170,tptp0))|~leaf_occ(X170,X168))|(occurrence_of(X170,tptp1)&(?[X171]: (occurrence_of(X171,tptp2)&min_precedes(X169,X171,tptp0)))))|(occurrence_of(X170,tptp2)&(?[X172]: (occurrence_of(X172,tptp1)&min_precedes(X169,X172,tptp0))))))))),
% 112.74/19.63 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 112.74/19.63 fof(f272,definition,(
% 112.74/19.63 ![X170]: (sP0_prd(X170)<=>(~occurrence_of(X170,tptp1)&~occurrence_of(X170,tptp2)))),
% 112.74/19.63 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 112.74/19.63 fof(f273,definition,(
% 112.74/19.63 ![X169,X170]: (sP1_prd(X170,X169)<=>(occurrence_of(X170,tptp1)&(?[X171]: (occurrence_of(X171,tptp2)&min_precedes(X169,X171,tptp0)))))),
% 112.74/19.63 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 112.74/19.63 fof(f274,plain,(
% 112.74/19.63 ?[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))|sP0_prd(X170))|~min_precedes(X169,X170,tptp0))|~leaf_occ(X170,X168))|sP1_prd(X170,X169))|(occurrence_of(X170,tptp2)&(?[X172]: (occurrence_of(X172,tptp1)&min_precedes(X169,X172,tptp0)))))))),
% 112.74/19.63 inference(formula_renaming,[status(thm)],[f271,f273,f272])).
% 112.74/19.63 fof(f275,plain,(
% 112.74/19.63 ((((occurrence_of(sK20_skl,tptp0)&subactivity_occurrence(sK19_skl,sK20_skl))&arboreal(sK19_skl))&~leaf_occ(sK19_skl,sK20_skl))&(![X169,X170]: ((((((~occurrence_of(X169,tptp3)|~next_subocc(sK19_skl,X169,tptp0))|sP0_prd(X170))|~min_precedes(X169,X170,tptp0))|~leaf_occ(X170,sK20_skl))|sP1_prd(X170,X169))|(occurrence_of(X170,tptp2)&(occurrence_of(sK21_skl(X170,X169),tptp1)&min_precedes(X169,sK21_skl(X170,X169),tptp0))))))),
% 112.74/19.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(X167,sK19_skl),skolemize(X168,sK20_skl),skolemize(X172,sK21_skl(X170,X169))],[f274])).
% 112.74/19.63 fof(f276,plain,(
% 112.74/19.63 occurrence_of(sK20_skl,tptp0)),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f275])).
% 112.74/19.63 fof(f277,plain,(
% 112.74/19.63 subactivity_occurrence(sK19_skl,sK20_skl)),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f275])).
% 112.74/19.63 fof(f278,plain,(
% 112.74/19.63 arboreal(sK19_skl)),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f275])).
% 112.74/19.63 fof(f279,plain,(
% 112.74/19.63 ~leaf_occ(sK19_skl,sK20_skl)),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f275])).
% 112.74/19.63 fof(f283,plain,(
% 112.74/19.63 ![X170]: ((~sP0_prd(X170)|(~occurrence_of(X170,tptp1)&~occurrence_of(X170,tptp2)))&(sP0_prd(X170)|(occurrence_of(X170,tptp1)|occurrence_of(X170,tptp2))))),
% 112.74/19.63 inference(NNF_transformation,[status(thm)],[f272])).
% 112.74/19.63 fof(f284,plain,(
% 112.74/19.63 (![X170]: (~sP0_prd(X170)|(~occurrence_of(X170,tptp1)&~occurrence_of(X170,tptp2))))&(![X170]: (sP0_prd(X170)|(occurrence_of(X170,tptp1)|occurrence_of(X170,tptp2))))),
% 112.74/19.63 inference(miniscoping,[status(thm)],[f283])).
% 112.74/19.63 fof(f285,plain,(
% 112.74/19.63 ![X0]: (~sP0_prd(X0)|~occurrence_of(X0,tptp1))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f284])).
% 112.74/19.63 fof(f286,plain,(
% 112.74/19.63 ![X0]: (~sP0_prd(X0)|~occurrence_of(X0,tptp2))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f284])).
% 112.74/19.63 fof(f287,plain,(
% 112.74/19.63 ![X0]: (sP0_prd(X0)|occurrence_of(X0,tptp1)|occurrence_of(X0,tptp2))),
% 112.74/19.63 inference(cnf_transformation,[status(thm)],[f284])).
% 112.74/19.63 fof(f359,plain,(
% 112.74/19.63 ![X0,X1]: (sP0_prd(X0)|occurrence_of(X0,tptp1)|~occurrence_of(X0,X1)|X1=tptp2)),
% 112.74/19.63 inference(resolution,[status(thm)],[f287,f74])).
% 112.74/19.63 fof(f838,plain,(
% 112.74/19.63 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|occurrence_of(sK16_skl(X0),tptp3))),
% 112.74/19.63 inference(resolution,[status(thm)],[f252,f276])).
% 112.74/19.63 fof(f846,plain,(
% 112.74/19.63 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f253,f277])).
% 112.74/19.63 fof(f848,plain,(
% 112.74/19.63 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f846,f276])).
% 112.74/19.63 fof(f1014,plain,(
% 112.74/19.63 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK17_skl(sK19_skl),tptp4)),
% 112.74/19.63 inference(resolution,[status(thm)],[f254,f277])).
% 112.74/19.63 fof(f1016,plain,(
% 112.74/19.63 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK17_skl(sK19_skl),tptp4)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1014,f276])).
% 112.74/19.63 fof(f1021,plain,(
% 112.74/19.63 ~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)),
% 112.74/19.63 inference(resolution,[status(thm)],[f255,f277])).
% 112.74/19.63 fof(f1023,plain,(
% 112.74/19.63 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1021,f276])).
% 112.74/19.63 fof(f1028,plain,(
% 112.74/19.63 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK18_skl(sK19_skl),tptp1)|occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 112.74/19.63 inference(resolution,[status(thm)],[f256,f277])).
% 112.74/19.63 fof(f1030,plain,(
% 112.74/19.63 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK18_skl(sK19_skl),tptp1)|occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1028,f276])).
% 112.74/19.63 fof(f1225,plain,(
% 112.74/19.63 ![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))),
% 112.74/19.63 inference(resolution,[status(thm)],[f258,f277])).
% 112.74/19.63 fof(f1228,plain,(
% 112.74/19.63 ![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))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1225,f276])).
% 112.74/19.63 fof(f1477,plain,(
% 112.74/19.63 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 112.74/19.63 inference(resolution,[status(thm)],[f838,f277])).
% 112.74/19.63 fof(f1479,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1477,f278])).
% 112.74/19.63 fof(f1480,plain,(
% 112.74/19.63 occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1479,f279])).
% 112.74/19.63 fof(f1523,plain,(
% 112.74/19.63 arboreal(sK16_skl(sK19_skl))|~atomic(tptp3)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1480,f88])).
% 112.74/19.63 fof(f1534,plain,(
% 112.74/19.63 arboreal(sK16_skl(sK19_skl))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1523,f264])).
% 112.74/19.63 fof(f1553,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f848,f278])).
% 112.74/19.63 fof(f1570,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1553,f147])).
% 112.74/19.63 fof(f1579,plain,(
% 112.74/19.63 min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1570,f279])).
% 112.74/19.63 fof(f1585,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK17_skl(sK19_skl),tptp4)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1016,f278])).
% 112.74/19.63 fof(f1629,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|activity_occurrence(sK17_skl(sK19_skl))),
% 112.74/19.63 inference(resolution,[status(thm)],[f1585,f67])).
% 112.74/19.63 fof(f1633,plain,(
% 112.74/19.63 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~occurrence_of(sK17_skl(sK19_skl),X0)|X0=tptp4)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1585,f74])).
% 112.74/19.63 fof(f1671,plain,(
% 112.74/19.63 activity_occurrence(sK17_skl(sK19_skl))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1629,f279])).
% 112.74/19.63 fof(f1673,plain,(
% 112.74/19.63 ![X0]: (~occurrence_of(sK17_skl(sK19_skl),X0)|X0=tptp4)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1633,f279])).
% 112.74/19.63 fof(f1676,plain,(
% 112.74/19.63 occurrence_of(sK17_skl(sK19_skl),sK0_skl(sK17_skl(sK19_skl)))),
% 112.74/19.63 inference(resolution,[status(thm)],[f1671,f71])).
% 112.74/19.63 fof(f1718,plain,(
% 112.74/19.63 min_precedes(sK4_skl(tptp0,sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1579,f114])).
% 112.74/19.63 fof(f1733,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1023,f278])).
% 112.74/19.63 fof(f1751,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))),
% 112.74/19.63 inference(resolution,[status(thm)],[f1733,f164])).
% 112.74/19.63 fof(f1752,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1733,f163])).
% 112.74/19.63 fof(f1768,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1733,f140])).
% 112.74/19.63 fof(f1792,plain,(
% 112.74/19.63 subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1751,f279])).
% 112.74/19.63 fof(f1793,plain,(
% 112.74/19.63 occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1752,f279])).
% 112.74/19.63 fof(f1809,plain,(
% 112.74/19.63 ~leaf(sK16_skl(sK19_skl),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1768,f279])).
% 112.74/19.63 fof(f1825,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK18_skl(sK19_skl),tptp1)|occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1030,f278])).
% 112.74/19.63 fof(f1826,plain,(
% 112.74/19.63 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK18_skl(sK19_skl),tptp1)|~sP0_prd(sK18_skl(sK19_skl))),
% 112.74/19.63 inference(resolution,[status(thm)],[f1825,f286])).
% 112.74/19.63 fof(f1877,plain,(
% 112.74/19.63 occurrence_of(sK18_skl(sK19_skl),tptp1)|~sP0_prd(sK18_skl(sK19_skl))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1826,f279])).
% 112.74/19.63 fof(f2015,plain,(
% 112.74/19.63 ![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))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1228,f278])).
% 112.74/19.63 fof(f2419,plain,(
% 112.74/19.63 sK0_skl(sK17_skl(sK19_skl))=tptp4),
% 112.74/19.63 inference(resolution,[status(thm)],[f1676,f1673])).
% 112.74/19.63 fof(f3279,plain,(
% 112.74/19.63 ~sP0_prd(sK18_skl(sK19_skl))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f1877,f285])).
% 112.74/19.63 fof(f4083,plain,(
% 112.74/19.63 leaf(sK16_skl(sK19_skl),tptp0)|min_precedes(sK16_skl(sK19_skl),sK6_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1718,f142])).
% 112.74/19.63 fof(f4111,plain,(
% 112.74/19.63 min_precedes(sK16_skl(sK19_skl),sK6_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f4083,f1809])).
% 112.74/19.63 fof(f4240,plain,(
% 112.74/19.63 ![X0,X1]: (~leaf_occ(X0,sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))|~min_precedes(X0,X1,tptp0))),
% 112.74/19.63 inference(resolution,[status(thm)],[f1793,f213])).
% 112.74/19.63 fof(f6101,plain,(
% 112.74/19.63 ~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)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1792,f253])).
% 112.74/19.63 fof(f6102,plain,(
% 112.74/19.63 ~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)),
% 112.74/19.63 inference(resolution,[status(thm)],[f1792,f252])).
% 112.74/19.63 fof(f6145,plain,(
% 112.74/19.63 ~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)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f6101,f1793])).
% 112.74/19.63 fof(f6146,plain,(
% 112.74/19.63 ~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)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f6102,f1793])).
% 112.74/19.63 fof(f16422,plain,(
% 112.74/19.63 ~leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))),
% 112.74/19.63 inference(resolution,[status(thm)],[f4240,f4111])).
% 112.74/19.63 fof(f43545,plain,(
% 112.74/19.63 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)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f6145,f1534])).
% 112.74/19.63 fof(f43546,plain,(
% 112.74/19.63 next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f43545,f16422])).
% 112.74/19.63 fof(f43598,plain,(
% 112.74/19.63 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)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f6146,f1534])).
% 112.74/19.63 fof(f43599,plain,(
% 112.74/19.63 occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3)),
% 112.74/19.63 inference(resolution,[status(thm)],[f43598,f16422])).
% 112.74/19.63 fof(f43785,plain,(
% 112.74/19.63 sP0_prd(sK16_skl(sK16_skl(sK19_skl)))|occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp1)|tptp3=tptp2),
% 112.74/19.63 inference(resolution,[status(thm)],[f43599,f359])).
% 112.74/19.63 fof(f43794,plain,(
% 112.74/19.63 activity_occurrence(sK16_skl(sK16_skl(sK19_skl)))),
% 112.74/19.63 inference(resolution,[status(thm)],[f43599,f67])).
% 112.74/19.63 fof(f43798,plain,(
% 112.74/19.63 ![X0]: (~occurrence_of(sK16_skl(sK16_skl(sK19_skl)),X0)|X0=tptp3)),
% 112.74/19.63 inference(resolution,[status(thm)],[f43599,f74])).
% 112.74/19.63 fof(f43816,plain,(
% 112.74/19.63 sP0_prd(sK16_skl(sK16_skl(sK19_skl)))|occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp1)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f43785,f269])).
% 112.74/19.63 fof(f43819,plain,(
% 112.74/19.63 occurrence_of(sK16_skl(sK16_skl(sK19_skl)),sK0_skl(sK16_skl(sK16_skl(sK19_skl))))),
% 112.74/19.63 inference(resolution,[status(thm)],[f43794,f71])).
% 112.74/19.63 fof(f44034,plain,(
% 112.74/19.63 min_precedes(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)),
% 112.74/19.63 inference(resolution,[status(thm)],[f43546,f147])).
% 112.74/19.63 fof(f44078,plain,(
% 112.74/19.63 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)),
% 112.74/19.63 inference(resolution,[status(thm)],[f44034,f2015])).
% 112.74/19.63 fof(f44155,plain,(
% 112.74/19.63 sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)|sK16_skl(sK16_skl(sK19_skl))=sK18_skl(sK19_skl)),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f44078,f279])).
% 112.74/19.63 fof(f45777,plain,(
% 112.74/19.63 sK0_skl(sK16_skl(sK16_skl(sK19_skl)))=tptp3),
% 112.74/19.63 inference(resolution,[status(thm)],[f43819,f43798])).
% 112.74/19.63 fof(f48718,plain,(
% 112.74/19.63 sP0_prd(sK16_skl(sK16_skl(sK19_skl)))|tptp1=tptp3),
% 112.74/19.63 inference(resolution,[status(thm)],[f43816,f43798])).
% 112.74/19.63 fof(f48880,plain,(
% 112.74/19.63 sP0_prd(sK16_skl(sK16_skl(sK19_skl)))),
% 112.74/19.63 inference(forward_subsumption_resolution,[status(thm)],[f48718,f268])).
% 112.74/19.68 fof(f55472,plain,(
% 112.74/19.68 sP0_prd(sK18_skl(sK19_skl))|sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)),
% 112.74/19.68 inference(paramodulation,[status(thm)],[f44155,f48880])).
% 112.74/19.68 fof(f55520,plain,(
% 112.74/19.68 sK16_skl(sK16_skl(sK19_skl))=sK17_skl(sK19_skl)),
% 112.74/19.68 inference(forward_subsumption_resolution,[status(thm)],[f55472,f3279])).
% 112.74/19.68 fof(f55578,plain,(
% 112.74/19.68 sK0_skl(sK17_skl(sK19_skl))=tptp3),
% 112.74/19.68 inference(backward_demodulation,[status(thm)],[f55520,f45777])).
% 112.74/19.68 fof(f55623,plain,(
% 112.74/19.68 tptp4=tptp3),
% 112.74/19.68 inference(forward_demodulation,[status(thm)],[f2419,f55578])).
% 112.74/19.68 fof(f55624,plain,(
% 112.74/19.68 $false),
% 112.74/19.68 inference(forward_subsumption_resolution,[status(thm)],[f55623,f265])).
% 112.74/19.68 % SZS output end CNFRefutation for theBenchmark.p
% 3.64/19.71 % Elapsed time: 14.320375 seconds
% 3.64/19.71 % CPU time: 113.374811 seconds
% 3.64/19.71 % Total memory used: 461.565 MB
% 3.64/19.71 % Net memory used: 429.323 MB
%------------------------------------------------------------------------------