%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO016+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 : n006.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 101.32s 23.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO016+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.10/10.98 % Computer : n006.cluster.edu
% 0.10/10.98 % Model : x86_64 x86_64
% 0.10/10.98 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.98 % Memory : 8046.5625MB
% 0.10/10.98 % OS : Linux 6.8.0-71-generic
% 0.10/10.98 % CPULimit : 300
% 0.10/10.98 % WCLimit : 300
% 0.10/10.98 % DateTime : Mon Sep 21 03:42:54 UTC 2026
% 0.10/10.99 % CPUTime :
% 0.10/11.01 % Drodi V4.1.1
% 101.32/23.86 % Refutation found
% 101.32/23.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 101.32/23.86 % SZS output start CNFRefutation for theBenchmark
% 101.32/23.86 fof(f9,axiom,(
% 101.32/23.86 (! [X18] :( legal(X18)=> arboreal(X18) ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f14,axiom,(
% 101.32/23.86 (! [X31,X32,X33] :( min_precedes(X31,X32,X33)=> (? [X34] :( root(X34,X33)& min_precedes(X34,X32,X33) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f17,axiom,(
% 101.32/23.86 (! [X41,X42] :( root(X41,X42)=> legal(X41) ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f23,axiom,(
% 101.32/23.86 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f26,axiom,(
% 101.32/23.86 (! [X69,X70,X71] :( min_precedes(X70,X71,X69)=> (? [X72] :( occurrence_of(X72,X69)& subactivity_occurrence(X70,X72)& subactivity_occurrence(X71,X72) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f27,axiom,(
% 101.32/23.86 (! [X73,X74] :( ( root(X74,X73)& ~ atomic(X73) )=> (? [X75] :( occurrence_of(X75,X73)& subactivity_occurrence(X74,X75) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f28,axiom,(
% 101.32/23.86 (! [X76,X77] :( ( occurrence_of(X77,X76)& ~ atomic(X76) )=> (? [X78] :( root(X78,X76)& subactivity_occurrence(X78,X77) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f30,axiom,(
% 101.32/23.86 (! [X83,X84,X85,X86] :( ( min_precedes(X83,X84,X85)& occurrence_of(X86,X85)& subactivity_occurrence(X84,X86) )=> subactivity_occurrence(X83,X86) ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f34,axiom,(
% 101.32/23.86 (! [X99,X100] :( root_occ(X99,X100)<=> (? [X101] :( occurrence_of(X100,X101)& subactivity_occurrence(X99,X100)& root(X99,X101) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f35,axiom,(
% 101.32/23.86 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f36,axiom,(
% 101.32/23.86 (! [X105,X106,X107,X108] :( ( occurrence_of(X107,X108)& root_occ(X105,X107)& root_occ(X106,X107) )=> X105 = X106 ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f37,axiom,(
% 101.32/23.86 (! [X109,X110,X111,X112] :( ( occurrence_of(X111,X112)& ~ atomic(X112)& leaf_occ(X109,X111)& leaf_occ(X110,X111) )=> X109 = X110 ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f38,axiom,(
% 101.32/23.86 (! [X113,X114,X115] :( ( occurrence_of(X113,X115)& leaf_occ(X114,X113) )=> ~ (? [X116] : min_precedes(X114,X116,X115) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f39,axiom,(
% 101.32/23.86 (! [X117,X118,X119] :( ( occurrence_of(X117,X119)& root_occ(X118,X117) )=> ~ (? [X120] : min_precedes(X120,X118,X119) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f41,axiom,(
% 101.32/23.86 (! [X126,X127,X128,X129] :( ( next_subocc(X127,X126,X129)& next_subocc(X128,X126,X129) )=> X127 = X128 ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f45,axiom,(
% 101.32/23.86 (! [X142,X143,X144] :( next_subocc(X142,X143,X144)=> ( arboreal(X142)& arboreal(X143) ) ) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f50,axiom,(
% 101.32/23.86 (! [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,tptp1)| occurrence_of(X165,tptp2) )& next_subocc(X164,X165,tptp0)& leaf_occ(X165,X162) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f52,axiom,(
% 101.32/23.86 ~ atomic(tptp0) ),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f63,conjecture,(
% 101.32/23.86 (! [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,tptp1)| occurrence_of(X169,tptp2) )& min_precedes(X168,X169,tptp0)& leaf_occ(X169,X167)& ( occurrence_of(X169,tptp1)=> ~ (? [X170] :( occurrence_of(X170,tptp2)& min_precedes(X168,X170,tptp0) ) ))& ( occurrence_of(X169,tptp2)=> ~ (? [X171] :( occurrence_of(X171,tptp1)& min_precedes(X168,X171,tptp0) ) )) ) )) )),
% 101.32/23.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.32/23.86 fof(f64,negated_conjecture,(
% 101.32/23.86 ~((! [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,tptp1)| occurrence_of(X169,tptp2) )& min_precedes(X168,X169,tptp0)& leaf_occ(X169,X167)& ( occurrence_of(X169,tptp1)=> ~ (? [X170] :( occurrence_of(X170,tptp2)& min_precedes(X168,X170,tptp0) ) ))& ( occurrence_of(X169,tptp2)=> ~ (? [X171] :( occurrence_of(X171,tptp1)& min_precedes(X168,X171,tptp0) ) )) ) )) ))),
% 101.32/23.86 inference(negated_conjecture,[status(cth)],[f63])).
% 101.32/23.86 fof(f89,plain,(
% 101.32/23.86 ![X18]: (~legal(X18)|arboreal(X18))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 101.32/23.86 fof(f90,plain,(
% 101.32/23.86 ![X0]: (~legal(X0)|arboreal(X0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f89])).
% 101.32/23.86 fof(f110,plain,(
% 101.32/23.86 ![X31,X32,X33]: (~min_precedes(X31,X32,X33)|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 101.32/23.86 fof(f111,plain,(
% 101.32/23.86 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f110])).
% 101.32/23.86 fof(f112,plain,(
% 101.32/23.86 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(root(sK4_skl(X33,X32),X33)&min_precedes(sK4_skl(X33,X32),X32,X33)))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X34,sK4_skl(X33,X32))],[f111])).
% 101.32/23.86 fof(f113,plain,(
% 101.32/23.86 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|root(sK4_skl(X2,X1),X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f112])).
% 101.32/23.86 fof(f114,plain,(
% 101.32/23.86 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK4_skl(X2,X1),X1,X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f112])).
% 101.32/23.86 fof(f121,plain,(
% 101.32/23.86 ![X41,X42]: (~root(X41,X42)|legal(X41))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 101.32/23.86 fof(f122,plain,(
% 101.32/23.86 ![X41]: ((![X42]: ~root(X41,X42))|legal(X41))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f121])).
% 101.32/23.86 fof(f123,plain,(
% 101.32/23.86 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f122])).
% 101.32/23.86 fof(f143,plain,(
% 101.32/23.86 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 101.32/23.86 fof(f144,plain,(
% 101.32/23.86 ![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))))))),
% 101.32/23.86 inference(NNF_transformation,[status(thm)],[f143])).
% 101.32/23.86 fof(f145,plain,(
% 101.32/23.86 (![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))))))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f144])).
% 101.32/23.86 fof(f146,plain,(
% 101.32/23.86 (![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)))))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f145])).
% 101.32/23.86 fof(f147,plain,(
% 101.32/23.86 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f146])).
% 101.32/23.86 fof(f148,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f146])).
% 101.32/23.86 fof(f150,plain,(
% 101.32/23.86 ![X0,X1,X2]: (next_subocc(X0,X1,X2)|~min_precedes(X0,X1,X2)|min_precedes(sK7_skl(X2,X1,X0),X1,X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f146])).
% 101.32/23.86 fof(f161,plain,(
% 101.32/23.86 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|(?[X72]: ((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 101.32/23.86 fof(f162,plain,(
% 101.32/23.86 ![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))))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f161])).
% 101.32/23.86 fof(f163,plain,(
% 101.32/23.86 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK9_skl(X1,X0,X2),X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f162])).
% 101.32/23.86 fof(f164,plain,(
% 101.32/23.86 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK9_skl(X1,X0,X2)))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f162])).
% 101.32/23.86 fof(f166,plain,(
% 101.32/23.86 ![X73,X74]: ((~root(X74,X73)|atomic(X73))|(?[X75]: (occurrence_of(X75,X73)&subactivity_occurrence(X74,X75))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 101.32/23.86 fof(f167,plain,(
% 101.32/23.86 ![X73,X74]: ((~root(X74,X73)|atomic(X73))|(occurrence_of(sK10_skl(X74,X73),X73)&subactivity_occurrence(X74,sK10_skl(X74,X73))))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X75,sK10_skl(X74,X73))],[f166])).
% 101.32/23.86 fof(f168,plain,(
% 101.32/23.86 ![X0,X1]: (~root(X0,X1)|atomic(X1)|occurrence_of(sK10_skl(X0,X1),X1))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f167])).
% 101.32/23.86 fof(f169,plain,(
% 101.32/23.86 ![X0,X1]: (~root(X0,X1)|atomic(X1)|subactivity_occurrence(X0,sK10_skl(X0,X1)))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f167])).
% 101.32/23.86 fof(f170,plain,(
% 101.32/23.86 ![X76,X77]: ((~occurrence_of(X77,X76)|atomic(X76))|(?[X78]: (root(X78,X76)&subactivity_occurrence(X78,X77))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 101.32/23.86 fof(f171,plain,(
% 101.32/23.86 ![X76,X77]: ((~occurrence_of(X77,X76)|atomic(X76))|(root(sK11_skl(X77,X76),X76)&subactivity_occurrence(sK11_skl(X77,X76),X77)))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X78,sK11_skl(X77,X76))],[f170])).
% 101.32/23.86 fof(f172,plain,(
% 101.32/23.86 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1)|root(sK11_skl(X0,X1),X1))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f171])).
% 101.32/23.86 fof(f173,plain,(
% 101.32/23.86 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1)|subactivity_occurrence(sK11_skl(X0,X1),X0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f171])).
% 101.32/23.86 fof(f177,plain,(
% 101.32/23.86 ![X83,X84,X85,X86]: (((~min_precedes(X83,X84,X85)|~occurrence_of(X86,X85))|~subactivity_occurrence(X84,X86))|subactivity_occurrence(X83,X86))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 101.32/23.86 fof(f178,plain,(
% 101.32/23.86 ![X83,X86]: ((![X84]: ((![X85]: (~min_precedes(X83,X84,X85)|~occurrence_of(X86,X85)))|~subactivity_occurrence(X84,X86)))|subactivity_occurrence(X83,X86))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f177])).
% 101.32/23.86 fof(f179,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f178])).
% 101.32/23.86 fof(f191,plain,(
% 101.32/23.86 ![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)))))),
% 101.32/23.86 inference(NNF_transformation,[status(thm)],[f34])).
% 101.32/23.86 fof(f192,plain,(
% 101.32/23.86 (![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)))))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f191])).
% 101.32/23.86 fof(f193,plain,(
% 101.32/23.86 (![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)))))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f192])).
% 101.32/23.86 fof(f197,plain,(
% 101.32/23.86 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f193])).
% 101.32/23.86 fof(f198,plain,(
% 101.32/23.86 ![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)))))),
% 101.32/23.86 inference(NNF_transformation,[status(thm)],[f35])).
% 101.32/23.86 fof(f199,plain,(
% 101.32/23.86 (![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)))))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f198])).
% 101.32/23.86 fof(f200,plain,(
% 101.32/23.86 (![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)))))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f199])).
% 101.32/23.86 fof(f202,plain,(
% 101.32/23.86 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f200])).
% 101.32/23.86 fof(f205,plain,(
% 101.32/23.86 ![X105,X106,X107,X108]: (((~occurrence_of(X107,X108)|~root_occ(X105,X107))|~root_occ(X106,X107))|X105=X106)),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 101.32/23.86 fof(f206,plain,(
% 101.32/23.86 ![X105,X106]: ((![X107]: (((![X108]: ~occurrence_of(X107,X108))|~root_occ(X105,X107))|~root_occ(X106,X107)))|X105=X106)),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f205])).
% 101.32/23.86 fof(f207,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f206])).
% 101.32/23.86 fof(f208,plain,(
% 101.32/23.86 ![X109,X110,X111,X112]: ((((~occurrence_of(X111,X112)|atomic(X112))|~leaf_occ(X109,X111))|~leaf_occ(X110,X111))|X109=X110)),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 101.32/23.86 fof(f209,plain,(
% 101.32/23.86 ![X109,X110]: ((![X111]: (((![X112]: (~occurrence_of(X111,X112)|atomic(X112)))|~leaf_occ(X109,X111))|~leaf_occ(X110,X111)))|X109=X110)),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f208])).
% 101.32/23.86 fof(f210,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|atomic(X1)|~leaf_occ(X2,X0)|~leaf_occ(X3,X0)|X2=X3)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f209])).
% 101.32/23.86 fof(f211,plain,(
% 101.32/23.86 ![X113,X114,X115]: ((~occurrence_of(X113,X115)|~leaf_occ(X114,X113))|(![X116]: ~min_precedes(X114,X116,X115)))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 101.32/23.86 fof(f212,plain,(
% 101.32/23.86 ![X114,X115]: ((![X113]: (~occurrence_of(X113,X115)|~leaf_occ(X114,X113)))|(![X116]: ~min_precedes(X114,X116,X115)))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f211])).
% 101.32/23.86 fof(f213,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f212])).
% 101.32/23.86 fof(f214,plain,(
% 101.32/23.86 ![X117,X118,X119]: ((~occurrence_of(X117,X119)|~root_occ(X118,X117))|(![X120]: ~min_precedes(X120,X118,X119)))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 101.32/23.86 fof(f215,plain,(
% 101.32/23.86 ![X118,X119]: ((![X117]: (~occurrence_of(X117,X119)|~root_occ(X118,X117)))|(![X120]: ~min_precedes(X120,X118,X119)))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f214])).
% 101.32/23.86 fof(f216,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~min_precedes(X3,X2,X1))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f215])).
% 101.32/23.86 fof(f220,plain,(
% 101.32/23.86 ![X126,X127,X128,X129]: ((~next_subocc(X127,X126,X129)|~next_subocc(X128,X126,X129))|X127=X128)),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 101.32/23.86 fof(f221,plain,(
% 101.32/23.86 ![X127,X128]: ((![X126,X129]: (~next_subocc(X127,X126,X129)|~next_subocc(X128,X126,X129)))|X127=X128)),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f220])).
% 101.32/23.86 fof(f222,plain,(
% 101.32/23.86 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~next_subocc(X3,X1,X2)|X0=X3)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f221])).
% 101.32/23.86 fof(f232,plain,(
% 101.32/23.86 ![X142,X143,X144]: (~next_subocc(X142,X143,X144)|(arboreal(X142)&arboreal(X143)))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 101.32/23.86 fof(f233,plain,(
% 101.32/23.86 ![X142,X143]: ((![X144]: ~next_subocc(X142,X143,X144))|(arboreal(X142)&arboreal(X143)))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f232])).
% 101.32/23.86 fof(f235,plain,(
% 101.32/23.86 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|arboreal(X1))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f233])).
% 101.32/23.86 fof(f249,plain,(
% 101.32/23.86 ![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,tptp1)|occurrence_of(X165,tptp2)))&next_subocc(X164,X165,tptp0))&leaf_occ(X165,X162))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 101.32/23.86 fof(f250,plain,(
% 101.32/23.86 ![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,tptp1)|occurrence_of(X165,tptp2)))&next_subocc(X164,X165,tptp0)))&leaf_occ(X165,X162))))),
% 101.32/23.86 inference(miniscoping,[status(thm)],[f249])).
% 101.32/23.86 fof(f251,plain,(
% 101.32/23.86 ![X161,X162]: ((((~occurrence_of(X162,tptp0)|~subactivity_occurrence(X161,X162))|~arboreal(X161))|leaf_occ(X161,X162))|((((((occurrence_of(sK18_skl(X162,X161),tptp3)&next_subocc(X161,sK18_skl(X162,X161),tptp0))&occurrence_of(sK17_skl(X162,X161),tptp4))&next_subocc(sK18_skl(X162,X161),sK17_skl(X162,X161),tptp0))&(occurrence_of(sK16_skl(X162,X161),tptp1)|occurrence_of(sK16_skl(X162,X161),tptp2)))&next_subocc(sK17_skl(X162,X161),sK16_skl(X162,X161),tptp0))&leaf_occ(sK16_skl(X162,X161),X162)))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X165,sK16_skl(X162,X161)),skolemize(X164,sK17_skl(X162,X161)),skolemize(X163,sK18_skl(X162,X161))],[f250])).
% 101.32/23.86 fof(f253,plain,(
% 101.32/23.86 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK18_skl(X0,X1),tptp0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f251])).
% 101.32/23.86 fof(f255,plain,(
% 101.32/23.86 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK18_skl(X0,X1),sK17_skl(X0,X1),tptp0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f251])).
% 101.32/23.86 fof(f257,plain,(
% 101.32/23.86 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK17_skl(X0,X1),sK16_skl(X0,X1),tptp0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f251])).
% 101.32/23.86 fof(f258,plain,(
% 101.32/23.86 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|leaf_occ(sK16_skl(X0,X1),X0))),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f251])).
% 101.32/23.86 fof(f260,plain,(
% 101.32/23.86 ~atomic(tptp0)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f52])).
% 101.32/23.86 fof(f271,plain,(
% 101.32/23.86 (?[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,tptp1)&~occurrence_of(X169,tptp2)))|~min_precedes(X168,X169,tptp0))|~leaf_occ(X169,X167))|(occurrence_of(X169,tptp1)&(?[X170]: (occurrence_of(X170,tptp2)&min_precedes(X168,X170,tptp0)))))|(occurrence_of(X169,tptp2)&(?[X171]: (occurrence_of(X171,tptp1)&min_precedes(X168,X171,tptp0))))))))),
% 101.32/23.86 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 101.32/23.86 fof(f272,definition,(
% 101.32/23.86 ![X169]: (sP0_prd(X169)<=>(~occurrence_of(X169,tptp1)&~occurrence_of(X169,tptp2)))),
% 101.32/23.86 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 101.32/23.86 fof(f273,definition,(
% 101.32/23.86 ![X168,X169]: (sP1_prd(X169,X168)<=>(occurrence_of(X169,tptp1)&(?[X170]: (occurrence_of(X170,tptp2)&min_precedes(X168,X170,tptp0)))))),
% 101.32/23.86 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 101.32/23.86 fof(f274,plain,(
% 101.32/23.86 ?[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))|sP0_prd(X169))|~min_precedes(X168,X169,tptp0))|~leaf_occ(X169,X167))|sP1_prd(X169,X168))|(occurrence_of(X169,tptp2)&(?[X171]: (occurrence_of(X171,tptp1)&min_precedes(X168,X171,tptp0)))))))),
% 101.32/23.86 inference(formula_renaming,[status(thm)],[f271,f273,f272])).
% 101.32/23.86 fof(f275,plain,(
% 101.32/23.86 ((((occurrence_of(sK20_skl,tptp0)&subactivity_occurrence(sK19_skl,sK20_skl))&arboreal(sK19_skl))&~leaf_occ(sK19_skl,sK20_skl))&(![X168,X169]: ((((((~occurrence_of(X168,tptp3)|~next_subocc(sK19_skl,X168,tptp0))|sP0_prd(X169))|~min_precedes(X168,X169,tptp0))|~leaf_occ(X169,sK20_skl))|sP1_prd(X169,X168))|(occurrence_of(X169,tptp2)&(occurrence_of(sK21_skl(X169,X168),tptp1)&min_precedes(X168,sK21_skl(X169,X168),tptp0))))))),
% 101.32/23.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(X166,sK19_skl),skolemize(X167,sK20_skl),skolemize(X171,sK21_skl(X169,X168))],[f274])).
% 101.32/23.86 fof(f276,plain,(
% 101.32/23.86 occurrence_of(sK20_skl,tptp0)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f275])).
% 101.32/23.86 fof(f277,plain,(
% 101.32/23.86 subactivity_occurrence(sK19_skl,sK20_skl)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f275])).
% 101.32/23.86 fof(f278,plain,(
% 101.32/23.86 arboreal(sK19_skl)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f275])).
% 101.32/23.86 fof(f279,plain,(
% 101.32/23.86 ~leaf_occ(sK19_skl,sK20_skl)),
% 101.32/23.86 inference(cnf_transformation,[status(thm)],[f275])).
% 101.32/23.86 fof(f344,plain,(
% 101.32/23.86 ![X0,X1]: (~min_precedes(X0,X1,tptp0)|~subactivity_occurrence(X1,sK20_skl)|subactivity_occurrence(X0,sK20_skl))),
% 101.32/23.86 inference(resolution,[status(thm)],[f179,f276])).
% 101.32/23.86 fof(f369,plain,(
% 101.32/23.86 ![X0,X1]: (~leaf_occ(X0,sK20_skl)|~min_precedes(X0,X1,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f213,f276])).
% 101.32/23.86 fof(f463,plain,(
% 101.32/23.86 atomic(tptp0)|root(sK11_skl(sK20_skl,tptp0),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f172,f276])).
% 101.32/23.86 fof(f466,plain,(
% 101.32/23.86 root(sK11_skl(sK20_skl,tptp0),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f463,f260])).
% 101.32/23.86 fof(f467,plain,(
% 101.32/23.86 atomic(tptp0)|subactivity_occurrence(sK11_skl(sK20_skl,tptp0),sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f466,f169])).
% 101.32/23.86 fof(f468,plain,(
% 101.32/23.86 atomic(tptp0)|occurrence_of(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f466,f168])).
% 101.32/23.86 fof(f472,plain,(
% 101.32/23.86 legal(sK11_skl(sK20_skl,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f466,f123])).
% 101.32/23.86 fof(f473,plain,(
% 101.32/23.86 subactivity_occurrence(sK11_skl(sK20_skl,tptp0),sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f467,f260])).
% 101.32/23.86 fof(f474,plain,(
% 101.32/23.86 occurrence_of(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f468,f260])).
% 101.32/23.86 fof(f475,plain,(
% 101.32/23.86 arboreal(sK11_skl(sK20_skl,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f472,f90])).
% 101.32/23.86 fof(f490,plain,(
% 101.32/23.86 atomic(tptp0)|subactivity_occurrence(sK11_skl(sK20_skl,tptp0),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f173,f276])).
% 101.32/23.86 fof(f493,plain,(
% 101.32/23.86 subactivity_occurrence(sK11_skl(sK20_skl,tptp0),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f490,f260])).
% 101.32/23.86 fof(f566,plain,(
% 101.32/23.86 ![X0,X1]: (~root_occ(X0,sK20_skl)|~root_occ(X1,sK20_skl)|X0=X1)),
% 101.32/23.86 inference(resolution,[status(thm)],[f207,f276])).
% 101.32/23.86 fof(f682,plain,(
% 101.32/23.86 ![X0]: (root_occ(X0,sK20_skl)|~subactivity_occurrence(X0,sK20_skl)|~root(X0,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f197,f276])).
% 101.32/23.86 fof(f687,plain,(
% 101.32/23.86 ![X0]: (root_occ(sK11_skl(sK20_skl,tptp0),X0)|~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK11_skl(sK20_skl,tptp0),X0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f197,f466])).
% 101.32/23.86 fof(f700,plain,(
% 101.32/23.86 ![X0,X1]: (atomic(tptp0)|~leaf_occ(X0,sK20_skl)|~leaf_occ(X1,sK20_skl)|X0=X1)),
% 101.32/23.86 inference(resolution,[status(thm)],[f210,f276])).
% 101.32/23.86 fof(f704,plain,(
% 101.32/23.86 ![X0,X1]: (~leaf_occ(X0,sK20_skl)|~leaf_occ(X1,sK20_skl)|X0=X1)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f700,f260])).
% 101.32/23.86 fof(f726,plain,(
% 101.32/23.86 root_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|~root(sK11_skl(sK20_skl,tptp0),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f682,f493])).
% 101.32/23.86 fof(f728,plain,(
% 101.32/23.86 root_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f726,f466])).
% 101.32/23.86 fof(f730,plain,(
% 101.32/23.86 ![X0]: (~root_occ(X0,sK20_skl)|X0=sK11_skl(sK20_skl,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f728,f566])).
% 101.32/23.86 fof(f844,plain,(
% 101.32/23.86 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|next_subocc(X0,sK18_skl(sK20_skl,X0),tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f253,f276])).
% 101.32/23.86 fof(f845,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f253,f493])).
% 101.32/23.86 fof(f846,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f253,f277])).
% 101.32/23.86 fof(f847,plain,(
% 101.32/23.86 ~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f845,f276])).
% 101.32/23.86 fof(f848,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f846,f276])).
% 101.32/23.86 fof(f1018,plain,(
% 101.32/23.86 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|next_subocc(sK18_skl(sK20_skl,X0),sK17_skl(sK20_skl,X0),tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f255,f276])).
% 101.32/23.86 fof(f1020,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f255,f493])).
% 101.32/23.86 fof(f1021,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f255,f277])).
% 101.32/23.86 fof(f1022,plain,(
% 101.32/23.86 ~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1020,f276])).
% 101.32/23.86 fof(f1023,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1021,f276])).
% 101.32/23.86 fof(f1212,plain,(
% 101.32/23.86 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|next_subocc(sK17_skl(sK20_skl,X0),sK16_skl(sK20_skl,X0),tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f257,f276])).
% 101.32/23.86 fof(f1214,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f257,f493])).
% 101.32/23.86 fof(f1216,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK19_skl),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f257,f277])).
% 101.32/23.86 fof(f1217,plain,(
% 101.32/23.86 ~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1214,f276])).
% 101.32/23.86 fof(f1219,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK19_skl),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1216,f276])).
% 101.32/23.86 fof(f1221,plain,(
% 101.32/23.86 ![X0]: (~subactivity_occurrence(X0,sK20_skl)|~arboreal(X0)|leaf_occ(X0,sK20_skl)|leaf_occ(sK16_skl(sK20_skl,X0),sK20_skl))),
% 101.32/23.86 inference(resolution,[status(thm)],[f258,f276])).
% 101.32/23.86 fof(f1223,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f258,f493])).
% 101.32/23.86 fof(f1225,plain,(
% 101.32/23.86 ~occurrence_of(sK20_skl,tptp0)|~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f258,f277])).
% 101.32/23.86 fof(f1226,plain,(
% 101.32/23.86 ~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1223,f276])).
% 101.32/23.86 fof(f1228,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1225,f276])).
% 101.32/23.86 fof(f1557,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK19_skl,sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f848,f278])).
% 101.32/23.86 fof(f1564,plain,(
% 101.32/23.86 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~next_subocc(X0,sK18_skl(sK20_skl,sK19_skl),tptp0)|X0=sK19_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1557,f222])).
% 101.32/23.86 fof(f1574,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK19_skl,sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1557,f147])).
% 101.32/23.86 fof(f1578,plain,(
% 101.32/23.86 ![X0]: (~next_subocc(X0,sK18_skl(sK20_skl,sK19_skl),tptp0)|X0=sK19_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1564,f279])).
% 101.32/23.86 fof(f1583,plain,(
% 101.32/23.86 min_precedes(sK19_skl,sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1574,f279])).
% 101.32/23.86 fof(f1698,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1023,f278])).
% 101.32/23.86 fof(f1705,plain,(
% 101.32/23.86 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~next_subocc(X0,sK17_skl(sK20_skl,sK19_skl),tptp0)|X0=sK18_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1698,f222])).
% 101.32/23.86 fof(f1713,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|arboreal(sK17_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1698,f235])).
% 101.32/23.86 fof(f1715,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK18_skl(sK20_skl,sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1698,f147])).
% 101.32/23.86 fof(f1719,plain,(
% 101.32/23.86 ![X0]: (~next_subocc(X0,sK17_skl(sK20_skl,sK19_skl),tptp0)|X0=sK18_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1705,f279])).
% 101.32/23.86 fof(f1724,plain,(
% 101.32/23.86 arboreal(sK17_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1713,f279])).
% 101.32/23.86 fof(f1725,plain,(
% 101.32/23.86 min_precedes(sK18_skl(sK20_skl,sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1715,f279])).
% 101.32/23.86 fof(f1764,plain,(
% 101.32/23.86 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK19_skl,X0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1583,f213])).
% 101.32/23.86 fof(f1774,plain,(
% 101.32/23.86 ![X0]: (~next_subocc(sK19_skl,X0,tptp0)|~min_precedes(sK18_skl(sK20_skl,sK19_skl),X0,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1583,f148])).
% 101.32/23.86 fof(f1871,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK19_skl),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1219,f278])).
% 101.32/23.86 fof(f1878,plain,(
% 101.32/23.86 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~next_subocc(X0,sK16_skl(sK20_skl,sK19_skl),tptp0)|X0=sK17_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1871,f222])).
% 101.32/23.86 fof(f1888,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|min_precedes(sK17_skl(sK20_skl,sK19_skl),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1871,f147])).
% 101.32/23.86 fof(f1892,plain,(
% 101.32/23.86 ![X0]: (~next_subocc(X0,sK16_skl(sK20_skl,sK19_skl),tptp0)|X0=sK17_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1878,f279])).
% 101.32/23.86 fof(f1898,plain,(
% 101.32/23.86 min_precedes(sK17_skl(sK20_skl,sK19_skl),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1888,f279])).
% 101.32/23.86 fof(f1899,plain,(
% 101.32/23.86 ~leaf_occ(sK19_skl,sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1764,f474])).
% 101.32/23.86 fof(f1922,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1228,f278])).
% 101.32/23.86 fof(f1929,plain,(
% 101.32/23.86 ![X0]: (leaf_occ(sK19_skl,sK20_skl)|~leaf_occ(X0,sK20_skl)|X0=sK16_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(resolution,[status(thm)],[f1922,f704])).
% 101.32/23.86 fof(f1949,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK20_skl)|subactivity_occurrence(sK16_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1922,f202])).
% 101.32/23.86 fof(f1955,plain,(
% 101.32/23.86 ![X0]: (~leaf_occ(X0,sK20_skl)|X0=sK16_skl(sK20_skl,sK19_skl))),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1929,f279])).
% 101.32/23.86 fof(f1972,plain,(
% 101.32/23.86 subactivity_occurrence(sK16_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1949,f279])).
% 101.32/23.86 fof(f2281,plain,(
% 101.32/23.86 ~occurrence_of(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),tptp0)|~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f473,f253])).
% 101.32/23.86 fof(f2322,plain,(
% 101.32/23.86 ~arboreal(sK11_skl(sK20_skl,tptp0))|leaf_occ(sK11_skl(sK20_skl,tptp0),sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f2281,f474])).
% 101.32/23.86 fof(f3176,plain,(
% 101.32/23.86 min_precedes(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1725,f114])).
% 101.32/23.86 fof(f3177,plain,(
% 101.32/23.86 root(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1725,f113])).
% 101.32/23.86 fof(f3462,plain,(
% 101.32/23.86 ~subactivity_occurrence(sK16_skl(sK20_skl,sK19_skl),sK20_skl)|subactivity_occurrence(sK17_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1898,f344])).
% 101.32/23.86 fof(f3465,plain,(
% 101.32/23.86 ~leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1898,f369])).
% 101.32/23.86 fof(f3501,plain,(
% 101.32/23.86 subactivity_occurrence(sK17_skl(sK20_skl,sK19_skl),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f3462,f1972])).
% 101.32/23.86 fof(f3508,plain,(
% 101.32/23.86 ~arboreal(sK17_skl(sK20_skl,sK19_skl))|leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f3501,f1221])).
% 101.32/23.86 fof(f3509,plain,(
% 101.32/23.86 ~arboreal(sK17_skl(sK20_skl,sK19_skl))|leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK16_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f3501,f1212])).
% 101.32/23.86 fof(f3511,plain,(
% 101.32/23.86 ~arboreal(sK17_skl(sK20_skl,sK19_skl))|leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f3501,f1018])).
% 101.32/23.86 fof(f3513,plain,(
% 101.32/23.86 ~arboreal(sK17_skl(sK20_skl,sK19_skl))|leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK19_skl),sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f3501,f844])).
% 101.32/23.86 fof(f3588,plain,(
% 101.32/23.86 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f3508,f1724])).
% 101.32/23.86 fof(f3589,plain,(
% 101.32/23.86 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK16_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f3509,f1724])).
% 101.32/23.86 fof(f3591,plain,(
% 101.32/23.86 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f3511,f1724])).
% 101.32/23.86 fof(f3593,plain,(
% 101.32/23.86 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK19_skl),sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f3513,f1724])).
% 101.32/23.86 fof(f3710,plain,(
% 101.32/23.86 leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f847,f475])).
% 101.32/23.86 fof(f3849,plain,(
% 101.32/23.86 leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1022,f475])).
% 101.32/23.86 fof(f4448,plain,(
% 101.32/23.86 ~next_subocc(sK19_skl,sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f1774,f1725])).
% 101.32/23.86 fof(f4572,plain,(
% 101.32/23.86 leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1217,f475])).
% 101.32/23.86 fof(f4667,plain,(
% 101.32/23.86 leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)|leaf_occ(sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f1226,f475])).
% 101.32/23.86 fof(f7476,plain,(
% 101.32/23.86 ~subactivity_occurrence(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|subactivity_occurrence(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f3176,f344])).
% 101.32/23.86 fof(f7479,plain,(
% 101.32/23.86 ~leaf_occ(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f3176,f369])).
% 101.32/23.86 fof(f7518,plain,(
% 101.32/23.86 subactivity_occurrence(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f7476,f3501])).
% 101.32/23.86 fof(f7539,plain,(
% 101.32/23.86 root_occ(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)|~root(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f7518,f682])).
% 101.32/23.86 fof(f7624,plain,(
% 101.32/23.86 root_occ(sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f7539,f3177])).
% 101.32/23.86 fof(f7686,plain,(
% 101.32/23.86 sK4_skl(tptp0,sK17_skl(sK20_skl,sK19_skl))=sK11_skl(sK20_skl,tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f7624,f730])).
% 101.32/23.86 fof(f7759,plain,(
% 101.32/23.86 ~leaf_occ(sK11_skl(sK20_skl,tptp0),sK20_skl)),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f7686,f7479])).
% 101.32/23.86 fof(f7762,plain,(
% 101.32/23.86 min_precedes(sK11_skl(sK20_skl,tptp0),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f7686,f3176])).
% 101.32/23.86 fof(f7787,plain,(
% 101.32/23.86 leaf_occ(sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK20_skl)),
% 101.32/23.86 inference(backward_subsumption_resolution,[status(thm)],[f4667,f7759])).
% 101.32/23.86 fof(f7788,plain,(
% 101.32/23.86 next_subocc(sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(backward_subsumption_resolution,[status(thm)],[f4572,f7759])).
% 101.32/23.86 fof(f7790,plain,(
% 101.32/23.86 next_subocc(sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(backward_subsumption_resolution,[status(thm)],[f3849,f7759])).
% 101.32/23.86 fof(f7792,plain,(
% 101.32/23.86 next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(backward_subsumption_resolution,[status(thm)],[f3710,f7759])).
% 101.32/23.86 fof(f7802,plain,(
% 101.32/23.86 sK16_skl(sK20_skl,sK11_skl(sK20_skl,tptp0))=sK16_skl(sK20_skl,sK19_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f7787,f1955])).
% 101.32/23.86 fof(f8698,plain,(
% 101.32/23.86 next_subocc(sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f7802,f7788])).
% 101.32/23.86 fof(f8793,plain,(
% 101.32/23.86 sK17_skl(sK20_skl,sK11_skl(sK20_skl,tptp0))=sK17_skl(sK20_skl,sK19_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f8698,f1892])).
% 101.32/23.86 fof(f8967,plain,(
% 101.32/23.86 next_subocc(sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0)),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f8793,f7790])).
% 101.32/23.86 fof(f8999,plain,(
% 101.32/23.86 sK18_skl(sK20_skl,sK11_skl(sK20_skl,tptp0))=sK18_skl(sK20_skl,sK19_skl)),
% 101.32/23.86 inference(resolution,[status(thm)],[f8967,f1719])).
% 101.32/23.86 fof(f9059,plain,(
% 101.32/23.86 next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f8999,f7792])).
% 101.32/23.86 fof(f9090,plain,(
% 101.32/23.86 sK11_skl(sK20_skl,tptp0)=sK19_skl),
% 101.32/23.86 inference(resolution,[status(thm)],[f9059,f1578])).
% 101.32/23.86 fof(f9129,plain,(
% 101.32/23.86 min_precedes(sK19_skl,sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f9090,f7762])).
% 101.32/23.86 fof(f9173,plain,(
% 101.32/23.86 ![X0]: (root_occ(sK11_skl(sK20_skl,tptp0),X0)|~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK19_skl,X0))),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f9090,f687])).
% 101.32/23.86 fof(f9177,plain,(
% 101.32/23.86 ~leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))),
% 101.32/23.86 inference(backward_demodulation,[status(thm)],[f9090,f1899])).
% 101.32/23.86 fof(f9222,plain,(
% 101.32/23.86 ![X0]: (root_occ(sK19_skl,X0)|~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK19_skl,X0))),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f9173])).
% 101.32/23.86 fof(f9920,plain,(
% 101.32/23.86 next_subocc(sK19_skl,sK17_skl(sK20_skl,sK19_skl),tptp0)|min_precedes(sK7_skl(tptp0,sK17_skl(sK20_skl,sK19_skl),sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f9129,f150])).
% 101.32/23.86 fof(f9951,plain,(
% 101.32/23.86 min_precedes(sK7_skl(tptp0,sK17_skl(sK20_skl,sK19_skl),sK19_skl),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f9920,f4448])).
% 101.32/23.86 fof(f15418,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK11_skl(sK20_skl,tptp0),sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f2322])).
% 101.32/23.86 fof(f15419,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0))|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f15418])).
% 101.32/23.86 fof(f15420,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))|next_subocc(sK11_skl(sK20_skl,tptp0),sK18_skl(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f15419])).
% 101.32/23.86 fof(f15421,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))|next_subocc(sK19_skl,sK18_skl(sK10_skl(sK11_skl(sK20_skl,tptp0),tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f15420])).
% 101.32/23.86 fof(f15422,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))|next_subocc(sK19_skl,sK18_skl(sK10_skl(sK19_skl,tptp0),sK11_skl(sK20_skl,tptp0)),tptp0)),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f15421])).
% 101.32/23.86 fof(f15423,plain,(
% 101.32/23.86 ~arboreal(sK19_skl)|leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))|next_subocc(sK19_skl,sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_demodulation,[status(thm)],[f9090,f15422])).
% 101.32/23.86 fof(f15424,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))|next_subocc(sK19_skl,sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f15423,f278])).
% 101.32/23.86 fof(f15449,plain,(
% 101.32/23.86 leaf_occ(sK19_skl,sK10_skl(sK19_skl,tptp0))|min_precedes(sK19_skl,sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f15424,f147])).
% 101.32/23.86 fof(f15463,plain,(
% 101.32/23.86 min_precedes(sK19_skl,sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),tptp0)),
% 101.32/23.86 inference(forward_subsumption_resolution,[status(thm)],[f15449,f9177])).
% 101.32/23.86 fof(f15768,plain,(
% 101.32/23.86 subactivity_occurrence(sK19_skl,sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))),
% 101.32/23.86 inference(resolution,[status(thm)],[f15463,f164])).
% 101.32/23.86 fof(f15769,plain,(
% 101.32/23.86 occurrence_of(sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0),tptp0)),
% 101.32/23.86 inference(resolution,[status(thm)],[f15463,f163])).
% 28.66/23.92 fof(f17927,plain,(
% 28.66/23.92 root_occ(sK19_skl,sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))|~subactivity_occurrence(sK19_skl,sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))),
% 28.66/23.92 inference(resolution,[status(thm)],[f15769,f9222])).
% 28.66/23.92 fof(f18021,plain,(
% 28.66/23.92 ![X0,X1]: (~root_occ(X0,sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))|~min_precedes(X1,X0,tptp0))),
% 28.66/23.92 inference(resolution,[status(thm)],[f15769,f216])).
% 28.66/23.92 fof(f18035,plain,(
% 28.66/23.92 root_occ(sK19_skl,sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))),
% 28.66/23.92 inference(forward_subsumption_resolution,[status(thm)],[f17927,f15768])).
% 28.66/23.92 fof(f29031,plain,(
% 28.66/23.92 leaf_occ(sK16_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK20_skl)),
% 28.66/23.92 inference(forward_subsumption_resolution,[status(thm)],[f3588,f3465])).
% 28.66/23.92 fof(f29045,plain,(
% 28.66/23.92 sK16_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl))=sK16_skl(sK20_skl,sK19_skl)),
% 28.66/23.92 inference(resolution,[status(thm)],[f29031,f1955])).
% 28.66/23.92 fof(f40900,plain,(
% 28.66/23.92 ~root_occ(sK17_skl(sK20_skl,sK19_skl),sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))),
% 28.66/23.92 inference(resolution,[status(thm)],[f18021,f9951])).
% 28.66/23.92 fof(f50086,plain,(
% 28.66/23.92 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 28.66/23.92 inference(forward_demodulation,[status(thm)],[f29045,f3589])).
% 28.66/23.92 fof(f50087,plain,(
% 28.66/23.92 next_subocc(sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK16_skl(sK20_skl,sK19_skl),tptp0)),
% 28.66/23.92 inference(forward_subsumption_resolution,[status(thm)],[f50086,f3465])).
% 28.66/23.92 fof(f50088,plain,(
% 28.66/23.92 sK17_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl))=sK17_skl(sK20_skl,sK19_skl)),
% 28.66/23.92 inference(resolution,[status(thm)],[f50087,f1892])).
% 28.66/23.92 fof(f50157,plain,(
% 28.66/23.92 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 28.66/23.92 inference(forward_demodulation,[status(thm)],[f50088,f3591])).
% 28.66/23.92 fof(f50158,plain,(
% 28.66/23.92 next_subocc(sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl)),sK17_skl(sK20_skl,sK19_skl),tptp0)),
% 28.66/23.92 inference(forward_subsumption_resolution,[status(thm)],[f50157,f3465])).
% 28.66/23.92 fof(f50159,plain,(
% 28.66/23.92 sK18_skl(sK20_skl,sK17_skl(sK20_skl,sK19_skl))=sK18_skl(sK20_skl,sK19_skl)),
% 28.66/23.92 inference(resolution,[status(thm)],[f50158,f1719])).
% 28.66/23.92 fof(f50228,plain,(
% 28.66/23.92 leaf_occ(sK17_skl(sK20_skl,sK19_skl),sK20_skl)|next_subocc(sK17_skl(sK20_skl,sK19_skl),sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 28.66/23.92 inference(forward_demodulation,[status(thm)],[f50159,f3593])).
% 28.66/23.92 fof(f50229,plain,(
% 28.66/23.92 next_subocc(sK17_skl(sK20_skl,sK19_skl),sK18_skl(sK20_skl,sK19_skl),tptp0)),
% 28.66/23.92 inference(forward_subsumption_resolution,[status(thm)],[f50228,f3465])).
% 28.66/23.92 fof(f50232,plain,(
% 28.66/23.92 sK17_skl(sK20_skl,sK19_skl)=sK19_skl),
% 28.66/23.92 inference(resolution,[status(thm)],[f50229,f1578])).
% 28.66/23.92 fof(f50313,plain,(
% 28.66/23.92 ~root_occ(sK19_skl,sK9_skl(sK18_skl(sK10_skl(sK19_skl,tptp0),sK19_skl),sK19_skl,tptp0))),
% 28.66/23.92 inference(backward_demodulation,[status(thm)],[f50232,f40900])).
% 28.66/23.92 fof(f50783,plain,(
% 28.66/23.92 $false),
% 28.66/23.92 inference(forward_subsumption_resolution,[status(thm)],[f50313,f18035])).
% 28.66/23.92 % SZS output end CNFRefutation for theBenchmark.p
% 28.66/23.94 % Elapsed time: 12.939104 seconds
% 28.66/23.94 % CPU time: 102.125315 seconds
% 28.66/23.94 % Total memory used: 355.056 MB
% 28.66/23.94 % Net memory used: 332.538 MB
%------------------------------------------------------------------------------