%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO017+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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:59:26 PM UTC 2026
% Result : Theorem 0.15s 11.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO017+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.10/10.37 % Computer : n002.cluster.edu
% 0.10/10.37 % Model : x86_64 x86_64
% 0.10/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.37 % Memory : 8046.5625MB
% 0.10/10.37 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Mon Sep 21 03:46:42 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.39 % Drodi V4.1.1
% 0.15/11.03 % Refutation found
% 0.15/11.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/11.03 % SZS output start CNFRefutation for theBenchmark
% 0.15/11.03 fof(f7,axiom,(
% 0.15/11.03 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f9,axiom,(
% 0.15/11.03 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f10,axiom,(
% 0.15/11.03 (! [X31,X32,X33] :( ( occurrence_of(X31,X33)& leaf_occ(X32,X31) )=> ~ (? [X34] : min_precedes(X32,X34,X33) )) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f17,axiom,(
% 0.15/11.03 (! [X51,X52] :( occurrence_of(X51,X52)=> ( arboreal(X51)<=> atomic(X52) ) ) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f27,axiom,(
% 0.15/11.03 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f33,axiom,(
% 0.15/11.03 (! [X101,X102] :( ( occurrence_of(X102,tptp0)& subactivity_occurrence(X101,X102)& arboreal(X101)& ~ leaf_occ(X101,X102) )=> (? [X103,X104,X105] :( occurrence_of(X103,tptp3)& next_subocc(X101,X103,tptp0)& occurrence_of(X104,tptp4)& min_precedes(X103,X104,tptp0)& ( occurrence_of(X105,tptp2)| occurrence_of(X105,tptp1) )& min_precedes(X104,X105,tptp0)& (! [X106] :( min_precedes(X103,X106,tptp0)=> ( X106 = X104| X106 = X105 ) ) )) )) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f36,axiom,(
% 0.15/11.03 atomic(tptp4) ),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f37,axiom,(
% 0.15/11.03 atomic(tptp2) ),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f38,axiom,(
% 0.15/11.03 atomic(tptp1) ),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f39,axiom,(
% 0.15/11.03 atomic(tptp3) ),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f40,axiom,(
% 0.15/11.03 tptp4 != tptp3 ),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f46,conjecture,(
% 0.15/11.03 (! [X107,X108] :( ( occurrence_of(X108,tptp0)& subactivity_occurrence(X107,X108)& arboreal(X107)& ~ leaf_occ(X107,X108) )=> (? [X109,X110] :( occurrence_of(X109,tptp3)& next_subocc(X107,X109,tptp0)& ( occurrence_of(X110,tptp2)| occurrence_of(X110,tptp1) )& min_precedes(X109,X110,tptp0)& leaf(X110,tptp0) ) )) )),
% 0.15/11.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/11.03 fof(f47,negated_conjecture,(
% 0.15/11.03 ~((! [X107,X108] :( ( occurrence_of(X108,tptp0)& subactivity_occurrence(X107,X108)& arboreal(X107)& ~ leaf_occ(X107,X108) )=> (? [X109,X110] :( occurrence_of(X109,tptp3)& next_subocc(X107,X109,tptp0)& ( occurrence_of(X110,tptp2)| occurrence_of(X110,tptp1) )& min_precedes(X109,X110,tptp0)& leaf(X110,tptp0) ) )) ))),
% 0.15/11.03 inference(negated_conjecture,[status(cth)],[f46])).
% 0.15/11.03 fof(f68,plain,(
% 0.15/11.03 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.15/11.03 fof(f69,plain,(
% 0.15/11.03 ![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))))),
% 0.15/11.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f68])).
% 0.15/11.03 fof(f70,plain,(
% 0.15/11.03 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/11.03 fof(f71,plain,(
% 0.15/11.03 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/11.03 fof(f77,plain,(
% 0.15/11.03 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.15/11.03 fof(f78,plain,(
% 0.15/11.03 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 0.15/11.03 inference(miniscoping,[status(thm)],[f77])).
% 0.15/11.03 fof(f79,plain,(
% 0.15/11.03 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f78])).
% 0.15/11.03 fof(f80,plain,(
% 0.15/11.03 ![X31,X32,X33]: ((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.15/11.03 fof(f81,plain,(
% 0.15/11.03 ![X32,X33]: ((![X31]: (~occurrence_of(X31,X33)|~leaf_occ(X32,X31)))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 0.15/11.03 inference(miniscoping,[status(thm)],[f80])).
% 0.15/11.03 fof(f82,plain,(
% 0.15/11.03 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f81])).
% 0.15/11.03 fof(f110,plain,(
% 0.15/11.03 ![X51,X52]: (~occurrence_of(X51,X52)|(arboreal(X51)<=>atomic(X52)))),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.15/11.03 fof(f111,plain,(
% 0.15/11.03 ![X51,X52]: (~occurrence_of(X51,X52)|((~arboreal(X51)|atomic(X52))&(arboreal(X51)|~atomic(X52))))),
% 0.15/11.03 inference(NNF_transformation,[status(thm)],[f110])).
% 0.15/11.03 fof(f113,plain,(
% 0.15/11.03 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f111])).
% 0.15/11.03 fof(f153,plain,(
% 0.15/11.03 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.15/11.03 fof(f154,plain,(
% 0.15/11.03 ![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))))))),
% 0.15/11.03 inference(NNF_transformation,[status(thm)],[f153])).
% 0.15/11.03 fof(f155,plain,(
% 0.15/11.03 (![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))))))),
% 0.15/11.03 inference(miniscoping,[status(thm)],[f154])).
% 0.15/11.03 fof(f156,plain,(
% 0.15/11.03 (![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)))))),
% 0.15/11.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f155])).
% 0.15/11.03 fof(f157,plain,(
% 0.15/11.03 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f156])).
% 0.15/11.03 fof(f158,plain,(
% 0.15/11.03 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f156])).
% 0.15/11.03 fof(f176,plain,(
% 0.15/11.03 ![X101,X102]: ((((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102))|(?[X103,X104,X105]: ((((((occurrence_of(X103,tptp3)&next_subocc(X101,X103,tptp0))&occurrence_of(X104,tptp4))&min_precedes(X103,X104,tptp0))&(occurrence_of(X105,tptp2)|occurrence_of(X105,tptp1)))&min_precedes(X104,X105,tptp0))&(![X106]: (~min_precedes(X103,X106,tptp0)|(X106=X104|X106=X105))))))),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.15/11.03 fof(f177,plain,(
% 0.15/11.03 ![X101]: ((![X102]: (((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102)))|(?[X103,X104,X105]: ((((((occurrence_of(X103,tptp3)&next_subocc(X101,X103,tptp0))&occurrence_of(X104,tptp4))&min_precedes(X103,X104,tptp0))&(occurrence_of(X105,tptp2)|occurrence_of(X105,tptp1)))&min_precedes(X104,X105,tptp0))&(![X106]: (~min_precedes(X103,X106,tptp0)|(X106=X104|X106=X105))))))),
% 0.15/11.03 inference(miniscoping,[status(thm)],[f176])).
% 0.15/11.03 fof(f178,plain,(
% 0.15/11.03 ![X101]: ((![X102]: (((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102)))|((((((occurrence_of(sK12_skl(X101),tptp3)&next_subocc(X101,sK12_skl(X101),tptp0))&occurrence_of(sK13_skl(X101),tptp4))&min_precedes(sK12_skl(X101),sK13_skl(X101),tptp0))&(occurrence_of(sK14_skl(X101),tptp2)|occurrence_of(sK14_skl(X101),tptp1)))&min_precedes(sK13_skl(X101),sK14_skl(X101),tptp0))&(![X106]: (~min_precedes(sK12_skl(X101),X106,tptp0)|(X106=sK13_skl(X101)|X106=sK14_skl(X101))))))),
% 0.15/11.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X103,sK12_skl(X101)),skolemize(X104,sK13_skl(X101)),skolemize(X105,sK14_skl(X101))],[f177])).
% 0.15/11.03 fof(f179,plain,(
% 0.15/11.03 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK12_skl(X1),tptp3))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/11.03 fof(f180,plain,(
% 0.15/11.03 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK12_skl(X1),tptp0))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/11.03 fof(f181,plain,(
% 0.15/11.03 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK13_skl(X1),tptp4))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/11.03 fof(f182,plain,(
% 0.15/11.03 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK12_skl(X1),sK13_skl(X1),tptp0))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/11.03 fof(f184,plain,(
% 0.15/11.03 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK13_skl(X1),sK14_skl(X1),tptp0))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/11.03 fof(f185,plain,(
% 0.15/11.03 ![X0,X1,X2]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|~min_precedes(sK12_skl(X1),X2,tptp0)|X2=sK13_skl(X1)|X2=sK14_skl(X1))),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.15/11.03 fof(f188,plain,(
% 0.15/11.03 atomic(tptp4)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/11.03 fof(f189,plain,(
% 0.15/11.03 atomic(tptp2)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f37])).
% 0.15/11.03 fof(f190,plain,(
% 0.15/11.03 atomic(tptp1)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f38])).
% 0.15/11.03 fof(f191,plain,(
% 0.15/11.03 atomic(tptp3)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/11.03 fof(f192,plain,(
% 0.15/11.03 ~tptp4=tptp3),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f40])).
% 0.15/11.03 fof(f198,plain,(
% 0.15/11.03 (?[X107,X108]: ((((occurrence_of(X108,tptp0)&subactivity_occurrence(X107,X108))&arboreal(X107))&~leaf_occ(X107,X108))&(![X109,X110]: ((((~occurrence_of(X109,tptp3)|~next_subocc(X107,X109,tptp0))|(~occurrence_of(X110,tptp2)&~occurrence_of(X110,tptp1)))|~min_precedes(X109,X110,tptp0))|~leaf(X110,tptp0)))))),
% 0.15/11.03 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.15/11.03 fof(f199,plain,(
% 0.15/11.03 ?[X107]: ((?[X108]: (((occurrence_of(X108,tptp0)&subactivity_occurrence(X107,X108))&arboreal(X107))&~leaf_occ(X107,X108)))&(![X110]: ((![X109]: (((~occurrence_of(X109,tptp3)|~next_subocc(X107,X109,tptp0))|(~occurrence_of(X110,tptp2)&~occurrence_of(X110,tptp1)))|~min_precedes(X109,X110,tptp0)))|~leaf(X110,tptp0))))),
% 0.15/11.03 inference(miniscoping,[status(thm)],[f198])).
% 0.15/11.03 fof(f200,plain,(
% 0.15/11.03 ((((occurrence_of(sK16_skl,tptp0)&subactivity_occurrence(sK15_skl,sK16_skl))&arboreal(sK15_skl))&~leaf_occ(sK15_skl,sK16_skl))&(![X110]: ((![X109]: (((~occurrence_of(X109,tptp3)|~next_subocc(sK15_skl,X109,tptp0))|(~occurrence_of(X110,tptp2)&~occurrence_of(X110,tptp1)))|~min_precedes(X109,X110,tptp0)))|~leaf(X110,tptp0))))),
% 0.15/11.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(X107,sK15_skl),skolemize(X108,sK16_skl)],[f199])).
% 0.15/11.03 fof(f201,plain,(
% 0.15/11.03 occurrence_of(sK16_skl,tptp0)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f200])).
% 0.15/11.03 fof(f202,plain,(
% 0.15/11.03 subactivity_occurrence(sK15_skl,sK16_skl)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f200])).
% 0.15/11.03 fof(f203,plain,(
% 0.15/11.03 arboreal(sK15_skl)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f200])).
% 0.15/11.03 fof(f204,plain,(
% 0.15/11.03 ~leaf_occ(sK15_skl,sK16_skl)),
% 0.15/11.03 inference(cnf_transformation,[status(thm)],[f200])).
% 0.15/11.03 fof(f243,definition,(
% 0.15/11.03 sQ6_spl <=> (arboreal(sK15_skl))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f245,plain,(
% 0.15/11.03 ~arboreal(sK15_skl)|sQ6_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f243])).
% 0.15/11.03 fof(f262,plain,(
% 0.15/11.03 $false|sQ6_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f245,f203])).
% 0.15/11.03 fof(f263,plain,(
% 0.15/11.03 sQ6_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f262])).
% 0.15/11.03 fof(f273,definition,(
% 0.15/11.03 sQ11_spl <=> (leaf_occ(sK15_skl,sK16_skl))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f274,plain,(
% 0.15/11.03 leaf_occ(sK15_skl,sK16_skl)|~sQ11_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f273])).
% 0.15/11.03 fof(f280,plain,(
% 0.15/11.03 $false|~sQ11_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f274,f204])).
% 0.15/11.03 fof(f281,plain,(
% 0.15/11.03 ~sQ11_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f280])).
% 0.15/11.03 fof(f383,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|occurrence_of(sK12_skl(X0),tptp3))),
% 0.15/11.03 inference(resolution,[status(thm)],[f179,f201])).
% 0.15/11.03 fof(f384,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|occurrence_of(sK13_skl(X0),tptp4))),
% 0.15/11.03 inference(resolution,[status(thm)],[f181,f201])).
% 0.15/11.03 fof(f385,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(X0,sK12_skl(X0),tptp0))),
% 0.15/11.03 inference(resolution,[status(thm)],[f180,f201])).
% 0.15/11.03 fof(f389,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|min_precedes(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 0.15/11.03 inference(resolution,[status(thm)],[f182,f201])).
% 0.15/11.03 fof(f390,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|min_precedes(sK13_skl(X0),sK14_skl(X0),tptp0))),
% 0.15/11.03 inference(resolution,[status(thm)],[f184,f201])).
% 0.15/11.03 fof(f529,plain,(
% 0.15/11.03 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK12_skl(sK15_skl),tptp3)),
% 0.15/11.03 inference(resolution,[status(thm)],[f383,f202])).
% 0.15/11.03 fof(f530,definition,(
% 0.15/11.03 sQ37_spl <=> (occurrence_of(sK12_skl(sK15_skl),tptp3))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f531,plain,(
% 0.15/11.03 occurrence_of(sK12_skl(sK15_skl),tptp3)|~sQ37_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f530])).
% 0.15/11.03 fof(f533,plain,(
% 0.15/11.03 ~sQ6_spl|sQ11_spl|sQ37_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f529,f243,f273,f530])).
% 0.15/11.03 fof(f534,plain,(
% 0.15/11.03 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK13_skl(sK15_skl),tptp4)),
% 0.15/11.03 inference(resolution,[status(thm)],[f384,f202])).
% 0.15/11.03 fof(f535,definition,(
% 0.15/11.03 sQ38_spl <=> (occurrence_of(sK13_skl(sK15_skl),tptp4))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f536,plain,(
% 0.15/11.03 occurrence_of(sK13_skl(sK15_skl),tptp4)|~sQ38_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f535])).
% 0.15/11.03 fof(f538,plain,(
% 0.15/11.03 ~sQ6_spl|sQ11_spl|sQ38_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f534,f243,f273,f535])).
% 0.15/11.03 fof(f553,definition,(
% 0.15/11.03 sQ40_spl <=> (atomic(tptp3))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f555,plain,(
% 0.15/11.03 ~atomic(tptp3)|sQ40_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f553])).
% 0.15/11.03 fof(f557,definition,(
% 0.15/11.03 sQ41_spl <=> (arboreal(sK12_skl(sK15_skl)))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f569,plain,(
% 0.15/11.03 $false|sQ40_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f555,f191])).
% 0.15/11.03 fof(f570,plain,(
% 0.15/11.03 sQ40_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f569])).
% 0.15/11.03 fof(f575,plain,(
% 0.15/11.03 ![X0]: (~occurrence_of(sK13_skl(sK15_skl),X0)|X0=tptp4|~sQ38_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f536,f79])).
% 0.15/11.03 fof(f585,definition,(
% 0.15/11.03 sQ45_spl <=> (atomic(tptp4))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f587,plain,(
% 0.15/11.03 ~atomic(tptp4)|sQ45_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f585])).
% 0.15/11.03 fof(f601,plain,(
% 0.15/11.03 $false|sQ45_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f587,f188])).
% 0.15/11.03 fof(f602,plain,(
% 0.15/11.03 sQ45_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f601])).
% 0.15/11.03 fof(f610,plain,(
% 0.15/11.03 arboreal(sK12_skl(sK15_skl))|~atomic(tptp3)|~sQ37_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f113,f531])).
% 0.15/11.03 fof(f614,plain,(
% 0.15/11.03 sQ41_spl|~sQ40_spl|~sQ37_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f610,f557,f553,f530])).
% 0.15/11.03 fof(f714,plain,(
% 0.15/11.03 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0)),
% 0.15/11.03 inference(resolution,[status(thm)],[f385,f202])).
% 0.15/11.03 fof(f715,definition,(
% 0.15/11.03 sQ57_spl <=> (next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f716,plain,(
% 0.15/11.03 next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0)|~sQ57_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f715])).
% 0.15/11.03 fof(f718,plain,(
% 0.15/11.03 ~sQ6_spl|sQ11_spl|sQ57_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f714,f243,f273,f715])).
% 0.15/11.03 fof(f719,plain,(
% 0.15/11.03 min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)|~sQ57_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f716,f157])).
% 0.15/11.03 fof(f731,plain,(
% 0.15/11.03 subactivity_occurrence(sK15_skl,sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0))|~sQ57_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f719,f71])).
% 0.15/11.03 fof(f732,plain,(
% 0.15/11.03 occurrence_of(sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0),tptp0)|~sQ57_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f719,f70])).
% 0.15/11.03 fof(f737,plain,(
% 0.15/11.03 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK15_skl,X0)|~sQ57_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f719,f82])).
% 0.15/11.03 fof(f827,plain,(
% 0.15/11.03 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 0.15/11.03 inference(resolution,[status(thm)],[f389,f202])).
% 0.15/11.03 fof(f828,definition,(
% 0.15/11.03 sQ72_spl <=> (min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f829,plain,(
% 0.15/11.03 min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)|~sQ72_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f828])).
% 0.15/11.03 fof(f831,plain,(
% 0.15/11.03 ~sQ6_spl|sQ11_spl|sQ72_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f827,f243,f273,f828])).
% 0.15/11.03 fof(f832,plain,(
% 0.15/11.03 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)),
% 0.15/11.03 inference(resolution,[status(thm)],[f390,f202])).
% 0.15/11.03 fof(f833,definition,(
% 0.15/11.03 sQ73_spl <=> (min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f834,plain,(
% 0.15/11.03 min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)|~sQ73_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f833])).
% 0.15/11.03 fof(f836,plain,(
% 0.15/11.03 ~sQ6_spl|sQ11_spl|sQ73_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f832,f243,f273,f833])).
% 0.15/11.03 fof(f846,plain,(
% 0.15/11.03 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|~sQ72_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f829,f71])).
% 0.15/11.03 fof(f847,plain,(
% 0.15/11.03 occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0)|~sQ72_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f829,f70])).
% 0.15/11.03 fof(f851,plain,(
% 0.15/11.03 ![X0]: (~next_subocc(sK12_skl(sK15_skl),X0,tptp0)|~min_precedes(sK13_skl(sK15_skl),X0,tptp0)|~sQ72_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f829,f158])).
% 0.15/11.03 fof(f852,plain,(
% 0.15/11.03 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK12_skl(sK15_skl),X0)|~sQ72_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f829,f82])).
% 0.15/11.03 fof(f1007,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|~arboreal(X0)|leaf_occ(X0,sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|next_subocc(X0,sK12_skl(X0),tptp0)|~sQ72_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f847,f180])).
% 0.15/11.03 fof(f1009,plain,(
% 0.15/11.03 ![X0]: (~subactivity_occurrence(X0,sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|~arboreal(X0)|leaf_occ(X0,sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|occurrence_of(sK12_skl(X0),tptp3)|~sQ72_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f847,f179])).
% 0.15/11.03 fof(f1438,definition,(
% 0.15/11.03 ![X0]: (sQ151_spl <=> (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|leaf_occ(sK15_skl,X0)))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f1439,plain,(
% 0.15/11.03 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|leaf_occ(sK15_skl,X0)|~sQ151_spl)),
% 0.15/11.03 inference(component_clause,[status(thm)],[f1438])).
% 0.15/11.03 fof(f1509,plain,(
% 0.15/11.03 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|~sQ57_spl|~sQ151_spl)),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f1439,f737])).
% 0.15/11.03 fof(f1534,definition,(
% 0.15/11.03 sQ154_spl <=> (atomic(tptp2))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f1536,plain,(
% 0.15/11.03 ~atomic(tptp2)|sQ154_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f1534])).
% 0.15/11.03 fof(f1559,plain,(
% 0.15/11.03 ~subactivity_occurrence(sK15_skl,sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0))|~sQ151_spl|~sQ57_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f1509,f732])).
% 0.15/11.03 fof(f1561,plain,(
% 0.15/11.03 $false|~sQ151_spl|~sQ57_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f1559,f731])).
% 0.15/11.03 fof(f1562,plain,(
% 0.15/11.03 ~sQ151_spl|~sQ57_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f1561])).
% 0.15/11.03 fof(f1762,definition,(
% 0.15/11.03 sQ174_spl <=> (atomic(tptp1))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f1764,plain,(
% 0.15/11.03 ~atomic(tptp1)|sQ174_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f1762])).
% 0.15/11.03 fof(f1780,plain,(
% 0.15/11.03 $false|sQ174_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f1764,f190])).
% 0.15/11.03 fof(f1781,plain,(
% 0.15/11.03 sQ174_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f1780])).
% 0.15/11.03 fof(f1794,plain,(
% 0.15/11.03 $false|sQ154_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f1536,f189])).
% 0.15/11.03 fof(f1795,plain,(
% 0.15/11.03 sQ154_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f1794])).
% 0.15/11.03 fof(f2094,plain,(
% 0.15/11.03 ~next_subocc(sK12_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)|~sQ72_spl|~sQ73_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f851,f834])).
% 0.15/11.03 fof(f2855,definition,(
% 0.15/11.03 sQ298_spl <=> (occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f2857,plain,(
% 0.15/11.03 ~occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0)|sQ298_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f2855])).
% 0.15/11.03 fof(f2864,plain,(
% 0.15/11.03 $false|~sQ72_spl|sQ298_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f2857,f847])).
% 0.15/11.03 fof(f2865,plain,(
% 0.15/11.03 ~sQ72_spl|sQ298_spl),
% 0.15/11.03 inference(contradiction_clause,[status(thm)],[f2864])).
% 0.15/11.03 fof(f3261,definition,(
% 0.15/11.03 sQ346_spl <=> (leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f3262,plain,(
% 0.15/11.03 leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|~sQ346_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f3261])).
% 0.15/11.03 fof(f3273,plain,(
% 0.15/11.03 ~occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0)|~sQ346_spl|~sQ72_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f3262,f852])).
% 0.15/11.03 fof(f3277,plain,(
% 0.15/11.03 ~sQ298_spl|~sQ346_spl|~sQ72_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f3273,f2855,f3261,f828])).
% 0.15/11.03 fof(f3439,plain,(
% 0.15/11.03 ~arboreal(sK12_skl(sK15_skl))|leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)|~sQ72_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f1007,f846])).
% 0.15/11.03 fof(f3444,definition,(
% 0.15/11.03 sQ377_spl <=> (next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f3445,plain,(
% 0.15/11.03 next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)|~sQ377_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f3444])).
% 0.15/11.03 fof(f3447,plain,(
% 0.15/11.03 ~sQ41_spl|sQ346_spl|sQ377_spl|~sQ72_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f3439,f557,f3261,f3444,f828])).
% 0.15/11.03 fof(f3528,plain,(
% 0.15/11.03 min_precedes(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)|~sQ377_spl),
% 0.15/11.03 inference(resolution,[status(thm)],[f3445,f157])).
% 0.15/11.03 fof(f3536,plain,(
% 0.15/11.03 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|~arboreal(sK15_skl)|leaf_occ(sK15_skl,X0)|sK12_skl(sK12_skl(sK15_skl))=sK13_skl(sK15_skl)|sK12_skl(sK12_skl(sK15_skl))=sK14_skl(sK15_skl)|~sQ377_spl)),
% 0.15/11.03 inference(resolution,[status(thm)],[f3528,f185])).
% 0.15/11.03 fof(f3564,definition,(
% 0.15/11.03 sQ392_spl <=> (sK12_skl(sK12_skl(sK15_skl))=sK13_skl(sK15_skl))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f3565,plain,(
% 0.15/11.03 sK12_skl(sK12_skl(sK15_skl))=sK13_skl(sK15_skl)|~sQ392_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f3564])).
% 0.15/11.03 fof(f3567,definition,(
% 0.15/11.03 sQ393_spl <=> (sK12_skl(sK12_skl(sK15_skl))=sK14_skl(sK15_skl))),
% 0.15/11.03 introduced(definition,[new_symbols(definition,[sQ393_spl])],[split_symbol_definition])).
% 0.15/11.03 fof(f3568,plain,(
% 0.15/11.03 sK12_skl(sK12_skl(sK15_skl))=sK14_skl(sK15_skl)|~sQ393_spl),
% 0.15/11.03 inference(component_clause,[status(thm)],[f3567])).
% 0.15/11.03 fof(f3570,plain,(
% 0.15/11.03 sQ151_spl|~sQ6_spl|sQ392_spl|sQ393_spl|~sQ377_spl),
% 0.15/11.03 inference(split_clause,[status(thm)],[f3536,f1438,f243,f3564,f3567,f3444])).
% 0.15/11.03 fof(f3620,plain,(
% 0.15/11.03 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)|~sQ393_spl|~sQ377_spl),
% 0.15/11.03 inference(forward_demodulation,[status(thm)],[f3568,f3445])).
% 0.15/11.03 fof(f3621,plain,(
% 0.15/11.03 $false|~sQ72_spl|~sQ73_spl|~sQ393_spl|~sQ377_spl),
% 0.15/11.03 inference(forward_subsumption_resolution,[status(thm)],[f3620,f2094])).
% 0.15/11.04 fof(f3622,plain,(
% 0.15/11.04 ~sQ72_spl|~sQ73_spl|~sQ393_spl|~sQ377_spl),
% 0.15/11.04 inference(contradiction_clause,[status(thm)],[f3621])).
% 0.15/11.04 fof(f3875,plain,(
% 0.15/11.04 ~arboreal(sK12_skl(sK15_skl))|leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3)|~sQ72_spl),
% 0.15/11.04 inference(resolution,[status(thm)],[f1009,f846])).
% 0.15/11.04 fof(f3880,definition,(
% 0.15/11.04 sQ434_spl <=> (occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3))),
% 0.15/11.04 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 0.15/11.04 fof(f3881,plain,(
% 0.15/11.04 occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3)|~sQ434_spl),
% 0.15/11.04 inference(component_clause,[status(thm)],[f3880])).
% 0.15/11.04 fof(f3883,plain,(
% 0.15/11.04 ~sQ41_spl|sQ346_spl|sQ434_spl|~sQ72_spl),
% 0.15/11.04 inference(split_clause,[status(thm)],[f3875,f557,f3261,f3880,f828])).
% 0.15/11.04 fof(f3884,plain,(
% 0.15/11.04 occurrence_of(sK13_skl(sK15_skl),tptp3)|~sQ392_spl|~sQ434_spl),
% 0.15/11.04 inference(forward_demodulation,[status(thm)],[f3565,f3881])).
% 0.15/11.04 fof(f3885,plain,(
% 0.15/11.04 tptp3=tptp4|~sQ392_spl|~sQ434_spl|~sQ38_spl),
% 0.15/11.04 inference(resolution,[status(thm)],[f3884,f575])).
% 0.15/11.04 fof(f3900,plain,(
% 0.15/11.04 $false|~sQ392_spl|~sQ434_spl|~sQ38_spl),
% 0.15/11.04 inference(forward_subsumption_resolution,[status(thm)],[f3885,f192])).
% 0.15/11.04 fof(f3901,plain,(
% 0.15/11.04 ~sQ392_spl|~sQ434_spl|~sQ38_spl),
% 0.15/11.04 inference(contradiction_clause,[status(thm)],[f3900])).
% 0.15/11.04 fof(f3902,plain,(
% 0.15/11.04 $false),
% 0.15/11.04 inference(sat_refutation,[status(thm)],[f263,f281,f533,f538,f570,f602,f614,f718,f831,f836,f1562,f1781,f1795,f2865,f3277,f3447,f3570,f3622,f3883,f3901])).
% 0.15/11.04 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/11.06 % Elapsed time: 0.662214 seconds
% 0.15/11.06 % CPU time: 4.991546 seconds
% 0.15/11.06 % Total memory used: 157.871 MB
% 0.15/11.06 % Net memory used: 154.144 MB
%------------------------------------------------------------------------------