%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO006+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 : n007.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:23 PM UTC 2026
% Result : Theorem 50.16s 6.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO006+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.07/0.33 % Computer : n007.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Mon Sep 21 03:39:20 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 % Drodi V4.1.1
% 50.16/6.94 % Refutation found
% 50.16/6.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 50.16/6.94 % SZS output start CNFRefutation for theBenchmark
% 50.16/6.94 fof(f3,axiom,(
% 50.16/6.94 (! [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 ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f4,axiom,(
% 50.16/6.94 (! [X12,X13] :( occurrence_of(X13,X12)=> ( activity(X12)& activity_occurrence(X13) ) ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f7,axiom,(
% 50.16/6.94 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f8,axiom,(
% 50.16/6.94 (! [X25,X26] :( ( leaf(X25,X26)& ~ atomic(X26) )=> (? [X27] :( occurrence_of(X27,X26)& leaf_occ(X25,X27) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f9,axiom,(
% 50.16/6.94 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f10,axiom,(
% 50.16/6.94 (! [X31,X32,X33] :( ( occurrence_of(X31,X33)& leaf_occ(X32,X31) )=> ~ (? [X34] : min_precedes(X32,X34,X33) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f13,axiom,(
% 50.16/6.94 (! [X41] :( activity_occurrence(X41)=> (? [X42] :( activity(X42)& occurrence_of(X41,X42) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f14,axiom,(
% 50.16/6.94 (! [X43] :( legal(X43)=> arboreal(X43) ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f17,axiom,(
% 50.16/6.94 (! [X51,X52] :( occurrence_of(X51,X52)=> ( arboreal(X51)<=> atomic(X52) ) ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f18,axiom,(
% 50.16/6.94 (! [X53,X54] :( root(X53,X54)=> legal(X53) ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f19,axiom,(
% 50.16/6.94 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f20,axiom,(
% 50.16/6.94 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f27,axiom,(
% 50.16/6.94 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f28,axiom,(
% 50.16/6.94 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f30,axiom,(
% 50.16/6.94 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f33,axiom,(
% 50.16/6.94 (! [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) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f35,axiom,(
% 50.16/6.94 ~ atomic(tptp0) ),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f39,axiom,(
% 50.16/6.94 atomic(tptp1) ),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f43,axiom,(
% 50.16/6.94 tptp1 != tptp3 ),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f46,axiom,(
% 50.16/6.94 (! [X104,X105] :( ( occurrence_of(X105,tptp0)& subactivity_occurrence(X104,X105)& arboreal(X104)& ~ leaf_occ(X104,X105) )=> (? [X106] :( occurrence_of(X106,tptp1)& next_subocc(X104,X106,tptp0) ) )) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f47,conjecture,(
% 50.16/6.94 ~ (? [X107] : occurrence_of(X107,tptp0) )),
% 50.16/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 50.16/6.94 fof(f48,negated_conjecture,(
% 50.16/6.94 ~(~ (? [X107] : occurrence_of(X107,tptp0) ))),
% 50.16/6.94 inference(negated_conjecture,[status(cth)],[f47])).
% 50.16/6.94 fof(f56,plain,(
% 50.16/6.94 ![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)),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 50.16/6.94 fof(f57,plain,(
% 50.16/6.94 ![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)),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f56])).
% 50.16/6.94 fof(f58,plain,(
% 50.16/6.94 ![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)),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f57])).
% 50.16/6.94 fof(f59,plain,(
% 50.16/6.94 ![X12,X13]: (~occurrence_of(X13,X12)|(activity(X12)&activity_occurrence(X13)))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 50.16/6.94 fof(f61,plain,(
% 50.16/6.94 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f59])).
% 50.16/6.94 fof(f69,plain,(
% 50.16/6.94 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 50.16/6.94 fof(f70,plain,(
% 50.16/6.94 ![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))))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f69])).
% 50.16/6.94 fof(f71,plain,(
% 50.16/6.94 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f70])).
% 50.16/6.94 fof(f72,plain,(
% 50.16/6.94 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f70])).
% 50.16/6.94 fof(f73,plain,(
% 50.16/6.94 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK2_skl(X1,X0,X2)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f70])).
% 50.16/6.94 fof(f74,plain,(
% 50.16/6.94 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(?[X27]: (occurrence_of(X27,X26)&leaf_occ(X25,X27))))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 50.16/6.94 fof(f75,plain,(
% 50.16/6.94 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(occurrence_of(sK3_skl(X26,X25),X26)&leaf_occ(X25,sK3_skl(X26,X25))))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X27,sK3_skl(X26,X25))],[f74])).
% 50.16/6.94 fof(f76,plain,(
% 50.16/6.94 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|occurrence_of(sK3_skl(X1,X0),X1))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f75])).
% 50.16/6.94 fof(f77,plain,(
% 50.16/6.94 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|leaf_occ(X0,sK3_skl(X1,X0)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f75])).
% 50.16/6.94 fof(f78,plain,(
% 50.16/6.94 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 50.16/6.94 fof(f79,plain,(
% 50.16/6.94 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f78])).
% 50.16/6.94 fof(f80,plain,(
% 50.16/6.94 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f79])).
% 50.16/6.94 fof(f81,plain,(
% 50.16/6.94 ![X31,X32,X33]: ((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 50.16/6.94 fof(f82,plain,(
% 50.16/6.94 ![X32,X33]: ((![X31]: (~occurrence_of(X31,X33)|~leaf_occ(X32,X31)))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f81])).
% 50.16/6.94 fof(f83,plain,(
% 50.16/6.94 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f82])).
% 50.16/6.94 fof(f90,plain,(
% 50.16/6.94 ![X41]: (~activity_occurrence(X41)|(?[X42]: (activity(X42)&occurrence_of(X41,X42))))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 50.16/6.94 fof(f91,plain,(
% 50.16/6.94 ![X41]: (~activity_occurrence(X41)|(activity(sK4_skl(X41))&occurrence_of(X41,sK4_skl(X41))))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f90])).
% 50.16/6.94 fof(f93,plain,(
% 50.16/6.94 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK4_skl(X0)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f91])).
% 50.16/6.94 fof(f94,plain,(
% 50.16/6.94 ![X43]: (~legal(X43)|arboreal(X43))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 50.16/6.94 fof(f95,plain,(
% 50.16/6.94 ![X0]: (~legal(X0)|arboreal(X0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f94])).
% 50.16/6.94 fof(f111,plain,(
% 50.16/6.94 ![X51,X52]: (~occurrence_of(X51,X52)|(arboreal(X51)<=>atomic(X52)))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 50.16/6.94 fof(f112,plain,(
% 50.16/6.94 ![X51,X52]: (~occurrence_of(X51,X52)|((~arboreal(X51)|atomic(X52))&(arboreal(X51)|~atomic(X52))))),
% 50.16/6.94 inference(NNF_transformation,[status(thm)],[f111])).
% 50.16/6.94 fof(f114,plain,(
% 50.16/6.94 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f112])).
% 50.16/6.94 fof(f115,plain,(
% 50.16/6.94 ![X53,X54]: (~root(X53,X54)|legal(X53))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 50.16/6.94 fof(f116,plain,(
% 50.16/6.94 ![X53]: ((![X54]: ~root(X53,X54))|legal(X53))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f115])).
% 50.16/6.94 fof(f117,plain,(
% 50.16/6.94 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f116])).
% 50.16/6.94 fof(f118,plain,(
% 50.16/6.94 ![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)))))),
% 50.16/6.94 inference(NNF_transformation,[status(thm)],[f19])).
% 50.16/6.94 fof(f119,plain,(
% 50.16/6.94 (![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)))))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f118])).
% 50.16/6.94 fof(f120,plain,(
% 50.16/6.94 (![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)))))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f119])).
% 50.16/6.94 fof(f121,plain,(
% 50.16/6.94 ![X0,X1]: (~leaf_occ(X0,X1)|occurrence_of(X1,sK8_skl(X1,X0)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f120])).
% 50.16/6.94 fof(f122,plain,(
% 50.16/6.94 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f120])).
% 50.16/6.94 fof(f123,plain,(
% 50.16/6.94 ![X0,X1]: (~leaf_occ(X0,X1)|leaf(X0,sK8_skl(X1,X0)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f120])).
% 50.16/6.94 fof(f125,plain,(
% 50.16/6.94 ![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)))))),
% 50.16/6.94 inference(NNF_transformation,[status(thm)],[f20])).
% 50.16/6.94 fof(f126,plain,(
% 50.16/6.94 (![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)))))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f125])).
% 50.16/6.94 fof(f127,plain,(
% 50.16/6.94 (![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)))))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f126])).
% 50.16/6.94 fof(f128,plain,(
% 50.16/6.94 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK9_skl(X1,X0)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f127])).
% 50.16/6.94 fof(f129,plain,(
% 50.16/6.94 ![X0,X1]: (~root_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f127])).
% 50.16/6.94 fof(f130,plain,(
% 50.16/6.94 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK9_skl(X1,X0)))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f127])).
% 50.16/6.94 fof(f131,plain,(
% 50.16/6.94 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f127])).
% 50.16/6.94 fof(f154,plain,(
% 50.16/6.94 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 50.16/6.94 fof(f155,plain,(
% 50.16/6.94 ![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))))))),
% 50.16/6.94 inference(NNF_transformation,[status(thm)],[f154])).
% 50.16/6.94 fof(f156,plain,(
% 50.16/6.94 (![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))))))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f155])).
% 50.16/6.94 fof(f157,plain,(
% 50.16/6.94 (![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)))))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f156])).
% 50.16/6.94 fof(f158,plain,(
% 50.16/6.94 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f157])).
% 50.16/6.94 fof(f159,plain,(
% 50.16/6.94 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f157])).
% 50.16/6.94 fof(f162,plain,(
% 50.16/6.94 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 50.16/6.94 fof(f163,plain,(
% 50.16/6.94 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f162])).
% 50.16/6.94 fof(f164,plain,(
% 50.16/6.94 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f163])).
% 50.16/6.94 fof(f168,plain,(
% 50.16/6.94 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 50.16/6.94 fof(f169,plain,(
% 50.16/6.94 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f168])).
% 50.16/6.94 fof(f170,plain,(
% 50.16/6.94 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f169])).
% 50.16/6.94 fof(f177,plain,(
% 50.16/6.94 ![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))))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 50.16/6.94 fof(f178,plain,(
% 50.16/6.94 ![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)))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f177])).
% 50.16/6.94 fof(f180,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK12_skl(X0),X0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f178])).
% 50.16/6.94 fof(f181,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK13_skl(X0),tptp3))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f178])).
% 50.16/6.94 fof(f182,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK13_skl(X0),X0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f178])).
% 50.16/6.94 fof(f183,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f178])).
% 50.16/6.94 fof(f185,plain,(
% 50.16/6.94 ~atomic(tptp0)),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f35])).
% 50.16/6.94 fof(f189,plain,(
% 50.16/6.94 atomic(tptp1)),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f39])).
% 50.16/6.94 fof(f193,plain,(
% 50.16/6.94 ~tptp1=tptp3),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f43])).
% 50.16/6.94 fof(f196,plain,(
% 50.16/6.94 ![X104,X105]: ((((~occurrence_of(X105,tptp0)|~subactivity_occurrence(X104,X105))|~arboreal(X104))|leaf_occ(X104,X105))|(?[X106]: (occurrence_of(X106,tptp1)&next_subocc(X104,X106,tptp0))))),
% 50.16/6.94 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 50.16/6.94 fof(f197,plain,(
% 50.16/6.94 ![X104]: ((![X105]: (((~occurrence_of(X105,tptp0)|~subactivity_occurrence(X104,X105))|~arboreal(X104))|leaf_occ(X104,X105)))|(?[X106]: (occurrence_of(X106,tptp1)&next_subocc(X104,X106,tptp0))))),
% 50.16/6.94 inference(miniscoping,[status(thm)],[f196])).
% 50.16/6.94 fof(f198,plain,(
% 50.16/6.94 ![X104]: ((![X105]: (((~occurrence_of(X105,tptp0)|~subactivity_occurrence(X104,X105))|~arboreal(X104))|leaf_occ(X104,X105)))|(occurrence_of(sK14_skl(X104),tptp1)&next_subocc(X104,sK14_skl(X104),tptp0)))),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X106,sK14_skl(X104))],[f197])).
% 50.16/6.94 fof(f199,plain,(
% 50.16/6.94 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp1))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f198])).
% 50.16/6.94 fof(f200,plain,(
% 50.16/6.94 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f198])).
% 50.16/6.94 fof(f201,plain,(
% 50.16/6.94 occurrence_of(sK15_skl,tptp0)),
% 50.16/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X107,sK15_skl)],[f48])).
% 50.16/6.94 fof(f202,plain,(
% 50.16/6.94 occurrence_of(sK15_skl,tptp0)),
% 50.16/6.94 inference(cnf_transformation,[status(thm)],[f201])).
% 50.16/6.94 fof(f203,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(sK15_skl,X0)|X0=tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f80,f202])).
% 50.16/6.94 fof(f282,plain,(
% 50.16/6.94 root_occ(sK12_skl(sK15_skl),sK15_skl)),
% 50.16/6.94 inference(resolution,[status(thm)],[f180,f202])).
% 50.16/6.94 fof(f283,plain,(
% 50.16/6.94 root(sK12_skl(sK15_skl),sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f282,f130])).
% 50.16/6.94 fof(f284,plain,(
% 50.16/6.94 occurrence_of(sK15_skl,sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f282,f128])).
% 50.16/6.94 fof(f285,plain,(
% 50.16/6.94 subactivity_occurrence(sK12_skl(sK15_skl),sK15_skl)),
% 50.16/6.94 inference(resolution,[status(thm)],[f282,f129])).
% 50.16/6.94 fof(f293,plain,(
% 50.16/6.94 leaf_occ(sK13_skl(sK15_skl),sK15_skl)),
% 50.16/6.94 inference(resolution,[status(thm)],[f182,f202])).
% 50.16/6.94 fof(f295,plain,(
% 50.16/6.94 leaf(sK13_skl(sK15_skl),sK8_skl(sK15_skl,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f293,f123])).
% 50.16/6.94 fof(f296,plain,(
% 50.16/6.94 occurrence_of(sK15_skl,sK8_skl(sK15_skl,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f293,f121])).
% 50.16/6.94 fof(f308,plain,(
% 50.16/6.94 sK9_skl(sK15_skl,sK12_skl(sK15_skl))=tptp0),
% 50.16/6.94 inference(resolution,[status(thm)],[f284,f203])).
% 50.16/6.94 fof(f333,plain,(
% 50.16/6.94 root(sK12_skl(sK15_skl),tptp0)),
% 50.16/6.94 inference(forward_demodulation,[status(thm)],[f308,f283])).
% 50.16/6.94 fof(f336,plain,(
% 50.16/6.94 legal(sK12_skl(sK15_skl))),
% 50.16/6.94 inference(resolution,[status(thm)],[f333,f117])).
% 50.16/6.94 fof(f337,plain,(
% 50.16/6.94 arboreal(sK12_skl(sK15_skl))),
% 50.16/6.94 inference(resolution,[status(thm)],[f336,f95])).
% 50.16/6.94 fof(f338,plain,(
% 50.16/6.94 sK8_skl(sK15_skl,sK13_skl(sK15_skl))=tptp0),
% 50.16/6.94 inference(resolution,[status(thm)],[f296,f203])).
% 50.16/6.94 fof(f363,plain,(
% 50.16/6.94 leaf(sK13_skl(sK15_skl),tptp0)),
% 50.16/6.94 inference(forward_demodulation,[status(thm)],[f338,f295])).
% 50.16/6.94 fof(f364,plain,(
% 50.16/6.94 atomic(tptp0)|leaf_occ(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f363,f77])).
% 50.16/6.94 fof(f365,plain,(
% 50.16/6.94 atomic(tptp0)|occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f363,f76])).
% 50.16/6.94 fof(f366,plain,(
% 50.16/6.94 leaf_occ(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f364,f185])).
% 50.16/6.94 fof(f367,plain,(
% 50.16/6.94 occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f365,f185])).
% 50.16/6.94 fof(f454,plain,(
% 50.16/6.94 subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f366,f122])).
% 50.16/6.94 fof(f501,plain,(
% 50.16/6.94 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f183,f202])).
% 50.16/6.94 fof(f502,plain,(
% 50.16/6.94 min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f501,f158])).
% 50.16/6.94 fof(f510,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK12_skl(sK15_skl),X0))),
% 50.16/6.94 inference(resolution,[status(thm)],[f502,f83])).
% 50.16/6.94 fof(f639,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK13_skl(sK15_skl),X0)|subactivity_occurrence(sK12_skl(sK15_skl),X0))),
% 50.16/6.94 inference(resolution,[status(thm)],[f164,f502])).
% 50.16/6.94 fof(f734,plain,(
% 50.16/6.94 ![X0]: (~subactivity_occurrence(X0,sK15_skl)|~arboreal(X0)|leaf_occ(X0,sK15_skl)|occurrence_of(sK14_skl(X0),tptp1))),
% 50.16/6.94 inference(resolution,[status(thm)],[f199,f202])).
% 50.16/6.94 fof(f736,plain,(
% 50.16/6.94 ![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))),
% 50.16/6.94 inference(resolution,[status(thm)],[f200,f367])).
% 50.16/6.94 fof(f759,plain,(
% 50.16/6.94 ~arboreal(sK12_skl(sK15_skl))|leaf_occ(sK12_skl(sK15_skl),sK15_skl)|occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 50.16/6.94 inference(resolution,[status(thm)],[f734,f285])).
% 50.16/6.94 fof(f760,plain,(
% 50.16/6.94 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f759,f337])).
% 50.16/6.94 fof(f767,plain,(
% 50.16/6.94 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|arboreal(sK14_skl(sK12_skl(sK15_skl)))|~atomic(tptp1)),
% 50.16/6.94 inference(resolution,[status(thm)],[f760,f114])).
% 50.16/6.94 fof(f771,plain,(
% 50.16/6.94 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f760,f61])).
% 50.16/6.94 fof(f777,plain,(
% 50.16/6.94 leaf_occ(sK12_skl(sK15_skl),sK15_skl)|arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f767,f189])).
% 50.16/6.94 fof(f785,plain,(
% 50.16/6.94 arboreal(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f777,f510])).
% 50.16/6.94 fof(f791,plain,(
% 50.16/6.94 arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f785,f202])).
% 50.16/6.94 fof(f795,plain,(
% 50.16/6.94 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f771,f510])).
% 50.16/6.94 fof(f801,plain,(
% 50.16/6.94 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f795,f202])).
% 50.16/6.94 fof(f802,plain,(
% 50.16/6.94 occurrence_of(sK14_skl(sK12_skl(sK15_skl)),sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 50.16/6.94 inference(resolution,[status(thm)],[f801,f93])).
% 50.16/6.94 fof(f817,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(sK14_skl(sK12_skl(sK15_skl)),X0)|X0=sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 50.16/6.94 inference(resolution,[status(thm)],[f802,f80])).
% 50.16/6.94 fof(f820,plain,(
% 50.16/6.94 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|leaf_occ(sK12_skl(sK15_skl),sK15_skl)),
% 50.16/6.94 inference(resolution,[status(thm)],[f817,f760])).
% 50.16/6.94 fof(f821,plain,(
% 50.16/6.94 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))|~occurrence_of(sK15_skl,tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f820,f510])).
% 50.16/6.94 fof(f827,plain,(
% 50.16/6.94 tptp1=sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f821,f202])).
% 50.16/6.94 fof(f853,plain,(
% 50.16/6.94 ~occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)|subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f639,f454])).
% 50.16/6.94 fof(f855,plain,(
% 50.16/6.94 subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK13_skl(sK15_skl)))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f853,f367])).
% 50.16/6.94 fof(f2216,plain,(
% 50.16/6.94 ~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)),
% 50.16/6.94 inference(resolution,[status(thm)],[f736,f855])).
% 50.16/6.94 fof(f2217,plain,(
% 50.16/6.94 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)),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f2216,f337])).
% 50.16/6.94 fof(f2218,plain,(
% 50.16/6.94 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)|~occurrence_of(sK3_skl(tptp0,sK13_skl(sK15_skl)),tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2217,f510])).
% 50.16/6.94 fof(f2225,plain,(
% 50.16/6.94 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f2218,f367])).
% 50.16/6.94 fof(f2227,plain,(
% 50.16/6.94 min_precedes(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2225,f158])).
% 50.16/6.94 fof(f2236,plain,(
% 50.16/6.94 ![X0]: (~next_subocc(sK12_skl(sK15_skl),X0,tptp0)|~min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2227,f159])).
% 50.16/6.94 fof(f2242,plain,(
% 50.16/6.94 subactivity_occurrence(sK14_skl(sK12_skl(sK15_skl)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2227,f73])).
% 50.16/6.94 fof(f2243,plain,(
% 50.16/6.94 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2227,f72])).
% 50.16/6.94 fof(f2244,plain,(
% 50.16/6.94 occurrence_of(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0),tptp0)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2227,f71])).
% 50.16/6.94 fof(f2263,plain,(
% 50.16/6.94 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)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f183])).
% 50.16/6.94 fof(f2264,plain,(
% 50.16/6.94 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp3)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f181])).
% 50.16/6.94 fof(f2266,plain,(
% 50.16/6.94 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))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f182])).
% 50.16/6.94 fof(f2267,plain,(
% 50.16/6.94 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))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f180])).
% 50.16/6.94 fof(f2269,plain,(
% 50.16/6.94 ![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))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f131])).
% 50.16/6.94 fof(f2271,plain,(
% 50.16/6.94 ![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)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f170])).
% 50.16/6.94 fof(f2276,plain,(
% 50.16/6.94 ![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)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2244,f58])).
% 50.16/6.94 fof(f2323,plain,(
% 50.16/6.94 activity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2264,f61])).
% 50.16/6.94 fof(f2327,plain,(
% 50.16/6.94 ![X0]: (~occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),X0)|X0=tptp3)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2264,f80])).
% 50.16/6.94 fof(f2330,plain,(
% 50.16/6.94 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))))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2323,f93])).
% 50.16/6.94 fof(f3558,plain,(
% 50.16/6.94 ![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)))),
% 50.16/6.94 inference(resolution,[status(thm)],[f2271,f2267])).
% 50.16/6.94 fof(f3560,plain,(
% 50.16/6.94 sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))=tptp3),
% 50.16/6.94 inference(resolution,[status(thm)],[f2330,f2327])).
% 50.16/6.94 fof(f3894,plain,(
% 50.16/6.94 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)),
% 50.16/6.94 inference(resolution,[status(thm)],[f2269,f2243])).
% 50.16/6.94 fof(f3897,plain,(
% 50.16/6.94 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 50.16/6.94 inference(forward_subsumption_resolution,[status(thm)],[f3894,f333])).
% 51.84/6.97 fof(f3906,plain,(
% 51.84/6.97 sK12_skl(sK15_skl)=sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 51.84/6.97 inference(resolution,[status(thm)],[f3897,f3558])).
% 51.84/6.97 fof(f3921,plain,(
% 51.84/6.97 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 51.84/6.97 inference(backward_demodulation,[status(thm)],[f3906,f2263])).
% 51.84/6.97 fof(f8701,plain,(
% 51.84/6.97 ![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)))),
% 51.84/6.97 inference(resolution,[status(thm)],[f2276,f2242])).
% 51.84/6.97 fof(f8705,plain,(
% 51.84/6.97 ![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)))),
% 51.84/6.97 inference(forward_subsumption_resolution,[status(thm)],[f8701,f791])).
% 51.84/6.97 fof(f8714,plain,(
% 51.84/6.97 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))),
% 51.84/6.97 inference(resolution,[status(thm)],[f8705,f2266])).
% 51.84/6.97 fof(f11552,plain,(
% 51.84/6.97 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)),
% 51.84/6.97 inference(resolution,[status(thm)],[f8714,f2236])).
% 51.84/6.97 fof(f11571,plain,(
% 51.84/6.97 sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))),
% 51.84/6.97 inference(forward_subsumption_resolution,[status(thm)],[f11552,f3921])).
% 51.84/6.97 fof(f11672,plain,(
% 51.84/6.97 sK4_skl(sK14_skl(sK12_skl(sK15_skl)))=tptp3),
% 51.84/6.97 inference(backward_demodulation,[status(thm)],[f11571,f3560])).
% 51.84/6.97 fof(f11710,plain,(
% 51.84/6.97 tptp1=tptp3),
% 51.84/6.97 inference(forward_demodulation,[status(thm)],[f827,f11672])).
% 51.84/6.97 fof(f11711,plain,(
% 51.84/6.97 $false),
% 51.84/6.97 inference(forward_subsumption_resolution,[status(thm)],[f11710,f193])).
% 51.84/6.97 % SZS output end CNFRefutation for theBenchmark.p
% 36.86/7.04 % Elapsed time: 6.685025 seconds
% 36.86/7.04 % CPU time: 52.546857 seconds
% 36.86/7.04 % Total memory used: 400.937 MB
% 36.86/7.04 % Net memory used: 377.502 MB
%------------------------------------------------------------------------------