%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO005+4 : 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 : n015.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:22 PM UTC 2026
% Result : Theorem 9.50s 6.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO005+4 : 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/5.37 % Computer : n015.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 03:44:55 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 9.50/6.68 % Refutation found
% 9.50/6.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.50/6.68 % SZS output start CNFRefutation for theBenchmark
% 9.50/6.68 fof(f3,axiom,(
% 9.50/6.68 (! [X8,X9,X10,X11] :( ( occurrence_of(X9,X8)& subactivity_occurrence(X10,X9)& leaf_occ(X11,X9)& arboreal(X10)& ~ min_precedes(X10,X11,X8) )=> X11 = X10 ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f4,axiom,(
% 9.50/6.68 (! [X12,X13] :( occurrence_of(X13,X12)=> ( activity(X12)& activity_occurrence(X13) ) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f7,axiom,(
% 9.50/6.68 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f8,axiom,(
% 9.50/6.68 (! [X25,X26] :( ( leaf(X25,X26)& ~ atomic(X26) )=> (? [X27] :( occurrence_of(X27,X26)& leaf_occ(X25,X27) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f9,axiom,(
% 9.50/6.68 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f10,axiom,(
% 9.50/6.68 (! [X31,X32,X33] :( ( occurrence_of(X31,X33)& leaf_occ(X32,X31) )=> ~ (? [X34] : min_precedes(X32,X34,X33) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f12,axiom,(
% 9.50/6.68 (! [X39,X40] :( subactivity_occurrence(X39,X40)=> ( activity_occurrence(X39)& activity_occurrence(X40) ) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f13,axiom,(
% 9.50/6.68 (! [X41] :( activity_occurrence(X41)=> (? [X42] :( activity(X42)& occurrence_of(X41,X42) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f14,axiom,(
% 9.50/6.68 (! [X43] :( legal(X43)=> arboreal(X43) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f17,axiom,(
% 9.50/6.68 (! [X51,X52] :( occurrence_of(X51,X52)=> ( arboreal(X51)<=> atomic(X52) ) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f18,axiom,(
% 9.50/6.68 (! [X53,X54] :( root(X53,X54)=> legal(X53) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f19,axiom,(
% 9.50/6.68 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f20,axiom,(
% 9.50/6.68 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f27,axiom,(
% 9.50/6.68 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f28,axiom,(
% 9.50/6.68 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f30,axiom,(
% 9.50/6.68 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f33,axiom,(
% 9.50/6.68 (! [X101] :( occurrence_of(X101,tptp0)=> (? [X102,X103] :( occurrence_of(X102,tptp4)& root_occ(X102,X101)& ( occurrence_of(X103,tptp3)| occurrence_of(X103,tptp2) )& leaf_occ(X103,X101)& next_subocc(X102,X103,tptp0) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f35,axiom,(
% 9.50/6.68 ~ atomic(tptp0) ),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f39,axiom,(
% 9.50/6.68 atomic(tptp1) ),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f43,axiom,(
% 9.50/6.68 tptp1 != tptp3 ),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f44,axiom,(
% 9.50/6.68 tptp1 != tptp2 ),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f47,axiom,(
% 9.50/6.68 (! [X106,X107] :( ( occurrence_of(X107,tptp0)& subactivity_occurrence(X106,X107)& arboreal(X106)& ~ leaf_occ(X106,X107) )=> (? [X108] :( occurrence_of(X108,tptp1)& next_subocc(X106,X108,tptp0) ) )) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f48,conjecture,(
% 9.50/6.68 ~ (? [X109] : occurrence_of(X109,tptp0) )),
% 9.50/6.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.50/6.68 fof(f49,negated_conjecture,(
% 9.50/6.68 ~(~ (? [X109] : occurrence_of(X109,tptp0) ))),
% 9.50/6.68 inference(negated_conjecture,[status(cth)],[f48])).
% 9.50/6.68 fof(f57,plain,(
% 9.50/6.68 ![X8,X9,X10,X11]: (((((~occurrence_of(X9,X8)|~subactivity_occurrence(X10,X9))|~leaf_occ(X11,X9))|~arboreal(X10))|min_precedes(X10,X11,X8))|X11=X10)),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 9.50/6.68 fof(f58,plain,(
% 9.50/6.68 ![X10,X11]: ((![X8]: (((![X9]: ((~occurrence_of(X9,X8)|~subactivity_occurrence(X10,X9))|~leaf_occ(X11,X9)))|~arboreal(X10))|min_precedes(X10,X11,X8)))|X11=X10)),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f57])).
% 9.50/6.68 fof(f59,plain,(
% 9.50/6.68 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~subactivity_occurrence(X2,X0)|~leaf_occ(X3,X0)|~arboreal(X2)|min_precedes(X2,X3,X1)|X3=X2)),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f58])).
% 9.50/6.68 fof(f60,plain,(
% 9.50/6.68 ![X12,X13]: (~occurrence_of(X13,X12)|(activity(X12)&activity_occurrence(X13)))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 9.50/6.68 fof(f62,plain,(
% 9.50/6.68 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f60])).
% 9.50/6.68 fof(f70,plain,(
% 9.50/6.68 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 9.50/6.68 fof(f71,plain,(
% 9.50/6.68 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|((occurrence_of(sK2_skl(X23,X22,X21),X21)&subactivity_occurrence(X22,sK2_skl(X23,X22,X21)))&subactivity_occurrence(X23,sK2_skl(X23,X22,X21))))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f70])).
% 9.50/6.68 fof(f72,plain,(
% 9.50/6.68 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f71])).
% 9.50/6.68 fof(f73,plain,(
% 9.50/6.68 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f71])).
% 9.50/6.68 fof(f74,plain,(
% 9.50/6.68 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK2_skl(X1,X0,X2)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f71])).
% 9.50/6.68 fof(f75,plain,(
% 9.50/6.68 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(?[X27]: (occurrence_of(X27,X26)&leaf_occ(X25,X27))))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 9.50/6.68 fof(f76,plain,(
% 9.50/6.68 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(occurrence_of(sK3_skl(X26,X25),X26)&leaf_occ(X25,sK3_skl(X26,X25))))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X27,sK3_skl(X26,X25))],[f75])).
% 9.50/6.68 fof(f77,plain,(
% 9.50/6.68 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|occurrence_of(sK3_skl(X1,X0),X1))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f76])).
% 9.50/6.68 fof(f78,plain,(
% 9.50/6.68 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|leaf_occ(X0,sK3_skl(X1,X0)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f76])).
% 9.50/6.68 fof(f79,plain,(
% 9.50/6.68 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 9.50/6.68 fof(f80,plain,(
% 9.50/6.68 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f79])).
% 9.50/6.68 fof(f81,plain,(
% 9.50/6.68 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f80])).
% 9.50/6.68 fof(f82,plain,(
% 9.50/6.68 ![X31,X32,X33]: ((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 9.50/6.68 fof(f83,plain,(
% 9.50/6.68 ![X32,X33]: ((![X31]: (~occurrence_of(X31,X33)|~leaf_occ(X32,X31)))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f82])).
% 9.50/6.68 fof(f84,plain,(
% 9.50/6.68 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f83])).
% 9.50/6.68 fof(f88,plain,(
% 9.50/6.68 ![X39,X40]: (~subactivity_occurrence(X39,X40)|(activity_occurrence(X39)&activity_occurrence(X40)))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 9.50/6.68 fof(f89,plain,(
% 9.50/6.68 ![X0,X1]: (~subactivity_occurrence(X0,X1)|activity_occurrence(X0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f88])).
% 9.50/6.68 fof(f91,plain,(
% 9.50/6.68 ![X41]: (~activity_occurrence(X41)|(?[X42]: (activity(X42)&occurrence_of(X41,X42))))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 9.50/6.68 fof(f92,plain,(
% 9.50/6.68 ![X41]: (~activity_occurrence(X41)|(activity(sK4_skl(X41))&occurrence_of(X41,sK4_skl(X41))))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f91])).
% 9.50/6.68 fof(f94,plain,(
% 9.50/6.68 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK4_skl(X0)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f92])).
% 9.50/6.68 fof(f95,plain,(
% 9.50/6.68 ![X43]: (~legal(X43)|arboreal(X43))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 9.50/6.68 fof(f96,plain,(
% 9.50/6.68 ![X0]: (~legal(X0)|arboreal(X0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f95])).
% 9.50/6.68 fof(f112,plain,(
% 9.50/6.68 ![X51,X52]: (~occurrence_of(X51,X52)|(arboreal(X51)<=>atomic(X52)))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 9.50/6.68 fof(f113,plain,(
% 9.50/6.68 ![X51,X52]: (~occurrence_of(X51,X52)|((~arboreal(X51)|atomic(X52))&(arboreal(X51)|~atomic(X52))))),
% 9.50/6.68 inference(NNF_transformation,[status(thm)],[f112])).
% 9.50/6.68 fof(f115,plain,(
% 9.50/6.68 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f113])).
% 9.50/6.68 fof(f116,plain,(
% 9.50/6.68 ![X53,X54]: (~root(X53,X54)|legal(X53))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 9.50/6.68 fof(f117,plain,(
% 9.50/6.68 ![X53]: ((![X54]: ~root(X53,X54))|legal(X53))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f116])).
% 9.50/6.68 fof(f118,plain,(
% 9.50/6.68 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f117])).
% 9.50/6.68 fof(f119,plain,(
% 9.50/6.68 ![X55,X56]: ((~leaf_occ(X55,X56)|(?[X57]: ((occurrence_of(X56,X57)&subactivity_occurrence(X55,X56))&leaf(X55,X57))))&(leaf_occ(X55,X56)|(![X57]: ((~occurrence_of(X56,X57)|~subactivity_occurrence(X55,X56))|~leaf(X55,X57)))))),
% 9.50/6.68 inference(NNF_transformation,[status(thm)],[f19])).
% 9.50/6.68 fof(f120,plain,(
% 9.50/6.68 (![X55,X56]: (~leaf_occ(X55,X56)|(?[X57]: ((occurrence_of(X56,X57)&subactivity_occurrence(X55,X56))&leaf(X55,X57)))))&(![X55,X56]: (leaf_occ(X55,X56)|(![X57]: ((~occurrence_of(X56,X57)|~subactivity_occurrence(X55,X56))|~leaf(X55,X57)))))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f119])).
% 9.50/6.68 fof(f121,plain,(
% 9.50/6.68 (![X55,X56]: (~leaf_occ(X55,X56)|((occurrence_of(X56,sK8_skl(X56,X55))&subactivity_occurrence(X55,X56))&leaf(X55,sK8_skl(X56,X55)))))&(![X55,X56]: (leaf_occ(X55,X56)|(![X57]: ((~occurrence_of(X56,X57)|~subactivity_occurrence(X55,X56))|~leaf(X55,X57)))))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f120])).
% 9.50/6.68 fof(f122,plain,(
% 9.50/6.68 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK8_skl(X1,X0)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f121])).
% 9.50/6.68 fof(f123,plain,(
% 9.50/6.68 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f121])).
% 9.50/6.68 fof(f124,plain,(
% 9.50/6.68 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK8_skl(X1,X0)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f121])).
% 9.50/6.68 fof(f126,plain,(
% 9.50/6.68 ![X58,X59]: ((~root_occ(X58,X59)|(?[X60]: ((occurrence_of(X59,X60)&subactivity_occurrence(X58,X59))&root(X58,X60))))&(root_occ(X58,X59)|(![X60]: ((~occurrence_of(X59,X60)|~subactivity_occurrence(X58,X59))|~root(X58,X60)))))),
% 9.50/6.68 inference(NNF_transformation,[status(thm)],[f20])).
% 9.50/6.68 fof(f127,plain,(
% 9.50/6.68 (![X58,X59]: (~root_occ(X58,X59)|(?[X60]: ((occurrence_of(X59,X60)&subactivity_occurrence(X58,X59))&root(X58,X60)))))&(![X58,X59]: (root_occ(X58,X59)|(![X60]: ((~occurrence_of(X59,X60)|~subactivity_occurrence(X58,X59))|~root(X58,X60)))))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f126])).
% 9.50/6.68 fof(f128,plain,(
% 9.50/6.68 (![X58,X59]: (~root_occ(X58,X59)|((occurrence_of(X59,sK9_skl(X59,X58))&subactivity_occurrence(X58,X59))&root(X58,sK9_skl(X59,X58)))))&(![X58,X59]: (root_occ(X58,X59)|(![X60]: ((~occurrence_of(X59,X60)|~subactivity_occurrence(X58,X59))|~root(X58,X60)))))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f127])).
% 9.50/6.68 fof(f129,plain,(
% 9.50/6.68 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK9_skl(X1,X0)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f128])).
% 9.50/6.68 fof(f130,plain,(
% 9.50/6.68 ![X0,X1]: (~root_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f128])).
% 9.50/6.68 fof(f131,plain,(
% 9.50/6.68 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK9_skl(X1,X0)))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f128])).
% 9.50/6.68 fof(f132,plain,(
% 9.50/6.68 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f128])).
% 9.50/6.68 fof(f155,plain,(
% 9.50/6.68 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 9.50/6.68 fof(f156,plain,(
% 9.50/6.68 ![X78,X79,X80]: ((~next_subocc(X78,X79,X80)|(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))&(next_subocc(X78,X79,X80)|(~min_precedes(X78,X79,X80)|(?[X81]: (min_precedes(X78,X81,X80)&min_precedes(X81,X79,X80))))))),
% 9.50/6.68 inference(NNF_transformation,[status(thm)],[f155])).
% 9.50/6.68 fof(f157,plain,(
% 9.50/6.68 (![X78,X79,X80]: (~next_subocc(X78,X79,X80)|(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80))))))&(![X78,X79,X80]: (next_subocc(X78,X79,X80)|(~min_precedes(X78,X79,X80)|(?[X81]: (min_precedes(X78,X81,X80)&min_precedes(X81,X79,X80))))))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f156])).
% 9.50/6.68 fof(f158,plain,(
% 9.50/6.68 (![X78,X79,X80]: (~next_subocc(X78,X79,X80)|(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80))))))&(![X78,X79,X80]: (next_subocc(X78,X79,X80)|(~min_precedes(X78,X79,X80)|(min_precedes(X78,sK11_skl(X80,X79,X78),X80)&min_precedes(sK11_skl(X80,X79,X78),X79,X80)))))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f157])).
% 9.50/6.68 fof(f159,plain,(
% 9.50/6.68 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f158])).
% 9.50/6.68 fof(f160,plain,(
% 9.50/6.68 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f158])).
% 9.50/6.68 fof(f163,plain,(
% 9.50/6.68 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 9.50/6.68 fof(f164,plain,(
% 9.50/6.68 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f163])).
% 9.50/6.68 fof(f165,plain,(
% 9.50/6.68 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f164])).
% 9.50/6.68 fof(f169,plain,(
% 9.50/6.68 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 9.50/6.68 fof(f170,plain,(
% 9.50/6.68 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f169])).
% 9.50/6.68 fof(f171,plain,(
% 9.50/6.68 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f170])).
% 9.50/6.68 fof(f178,plain,(
% 9.50/6.68 ![X101]: (~occurrence_of(X101,tptp0)|(?[X102,X103]: ((((occurrence_of(X102,tptp4)&root_occ(X102,X101))&(occurrence_of(X103,tptp3)|occurrence_of(X103,tptp2)))&leaf_occ(X103,X101))&next_subocc(X102,X103,tptp0))))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 9.50/6.68 fof(f179,plain,(
% 9.50/6.68 ![X101]: (~occurrence_of(X101,tptp0)|((((occurrence_of(sK12_skl(X101),tptp4)&root_occ(sK12_skl(X101),X101))&(occurrence_of(sK13_skl(X101),tptp3)|occurrence_of(sK13_skl(X101),tptp2)))&leaf_occ(sK13_skl(X101),X101))&next_subocc(sK12_skl(X101),sK13_skl(X101),tptp0)))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f178])).
% 9.50/6.68 fof(f181,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK12_skl(X0),X0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f179])).
% 9.50/6.68 fof(f182,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK13_skl(X0),tptp3)|occurrence_of(sK13_skl(X0),tptp2))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f179])).
% 9.50/6.68 fof(f183,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK13_skl(X0),X0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f179])).
% 9.50/6.68 fof(f184,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f179])).
% 9.50/6.68 fof(f186,plain,(
% 9.50/6.68 ~atomic(tptp0)),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f35])).
% 9.50/6.68 fof(f190,plain,(
% 9.50/6.68 atomic(tptp1)),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f39])).
% 9.50/6.68 fof(f194,plain,(
% 9.50/6.68 ~tptp1=tptp3),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f43])).
% 9.50/6.68 fof(f195,plain,(
% 9.50/6.68 ~tptp1=tptp2),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f44])).
% 9.50/6.68 fof(f199,plain,(
% 9.50/6.68 ![X106,X107]: ((((~occurrence_of(X107,tptp0)|~subactivity_occurrence(X106,X107))|~arboreal(X106))|leaf_occ(X106,X107))|(?[X108]: (occurrence_of(X108,tptp1)&next_subocc(X106,X108,tptp0))))),
% 9.50/6.68 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 9.50/6.68 fof(f200,plain,(
% 9.50/6.68 ![X106]: ((![X107]: (((~occurrence_of(X107,tptp0)|~subactivity_occurrence(X106,X107))|~arboreal(X106))|leaf_occ(X106,X107)))|(?[X108]: (occurrence_of(X108,tptp1)&next_subocc(X106,X108,tptp0))))),
% 9.50/6.68 inference(miniscoping,[status(thm)],[f199])).
% 9.50/6.68 fof(f201,plain,(
% 9.50/6.68 ![X106]: ((![X107]: (((~occurrence_of(X107,tptp0)|~subactivity_occurrence(X106,X107))|~arboreal(X106))|leaf_occ(X106,X107)))|(occurrence_of(sK14_skl(X106),tptp1)&next_subocc(X106,sK14_skl(X106),tptp0)))),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X108,sK14_skl(X106))],[f200])).
% 9.50/6.68 fof(f202,plain,(
% 9.50/6.68 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp1))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f201])).
% 9.50/6.68 fof(f203,plain,(
% 9.50/6.68 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f201])).
% 9.50/6.68 fof(f204,plain,(
% 9.50/6.68 occurrence_of(sK15_skl,tptp0)),
% 9.50/6.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X109,sK15_skl)],[f49])).
% 9.50/6.68 fof(f205,plain,(
% 9.50/6.68 occurrence_of(sK15_skl,tptp0)),
% 9.50/6.68 inference(cnf_transformation,[status(thm)],[f204])).
% 9.50/6.68 fof(f206,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(sK15_skl,X0)|X0=tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f81,f205])).
% 9.50/6.68 fof(f285,plain,(
% 9.50/6.68 root_occ(sK12_skl(sK15_skl),sK15_skl)),
% 9.50/6.68 inference(resolution,[status(thm)],[f181,f205])).
% 9.50/6.68 fof(f286,plain,(
% 9.50/6.68 root(sK12_skl(sK15_skl),sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f285,f131])).
% 9.50/6.68 fof(f287,plain,(
% 9.50/6.68 occurrence_of(sK15_skl,sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f285,f129])).
% 9.50/6.68 fof(f288,plain,(
% 9.50/6.68 subactivity_occurrence(sK12_skl(sK15_skl),sK15_skl)),
% 9.50/6.68 inference(resolution,[status(thm)],[f285,f130])).
% 9.50/6.68 fof(f296,plain,(
% 9.50/6.68 leaf_occ(sK13_skl(sK15_skl),sK15_skl)),
% 9.50/6.68 inference(resolution,[status(thm)],[f183,f205])).
% 9.50/6.68 fof(f298,plain,(
% 9.50/6.68 leaf(sK13_skl(sK15_skl),sK8_skl(sK15_skl,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f296,f124])).
% 9.50/6.68 fof(f299,plain,(
% 9.50/6.68 occurrence_of(sK15_skl,sK8_skl(sK15_skl,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f296,f122])).
% 9.50/6.68 fof(f311,plain,(
% 9.50/6.68 sK9_skl(sK15_skl,sK12_skl(sK15_skl))=tptp0),
% 9.50/6.68 inference(resolution,[status(thm)],[f287,f206])).
% 9.50/6.68 fof(f336,plain,(
% 9.50/6.68 root(sK12_skl(sK15_skl),tptp0)),
% 9.50/6.68 inference(forward_demodulation,[status(thm)],[f311,f286])).
% 9.50/6.68 fof(f339,plain,(
% 9.50/6.68 legal(sK12_skl(sK15_skl))),
% 9.50/6.68 inference(resolution,[status(thm)],[f336,f118])).
% 9.50/6.68 fof(f340,plain,(
% 9.50/6.68 arboreal(sK12_skl(sK15_skl))),
% 9.50/6.68 inference(resolution,[status(thm)],[f339,f96])).
% 9.50/6.68 fof(f341,plain,(
% 9.50/6.68 sK8_skl(sK15_skl,sK13_skl(sK15_skl))=tptp0),
% 9.50/6.68 inference(resolution,[status(thm)],[f299,f206])).
% 9.50/6.68 fof(f366,plain,(
% 9.50/6.68 leaf(sK13_skl(sK15_skl),tptp0)),
% 9.50/6.68 inference(forward_demodulation,[status(thm)],[f341,f298])).
% 9.50/6.68 fof(f367,plain,(
% 9.50/6.68 atomic(tptp0)|leaf_occ(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f366,f78])).
% 9.50/6.68 fof(f368,plain,(
% 9.50/6.68 atomic(tptp0)|occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f366,f77])).
% 9.50/6.68 fof(f369,plain,(
% 9.50/6.68 leaf_occ(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f367,f186])).
% 9.50/6.68 fof(f370,plain,(
% 9.50/6.68 occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f368,f186])).
% 9.50/6.68 fof(f445,plain,(
% 9.50/6.68 subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f369,f123])).
% 9.50/6.68 fof(f474,plain,(
% 9.50/6.68 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f184,f205])).
% 9.50/6.68 fof(f475,plain,(
% 9.50/6.68 min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f474,f159])).
% 9.50/6.68 fof(f484,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK12_skl(sK15_skl),X0))),
% 9.50/6.68 inference(resolution,[status(thm)],[f475,f84])).
% 9.50/6.68 fof(f650,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK13_skl(sK15_skl),X0)|subactivity_occurrence(sK12_skl(sK15_skl),X0))),
% 9.50/6.68 inference(resolution,[status(thm)],[f165,f475])).
% 9.50/6.68 fof(f762,plain,(
% 9.50/6.68 ![X0]: (~subactivity_occurrence(X0,sK15_skl)|~arboreal(X0)|leaf_occ(X0,sK15_skl)|occurrence_of(sK14_skl(X0),tptp1))),
% 9.50/6.68 inference(resolution,[status(thm)],[f202,f205])).
% 9.50/6.68 fof(f764,plain,(
% 9.50/6.68 ![X0]: (~subactivity_occurrence(X0,sK3_skl(tptp0,sK13_skl(sK15_skl)))|~arboreal(X0)|leaf_occ(X0,sK3_skl(tptp0,sK13_skl(sK15_skl)))|next_subocc(X0,sK14_skl(X0),tptp0))),
% 9.50/6.68 inference(resolution,[status(thm)],[f203,f370])).
% 9.50/6.68 fof(f805,plain,(
% 9.50/6.68 ~occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)|subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f650,f445])).
% 9.50/6.68 fof(f807,plain,(
% 9.50/6.68 subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f805,f370])).
% 9.50/6.68 fof(f839,plain,(
% 9.50/6.68 ~arboreal(sK12_skl(sK15_skl))|leaf_occ(sK12_skl(sK15_skl),sK15_skl)|occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 9.50/6.68 inference(resolution,[status(thm)],[f762,f288])).
% 9.50/6.68 fof(f840,plain,(
% 9.50/6.68 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f839,f340])).
% 9.50/6.68 fof(f849,plain,(
% 9.50/6.68 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|arboreal(sK14_skl(sK12_skl(sK15_skl)))|~atomic(tptp1)),
% 9.50/6.68 inference(resolution,[status(thm)],[f840,f115])).
% 9.50/6.68 fof(f853,plain,(
% 9.50/6.68 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(resolution,[status(thm)],[f840,f62])).
% 9.50/6.68 fof(f859,plain,(
% 9.50/6.68 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f849,f190])).
% 9.50/6.68 fof(f868,plain,(
% 9.50/6.68 arboreal(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f859,f484])).
% 9.50/6.68 fof(f875,plain,(
% 9.50/6.68 arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f868,f205])).
% 9.50/6.68 fof(f876,plain,(
% 9.50/6.68 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f853,f484])).
% 9.50/6.68 fof(f883,plain,(
% 9.50/6.68 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f876,f205])).
% 9.50/6.68 fof(f884,plain,(
% 9.50/6.68 occurrence_of(sK14_skl(sK12_skl(sK15_skl)),sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 9.50/6.68 inference(resolution,[status(thm)],[f883,f94])).
% 9.50/6.68 fof(f899,plain,(
% 9.50/6.68 ![X0]: (~occurrence_of(sK14_skl(sK12_skl(sK15_skl)),X0)|X0=sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 9.50/6.68 inference(resolution,[status(thm)],[f884,f81])).
% 9.50/6.68 fof(f902,plain,(
% 9.50/6.68 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|leaf_occ(sK12_skl(sK15_skl),sK15_skl)),
% 9.50/6.68 inference(resolution,[status(thm)],[f899,f840])).
% 9.50/6.68 fof(f903,plain,(
% 9.50/6.68 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f902,f484])).
% 9.50/6.68 fof(f910,plain,(
% 9.50/6.68 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f903,f205])).
% 9.50/6.68 fof(f2252,plain,(
% 9.50/6.68 ~arboreal(sK12_skl(sK15_skl))|leaf_occ(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))|next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f764,f807])).
% 9.50/6.68 fof(f2253,plain,(
% 9.50/6.68 leaf_occ(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))|next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f2252,f340])).
% 9.50/6.68 fof(f2254,plain,(
% 9.50/6.68 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)|~occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f2253,f484])).
% 9.50/6.68 fof(f2261,plain,(
% 9.50/6.68 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(forward_subsumption_resolution,[status(thm)],[f2254,f370])).
% 9.50/6.68 fof(f2263,plain,(
% 9.50/6.68 min_precedes(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f2261,f159])).
% 9.50/6.68 fof(f2272,plain,(
% 9.50/6.68 ![X0]: (~next_subocc(sK12_skl(sK15_skl),X0,tptp0)|~min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0))),
% 9.50/6.68 inference(resolution,[status(thm)],[f2263,f160])).
% 9.50/6.68 fof(f2278,plain,(
% 9.50/6.68 subactivity_occurrence(sK14_skl(sK12_skl(sK15_skl)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.68 inference(resolution,[status(thm)],[f2263,f74])).
% 9.50/6.68 fof(f2279,plain,(
% 9.50/6.68 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.68 inference(resolution,[status(thm)],[f2263,f73])).
% 9.50/6.68 fof(f2280,plain,(
% 9.50/6.68 occurrence_of(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0),tptp0)),
% 9.50/6.68 inference(resolution,[status(thm)],[f2263,f72])).
% 9.50/6.68 fof(f2300,plain,(
% 9.50/6.68 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp3)|occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp2)),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f182])).
% 9.50/6.69 fof(f2301,plain,(
% 9.50/6.69 next_subocc(sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f184])).
% 9.50/6.69 fof(f2303,plain,(
% 9.50/6.69 leaf_occ(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f183])).
% 9.50/6.69 fof(f2304,plain,(
% 9.50/6.69 root_occ(sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f181])).
% 9.50/6.69 fof(f2306,plain,(
% 9.50/6.69 ![X0]: (root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~subactivity_occurrence(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~root(X0,tptp0))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f132])).
% 9.50/6.69 fof(f2308,plain,(
% 9.50/6.69 ![X0,X1]: (~root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~root_occ(X1,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|X0=X1)),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f171])).
% 9.50/6.69 fof(f2313,plain,(
% 9.50/6.69 ![X0,X1]: (~subactivity_occurrence(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~leaf_occ(X1,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~arboreal(X0)|min_precedes(X0,X1,tptp0)|X1=X0)),
% 9.50/6.69 inference(resolution,[status(thm)],[f2280,f59])).
% 9.50/6.69 fof(f3077,plain,(
% 9.50/6.69 subactivity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2303,f123])).
% 9.50/6.69 fof(f3185,plain,(
% 9.50/6.69 activity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 9.50/6.69 inference(resolution,[status(thm)],[f3077,f89])).
% 9.50/6.69 fof(f3186,plain,(
% 9.50/6.69 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))))),
% 9.50/6.69 inference(resolution,[status(thm)],[f3185,f94])).
% 9.50/6.69 fof(f3511,plain,(
% 9.50/6.69 ![X0]: (~root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|X0=sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2308,f2304])).
% 9.50/6.69 fof(f3602,plain,(
% 9.50/6.69 ![X0]: (~occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),X0)|X0=sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))))),
% 9.50/6.69 inference(resolution,[status(thm)],[f3186,f81])).
% 9.50/6.69 fof(f3862,plain,(
% 9.50/6.69 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~root(sK12_skl(sK15_skl),tptp0)),
% 9.50/6.69 inference(resolution,[status(thm)],[f2306,f2279])).
% 9.50/6.69 fof(f3865,plain,(
% 9.50/6.69 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.69 inference(forward_subsumption_resolution,[status(thm)],[f3862,f336])).
% 9.50/6.69 fof(f3866,plain,(
% 9.50/6.69 sK12_skl(sK15_skl)=sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 9.50/6.69 inference(resolution,[status(thm)],[f3865,f3511])).
% 9.50/6.69 fof(f3881,plain,(
% 9.50/6.69 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 9.50/6.69 inference(backward_demodulation,[status(thm)],[f3866,f2301])).
% 9.50/6.69 fof(f4386,plain,(
% 9.50/6.69 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp2)|tptp3=sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2300,f3602])).
% 9.50/6.69 fof(f4769,plain,(
% 9.50/6.69 tptp3=sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))|tptp2=sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 9.50/6.69 inference(resolution,[status(thm)],[f4386,f3602])).
% 9.50/6.69 fof(f7909,plain,(
% 9.50/6.69 ![X0]: (~leaf_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~arboreal(sK14_skl(sK12_skl(sK15_skl)))|min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0)|X0=sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.69 inference(resolution,[status(thm)],[f2313,f2278])).
% 9.50/6.69 fof(f7913,plain,(
% 9.50/6.69 ![X0]: (~leaf_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0)|X0=sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.69 inference(forward_subsumption_resolution,[status(thm)],[f7909,f875])).
% 9.50/6.69 fof(f7922,plain,(
% 9.50/6.69 min_precedes(sK14_skl(sK12_skl(sK15_skl)),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)|sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))),
% 9.50/6.69 inference(resolution,[status(thm)],[f7913,f2303])).
% 9.50/6.69 fof(f8605,plain,(
% 9.50/6.69 sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))|~next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 9.50/6.69 inference(resolution,[status(thm)],[f7922,f2272])).
% 9.50/6.69 fof(f8624,plain,(
% 9.50/6.69 sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))),
% 9.50/6.69 inference(forward_subsumption_resolution,[status(thm)],[f8605,f3881])).
% 9.50/6.69 fof(f8691,plain,(
% 9.50/6.69 tptp3=sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))|tptp2=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.69 inference(backward_demodulation,[status(thm)],[f8624,f4769])).
% 9.50/6.69 fof(f8762,plain,(
% 9.50/6.69 tptp3=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|tptp2=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.69 inference(forward_demodulation,[status(thm)],[f8624,f8691])).
% 9.50/6.69 fof(f8763,plain,(
% 9.50/6.69 tptp3=tptp1|tptp2=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
% 9.50/6.69 inference(forward_demodulation,[status(thm)],[f910,f8762])).
% 9.50/6.69 fof(f8764,plain,(
% 9.50/6.69 tptp3=tptp1|tptp2=tptp1),
% 9.50/6.69 inference(forward_demodulation,[status(thm)],[f910,f8763])).
% 9.50/6.69 fof(f8765,plain,(
% 9.50/6.69 tptp2=tptp1),
% 9.50/6.69 inference(forward_subsumption_resolution,[status(thm)],[f8764,f194])).
% 9.50/6.71 fof(f8796,plain,(
% 9.50/6.71 $false),
% 9.50/6.71 inference(forward_subsumption_resolution,[status(thm)],[f8765,f195])).
% 9.50/6.71 % SZS output end CNFRefutation for theBenchmark.p
% 1.72/6.72 % Elapsed time: 1.332924 seconds
% 1.72/6.72 % CPU time: 10.335729 seconds
% 1.72/6.72 % Total memory used: 199.745 MB
% 1.72/6.72 % Net memory used: 191.411 MB
%------------------------------------------------------------------------------