%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO014+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:25 PM UTC 2026
% Result : Theorem 50.13s 6.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+3 : 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.09/0.54 % Computer : n018.cluster.edu
% 0.09/0.54 % Model : x86_64 x86_64
% 0.09/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.54 % Memory : 8046.5625MB
% 0.09/0.54 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 03:44:59 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.15/0.56 % Drodi V4.1.1
% 50.13/6.95 % Refutation found
% 50.13/6.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 50.13/6.95 % SZS output start CNFRefutation for theBenchmark
% 50.13/6.95 fof(f1,axiom,(
% 50.13/6.95 (! [X0,X1] :( occurrence_of(X1,X0)=> ( activity(X0)& activity_occurrence(X1) ) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f2,axiom,(
% 50.13/6.95 (! [X2] :( activity_occurrence(X2)=> (? [X3] :( activity(X3)& occurrence_of(X2,X3) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f3,axiom,(
% 50.13/6.95 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f6,axiom,(
% 50.13/6.95 (! [X10,X11,X12] :( ( earlier(X10,X11)& earlier(X11,X12) )=> earlier(X10,X12) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f11,axiom,(
% 50.13/6.95 (! [X21,X22] :( precedes(X21,X22)<=> ( earlier(X21,X22)& legal(X22) ) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f14,axiom,(
% 50.13/6.95 (! [X31,X32,X33] :( min_precedes(X31,X32,X33)=> (? [X34] :( root(X34,X33)& min_precedes(X34,X32,X33) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f16,axiom,(
% 50.13/6.95 (! [X38,X39,X40] :( min_precedes(X38,X39,X40)=> precedes(X38,X39) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f19,axiom,(
% 50.13/6.95 (! [X45,X46,X47,X48] :( ( min_precedes(X45,X46,X48)& min_precedes(X45,X47,X48)& precedes(X46,X47) )=> min_precedes(X46,X47,X48) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f23,axiom,(
% 50.13/6.95 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f30,axiom,(
% 50.13/6.95 (! [X83,X84,X85,X86] :( ( min_precedes(X83,X84,X85)& occurrence_of(X86,X85)& subactivity_occurrence(X84,X86) )=> subactivity_occurrence(X83,X86) ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f34,axiom,(
% 50.13/6.95 (! [X99,X100] :( root_occ(X99,X100)<=> (? [X101] :( occurrence_of(X100,X101)& subactivity_occurrence(X99,X100)& root(X99,X101) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f35,axiom,(
% 50.13/6.95 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f36,axiom,(
% 50.13/6.95 (! [X105,X106,X107,X108] :( ( occurrence_of(X107,X108)& root_occ(X105,X107)& root_occ(X106,X107) )=> X105 = X106 ) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f46,axiom,(
% 50.13/6.95 (! [X145,X146] :( ( leaf(X145,X146)& ~ atomic(X146) )=> (? [X147] :( occurrence_of(X147,X146)& leaf_occ(X145,X147) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f50,axiom,(
% 50.13/6.95 (! [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)& next_subocc(X163,X164,tptp0)& ( occurrence_of(X165,tptp2)| occurrence_of(X165,tptp1) )& next_subocc(X164,X165,tptp0)& leaf(X165,tptp0) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f52,axiom,(
% 50.13/6.95 ~ atomic(tptp0) ),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f62,axiom,(
% 50.13/6.95 tptp2 != tptp1 ),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f63,conjecture,(
% 50.13/6.95 (! [X166,X167] :( ( occurrence_of(X167,tptp0)& subactivity_occurrence(X166,X167)& arboreal(X166)& ~ leaf_occ(X166,X167) )=> (? [X168,X169] :( occurrence_of(X168,tptp3)& next_subocc(X166,X168,tptp0)& ( occurrence_of(X169,tptp2)| occurrence_of(X169,tptp1) )& min_precedes(X168,X169,tptp0)& leaf(X169,tptp0) ) )) )),
% 50.13/6.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.13/6.95 fof(f64,negated_conjecture,(
% 50.13/6.95 ~((! [X166,X167] :( ( occurrence_of(X167,tptp0)& subactivity_occurrence(X166,X167)& arboreal(X166)& ~ leaf_occ(X166,X167) )=> (? [X168,X169] :( occurrence_of(X168,tptp3)& next_subocc(X166,X168,tptp0)& ( occurrence_of(X169,tptp2)| occurrence_of(X169,tptp1) )& min_precedes(X168,X169,tptp0)& leaf(X169,tptp0) ) )) ))),
% 50.13/6.95 inference(negated_conjecture,[status(cth)],[f63])).
% 50.13/6.95 fof(f65,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X1,X0)|(activity(X0)&activity_occurrence(X1)))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 50.13/6.95 fof(f67,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f65])).
% 50.13/6.95 fof(f68,plain,(
% 50.13/6.95 ![X2]: (~activity_occurrence(X2)|(?[X3]: (activity(X3)&occurrence_of(X2,X3))))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 50.13/6.95 fof(f69,plain,(
% 50.13/6.95 ![X2]: (~activity_occurrence(X2)|(activity(sK0_skl(X2))&occurrence_of(X2,sK0_skl(X2))))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X3,sK0_skl(X2))],[f68])).
% 50.13/6.95 fof(f71,plain,(
% 50.13/6.95 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK0_skl(X0)))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f69])).
% 50.13/6.95 fof(f72,plain,(
% 50.13/6.95 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 50.13/6.95 fof(f73,plain,(
% 50.13/6.95 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f72])).
% 50.13/6.95 fof(f74,plain,(
% 50.13/6.95 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f73])).
% 50.13/6.95 fof(f79,plain,(
% 50.13/6.95 ![X10,X11,X12]: ((~earlier(X10,X11)|~earlier(X11,X12))|earlier(X10,X12))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 50.13/6.95 fof(f80,plain,(
% 50.13/6.95 ![X10,X12]: ((![X11]: (~earlier(X10,X11)|~earlier(X11,X12)))|earlier(X10,X12))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f79])).
% 50.13/6.95 fof(f81,plain,(
% 50.13/6.95 ![X0,X1,X2]: (~earlier(X0,X1)|~earlier(X1,X2)|earlier(X0,X2))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f80])).
% 50.13/6.95 fof(f94,plain,(
% 50.13/6.95 ![X21,X22]: ((~precedes(X21,X22)|(earlier(X21,X22)&legal(X22)))&(precedes(X21,X22)|(~earlier(X21,X22)|~legal(X22))))),
% 50.13/6.95 inference(NNF_transformation,[status(thm)],[f11])).
% 50.13/6.95 fof(f95,plain,(
% 50.13/6.95 (![X21,X22]: (~precedes(X21,X22)|(earlier(X21,X22)&legal(X22))))&(![X21,X22]: (precedes(X21,X22)|(~earlier(X21,X22)|~legal(X22))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f94])).
% 50.13/6.95 fof(f96,plain,(
% 50.13/6.95 ![X0,X1]: (~precedes(X0,X1)|earlier(X0,X1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f95])).
% 50.13/6.95 fof(f97,plain,(
% 50.13/6.95 ![X0,X1]: (~precedes(X0,X1)|legal(X1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f95])).
% 50.13/6.95 fof(f98,plain,(
% 50.13/6.95 ![X0,X1]: (precedes(X0,X1)|~earlier(X0,X1)|~legal(X1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f95])).
% 50.13/6.95 fof(f110,plain,(
% 50.13/6.95 ![X31,X32,X33]: (~min_precedes(X31,X32,X33)|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 50.13/6.95 fof(f111,plain,(
% 50.13/6.95 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f110])).
% 50.13/6.95 fof(f112,plain,(
% 50.13/6.95 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(root(sK4_skl(X33,X32),X33)&min_precedes(sK4_skl(X33,X32),X32,X33)))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X34,sK4_skl(X33,X32))],[f111])).
% 50.13/6.95 fof(f113,plain,(
% 50.13/6.95 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|root(sK4_skl(X2,X1),X2))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f112])).
% 50.13/6.95 fof(f114,plain,(
% 50.13/6.95 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK4_skl(X2,X1),X1,X2))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f112])).
% 50.13/6.95 fof(f118,plain,(
% 50.13/6.95 ![X38,X39,X40]: (~min_precedes(X38,X39,X40)|precedes(X38,X39))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 50.13/6.95 fof(f119,plain,(
% 50.13/6.95 ![X38,X39]: ((![X40]: ~min_precedes(X38,X39,X40))|precedes(X38,X39))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f118])).
% 50.13/6.95 fof(f120,plain,(
% 50.13/6.95 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|precedes(X0,X1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f119])).
% 50.13/6.95 fof(f126,plain,(
% 50.13/6.95 ![X45,X46,X47,X48]: (((~min_precedes(X45,X46,X48)|~min_precedes(X45,X47,X48))|~precedes(X46,X47))|min_precedes(X46,X47,X48))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 50.13/6.95 fof(f127,plain,(
% 50.13/6.95 ![X46,X47,X48]: (((![X45]: (~min_precedes(X45,X46,X48)|~min_precedes(X45,X47,X48)))|~precedes(X46,X47))|min_precedes(X46,X47,X48))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f126])).
% 50.13/6.95 fof(f128,plain,(
% 50.13/6.95 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~min_precedes(X0,X3,X2)|~precedes(X1,X3)|min_precedes(X1,X3,X2))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f127])).
% 50.13/6.95 fof(f143,plain,(
% 50.13/6.95 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 50.13/6.95 fof(f144,plain,(
% 50.13/6.95 ![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))))))),
% 50.13/6.95 inference(NNF_transformation,[status(thm)],[f143])).
% 50.13/6.95 fof(f145,plain,(
% 50.13/6.95 (![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))))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f144])).
% 50.13/6.95 fof(f146,plain,(
% 50.13/6.95 (![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)))))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f145])).
% 50.13/6.95 fof(f147,plain,(
% 50.13/6.95 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f146])).
% 50.13/6.95 fof(f177,plain,(
% 50.13/6.95 ![X83,X84,X85,X86]: (((~min_precedes(X83,X84,X85)|~occurrence_of(X86,X85))|~subactivity_occurrence(X84,X86))|subactivity_occurrence(X83,X86))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 50.13/6.95 fof(f178,plain,(
% 50.13/6.95 ![X83,X86]: ((![X84]: ((![X85]: (~min_precedes(X83,X84,X85)|~occurrence_of(X86,X85)))|~subactivity_occurrence(X84,X86)))|subactivity_occurrence(X83,X86))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f177])).
% 50.13/6.95 fof(f179,plain,(
% 50.13/6.95 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f178])).
% 50.13/6.95 fof(f191,plain,(
% 50.13/6.95 ![X99,X100]: ((~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101))))&(root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 50.13/6.95 inference(NNF_transformation,[status(thm)],[f34])).
% 50.13/6.95 fof(f192,plain,(
% 50.13/6.95 (![X99,X100]: (~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f191])).
% 50.13/6.95 fof(f193,plain,(
% 50.13/6.95 (![X99,X100]: (~root_occ(X99,X100)|((occurrence_of(X100,sK13_skl(X100,X99))&subactivity_occurrence(X99,X100))&root(X99,sK13_skl(X100,X99)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f192])).
% 50.13/6.95 fof(f197,plain,(
% 50.13/6.95 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f193])).
% 50.13/6.95 fof(f198,plain,(
% 50.13/6.95 ![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)))))),
% 50.13/6.95 inference(NNF_transformation,[status(thm)],[f35])).
% 50.13/6.95 fof(f199,plain,(
% 50.13/6.95 (![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)))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f198])).
% 50.13/6.95 fof(f200,plain,(
% 50.13/6.95 (![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)))))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f199])).
% 50.13/6.95 fof(f202,plain,(
% 50.13/6.95 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f200])).
% 50.13/6.95 fof(f205,plain,(
% 50.13/6.95 ![X105,X106,X107,X108]: (((~occurrence_of(X107,X108)|~root_occ(X105,X107))|~root_occ(X106,X107))|X105=X106)),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 50.13/6.95 fof(f206,plain,(
% 50.13/6.95 ![X105,X106]: ((![X107]: (((![X108]: ~occurrence_of(X107,X108))|~root_occ(X105,X107))|~root_occ(X106,X107)))|X105=X106)),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f205])).
% 50.13/6.95 fof(f207,plain,(
% 50.13/6.95 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f206])).
% 50.13/6.95 fof(f236,plain,(
% 50.13/6.95 ![X145,X146]: ((~leaf(X145,X146)|atomic(X146))|(?[X147]: (occurrence_of(X147,X146)&leaf_occ(X145,X147))))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 50.13/6.95 fof(f237,plain,(
% 50.13/6.95 ![X145,X146]: ((~leaf(X145,X146)|atomic(X146))|(occurrence_of(sK15_skl(X146,X145),X146)&leaf_occ(X145,sK15_skl(X146,X145))))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X147,sK15_skl(X146,X145))],[f236])).
% 50.13/6.95 fof(f238,plain,(
% 50.13/6.95 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|occurrence_of(sK15_skl(X1,X0),X1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f237])).
% 50.13/6.95 fof(f239,plain,(
% 50.13/6.95 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|leaf_occ(X0,sK15_skl(X1,X0)))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f237])).
% 50.13/6.95 fof(f249,plain,(
% 50.13/6.95 ![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))&next_subocc(X163,X164,tptp0))&(occurrence_of(X165,tptp2)|occurrence_of(X165,tptp1)))&next_subocc(X164,X165,tptp0))&leaf(X165,tptp0))))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 50.13/6.95 fof(f250,plain,(
% 50.13/6.95 ![X161]: ((![X162]: (((~occurrence_of(X162,tptp0)|~subactivity_occurrence(X161,X162))|~arboreal(X161))|leaf_occ(X161,X162)))|(?[X165]: ((?[X164]: (((?[X163]: (((occurrence_of(X163,tptp3)&next_subocc(X161,X163,tptp0))&occurrence_of(X164,tptp4))&next_subocc(X163,X164,tptp0)))&(occurrence_of(X165,tptp2)|occurrence_of(X165,tptp1)))&next_subocc(X164,X165,tptp0)))&leaf(X165,tptp0))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f249])).
% 50.13/6.95 fof(f251,plain,(
% 50.13/6.95 ![X161]: ((![X162]: (((~occurrence_of(X162,tptp0)|~subactivity_occurrence(X161,X162))|~arboreal(X161))|leaf_occ(X161,X162)))|((((((occurrence_of(sK18_skl(X161),tptp3)&next_subocc(X161,sK18_skl(X161),tptp0))&occurrence_of(sK17_skl(X161),tptp4))&next_subocc(sK18_skl(X161),sK17_skl(X161),tptp0))&(occurrence_of(sK16_skl(X161),tptp2)|occurrence_of(sK16_skl(X161),tptp1)))&next_subocc(sK17_skl(X161),sK16_skl(X161),tptp0))&leaf(sK16_skl(X161),tptp0)))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X165,sK16_skl(X161)),skolemize(X164,sK17_skl(X161)),skolemize(X163,sK18_skl(X161))],[f250])).
% 50.13/6.95 fof(f252,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK18_skl(X1),tptp3))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f251])).
% 50.13/6.95 fof(f253,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK18_skl(X1),tptp0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f251])).
% 50.13/6.95 fof(f255,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK18_skl(X1),sK17_skl(X1),tptp0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f251])).
% 50.13/6.95 fof(f256,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp2)|occurrence_of(sK16_skl(X1),tptp1))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f251])).
% 50.13/6.95 fof(f257,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK17_skl(X1),sK16_skl(X1),tptp0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f251])).
% 50.13/6.95 fof(f258,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|leaf(sK16_skl(X1),tptp0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f251])).
% 50.13/6.95 fof(f260,plain,(
% 50.13/6.95 ~atomic(tptp0)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f52])).
% 50.13/6.95 fof(f270,plain,(
% 50.13/6.95 ~tptp2=tptp1),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f62])).
% 50.13/6.95 fof(f271,plain,(
% 50.13/6.95 (?[X166,X167]: ((((occurrence_of(X167,tptp0)&subactivity_occurrence(X166,X167))&arboreal(X166))&~leaf_occ(X166,X167))&(![X168,X169]: ((((~occurrence_of(X168,tptp3)|~next_subocc(X166,X168,tptp0))|(~occurrence_of(X169,tptp2)&~occurrence_of(X169,tptp1)))|~min_precedes(X168,X169,tptp0))|~leaf(X169,tptp0)))))),
% 50.13/6.95 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 50.13/6.95 fof(f272,plain,(
% 50.13/6.95 ?[X166]: ((?[X167]: (((occurrence_of(X167,tptp0)&subactivity_occurrence(X166,X167))&arboreal(X166))&~leaf_occ(X166,X167)))&(![X169]: ((![X168]: (((~occurrence_of(X168,tptp3)|~next_subocc(X166,X168,tptp0))|(~occurrence_of(X169,tptp2)&~occurrence_of(X169,tptp1)))|~min_precedes(X168,X169,tptp0)))|~leaf(X169,tptp0))))),
% 50.13/6.95 inference(miniscoping,[status(thm)],[f271])).
% 50.13/6.95 fof(f273,plain,(
% 50.13/6.95 ((((occurrence_of(sK20_skl,tptp0)&subactivity_occurrence(sK19_skl,sK20_skl))&arboreal(sK19_skl))&~leaf_occ(sK19_skl,sK20_skl))&(![X169]: ((![X168]: (((~occurrence_of(X168,tptp3)|~next_subocc(sK19_skl,X168,tptp0))|(~occurrence_of(X169,tptp2)&~occurrence_of(X169,tptp1)))|~min_precedes(X168,X169,tptp0)))|~leaf(X169,tptp0))))),
% 50.13/6.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X166,sK19_skl),skolemize(X167,sK20_skl)],[f272])).
% 50.13/6.95 fof(f274,plain,(
% 50.13/6.95 occurrence_of(sK20_skl,tptp0)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f273])).
% 50.13/6.95 fof(f275,plain,(
% 50.13/6.95 subactivity_occurrence(sK19_skl,sK20_skl)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f273])).
% 50.13/6.95 fof(f276,plain,(
% 50.13/6.95 arboreal(sK19_skl)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f273])).
% 50.13/6.95 fof(f277,plain,(
% 50.13/6.95 ~leaf_occ(sK19_skl,sK20_skl)),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f273])).
% 50.13/6.95 fof(f278,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp3)|~next_subocc(sK19_skl,X0,tptp0)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0)|~leaf(X1,tptp0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f273])).
% 50.13/6.95 fof(f279,plain,(
% 50.13/6.95 ![X0,X1]: (~occurrence_of(X0,tptp3)|~next_subocc(sK19_skl,X0,tptp0)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0)|~leaf(X1,tptp0))),
% 50.13/6.95 inference(cnf_transformation,[status(thm)],[f273])).
% 50.13/6.95 fof(f698,plain,(
% 50.13/6.95 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|occurrence_of(sK18_skl(X0),tptp3))),
% 50.13/6.95 inference(resolution,[status(thm)],[f252,f274])).
% 50.13/6.95 fof(f736,plain,(
% 50.13/6.95 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK18_skl(sK19_skl),tptp3)),
% 50.13/6.95 inference(resolution,[status(thm)],[f698,f275])).
% 50.13/6.95 fof(f738,plain,(
% 50.13/6.95 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK18_skl(sK19_skl),tptp3)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f736,f276])).
% 50.13/6.95 fof(f739,plain,(
% 50.13/6.95 occurrence_of(sK18_skl(sK19_skl),tptp3)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f738,f277])).
% 50.13/6.95 fof(f855,plain,(
% 50.13/6.95 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|next_subocc(X0,sK18_skl(X0),tptp0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f253,f274])).
% 50.13/6.95 fof(f861,plain,(
% 50.13/6.95 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|next_subocc(sK18_skl(X0),sK17_skl(X0),tptp0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f255,f274])).
% 50.13/6.95 fof(f870,plain,(
% 50.13/6.95 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f855,f275])).
% 50.13/6.95 fof(f872,plain,(
% 50.13/6.95 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f870,f276])).
% 50.13/6.95 fof(f873,plain,(
% 50.13/6.95 next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f872,f277])).
% 50.13/6.95 fof(f876,plain,(
% 50.13/6.95 min_precedes(sK19_skl,sK18_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f873,f147])).
% 50.13/6.95 fof(f892,plain,(
% 50.13/6.95 min_precedes(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK18_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f876,f114])).
% 50.13/6.95 fof(f894,plain,(
% 50.13/6.95 root(sK4_skl(tptp0,sK18_skl(sK19_skl)),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f876,f113])).
% 50.13/6.95 fof(f932,plain,(
% 50.13/6.95 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f861,f275])).
% 50.13/6.95 fof(f934,plain,(
% 50.13/6.95 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f932,f276])).
% 50.13/6.95 fof(f1011,plain,(
% 50.13/6.95 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|occurrence_of(sK16_skl(X0),tptp2)|occurrence_of(sK16_skl(X0),tptp1))),
% 50.13/6.95 inference(resolution,[status(thm)],[f256,f274])).
% 50.13/6.95 fof(f1015,plain,(
% 50.13/6.95 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|next_subocc(sK17_skl(X0),sK16_skl(X0),tptp0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f257,f274])).
% 50.13/6.95 fof(f1019,plain,(
% 50.13/6.95 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|leaf(sK16_skl(X0),tptp0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f258,f274])).
% 50.13/6.95 fof(f1032,plain,(
% 50.13/6.95 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp2)|occurrence_of(sK16_skl(sK19_skl),tptp1)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1011,f275])).
% 50.13/6.95 fof(f1034,plain,(
% 50.13/6.95 leaf_occ(sK19_skl,sK20_skl)|occurrence_of(sK16_skl(sK19_skl),tptp2)|occurrence_of(sK16_skl(sK19_skl),tptp1)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1032,f276])).
% 50.13/6.95 fof(f1071,plain,(
% 50.13/6.95 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1015,f275])).
% 50.13/6.95 fof(f1073,plain,(
% 50.13/6.95 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1071,f276])).
% 50.13/6.95 fof(f1076,plain,(
% 50.13/6.95 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|leaf(sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1019,f275])).
% 50.13/6.95 fof(f1078,plain,(
% 50.13/6.95 leaf_occ(sK19_skl,sK20_skl)|leaf(sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1076,f276])).
% 50.13/6.95 fof(f1181,plain,(
% 50.13/6.95 leaf(sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1078,f277])).
% 50.13/6.95 fof(f1183,plain,(
% 50.13/6.95 atomic(tptp0)|leaf_occ(sK16_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1181,f239])).
% 50.13/6.95 fof(f1184,plain,(
% 50.13/6.95 atomic(tptp0)|occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1181,f238])).
% 50.13/6.95 fof(f1186,plain,(
% 50.13/6.95 leaf_occ(sK16_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1183,f260])).
% 50.13/6.95 fof(f1187,plain,(
% 50.13/6.95 occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1184,f260])).
% 50.13/6.95 fof(f1205,plain,(
% 50.13/6.95 ![X0]: (root_occ(X0,sK15_skl(tptp0,sK16_skl(sK19_skl)))|~subactivity_occurrence(X0,sK15_skl(tptp0,sK16_skl(sK19_skl)))|~root(X0,tptp0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1187,f197])).
% 50.13/6.95 fof(f1207,plain,(
% 50.13/6.95 ![X0,X1]: (~root_occ(X0,sK15_skl(tptp0,sK16_skl(sK19_skl)))|~root_occ(X1,sK15_skl(tptp0,sK16_skl(sK19_skl)))|X0=X1)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1187,f207])).
% 50.13/6.95 fof(f1226,plain,(
% 50.13/6.95 next_subocc(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f934,f277])).
% 50.13/6.95 fof(f1229,plain,(
% 50.13/6.95 min_precedes(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1226,f147])).
% 50.13/6.95 fof(f1252,plain,(
% 50.13/6.95 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK17_skl(sK19_skl),X0)|subactivity_occurrence(sK18_skl(sK19_skl),X0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1229,f179])).
% 50.13/6.95 fof(f1254,plain,(
% 50.13/6.95 precedes(sK18_skl(sK19_skl),sK17_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1229,f120])).
% 50.13/6.95 fof(f1263,plain,(
% 50.13/6.95 earlier(sK18_skl(sK19_skl),sK17_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1254,f96])).
% 50.13/6.95 fof(f1303,plain,(
% 50.13/6.95 occurrence_of(sK16_skl(sK19_skl),tptp2)|occurrence_of(sK16_skl(sK19_skl),tptp1)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1034,f277])).
% 50.13/6.95 fof(f1321,plain,(
% 50.13/6.95 occurrence_of(sK16_skl(sK19_skl),tptp1)|activity_occurrence(sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1303,f67])).
% 50.13/6.95 fof(f1328,plain,(
% 50.13/6.95 activity_occurrence(sK16_skl(sK19_skl))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1321,f67])).
% 50.13/6.95 fof(f1329,plain,(
% 50.13/6.95 occurrence_of(sK16_skl(sK19_skl),sK0_skl(sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1328,f71])).
% 50.13/6.95 fof(f1387,plain,(
% 50.13/6.95 ![X0]: (~occurrence_of(sK16_skl(sK19_skl),X0)|X0=sK0_skl(sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1329,f74])).
% 50.13/6.95 fof(f1394,plain,(
% 50.13/6.95 next_subocc(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1073,f277])).
% 50.13/6.95 fof(f1397,plain,(
% 50.13/6.95 min_precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1394,f147])).
% 50.13/6.95 fof(f1419,plain,(
% 50.13/6.95 min_precedes(sK4_skl(tptp0,sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1397,f114])).
% 50.13/6.95 fof(f1421,plain,(
% 50.13/6.95 root(sK4_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1397,f113])).
% 50.13/6.95 fof(f1425,plain,(
% 50.13/6.95 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK16_skl(sK19_skl),X0)|subactivity_occurrence(sK17_skl(sK19_skl),X0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1397,f179])).
% 50.13/6.95 fof(f1427,plain,(
% 50.13/6.95 precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1397,f120])).
% 50.13/6.95 fof(f1436,plain,(
% 50.13/6.95 earlier(sK17_skl(sK19_skl),sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1427,f96])).
% 50.13/6.95 fof(f1437,plain,(
% 50.13/6.95 legal(sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1427,f97])).
% 50.13/6.95 fof(f1448,plain,(
% 50.13/6.95 ![X0]: (~earlier(X0,sK17_skl(sK19_skl))|earlier(X0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1436,f81])).
% 50.13/6.95 fof(f1464,plain,(
% 50.13/6.95 subactivity_occurrence(sK16_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1186,f202])).
% 50.13/6.95 fof(f1490,plain,(
% 50.13/6.95 tptp2=sK0_skl(sK16_skl(sK19_skl))|occurrence_of(sK16_skl(sK19_skl),tptp1)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1387,f1303])).
% 50.13/6.95 fof(f1492,plain,(
% 50.13/6.95 earlier(sK18_skl(sK19_skl),sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1448,f1263])).
% 50.13/6.95 fof(f1533,plain,(
% 50.13/6.95 precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl))|~legal(sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1492,f98])).
% 50.13/6.95 fof(f1536,plain,(
% 50.13/6.95 precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f1533,f1437])).
% 50.13/6.95 fof(f1573,plain,(
% 50.13/6.95 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK18_skl(sK19_skl),X0)|subactivity_occurrence(sK4_skl(tptp0,sK18_skl(sK19_skl)),X0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f892,f179])).
% 50.13/6.95 fof(f1984,plain,(
% 50.13/6.95 ![X0]: (~min_precedes(sK4_skl(tptp0,sK16_skl(sK19_skl)),X0,tptp0)|~precedes(X0,sK16_skl(sK19_skl))|min_precedes(X0,sK16_skl(sK19_skl),tptp0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1419,f128])).
% 50.13/6.95 fof(f1995,plain,(
% 50.13/6.95 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK16_skl(sK19_skl),X0)|subactivity_occurrence(sK4_skl(tptp0,sK16_skl(sK19_skl)),X0))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1419,f179])).
% 50.13/6.95 fof(f2055,plain,(
% 50.13/6.95 tptp2=sK0_skl(sK16_skl(sK19_skl))|tptp1=sK0_skl(sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1490,f1387])).
% 50.13/6.95 fof(f2188,plain,(
% 50.13/6.95 occurrence_of(sK16_skl(sK19_skl),tptp2)|tptp1=sK0_skl(sK16_skl(sK19_skl))),
% 50.13/6.95 inference(paramodulation,[status(thm)],[f2055,f1329])).
% 50.13/6.95 fof(f2579,plain,(
% 50.13/6.95 ~occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)|subactivity_occurrence(sK17_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1425,f1464])).
% 50.13/6.95 fof(f2580,plain,(
% 50.13/6.95 subactivity_occurrence(sK17_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f2579,f1187])).
% 50.13/6.95 fof(f2581,plain,(
% 50.13/6.95 ~occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)|subactivity_occurrence(sK18_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f2580,f1252])).
% 50.13/6.95 fof(f2585,plain,(
% 50.13/6.95 subactivity_occurrence(sK18_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f2581,f1187])).
% 50.13/6.95 fof(f4884,plain,(
% 50.13/6.95 ~occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)|subactivity_occurrence(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1573,f2585])).
% 50.13/6.95 fof(f4894,plain,(
% 50.13/6.95 subactivity_occurrence(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f4884,f1187])).
% 50.13/6.95 fof(f4946,plain,(
% 50.13/6.95 ~occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)|subactivity_occurrence(sK4_skl(tptp0,sK16_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f1995,f1464])).
% 50.13/6.95 fof(f4950,plain,(
% 50.13/6.95 subactivity_occurrence(sK4_skl(tptp0,sK16_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f4946,f1187])).
% 50.13/6.95 fof(f6534,plain,(
% 50.13/6.95 root_occ(sK4_skl(tptp0,sK16_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))|~root(sK4_skl(tptp0,sK16_skl(sK19_skl)),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1205,f4950])).
% 50.13/6.95 fof(f6536,plain,(
% 50.13/6.95 root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))|~root(sK4_skl(tptp0,sK18_skl(sK19_skl)),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f1205,f4894])).
% 50.13/6.95 fof(f6542,plain,(
% 50.13/6.95 root_occ(sK4_skl(tptp0,sK16_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f6534,f1421])).
% 50.13/6.95 fof(f6544,plain,(
% 50.13/6.95 root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK15_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f6536,f894])).
% 50.13/6.95 fof(f6565,plain,(
% 50.13/6.95 ![X0]: (~root_occ(X0,sK15_skl(tptp0,sK16_skl(sK19_skl)))|X0=sK4_skl(tptp0,sK16_skl(sK19_skl)))),
% 50.13/6.95 inference(resolution,[status(thm)],[f6542,f1207])).
% 50.13/6.95 fof(f6581,plain,(
% 50.13/6.95 sK4_skl(tptp0,sK18_skl(sK19_skl))=sK4_skl(tptp0,sK16_skl(sK19_skl))),
% 50.13/6.95 inference(resolution,[status(thm)],[f6565,f6544])).
% 50.13/6.95 fof(f24972,plain,(
% 50.13/6.95 ![X0]: (~min_precedes(sK4_skl(tptp0,sK18_skl(sK19_skl)),X0,tptp0)|~precedes(X0,sK16_skl(sK19_skl))|min_precedes(X0,sK16_skl(sK19_skl),tptp0))),
% 50.13/6.95 inference(forward_demodulation,[status(thm)],[f6581,f1984])).
% 50.13/6.95 fof(f24980,plain,(
% 50.13/6.95 ~precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl))|min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f24972,f892])).
% 50.13/6.95 fof(f24986,plain,(
% 50.13/6.95 min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f24980,f1536])).
% 50.13/6.95 fof(f24991,plain,(
% 50.13/6.95 ~occurrence_of(sK18_skl(sK19_skl),tptp3)|~next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)|~occurrence_of(sK16_skl(sK19_skl),tptp1)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f24986,f279])).
% 50.13/6.95 fof(f24992,plain,(
% 50.13/6.95 ~occurrence_of(sK18_skl(sK19_skl),tptp3)|~next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)|~occurrence_of(sK16_skl(sK19_skl),tptp2)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(resolution,[status(thm)],[f24986,f278])).
% 50.13/6.95 fof(f25019,plain,(
% 50.13/6.95 ~next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)|~occurrence_of(sK16_skl(sK19_skl),tptp1)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 50.13/6.95 inference(forward_subsumption_resolution,[status(thm)],[f24991,f739])).
% 8.06/7.00 fof(f25020,plain,(
% 8.06/7.00 ~next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)|~occurrence_of(sK16_skl(sK19_skl),tptp2)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 8.06/7.00 inference(forward_subsumption_resolution,[status(thm)],[f24992,f739])).
% 8.06/7.00 fof(f26891,plain,(
% 8.06/7.00 ~occurrence_of(sK16_skl(sK19_skl),tptp1)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 8.06/7.00 inference(forward_subsumption_resolution,[status(thm)],[f25019,f873])).
% 8.06/7.00 fof(f26892,plain,(
% 8.06/7.00 ~leaf(sK16_skl(sK19_skl),tptp0)|tptp2=sK0_skl(sK16_skl(sK19_skl))),
% 8.06/7.00 inference(resolution,[status(thm)],[f26891,f1490])).
% 8.06/7.00 fof(f26894,plain,(
% 8.06/7.00 tptp2=sK0_skl(sK16_skl(sK19_skl))),
% 8.06/7.00 inference(forward_subsumption_resolution,[status(thm)],[f26892,f1181])).
% 8.06/7.00 fof(f27022,plain,(
% 8.06/7.00 occurrence_of(sK16_skl(sK19_skl),tptp2)|tptp1=tptp2),
% 8.06/7.00 inference(backward_demodulation,[status(thm)],[f26894,f2188])).
% 8.06/7.00 fof(f27086,plain,(
% 8.06/7.00 occurrence_of(sK16_skl(sK19_skl),tptp2)),
% 8.06/7.00 inference(forward_subsumption_resolution,[status(thm)],[f27022,f270])).
% 8.06/7.00 fof(f27387,plain,(
% 8.06/7.00 ~occurrence_of(sK16_skl(sK19_skl),tptp2)|~leaf(sK16_skl(sK19_skl),tptp0)),
% 8.06/7.00 inference(forward_subsumption_resolution,[status(thm)],[f25020,f873])).
% 8.06/7.00 fof(f27388,plain,(
% 8.06/7.00 ~leaf(sK16_skl(sK19_skl),tptp0)),
% 8.06/7.00 inference(resolution,[status(thm)],[f27387,f27086])).
% 8.06/7.00 fof(f27389,plain,(
% 8.06/7.00 $false),
% 8.06/7.00 inference(forward_subsumption_resolution,[status(thm)],[f27388,f1181])).
% 8.06/7.00 % SZS output end CNFRefutation for theBenchmark.p
% 8.06/7.03 % Elapsed time: 6.464136 seconds
% 8.06/7.03 % CPU time: 50.927451 seconds
% 8.06/7.03 % Total memory used: 326.174 MB
% 8.06/7.03 % Net memory used: 309.112 MB
%------------------------------------------------------------------------------