%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO004+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 15.16s 2.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO004+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.57 % Computer : n011.cluster.edu
% 0.11/0.57 % Model : x86_64 x86_64
% 0.11/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.57 % Memory : 8046.5625MB
% 0.11/0.57 % OS : Linux 6.8.0-71-generic
% 0.11/0.57 % CPULimit : 300
% 0.11/0.57 % WCLimit : 300
% 0.11/0.57 % DateTime : Mon Sep 21 03:40:56 UTC 2026
% 0.11/0.57 % CPUTime :
% 0.11/0.58 % Drodi V4.1.1
% 15.16/2.52 % Refutation found
% 15.16/2.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.16/2.52 % SZS output start CNFRefutation for theBenchmark
% 15.16/2.52 fof(f3,axiom,(
% 15.16/2.52 (! [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 ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f4,axiom,(
% 15.16/2.52 (! [X12,X13] :( occurrence_of(X13,X12)=> ( activity(X12)& activity_occurrence(X13) ) ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f7,axiom,(
% 15.16/2.52 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f8,axiom,(
% 15.16/2.52 (! [X25,X26] :( ( leaf(X25,X26)& ~ atomic(X26) )=> (? [X27] :( occurrence_of(X27,X26)& leaf_occ(X25,X27) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f9,axiom,(
% 15.16/2.52 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f10,axiom,(
% 15.16/2.52 (! [X31,X32,X33] :( ( occurrence_of(X31,X33)& leaf_occ(X32,X31) )=> ~ (? [X34] : min_precedes(X32,X34,X33) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f13,axiom,(
% 15.16/2.52 (! [X41] :( activity_occurrence(X41)=> (? [X42] :( activity(X42)& occurrence_of(X41,X42) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f14,axiom,(
% 15.16/2.52 (! [X43] :( legal(X43)=> arboreal(X43) ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f17,axiom,(
% 15.16/2.52 (! [X51,X52] :( occurrence_of(X51,X52)=> ( arboreal(X51)<=> atomic(X52) ) ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f18,axiom,(
% 15.16/2.52 (! [X53,X54] :( root(X53,X54)=> legal(X53) ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f19,axiom,(
% 15.16/2.52 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f20,axiom,(
% 15.16/2.52 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f27,axiom,(
% 15.16/2.52 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f28,axiom,(
% 15.16/2.52 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f30,axiom,(
% 15.16/2.52 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f33,axiom,(
% 15.16/2.52 (! [X101] :( occurrence_of(X101,tptp0)=> (? [X102,X103] :( occurrence_of(X102,tptp4)& root_occ(X102,X101)& occurrence_of(X103,tptp3)& leaf_occ(X103,X101)& next_subocc(X102,X103,tptp0) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f35,axiom,(
% 15.16/2.52 ~ atomic(tptp0) ),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f39,axiom,(
% 15.16/2.52 atomic(tptp1) ),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f43,axiom,(
% 15.16/2.52 tptp1 != tptp3 ),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f48,axiom,(
% 15.16/2.52 (! [X108,X109] :( ( occurrence_of(X109,tptp0)& subactivity_occurrence(X108,X109)& arboreal(X108)& ~ leaf_occ(X108,X109) )=> (? [X110] :( occurrence_of(X110,tptp1)& next_subocc(X108,X110,tptp0) ) )) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f49,conjecture,(
% 15.16/2.52 ~ (? [X111] : occurrence_of(X111,tptp0) )),
% 15.16/2.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.52 fof(f50,negated_conjecture,(
% 15.16/2.52 ~(~ (? [X111] : occurrence_of(X111,tptp0) ))),
% 15.16/2.52 inference(negated_conjecture,[status(cth)],[f49])).
% 15.16/2.52 fof(f58,plain,(
% 15.16/2.52 ![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)),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 15.16/2.52 fof(f59,plain,(
% 15.16/2.52 ![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)),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f58])).
% 15.16/2.52 fof(f60,plain,(
% 15.16/2.52 ![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)),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f59])).
% 15.16/2.52 fof(f61,plain,(
% 15.16/2.52 ![X12,X13]: (~occurrence_of(X13,X12)|(activity(X12)&activity_occurrence(X13)))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 15.16/2.52 fof(f63,plain,(
% 15.16/2.52 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f61])).
% 15.16/2.52 fof(f71,plain,(
% 15.16/2.52 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 15.16/2.52 fof(f72,plain,(
% 15.16/2.52 ![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))))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f71])).
% 15.16/2.52 fof(f73,plain,(
% 15.16/2.52 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f72])).
% 15.16/2.52 fof(f74,plain,(
% 15.16/2.52 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f72])).
% 15.16/2.52 fof(f75,plain,(
% 15.16/2.52 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK2_skl(X1,X0,X2)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f72])).
% 15.16/2.52 fof(f76,plain,(
% 15.16/2.52 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(?[X27]: (occurrence_of(X27,X26)&leaf_occ(X25,X27))))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 15.16/2.52 fof(f77,plain,(
% 15.16/2.52 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(occurrence_of(sK3_skl(X26,X25),X26)&leaf_occ(X25,sK3_skl(X26,X25))))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X27,sK3_skl(X26,X25))],[f76])).
% 15.16/2.52 fof(f78,plain,(
% 15.16/2.52 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|occurrence_of(sK3_skl(X1,X0),X1))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f77])).
% 15.16/2.52 fof(f79,plain,(
% 15.16/2.52 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|leaf_occ(X0,sK3_skl(X1,X0)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f77])).
% 15.16/2.52 fof(f80,plain,(
% 15.16/2.52 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 15.16/2.52 fof(f81,plain,(
% 15.16/2.52 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f80])).
% 15.16/2.52 fof(f82,plain,(
% 15.16/2.52 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f81])).
% 15.16/2.52 fof(f83,plain,(
% 15.16/2.52 ![X31,X32,X33]: ((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 15.16/2.52 fof(f84,plain,(
% 15.16/2.52 ![X32,X33]: ((![X31]: (~occurrence_of(X31,X33)|~leaf_occ(X32,X31)))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f83])).
% 15.16/2.52 fof(f85,plain,(
% 15.16/2.52 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f84])).
% 15.16/2.52 fof(f92,plain,(
% 15.16/2.52 ![X41]: (~activity_occurrence(X41)|(?[X42]: (activity(X42)&occurrence_of(X41,X42))))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 15.16/2.52 fof(f93,plain,(
% 15.16/2.52 ![X41]: (~activity_occurrence(X41)|(activity(sK4_skl(X41))&occurrence_of(X41,sK4_skl(X41))))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f92])).
% 15.16/2.52 fof(f95,plain,(
% 15.16/2.52 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK4_skl(X0)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f93])).
% 15.16/2.52 fof(f96,plain,(
% 15.16/2.52 ![X43]: (~legal(X43)|arboreal(X43))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 15.16/2.52 fof(f97,plain,(
% 15.16/2.52 ![X0]: (~legal(X0)|arboreal(X0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f96])).
% 15.16/2.52 fof(f113,plain,(
% 15.16/2.52 ![X51,X52]: (~occurrence_of(X51,X52)|(arboreal(X51)<=>atomic(X52)))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 15.16/2.52 fof(f114,plain,(
% 15.16/2.52 ![X51,X52]: (~occurrence_of(X51,X52)|((~arboreal(X51)|atomic(X52))&(arboreal(X51)|~atomic(X52))))),
% 15.16/2.52 inference(NNF_transformation,[status(thm)],[f113])).
% 15.16/2.52 fof(f116,plain,(
% 15.16/2.52 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f114])).
% 15.16/2.52 fof(f117,plain,(
% 15.16/2.52 ![X53,X54]: (~root(X53,X54)|legal(X53))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 15.16/2.52 fof(f118,plain,(
% 15.16/2.52 ![X53]: ((![X54]: ~root(X53,X54))|legal(X53))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f117])).
% 15.16/2.52 fof(f119,plain,(
% 15.16/2.52 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f118])).
% 15.16/2.52 fof(f120,plain,(
% 15.16/2.52 ![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)))))),
% 15.16/2.52 inference(NNF_transformation,[status(thm)],[f19])).
% 15.16/2.52 fof(f121,plain,(
% 15.16/2.52 (![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)))))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f120])).
% 15.16/2.52 fof(f122,plain,(
% 15.16/2.52 (![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)))))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f121])).
% 15.16/2.52 fof(f123,plain,(
% 15.16/2.52 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK8_skl(X1,X0)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f122])).
% 15.16/2.52 fof(f124,plain,(
% 15.16/2.52 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f122])).
% 15.16/2.52 fof(f125,plain,(
% 15.16/2.52 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK8_skl(X1,X0)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f122])).
% 15.16/2.52 fof(f127,plain,(
% 15.16/2.52 ![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)))))),
% 15.16/2.52 inference(NNF_transformation,[status(thm)],[f20])).
% 15.16/2.52 fof(f128,plain,(
% 15.16/2.52 (![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)))))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f127])).
% 15.16/2.52 fof(f129,plain,(
% 15.16/2.52 (![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)))))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f128])).
% 15.16/2.52 fof(f130,plain,(
% 15.16/2.52 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK9_skl(X1,X0)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f129])).
% 15.16/2.52 fof(f131,plain,(
% 15.16/2.52 ![X0,X1]: (~root_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f129])).
% 15.16/2.52 fof(f132,plain,(
% 15.16/2.52 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK9_skl(X1,X0)))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f129])).
% 15.16/2.52 fof(f133,plain,(
% 15.16/2.52 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f129])).
% 15.16/2.52 fof(f156,plain,(
% 15.16/2.52 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 15.16/2.52 fof(f157,plain,(
% 15.16/2.52 ![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))))))),
% 15.16/2.52 inference(NNF_transformation,[status(thm)],[f156])).
% 15.16/2.52 fof(f158,plain,(
% 15.16/2.52 (![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))))))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f157])).
% 15.16/2.52 fof(f159,plain,(
% 15.16/2.52 (![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)))))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f158])).
% 15.16/2.52 fof(f160,plain,(
% 15.16/2.52 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f159])).
% 15.16/2.52 fof(f161,plain,(
% 15.16/2.52 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f159])).
% 15.16/2.52 fof(f164,plain,(
% 15.16/2.52 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 15.16/2.52 fof(f165,plain,(
% 15.16/2.52 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f164])).
% 15.16/2.52 fof(f166,plain,(
% 15.16/2.52 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f165])).
% 15.16/2.52 fof(f170,plain,(
% 15.16/2.52 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 15.16/2.52 fof(f171,plain,(
% 15.16/2.52 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f170])).
% 15.16/2.52 fof(f172,plain,(
% 15.16/2.52 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f171])).
% 15.16/2.52 fof(f179,plain,(
% 15.16/2.52 ![X101]: (~occurrence_of(X101,tptp0)|(?[X102,X103]: ((((occurrence_of(X102,tptp4)&root_occ(X102,X101))&occurrence_of(X103,tptp3))&leaf_occ(X103,X101))&next_subocc(X102,X103,tptp0))))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 15.16/2.52 fof(f180,plain,(
% 15.16/2.52 ![X101]: (~occurrence_of(X101,tptp0)|((((occurrence_of(sK12_skl(X101),tptp4)&root_occ(sK12_skl(X101),X101))&occurrence_of(sK13_skl(X101),tptp3))&leaf_occ(sK13_skl(X101),X101))&next_subocc(sK12_skl(X101),sK13_skl(X101),tptp0)))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f179])).
% 15.16/2.52 fof(f182,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK12_skl(X0),X0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f180])).
% 15.16/2.52 fof(f183,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK13_skl(X0),tptp3))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f180])).
% 15.16/2.52 fof(f184,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK13_skl(X0),X0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f180])).
% 15.16/2.52 fof(f185,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f180])).
% 15.16/2.52 fof(f187,plain,(
% 15.16/2.52 ~atomic(tptp0)),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f35])).
% 15.16/2.52 fof(f191,plain,(
% 15.16/2.52 atomic(tptp1)),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f39])).
% 15.16/2.52 fof(f195,plain,(
% 15.16/2.52 ~tptp1=tptp3),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f43])).
% 15.16/2.52 fof(f202,plain,(
% 15.16/2.52 ![X108,X109]: ((((~occurrence_of(X109,tptp0)|~subactivity_occurrence(X108,X109))|~arboreal(X108))|leaf_occ(X108,X109))|(?[X110]: (occurrence_of(X110,tptp1)&next_subocc(X108,X110,tptp0))))),
% 15.16/2.52 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 15.16/2.52 fof(f203,plain,(
% 15.16/2.52 ![X108]: ((![X109]: (((~occurrence_of(X109,tptp0)|~subactivity_occurrence(X108,X109))|~arboreal(X108))|leaf_occ(X108,X109)))|(?[X110]: (occurrence_of(X110,tptp1)&next_subocc(X108,X110,tptp0))))),
% 15.16/2.52 inference(miniscoping,[status(thm)],[f202])).
% 15.16/2.52 fof(f204,plain,(
% 15.16/2.52 ![X108]: ((![X109]: (((~occurrence_of(X109,tptp0)|~subactivity_occurrence(X108,X109))|~arboreal(X108))|leaf_occ(X108,X109)))|(occurrence_of(sK14_skl(X108),tptp1)&next_subocc(X108,sK14_skl(X108),tptp0)))),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X110,sK14_skl(X108))],[f203])).
% 15.16/2.52 fof(f205,plain,(
% 15.16/2.52 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp1))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f204])).
% 15.16/2.52 fof(f206,plain,(
% 15.16/2.52 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f204])).
% 15.16/2.52 fof(f207,plain,(
% 15.16/2.52 occurrence_of(sK15_skl,tptp0)),
% 15.16/2.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X111,sK15_skl)],[f50])).
% 15.16/2.52 fof(f208,plain,(
% 15.16/2.52 occurrence_of(sK15_skl,tptp0)),
% 15.16/2.52 inference(cnf_transformation,[status(thm)],[f207])).
% 15.16/2.52 fof(f209,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(sK15_skl,X0)|X0=tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f82,f208])).
% 15.16/2.52 fof(f288,plain,(
% 15.16/2.52 root_occ(sK12_skl(sK15_skl),sK15_skl)),
% 15.16/2.52 inference(resolution,[status(thm)],[f182,f208])).
% 15.16/2.52 fof(f289,plain,(
% 15.16/2.52 root(sK12_skl(sK15_skl),sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f288,f132])).
% 15.16/2.52 fof(f290,plain,(
% 15.16/2.52 occurrence_of(sK15_skl,sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f288,f130])).
% 15.16/2.52 fof(f291,plain,(
% 15.16/2.52 subactivity_occurrence(sK12_skl(sK15_skl),sK15_skl)),
% 15.16/2.52 inference(resolution,[status(thm)],[f288,f131])).
% 15.16/2.52 fof(f299,plain,(
% 15.16/2.52 leaf_occ(sK13_skl(sK15_skl),sK15_skl)),
% 15.16/2.52 inference(resolution,[status(thm)],[f184,f208])).
% 15.16/2.52 fof(f301,plain,(
% 15.16/2.52 leaf(sK13_skl(sK15_skl),sK8_skl(sK15_skl,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f299,f125])).
% 15.16/2.52 fof(f302,plain,(
% 15.16/2.52 occurrence_of(sK15_skl,sK8_skl(sK15_skl,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f299,f123])).
% 15.16/2.52 fof(f314,plain,(
% 15.16/2.52 sK9_skl(sK15_skl,sK12_skl(sK15_skl))=tptp0),
% 15.16/2.52 inference(resolution,[status(thm)],[f290,f209])).
% 15.16/2.52 fof(f339,plain,(
% 15.16/2.52 root(sK12_skl(sK15_skl),tptp0)),
% 15.16/2.52 inference(forward_demodulation,[status(thm)],[f314,f289])).
% 15.16/2.52 fof(f342,plain,(
% 15.16/2.52 legal(sK12_skl(sK15_skl))),
% 15.16/2.52 inference(resolution,[status(thm)],[f339,f119])).
% 15.16/2.52 fof(f343,plain,(
% 15.16/2.52 arboreal(sK12_skl(sK15_skl))),
% 15.16/2.52 inference(resolution,[status(thm)],[f342,f97])).
% 15.16/2.52 fof(f344,plain,(
% 15.16/2.52 sK8_skl(sK15_skl,sK13_skl(sK15_skl))=tptp0),
% 15.16/2.52 inference(resolution,[status(thm)],[f302,f209])).
% 15.16/2.52 fof(f369,plain,(
% 15.16/2.52 leaf(sK13_skl(sK15_skl),tptp0)),
% 15.16/2.52 inference(forward_demodulation,[status(thm)],[f344,f301])).
% 15.16/2.52 fof(f370,plain,(
% 15.16/2.52 atomic(tptp0)|leaf_occ(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f369,f79])).
% 15.16/2.52 fof(f371,plain,(
% 15.16/2.52 atomic(tptp0)|occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f369,f78])).
% 15.16/2.52 fof(f372,plain,(
% 15.16/2.52 leaf_occ(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f370,f187])).
% 15.16/2.52 fof(f373,plain,(
% 15.16/2.52 occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f371,f187])).
% 15.16/2.52 fof(f460,plain,(
% 15.16/2.52 subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f372,f124])).
% 15.16/2.52 fof(f507,plain,(
% 15.16/2.52 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f185,f208])).
% 15.16/2.52 fof(f508,plain,(
% 15.16/2.52 min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f507,f160])).
% 15.16/2.52 fof(f516,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK12_skl(sK15_skl),X0))),
% 15.16/2.52 inference(resolution,[status(thm)],[f508,f85])).
% 15.16/2.52 fof(f645,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK13_skl(sK15_skl),X0)|subactivity_occurrence(sK12_skl(sK15_skl),X0))),
% 15.16/2.52 inference(resolution,[status(thm)],[f166,f508])).
% 15.16/2.52 fof(f766,plain,(
% 15.16/2.52 ~occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)|subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f645,f460])).
% 15.16/2.52 fof(f768,plain,(
% 15.16/2.52 subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f766,f373])).
% 15.16/2.52 fof(f869,plain,(
% 15.16/2.52 ![X0]: (~subactivity_occurrence(X0,sK15_skl)|~arboreal(X0)|leaf_occ(X0,sK15_skl)|occurrence_of(sK14_skl(X0),tptp1))),
% 15.16/2.52 inference(resolution,[status(thm)],[f205,f208])).
% 15.16/2.52 fof(f873,plain,(
% 15.16/2.52 ![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))),
% 15.16/2.52 inference(resolution,[status(thm)],[f206,f373])).
% 15.16/2.52 fof(f876,plain,(
% 15.16/2.52 ~arboreal(sK12_skl(sK15_skl))|leaf_occ(sK12_skl(sK15_skl),sK15_skl)|occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 15.16/2.52 inference(resolution,[status(thm)],[f869,f291])).
% 15.16/2.52 fof(f877,plain,(
% 15.16/2.52 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f876,f343])).
% 15.16/2.52 fof(f883,plain,(
% 15.16/2.52 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|arboreal(sK14_skl(sK12_skl(sK15_skl)))|~atomic(tptp1)),
% 15.16/2.52 inference(resolution,[status(thm)],[f877,f116])).
% 15.16/2.52 fof(f887,plain,(
% 15.16/2.52 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f877,f63])).
% 15.16/2.52 fof(f893,plain,(
% 15.16/2.52 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f883,f191])).
% 15.16/2.52 fof(f905,plain,(
% 15.16/2.52 arboreal(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f893,f516])).
% 15.16/2.52 fof(f912,plain,(
% 15.16/2.52 arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f905,f208])).
% 15.16/2.52 fof(f913,plain,(
% 15.16/2.52 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f887,f516])).
% 15.16/2.52 fof(f920,plain,(
% 15.16/2.52 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f913,f208])).
% 15.16/2.52 fof(f921,plain,(
% 15.16/2.52 occurrence_of(sK14_skl(sK12_skl(sK15_skl)),sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 15.16/2.52 inference(resolution,[status(thm)],[f920,f95])).
% 15.16/2.52 fof(f936,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(sK14_skl(sK12_skl(sK15_skl)),X0)|X0=sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 15.16/2.52 inference(resolution,[status(thm)],[f921,f82])).
% 15.16/2.52 fof(f944,plain,(
% 15.16/2.52 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|leaf_occ(sK12_skl(sK15_skl),sK15_skl)),
% 15.16/2.52 inference(resolution,[status(thm)],[f936,f877])).
% 15.16/2.52 fof(f945,plain,(
% 15.16/2.52 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f944,f516])).
% 15.16/2.52 fof(f952,plain,(
% 15.16/2.52 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f945,f208])).
% 15.16/2.52 fof(f2518,plain,(
% 15.16/2.52 ~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)),
% 15.16/2.52 inference(resolution,[status(thm)],[f873,f768])).
% 15.16/2.52 fof(f2519,plain,(
% 15.16/2.52 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)),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f2518,f343])).
% 15.16/2.52 fof(f2586,plain,(
% 15.16/2.52 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)|~occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2519,f516])).
% 15.16/2.52 fof(f2593,plain,(
% 15.16/2.52 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 15.16/2.52 inference(forward_subsumption_resolution,[status(thm)],[f2586,f373])).
% 15.16/2.52 fof(f2595,plain,(
% 15.16/2.52 min_precedes(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2593,f160])).
% 15.16/2.52 fof(f2604,plain,(
% 15.16/2.52 ![X0]: (~next_subocc(sK12_skl(sK15_skl),X0,tptp0)|~min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2595,f161])).
% 15.16/2.52 fof(f2610,plain,(
% 15.16/2.52 subactivity_occurrence(sK14_skl(sK12_skl(sK15_skl)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2595,f75])).
% 15.16/2.52 fof(f2611,plain,(
% 15.16/2.52 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2595,f74])).
% 15.16/2.52 fof(f2612,plain,(
% 15.16/2.52 occurrence_of(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0),tptp0)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2595,f73])).
% 15.16/2.52 fof(f2632,plain,(
% 15.16/2.52 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)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f185])).
% 15.16/2.52 fof(f2633,plain,(
% 15.16/2.52 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp3)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f183])).
% 15.16/2.52 fof(f2635,plain,(
% 15.16/2.52 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))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f184])).
% 15.16/2.52 fof(f2636,plain,(
% 15.16/2.52 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))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f182])).
% 15.16/2.52 fof(f2638,plain,(
% 15.16/2.52 ![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))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f133])).
% 15.16/2.52 fof(f2640,plain,(
% 15.16/2.52 ![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)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f172])).
% 15.16/2.52 fof(f2645,plain,(
% 15.16/2.52 ![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)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2612,f60])).
% 15.16/2.52 fof(f2732,plain,(
% 15.16/2.52 activity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2633,f63])).
% 15.16/2.52 fof(f2736,plain,(
% 15.16/2.52 ![X0]: (~occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),X0)|X0=tptp3)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2633,f82])).
% 15.16/2.52 fof(f2739,plain,(
% 15.16/2.52 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))))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2732,f95])).
% 15.16/2.52 fof(f3634,plain,(
% 15.16/2.52 ![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)))),
% 15.16/2.52 inference(resolution,[status(thm)],[f2640,f2636])).
% 15.16/2.52 fof(f3636,plain,(
% 15.16/2.52 sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))=tptp3),
% 15.16/2.52 inference(resolution,[status(thm)],[f2739,f2736])).
% 15.16/2.52 fof(f3958,plain,(
% 15.16/2.52 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)),
% 15.16/2.52 inference(resolution,[status(thm)],[f2638,f2611])).
% 15.16/2.52 fof(f3961,plain,(
% 15.16/2.52 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 15.16/2.54 inference(forward_subsumption_resolution,[status(thm)],[f3958,f339])).
% 15.16/2.54 fof(f3962,plain,(
% 15.16/2.54 sK12_skl(sK15_skl)=sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 15.16/2.54 inference(resolution,[status(thm)],[f3961,f3634])).
% 15.16/2.54 fof(f3979,plain,(
% 15.16/2.54 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 15.16/2.54 inference(backward_demodulation,[status(thm)],[f3962,f2632])).
% 15.16/2.54 fof(f7976,plain,(
% 15.16/2.54 ![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)))),
% 15.16/2.54 inference(resolution,[status(thm)],[f2645,f2610])).
% 15.16/2.54 fof(f7980,plain,(
% 15.16/2.54 ![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)))),
% 15.16/2.54 inference(forward_subsumption_resolution,[status(thm)],[f7976,f912])).
% 15.16/2.54 fof(f7989,plain,(
% 15.16/2.54 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))),
% 15.16/2.54 inference(resolution,[status(thm)],[f7980,f2635])).
% 15.16/2.54 fof(f8741,plain,(
% 15.16/2.54 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)),
% 15.16/2.54 inference(resolution,[status(thm)],[f7989,f2604])).
% 15.16/2.54 fof(f8760,plain,(
% 15.16/2.54 sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))),
% 15.16/2.54 inference(forward_subsumption_resolution,[status(thm)],[f8741,f3979])).
% 15.16/2.54 fof(f8861,plain,(
% 15.16/2.54 sK4_skl(sK14_skl(sK12_skl(sK15_skl)))=tptp3),
% 15.16/2.54 inference(backward_demodulation,[status(thm)],[f8760,f3636])).
% 15.16/2.54 fof(f8899,plain,(
% 15.16/2.54 tptp1=tptp3),
% 15.16/2.54 inference(forward_demodulation,[status(thm)],[f952,f8861])).
% 15.16/2.54 fof(f8900,plain,(
% 15.16/2.54 $false),
% 15.16/2.54 inference(forward_subsumption_resolution,[status(thm)],[f8899,f195])).
% 15.16/2.54 % SZS output end CNFRefutation for theBenchmark.p
% 15.16/2.57 % Elapsed time: 1.985277 seconds
% 15.16/2.57 % CPU time: 15.481214 seconds
% 15.16/2.57 % Total memory used: 236.536 MB
% 15.16/2.57 % Net memory used: 226.370 MB
%------------------------------------------------------------------------------