%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO002+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 : n003.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:21 PM UTC 2026
% Result : Theorem 12.72s 7.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO002+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.36 % Computer : n003.cluster.edu
% 0.11/5.36 % Model : x86_64 x86_64
% 0.11/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.36 % Memory : 8046.5625MB
% 0.11/5.36 % OS : Linux 6.8.0-71-generic
% 0.11/5.36 % CPULimit : 300
% 0.11/5.36 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 03:42:20 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.38 % Drodi V4.1.1
% 12.72/7.25 % Refutation found
% 12.72/7.25 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.72/7.25 % SZS output start CNFRefutation for theBenchmark
% 12.72/7.25 fof(f1,axiom,(
% 12.72/7.25 (! [X0,X1] :( ( occurrence_of(X1,X0)& ~ atomic(X0) )=> (? [X2] :( root(X2,X0)& subactivity_occurrence(X2,X1) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f3,axiom,(
% 12.72/7.25 (! [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 ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f7,axiom,(
% 12.72/7.25 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f9,axiom,(
% 12.72/7.25 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f12,axiom,(
% 12.72/7.25 (! [X39,X40] :( subactivity_occurrence(X39,X40)=> ( activity_occurrence(X39)& activity_occurrence(X40) ) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f13,axiom,(
% 12.72/7.25 (! [X41] :( activity_occurrence(X41)=> (? [X42] :( activity(X42)& occurrence_of(X41,X42) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f14,axiom,(
% 12.72/7.25 (! [X43] :( legal(X43)=> arboreal(X43) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f18,axiom,(
% 12.72/7.25 (! [X53,X54] :( root(X53,X54)=> legal(X53) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f19,axiom,(
% 12.72/7.25 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f20,axiom,(
% 12.72/7.25 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f27,axiom,(
% 12.72/7.25 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f30,axiom,(
% 12.72/7.25 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f33,axiom,(
% 12.72/7.25 (! [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) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f47,axiom,(
% 12.72/7.25 (! [X109,X110,X111,X112,X113] :( send_message(X109,X110,X111,X112,X113)=> ( X109 != tptp4& X109 != tptp3& X109 != tptp2 ) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f48,axiom,(
% 12.72/7.25 (! [X114,X115,X116,X117,X118,X119] :( ( send_message(X114,X115,X116,X117,X118)& occurrence_of(X119,X114) )=> min_precedes(X117,X119,X118) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f49,axiom,(
% 12.72/7.25 (! [X120,X121,X122] :( tptp1(X120,X121,X122)=> ( activity(X120)& ~ atomic(X120)& ~ atomic(X121)& root(X122,X121) ) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f50,axiom,(
% 12.72/7.25 (! [X123,X124,X125,X126] :( ( tptp1(X123,X124,X125)& occurrence_of(X126,X123) )=> (? [X127,X128,X129,X130] :( send_message(X127,X128,X129,X125,X124)& occurrence_of(X130,X127)& root_occ(X130,X126) ) )) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f52,conjecture,(
% 12.72/7.25 ~ (? [X133,X134,X135] :( tptp1(X133,tptp0,X134)& occurrence_of(X135,X133) ) )),
% 12.72/7.25 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.72/7.25 fof(f53,negated_conjecture,(
% 12.72/7.25 ~(~ (? [X133,X134,X135] :( tptp1(X133,tptp0,X134)& occurrence_of(X135,X133) ) ))),
% 12.72/7.25 inference(negated_conjecture,[status(cth)],[f52])).
% 12.72/7.25 fof(f54,plain,(
% 12.72/7.25 ![X0,X1]: ((~occurrence_of(X1,X0)|atomic(X0))|(?[X2]: (root(X2,X0)&subactivity_occurrence(X2,X1))))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 12.72/7.25 fof(f55,plain,(
% 12.72/7.25 ![X0,X1]: ((~occurrence_of(X1,X0)|atomic(X0))|(root(sK0_skl(X1,X0),X0)&subactivity_occurrence(sK0_skl(X1,X0),X1)))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X2,sK0_skl(X1,X0))],[f54])).
% 12.72/7.25 fof(f56,plain,(
% 12.72/7.25 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1)|root(sK0_skl(X0,X1),X1))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f55])).
% 12.72/7.25 fof(f57,plain,(
% 12.72/7.25 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1)|subactivity_occurrence(sK0_skl(X0,X1),X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f55])).
% 12.72/7.25 fof(f61,plain,(
% 12.72/7.25 ![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)),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 12.72/7.25 fof(f62,plain,(
% 12.72/7.25 ![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)),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f61])).
% 12.72/7.25 fof(f63,plain,(
% 12.72/7.25 ![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)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f62])).
% 12.72/7.25 fof(f74,plain,(
% 12.72/7.25 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 12.72/7.25 fof(f75,plain,(
% 12.72/7.25 ![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))))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f74])).
% 12.72/7.25 fof(f76,plain,(
% 12.72/7.25 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f75])).
% 12.72/7.25 fof(f77,plain,(
% 12.72/7.25 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f75])).
% 12.72/7.25 fof(f78,plain,(
% 12.72/7.25 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK2_skl(X1,X0,X2)))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f75])).
% 12.72/7.25 fof(f83,plain,(
% 12.72/7.25 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 12.72/7.25 fof(f84,plain,(
% 12.72/7.25 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f83])).
% 12.72/7.25 fof(f85,plain,(
% 12.72/7.25 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f84])).
% 12.72/7.25 fof(f92,plain,(
% 12.72/7.25 ![X39,X40]: (~subactivity_occurrence(X39,X40)|(activity_occurrence(X39)&activity_occurrence(X40)))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 12.72/7.25 fof(f93,plain,(
% 12.72/7.25 ![X0,X1]: (~subactivity_occurrence(X0,X1)|activity_occurrence(X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f92])).
% 12.72/7.25 fof(f95,plain,(
% 12.72/7.25 ![X41]: (~activity_occurrence(X41)|(?[X42]: (activity(X42)&occurrence_of(X41,X42))))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 12.72/7.25 fof(f96,plain,(
% 12.72/7.25 ![X41]: (~activity_occurrence(X41)|(activity(sK4_skl(X41))&occurrence_of(X41,sK4_skl(X41))))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f95])).
% 12.72/7.25 fof(f98,plain,(
% 12.72/7.25 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK4_skl(X0)))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f96])).
% 12.72/7.25 fof(f99,plain,(
% 12.72/7.25 ![X43]: (~legal(X43)|arboreal(X43))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 12.72/7.25 fof(f100,plain,(
% 12.72/7.25 ![X0]: (~legal(X0)|arboreal(X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f99])).
% 12.72/7.25 fof(f120,plain,(
% 12.72/7.25 ![X53,X54]: (~root(X53,X54)|legal(X53))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 12.72/7.25 fof(f121,plain,(
% 12.72/7.25 ![X53]: ((![X54]: ~root(X53,X54))|legal(X53))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f120])).
% 12.72/7.25 fof(f122,plain,(
% 12.72/7.25 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f121])).
% 12.72/7.25 fof(f123,plain,(
% 12.72/7.25 ![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)))))),
% 12.72/7.25 inference(NNF_transformation,[status(thm)],[f19])).
% 12.72/7.25 fof(f124,plain,(
% 12.72/7.25 (![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)))))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f123])).
% 12.72/7.25 fof(f125,plain,(
% 12.72/7.25 (![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)))))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f124])).
% 12.72/7.25 fof(f127,plain,(
% 12.72/7.25 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f125])).
% 12.72/7.25 fof(f130,plain,(
% 12.72/7.25 ![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)))))),
% 12.72/7.25 inference(NNF_transformation,[status(thm)],[f20])).
% 12.72/7.25 fof(f131,plain,(
% 12.72/7.25 (![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)))))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f130])).
% 12.72/7.25 fof(f132,plain,(
% 12.72/7.25 (![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)))))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f131])).
% 12.72/7.25 fof(f136,plain,(
% 12.72/7.25 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f132])).
% 12.72/7.25 fof(f159,plain,(
% 12.72/7.25 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 12.72/7.25 fof(f160,plain,(
% 12.72/7.25 ![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))))))),
% 12.72/7.25 inference(NNF_transformation,[status(thm)],[f159])).
% 12.72/7.25 fof(f161,plain,(
% 12.72/7.25 (![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))))))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f160])).
% 12.72/7.25 fof(f162,plain,(
% 12.72/7.25 (![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)))))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f161])).
% 12.72/7.25 fof(f164,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f162])).
% 12.72/7.25 fof(f173,plain,(
% 12.72/7.25 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 12.72/7.25 fof(f174,plain,(
% 12.72/7.25 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f173])).
% 12.72/7.25 fof(f175,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f174])).
% 12.72/7.25 fof(f182,plain,(
% 12.72/7.25 ![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))))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 12.72/7.25 fof(f183,plain,(
% 12.72/7.25 ![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)))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f182])).
% 12.72/7.25 fof(f185,plain,(
% 12.72/7.25 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK12_skl(X0),X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f183])).
% 12.72/7.25 fof(f186,plain,(
% 12.72/7.25 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK13_skl(X0),tptp3)|occurrence_of(sK13_skl(X0),tptp2))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f183])).
% 12.72/7.25 fof(f187,plain,(
% 12.72/7.25 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK13_skl(X0),X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f183])).
% 12.72/7.25 fof(f188,plain,(
% 12.72/7.25 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f183])).
% 12.72/7.25 fof(f206,plain,(
% 12.72/7.25 ![X109,X110,X111,X112,X113]: (~send_message(X109,X110,X111,X112,X113)|((~X109=tptp4&~X109=tptp3)&~X109=tptp2))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 12.72/7.25 fof(f207,plain,(
% 12.72/7.25 ![X109]: ((![X110,X111,X112,X113]: ~send_message(X109,X110,X111,X112,X113))|((~X109=tptp4&~X109=tptp3)&~X109=tptp2))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f206])).
% 12.72/7.25 fof(f209,plain,(
% 12.72/7.25 ![X0,X1,X2,X3,X4]: (~send_message(X0,X1,X2,X3,X4)|~X0=tptp3)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f207])).
% 12.72/7.25 fof(f210,plain,(
% 12.72/7.25 ![X0,X1,X2,X3,X4]: (~send_message(X0,X1,X2,X3,X4)|~X0=tptp2)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f207])).
% 12.72/7.25 fof(f211,plain,(
% 12.72/7.25 ![X114,X115,X116,X117,X118,X119]: ((~send_message(X114,X115,X116,X117,X118)|~occurrence_of(X119,X114))|min_precedes(X117,X119,X118))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 12.72/7.25 fof(f212,plain,(
% 12.72/7.25 ![X117,X118,X119]: ((![X114]: ((![X115,X116]: ~send_message(X114,X115,X116,X117,X118))|~occurrence_of(X119,X114)))|min_precedes(X117,X119,X118))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f211])).
% 12.72/7.25 fof(f213,plain,(
% 12.72/7.25 ![X0,X1,X2,X3,X4,X5]: (~send_message(X0,X1,X2,X3,X4)|~occurrence_of(X5,X0)|min_precedes(X3,X5,X4))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f212])).
% 12.72/7.25 fof(f214,plain,(
% 12.72/7.25 ![X120,X121,X122]: (~tptp1(X120,X121,X122)|(((activity(X120)&~atomic(X120))&~atomic(X121))&root(X122,X121)))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 12.72/7.25 fof(f216,plain,(
% 12.72/7.25 ![X0,X1,X2]: (~tptp1(X0,X1,X2)|~atomic(X0))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f214])).
% 12.72/7.25 fof(f218,plain,(
% 12.72/7.25 ![X0,X1,X2]: (~tptp1(X0,X1,X2)|root(X2,X1))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f214])).
% 12.72/7.25 fof(f219,plain,(
% 12.72/7.25 ![X123,X124,X125,X126]: ((~tptp1(X123,X124,X125)|~occurrence_of(X126,X123))|(?[X127,X128,X129,X130]: ((send_message(X127,X128,X129,X125,X124)&occurrence_of(X130,X127))&root_occ(X130,X126))))),
% 12.72/7.25 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 12.72/7.25 fof(f220,plain,(
% 12.72/7.25 ![X124,X125,X126]: ((![X123]: (~tptp1(X123,X124,X125)|~occurrence_of(X126,X123)))|(?[X130]: ((?[X127]: ((?[X128,X129]: send_message(X127,X128,X129,X125,X124))&occurrence_of(X130,X127)))&root_occ(X130,X126))))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f219])).
% 12.72/7.25 fof(f221,plain,(
% 12.72/7.25 ![X124,X125,X126]: ((![X123]: (~tptp1(X123,X124,X125)|~occurrence_of(X126,X123)))|((send_message(sK15_skl(X126,X125,X124),sK16_skl(X126,X125,X124),sK17_skl(X126,X125,X124),X125,X124)&occurrence_of(sK14_skl(X126,X125,X124),sK15_skl(X126,X125,X124)))&root_occ(sK14_skl(X126,X125,X124),X126)))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(X130,sK14_skl(X126,X125,X124)),skolemize(X127,sK15_skl(X126,X125,X124)),skolemize(X128,sK16_skl(X126,X125,X124)),skolemize(X129,sK17_skl(X126,X125,X124))],[f220])).
% 12.72/7.25 fof(f222,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~tptp1(X0,X1,X2)|~occurrence_of(X3,X0)|send_message(sK15_skl(X3,X2,X1),sK16_skl(X3,X2,X1),sK17_skl(X3,X2,X1),X2,X1))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f221])).
% 12.72/7.25 fof(f223,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~tptp1(X0,X1,X2)|~occurrence_of(X3,X0)|occurrence_of(sK14_skl(X3,X2,X1),sK15_skl(X3,X2,X1)))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f221])).
% 12.72/7.25 fof(f224,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~tptp1(X0,X1,X2)|~occurrence_of(X3,X0)|root_occ(sK14_skl(X3,X2,X1),X3))),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f221])).
% 12.72/7.25 fof(f226,plain,(
% 12.72/7.25 ?[X133]: ((?[X134]: tptp1(X133,tptp0,X134))&(?[X135]: occurrence_of(X135,X133)))),
% 12.72/7.25 inference(miniscoping,[status(thm)],[f53])).
% 12.72/7.25 fof(f227,plain,(
% 12.72/7.25 (tptp1(sK18_skl,tptp0,sK19_skl)&occurrence_of(sK20_skl,sK18_skl))),
% 12.72/7.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(X133,sK18_skl),skolemize(X134,sK19_skl),skolemize(X135,sK20_skl)],[f226])).
% 12.72/7.25 fof(f228,plain,(
% 12.72/7.25 tptp1(sK18_skl,tptp0,sK19_skl)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f227])).
% 12.72/7.25 fof(f229,plain,(
% 12.72/7.25 occurrence_of(sK20_skl,sK18_skl)),
% 12.72/7.25 inference(cnf_transformation,[status(thm)],[f227])).
% 12.72/7.25 fof(f231,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~send_message(tptp3,X0,X1,X2,X3))),
% 12.72/7.25 inference(destructive_equality_resolution,[status(thm)],[f209])).
% 12.72/7.25 fof(f232,plain,(
% 12.72/7.25 ![X0,X1,X2,X3]: (~send_message(tptp2,X0,X1,X2,X3))),
% 12.72/7.25 inference(destructive_equality_resolution,[status(thm)],[f210])).
% 12.72/7.25 fof(f233,plain,(
% 12.72/7.25 ~atomic(sK18_skl)),
% 12.72/7.25 inference(resolution,[status(thm)],[f216,f228])).
% 12.72/7.25 fof(f235,plain,(
% 12.72/7.25 root(sK19_skl,tptp0)),
% 12.72/7.25 inference(resolution,[status(thm)],[f218,f228])).
% 12.72/7.25 fof(f238,plain,(
% 12.72/7.25 atomic(sK18_skl)|root(sK0_skl(sK20_skl,sK18_skl),sK18_skl)),
% 12.72/7.25 inference(resolution,[status(thm)],[f56,f229])).
% 12.72/7.25 fof(f239,plain,(
% 12.72/7.25 root(sK0_skl(sK20_skl,sK18_skl),sK18_skl)),
% 12.72/7.25 inference(forward_subsumption_resolution,[status(thm)],[f238,f233])).
% 12.72/7.25 fof(f242,plain,(
% 12.72/7.25 legal(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.25 inference(resolution,[status(thm)],[f122,f239])).
% 12.72/7.25 fof(f245,plain,(
% 12.72/7.25 atomic(sK18_skl)|subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK20_skl)),
% 12.72/7.25 inference(resolution,[status(thm)],[f57,f229])).
% 12.72/7.25 fof(f246,plain,(
% 12.72/7.25 subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK20_skl)),
% 12.72/7.25 inference(forward_subsumption_resolution,[status(thm)],[f245,f233])).
% 12.72/7.25 fof(f248,plain,(
% 12.72/7.25 arboreal(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.25 inference(resolution,[status(thm)],[f242,f100])).
% 12.72/7.25 fof(f250,plain,(
% 12.72/7.25 activity_occurrence(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.25 inference(resolution,[status(thm)],[f246,f93])).
% 12.72/7.25 fof(f259,plain,(
% 12.72/7.25 occurrence_of(sK0_skl(sK20_skl,sK18_skl),sK4_skl(sK0_skl(sK20_skl,sK18_skl)))),
% 12.72/7.25 inference(resolution,[status(thm)],[f98,f250])).
% 12.72/7.25 fof(f289,plain,(
% 12.72/7.25 ![X0]: (~occurrence_of(sK0_skl(sK20_skl,sK18_skl),X0)|X0=sK4_skl(sK0_skl(sK20_skl,sK18_skl)))),
% 12.72/7.26 inference(resolution,[status(thm)],[f259,f85])).
% 12.72/7.26 fof(f348,plain,(
% 12.72/7.26 ![X0,X1]: (~root_occ(X0,sK20_skl)|~root_occ(X1,sK20_skl)|X0=X1)),
% 12.72/7.26 inference(resolution,[status(thm)],[f175,f229])).
% 12.72/7.26 fof(f417,plain,(
% 12.72/7.26 ![X0]: (root_occ(X0,sK20_skl)|~subactivity_occurrence(X0,sK20_skl)|~root(X0,sK18_skl))),
% 12.72/7.26 inference(resolution,[status(thm)],[f136,f229])).
% 12.72/7.26 fof(f418,plain,(
% 12.72/7.26 root_occ(sK0_skl(sK20_skl,sK18_skl),sK20_skl)|~subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK20_skl)),
% 12.72/7.26 inference(resolution,[status(thm)],[f417,f239])).
% 12.72/7.26 fof(f419,plain,(
% 12.72/7.26 root_occ(sK0_skl(sK20_skl,sK18_skl),sK20_skl)),
% 12.72/7.26 inference(forward_subsumption_resolution,[status(thm)],[f418,f246])).
% 12.72/7.26 fof(f420,plain,(
% 12.72/7.26 ![X0]: (~root_occ(X0,sK20_skl)|X0=sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(resolution,[status(thm)],[f419,f348])).
% 12.72/7.26 fof(f452,plain,(
% 12.72/7.26 ![X0]: (~occurrence_of(X0,sK18_skl)|root_occ(sK14_skl(X0,sK19_skl,tptp0),X0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f224,f228])).
% 12.72/7.26 fof(f453,plain,(
% 12.72/7.26 root_occ(sK14_skl(sK20_skl,sK19_skl,tptp0),sK20_skl)),
% 12.72/7.26 inference(resolution,[status(thm)],[f452,f229])).
% 12.72/7.26 fof(f466,plain,(
% 12.72/7.26 sK14_skl(sK20_skl,sK19_skl,tptp0)=sK0_skl(sK20_skl,sK18_skl)),
% 12.72/7.26 inference(resolution,[status(thm)],[f453,f420])).
% 12.72/7.26 fof(f522,plain,(
% 12.72/7.26 ![X0]: (~occurrence_of(X0,sK18_skl)|occurrence_of(sK14_skl(X0,sK19_skl,tptp0),sK15_skl(X0,sK19_skl,tptp0)))),
% 12.72/7.26 inference(resolution,[status(thm)],[f223,f228])).
% 12.72/7.26 fof(f523,plain,(
% 12.72/7.26 occurrence_of(sK14_skl(sK20_skl,sK19_skl,tptp0),sK15_skl(sK20_skl,sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f522,f229])).
% 12.72/7.26 fof(f524,plain,(
% 12.72/7.26 occurrence_of(sK0_skl(sK20_skl,sK18_skl),sK15_skl(sK20_skl,sK19_skl,tptp0))),
% 12.72/7.26 inference(forward_demodulation,[status(thm)],[f466,f523])).
% 12.72/7.26 fof(f525,plain,(
% 12.72/7.26 sK15_skl(sK20_skl,sK19_skl,tptp0)=sK4_skl(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(resolution,[status(thm)],[f524,f289])).
% 12.72/7.26 fof(f551,plain,(
% 12.72/7.26 ![X0]: (~occurrence_of(X0,sK18_skl)|send_message(sK15_skl(X0,sK19_skl,tptp0),sK16_skl(X0,sK19_skl,tptp0),sK17_skl(X0,sK19_skl,tptp0),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f222,f228])).
% 12.72/7.26 fof(f552,plain,(
% 12.72/7.26 send_message(sK15_skl(sK20_skl,sK19_skl,tptp0),sK16_skl(sK20_skl,sK19_skl,tptp0),sK17_skl(sK20_skl,sK19_skl,tptp0),sK19_skl,tptp0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f551,f229])).
% 12.72/7.26 fof(f553,plain,(
% 12.72/7.26 ![X0]: (~occurrence_of(X0,sK15_skl(sK20_skl,sK19_skl,tptp0))|min_precedes(sK19_skl,X0,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f552,f213])).
% 12.72/7.26 fof(f558,plain,(
% 12.72/7.26 min_precedes(sK19_skl,sK0_skl(sK20_skl,sK18_skl),tptp0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f553,f524])).
% 12.72/7.26 fof(f565,plain,(
% 12.72/7.26 ![X0]: (~next_subocc(sK19_skl,X0,tptp0)|~min_precedes(sK0_skl(sK20_skl,sK18_skl),X0,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f558,f164])).
% 12.72/7.26 fof(f569,plain,(
% 12.72/7.26 subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f558,f78])).
% 12.72/7.26 fof(f570,plain,(
% 12.72/7.26 subactivity_occurrence(sK19_skl,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f558,f77])).
% 12.72/7.26 fof(f572,plain,(
% 12.72/7.26 occurrence_of(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0),tptp0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f558,f76])).
% 12.72/7.26 fof(f716,plain,(
% 12.72/7.26 occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp3)|occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp2)),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f186])).
% 12.72/7.26 fof(f717,plain,(
% 12.72/7.26 next_subocc(sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f188])).
% 12.72/7.26 fof(f719,plain,(
% 12.72/7.26 leaf_occ(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f187])).
% 12.72/7.26 fof(f720,plain,(
% 12.72/7.26 root_occ(sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f185])).
% 12.72/7.26 fof(f722,plain,(
% 12.72/7.26 ![X0]: (root_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~subactivity_occurrence(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~root(X0,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f136])).
% 12.72/7.26 fof(f725,plain,(
% 12.72/7.26 ![X0,X1]: (~root_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~root_occ(X1,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|X0=X1)),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f175])).
% 12.72/7.26 fof(f729,plain,(
% 12.72/7.26 ![X0,X1]: (~subactivity_occurrence(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~leaf_occ(X1,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~arboreal(X0)|min_precedes(X0,X1,tptp0)|X1=X0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f572,f63])).
% 12.72/7.26 fof(f1243,plain,(
% 12.72/7.26 subactivity_occurrence(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f719,f127])).
% 12.72/7.26 fof(f1326,plain,(
% 12.72/7.26 activity_occurrence(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))),
% 12.72/7.26 inference(resolution,[status(thm)],[f1243,f93])).
% 12.72/7.26 fof(f1327,plain,(
% 12.72/7.26 occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))))),
% 12.72/7.26 inference(resolution,[status(thm)],[f1326,f98])).
% 12.72/7.26 fof(f1528,plain,(
% 12.72/7.26 ![X0]: (~root_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|X0=sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))),
% 12.72/7.26 inference(resolution,[status(thm)],[f725,f720])).
% 12.72/7.26 fof(f1680,plain,(
% 12.72/7.26 ![X0]: (~occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),X0)|X0=sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))))),
% 12.72/7.26 inference(resolution,[status(thm)],[f1327,f85])).
% 12.72/7.26 fof(f2537,plain,(
% 12.72/7.26 root_occ(sK19_skl,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~root(sK19_skl,tptp0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f722,f570])).
% 12.72/7.26 fof(f2541,plain,(
% 12.72/7.26 root_occ(sK19_skl,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(forward_subsumption_resolution,[status(thm)],[f2537,f235])).
% 12.72/7.26 fof(f2543,plain,(
% 12.72/7.26 sK19_skl=sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
% 12.72/7.26 inference(resolution,[status(thm)],[f2541,f1528])).
% 12.72/7.26 fof(f2560,plain,(
% 12.72/7.26 next_subocc(sK19_skl,sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0)),
% 12.72/7.26 inference(backward_demodulation,[status(thm)],[f2543,f717])).
% 12.72/7.26 fof(f2907,plain,(
% 12.72/7.26 occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp2)|tptp3=sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))),
% 12.72/7.26 inference(resolution,[status(thm)],[f716,f1680])).
% 12.72/7.26 fof(f3239,plain,(
% 12.72/7.26 tptp3=sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))|tptp2=sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))),
% 12.72/7.26 inference(resolution,[status(thm)],[f2907,f1680])).
% 12.72/7.26 fof(f4012,plain,(
% 12.72/7.26 ![X0]: (~leaf_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|~arboreal(sK0_skl(sK20_skl,sK18_skl))|min_precedes(sK0_skl(sK20_skl,sK18_skl),X0,tptp0)|X0=sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(resolution,[status(thm)],[f729,f569])).
% 12.72/7.26 fof(f4014,plain,(
% 12.72/7.26 ![X0]: (~leaf_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))|min_precedes(sK0_skl(sK20_skl,sK18_skl),X0,tptp0)|X0=sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(forward_subsumption_resolution,[status(thm)],[f4012,f248])).
% 12.72/7.26 fof(f4016,plain,(
% 12.72/7.26 min_precedes(sK0_skl(sK20_skl,sK18_skl),sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0)|sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))=sK0_skl(sK20_skl,sK18_skl)),
% 12.72/7.26 inference(resolution,[status(thm)],[f4014,f719])).
% 12.72/7.26 fof(f6428,plain,(
% 12.72/7.26 sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))=sK0_skl(sK20_skl,sK18_skl)|~next_subocc(sK19_skl,sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0)),
% 12.72/7.26 inference(resolution,[status(thm)],[f4016,f565])).
% 12.72/7.26 fof(f6447,plain,(
% 12.72/7.26 sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))=sK0_skl(sK20_skl,sK18_skl)),
% 12.72/7.26 inference(forward_subsumption_resolution,[status(thm)],[f6428,f2560])).
% 12.72/7.26 fof(f6528,plain,(
% 12.72/7.26 tptp3=sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))|tptp2=sK4_skl(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(backward_demodulation,[status(thm)],[f6447,f3239])).
% 12.72/7.26 fof(f6629,plain,(
% 12.72/7.26 tptp3=sK4_skl(sK0_skl(sK20_skl,sK18_skl))|tptp2=sK4_skl(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(forward_demodulation,[status(thm)],[f6447,f6528])).
% 12.72/7.26 fof(f6630,plain,(
% 12.72/7.26 tptp3=sK15_skl(sK20_skl,sK19_skl,tptp0)|tptp2=sK4_skl(sK0_skl(sK20_skl,sK18_skl))),
% 12.72/7.26 inference(forward_demodulation,[status(thm)],[f525,f6629])).
% 12.72/7.26 fof(f6631,plain,(
% 12.72/7.26 tptp3=sK15_skl(sK20_skl,sK19_skl,tptp0)|tptp2=sK15_skl(sK20_skl,sK19_skl,tptp0)),
% 12.72/7.26 inference(forward_demodulation,[status(thm)],[f525,f6630])).
% 12.72/7.26 fof(f6853,plain,(
% 12.72/7.26 send_message(tptp3,sK16_skl(sK20_skl,sK19_skl,tptp0),sK17_skl(sK20_skl,sK19_skl,tptp0),sK19_skl,tptp0)|tptp2=sK15_skl(sK20_skl,sK19_skl,tptp0)),
% 12.72/7.26 inference(paramodulation,[status(thm)],[f6631,f552])).
% 12.72/7.26 fof(f6859,plain,(
% 12.72/7.26 tptp2=sK15_skl(sK20_skl,sK19_skl,tptp0)),
% 12.72/7.26 inference(forward_subsumption_resolution,[status(thm)],[f6853,f231])).
% 10.58/7.28 fof(f6871,plain,(
% 10.58/7.28 send_message(tptp2,sK16_skl(sK20_skl,sK19_skl,tptp0),sK17_skl(sK20_skl,sK19_skl,tptp0),sK19_skl,tptp0)),
% 10.58/7.28 inference(backward_demodulation,[status(thm)],[f6859,f552])).
% 10.58/7.28 fof(f6880,plain,(
% 10.58/7.28 $false),
% 10.58/7.28 inference(forward_subsumption_resolution,[status(thm)],[f6871,f232])).
% 10.58/7.28 % SZS output end CNFRefutation for theBenchmark.p
% 8.26/7.35 % Elapsed time: 1.969032 seconds
% 8.26/7.35 % CPU time: 14.916244 seconds
% 8.26/7.35 % Total memory used: 229.626 MB
% 8.26/7.35 % Net memory used: 222.009 MB
%------------------------------------------------------------------------------