%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO018+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 : n017.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 27.77s 4.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO018+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.11/0.55 % Computer : n017.cluster.edu
% 0.11/0.55 % Model : x86_64 x86_64
% 0.11/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.55 % Memory : 8046.5625MB
% 0.11/0.55 % OS : Linux 6.8.0-71-generic
% 0.11/0.55 % CPULimit : 300
% 0.11/0.55 % WCLimit : 300
% 0.11/0.55 % DateTime : Mon Sep 21 03:39:12 UTC 2026
% 0.11/0.55 % CPUTime :
% 0.11/0.57 % Drodi V4.1.1
% 27.77/4.18 % Refutation found
% 27.77/4.18 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.77/4.18 % SZS output start CNFRefutation for theBenchmark
% 27.77/4.18 fof(f7,axiom,(
% 27.77/4.18 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f9,axiom,(
% 27.77/4.18 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f10,axiom,(
% 27.77/4.18 (! [X31,X32,X33] :( ( occurrence_of(X31,X33)& leaf_occ(X32,X31) )=> ~ (? [X34] : min_precedes(X32,X34,X33) )) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f17,axiom,(
% 27.77/4.18 (! [X51,X52] :( occurrence_of(X51,X52)=> ( arboreal(X51)<=> atomic(X52) ) ) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f27,axiom,(
% 27.77/4.18 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f33,axiom,(
% 27.77/4.18 (! [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,tptp1)| occurrence_of(X105,tptp2) )& min_precedes(X104,X105,tptp0)& (! [X106] :( min_precedes(X103,X106,tptp0)=> ( X106 = X104| X106 = X105 ) ) )) )) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f36,axiom,(
% 27.77/4.18 atomic(tptp4) ),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f39,axiom,(
% 27.77/4.18 atomic(tptp3) ),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f40,axiom,(
% 27.77/4.18 tptp4 != tptp3 ),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f46,conjecture,(
% 27.77/4.18 (! [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,tptp1)| occurrence_of(X110,tptp2) )& min_precedes(X109,X110,tptp0)& leaf_occ(X110,X108)& ( occurrence_of(X110,tptp1)=> ~ (? [X111] :( occurrence_of(X111,tptp2)& min_precedes(X109,X111,tptp0) ) ))& ( occurrence_of(X110,tptp2)=> ~ (? [X112] :( occurrence_of(X112,tptp1)& min_precedes(X109,X112,tptp0) ) )) ) )) )),
% 27.77/4.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.77/4.18 fof(f47,negated_conjecture,(
% 27.77/4.18 ~((! [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,tptp1)| occurrence_of(X110,tptp2) )& min_precedes(X109,X110,tptp0)& leaf_occ(X110,X108)& ( occurrence_of(X110,tptp1)=> ~ (? [X111] :( occurrence_of(X111,tptp2)& min_precedes(X109,X111,tptp0) ) ))& ( occurrence_of(X110,tptp2)=> ~ (? [X112] :( occurrence_of(X112,tptp1)& min_precedes(X109,X112,tptp0) ) )) ) )) ))),
% 27.77/4.18 inference(negated_conjecture,[status(cth)],[f46])).
% 27.77/4.18 fof(f68,plain,(
% 27.77/4.18 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 27.77/4.18 fof(f69,plain,(
% 27.77/4.18 ![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))))),
% 27.77/4.18 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f68])).
% 27.77/4.18 fof(f70,plain,(
% 27.77/4.18 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f69])).
% 27.77/4.18 fof(f71,plain,(
% 27.77/4.18 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f69])).
% 27.77/4.18 fof(f77,plain,(
% 27.77/4.18 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 27.77/4.18 fof(f78,plain,(
% 27.77/4.18 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 27.77/4.18 inference(miniscoping,[status(thm)],[f77])).
% 27.77/4.18 fof(f79,plain,(
% 27.77/4.18 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f78])).
% 27.77/4.18 fof(f80,plain,(
% 27.77/4.18 ![X31,X32,X33]: ((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 27.77/4.18 fof(f81,plain,(
% 27.77/4.18 ![X32,X33]: ((![X31]: (~occurrence_of(X31,X33)|~leaf_occ(X32,X31)))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 27.77/4.18 inference(miniscoping,[status(thm)],[f80])).
% 27.77/4.18 fof(f82,plain,(
% 27.77/4.18 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f81])).
% 27.77/4.18 fof(f110,plain,(
% 27.77/4.18 ![X51,X52]: (~occurrence_of(X51,X52)|(arboreal(X51)<=>atomic(X52)))),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 27.77/4.18 fof(f111,plain,(
% 27.77/4.18 ![X51,X52]: (~occurrence_of(X51,X52)|((~arboreal(X51)|atomic(X52))&(arboreal(X51)|~atomic(X52))))),
% 27.77/4.18 inference(NNF_transformation,[status(thm)],[f110])).
% 27.77/4.18 fof(f113,plain,(
% 27.77/4.18 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f111])).
% 27.77/4.18 fof(f153,plain,(
% 27.77/4.18 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 27.77/4.18 fof(f154,plain,(
% 27.77/4.18 ![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))))))),
% 27.77/4.18 inference(NNF_transformation,[status(thm)],[f153])).
% 27.77/4.18 fof(f155,plain,(
% 27.77/4.18 (![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))))))),
% 27.77/4.18 inference(miniscoping,[status(thm)],[f154])).
% 27.77/4.18 fof(f156,plain,(
% 27.77/4.18 (![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)))))),
% 27.77/4.18 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f155])).
% 27.77/4.18 fof(f157,plain,(
% 27.77/4.18 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f156])).
% 27.77/4.18 fof(f158,plain,(
% 27.77/4.18 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f156])).
% 27.77/4.18 fof(f176,plain,(
% 27.77/4.18 ![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,tptp1)|occurrence_of(X105,tptp2)))&min_precedes(X104,X105,tptp0))&(![X106]: (~min_precedes(X103,X106,tptp0)|(X106=X104|X106=X105))))))),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 27.77/4.18 fof(f177,plain,(
% 27.77/4.18 ![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,tptp1)|occurrence_of(X105,tptp2)))&min_precedes(X104,X105,tptp0))&(![X106]: (~min_precedes(X103,X106,tptp0)|(X106=X104|X106=X105))))))),
% 27.77/4.18 inference(miniscoping,[status(thm)],[f176])).
% 27.77/4.18 fof(f178,plain,(
% 27.77/4.18 ![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),tptp1)|occurrence_of(sK14_skl(X101),tptp2)))&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))))))),
% 27.77/4.18 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])).
% 27.77/4.18 fof(f179,plain,(
% 27.77/4.18 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK12_skl(X1),tptp3))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f178])).
% 27.77/4.18 fof(f180,plain,(
% 27.77/4.18 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK12_skl(X1),tptp0))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f178])).
% 27.77/4.18 fof(f181,plain,(
% 27.77/4.18 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK13_skl(X1),tptp4))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f178])).
% 27.77/4.18 fof(f182,plain,(
% 27.77/4.18 ![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))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f178])).
% 27.77/4.18 fof(f184,plain,(
% 27.77/4.18 ![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))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f178])).
% 27.77/4.18 fof(f185,plain,(
% 27.77/4.18 ![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))),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f178])).
% 27.77/4.18 fof(f188,plain,(
% 27.77/4.18 atomic(tptp4)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f36])).
% 27.77/4.18 fof(f191,plain,(
% 27.77/4.18 atomic(tptp3)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f39])).
% 27.77/4.18 fof(f192,plain,(
% 27.77/4.18 ~tptp4=tptp3),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f40])).
% 27.77/4.18 fof(f198,plain,(
% 27.77/4.18 (?[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,tptp1)&~occurrence_of(X110,tptp2)))|~min_precedes(X109,X110,tptp0))|~leaf_occ(X110,X108))|(occurrence_of(X110,tptp1)&(?[X111]: (occurrence_of(X111,tptp2)&min_precedes(X109,X111,tptp0)))))|(occurrence_of(X110,tptp2)&(?[X112]: (occurrence_of(X112,tptp1)&min_precedes(X109,X112,tptp0))))))))),
% 27.77/4.18 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 27.77/4.18 fof(f199,definition,(
% 27.77/4.18 ![X110]: (sP0_prd(X110)<=>(~occurrence_of(X110,tptp1)&~occurrence_of(X110,tptp2)))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 27.77/4.18 fof(f200,definition,(
% 27.77/4.18 ![X109,X110]: (sP1_prd(X110,X109)<=>(occurrence_of(X110,tptp1)&(?[X111]: (occurrence_of(X111,tptp2)&min_precedes(X109,X111,tptp0)))))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 27.77/4.18 fof(f201,plain,(
% 27.77/4.18 ?[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))|sP0_prd(X110))|~min_precedes(X109,X110,tptp0))|~leaf_occ(X110,X108))|sP1_prd(X110,X109))|(occurrence_of(X110,tptp2)&(?[X112]: (occurrence_of(X112,tptp1)&min_precedes(X109,X112,tptp0)))))))),
% 27.77/4.18 inference(formula_renaming,[status(thm)],[f198,f200,f199])).
% 27.77/4.18 fof(f202,plain,(
% 27.77/4.18 ((((occurrence_of(sK16_skl,tptp0)&subactivity_occurrence(sK15_skl,sK16_skl))&arboreal(sK15_skl))&~leaf_occ(sK15_skl,sK16_skl))&(![X109,X110]: ((((((~occurrence_of(X109,tptp3)|~next_subocc(sK15_skl,X109,tptp0))|sP0_prd(X110))|~min_precedes(X109,X110,tptp0))|~leaf_occ(X110,sK16_skl))|sP1_prd(X110,X109))|(occurrence_of(X110,tptp2)&(occurrence_of(sK17_skl(X110,X109),tptp1)&min_precedes(X109,sK17_skl(X110,X109),tptp0))))))),
% 27.77/4.18 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X107,sK15_skl),skolemize(X108,sK16_skl),skolemize(X112,sK17_skl(X110,X109))],[f201])).
% 27.77/4.18 fof(f203,plain,(
% 27.77/4.18 occurrence_of(sK16_skl,tptp0)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f202])).
% 27.77/4.18 fof(f204,plain,(
% 27.77/4.18 subactivity_occurrence(sK15_skl,sK16_skl)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f202])).
% 27.77/4.18 fof(f205,plain,(
% 27.77/4.18 arboreal(sK15_skl)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f202])).
% 27.77/4.18 fof(f206,plain,(
% 27.77/4.18 ~leaf_occ(sK15_skl,sK16_skl)),
% 27.77/4.18 inference(cnf_transformation,[status(thm)],[f202])).
% 27.77/4.18 fof(f308,definition,(
% 27.77/4.18 sQ14_spl <=> (arboreal(sK15_skl))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f310,plain,(
% 27.77/4.18 ~arboreal(sK15_skl)|sQ14_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f308])).
% 27.77/4.18 fof(f343,plain,(
% 27.77/4.18 $false|sQ14_spl),
% 27.77/4.18 inference(forward_subsumption_resolution,[status(thm)],[f310,f205])).
% 27.77/4.18 fof(f344,plain,(
% 27.77/4.18 sQ14_spl),
% 27.77/4.18 inference(contradiction_clause,[status(thm)],[f343])).
% 27.77/4.18 fof(f352,definition,(
% 27.77/4.18 sQ21_spl <=> (leaf_occ(sK15_skl,sK16_skl))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f353,plain,(
% 27.77/4.18 leaf_occ(sK15_skl,sK16_skl)|~sQ21_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f352])).
% 27.77/4.18 fof(f356,plain,(
% 27.77/4.18 $false|~sQ21_spl),
% 27.77/4.18 inference(forward_subsumption_resolution,[status(thm)],[f353,f206])).
% 27.77/4.18 fof(f357,plain,(
% 27.77/4.18 ~sQ21_spl),
% 27.77/4.18 inference(contradiction_clause,[status(thm)],[f356])).
% 27.77/4.18 fof(f699,plain,(
% 27.77/4.18 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|occurrence_of(sK13_skl(X0),tptp4))),
% 27.77/4.18 inference(resolution,[status(thm)],[f181,f203])).
% 27.77/4.18 fof(f700,plain,(
% 27.77/4.18 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|occurrence_of(sK12_skl(X0),tptp3))),
% 27.77/4.18 inference(resolution,[status(thm)],[f179,f203])).
% 27.77/4.18 fof(f701,plain,(
% 27.77/4.18 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(X0,sK12_skl(X0),tptp0))),
% 27.77/4.18 inference(resolution,[status(thm)],[f180,f203])).
% 27.77/4.18 fof(f702,plain,(
% 27.77/4.18 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|min_precedes(sK13_skl(X0),sK14_skl(X0),tptp0))),
% 27.77/4.18 inference(resolution,[status(thm)],[f184,f203])).
% 27.77/4.18 fof(f847,plain,(
% 27.77/4.18 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|min_precedes(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 27.77/4.18 inference(resolution,[status(thm)],[f182,f203])).
% 27.77/4.18 fof(f1336,plain,(
% 27.77/4.18 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK13_skl(sK15_skl),tptp4)),
% 27.77/4.18 inference(resolution,[status(thm)],[f699,f204])).
% 27.77/4.18 fof(f1337,definition,(
% 27.77/4.18 sQ113_spl <=> (occurrence_of(sK13_skl(sK15_skl),tptp4))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1338,plain,(
% 27.77/4.18 occurrence_of(sK13_skl(sK15_skl),tptp4)|~sQ113_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1337])).
% 27.77/4.18 fof(f1340,plain,(
% 27.77/4.18 ~sQ14_spl|sQ21_spl|sQ113_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f1336,f308,f352,f1337])).
% 27.77/4.18 fof(f1341,plain,(
% 27.77/4.18 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK12_skl(sK15_skl),tptp3)),
% 27.77/4.18 inference(resolution,[status(thm)],[f700,f204])).
% 27.77/4.18 fof(f1342,definition,(
% 27.77/4.18 sQ114_spl <=> (occurrence_of(sK12_skl(sK15_skl),tptp3))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1343,plain,(
% 27.77/4.18 occurrence_of(sK12_skl(sK15_skl),tptp3)|~sQ114_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1342])).
% 27.77/4.18 fof(f1345,plain,(
% 27.77/4.18 ~sQ14_spl|sQ21_spl|sQ114_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f1341,f308,f352,f1342])).
% 27.77/4.18 fof(f1355,plain,(
% 27.77/4.18 ![X0]: (~occurrence_of(sK13_skl(sK15_skl),X0)|X0=tptp4|~sQ113_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f1338,f79])).
% 27.77/4.18 fof(f1372,definition,(
% 27.77/4.18 sQ118_spl <=> (atomic(tptp4))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1374,plain,(
% 27.77/4.18 ~atomic(tptp4)|sQ118_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1372])).
% 27.77/4.18 fof(f1402,plain,(
% 27.77/4.18 arboreal(sK12_skl(sK15_skl))|~atomic(tptp3)|~sQ114_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f1343,f113])).
% 27.77/4.18 fof(f1423,definition,(
% 27.77/4.18 sQ127_spl <=> (atomic(tptp3))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1425,plain,(
% 27.77/4.18 ~atomic(tptp3)|sQ127_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1423])).
% 27.77/4.18 fof(f1430,definition,(
% 27.77/4.18 sQ129_spl <=> (arboreal(sK12_skl(sK15_skl)))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1433,plain,(
% 27.77/4.18 sQ129_spl|~sQ127_spl|~sQ114_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f1402,f1430,f1423,f1342])).
% 27.77/4.18 fof(f1467,plain,(
% 27.77/4.18 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0)),
% 27.77/4.18 inference(resolution,[status(thm)],[f701,f204])).
% 27.77/4.18 fof(f1468,definition,(
% 27.77/4.18 sQ133_spl <=> (next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1469,plain,(
% 27.77/4.18 next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0)|~sQ133_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1468])).
% 27.77/4.18 fof(f1471,plain,(
% 27.77/4.18 ~sQ14_spl|sQ21_spl|sQ133_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f1467,f308,f352,f1468])).
% 27.77/4.18 fof(f1496,plain,(
% 27.77/4.18 min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)|~sQ133_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f1469,f157])).
% 27.77/4.18 fof(f1517,plain,(
% 27.77/4.18 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK15_skl,X0)|~sQ133_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f1496,f82])).
% 27.77/4.18 fof(f1583,plain,(
% 27.77/4.18 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)),
% 27.77/4.18 inference(resolution,[status(thm)],[f702,f204])).
% 27.77/4.18 fof(f1584,definition,(
% 27.77/4.18 sQ148_spl <=> (min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1585,plain,(
% 27.77/4.18 min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)|~sQ148_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1584])).
% 27.77/4.18 fof(f1587,plain,(
% 27.77/4.18 ~sQ14_spl|sQ21_spl|sQ148_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f1583,f308,f352,f1584])).
% 27.77/4.18 fof(f1588,plain,(
% 27.77/4.18 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 27.77/4.18 inference(resolution,[status(thm)],[f847,f204])).
% 27.77/4.18 fof(f1589,definition,(
% 27.77/4.18 sQ149_spl <=> (min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1590,plain,(
% 27.77/4.18 min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)|~sQ149_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1589])).
% 27.77/4.18 fof(f1592,plain,(
% 27.77/4.18 ~sQ14_spl|sQ21_spl|sQ149_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f1588,f308,f352,f1589])).
% 27.77/4.18 fof(f1712,plain,(
% 27.77/4.18 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|~sQ149_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f1590,f71])).
% 27.77/4.18 fof(f1713,plain,(
% 27.77/4.18 occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0)|~sQ149_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f1590,f70])).
% 27.77/4.18 fof(f1718,plain,(
% 27.77/4.18 ![X0]: (~next_subocc(sK12_skl(sK15_skl),X0,tptp0)|~min_precedes(sK13_skl(sK15_skl),X0,tptp0)|~sQ149_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f1590,f158])).
% 27.77/4.18 fof(f1719,plain,(
% 27.77/4.18 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK12_skl(sK15_skl),X0)|~sQ149_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f1590,f82])).
% 27.77/4.18 fof(f1723,definition,(
% 27.77/4.18 ![X0]: (sQ166_spl <=> (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|leaf_occ(sK15_skl,X0)))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f1724,plain,(
% 27.77/4.18 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|leaf_occ(sK15_skl,X0)|~sQ166_spl)),
% 27.77/4.18 inference(component_clause,[status(thm)],[f1723])).
% 27.77/4.18 fof(f1804,plain,(
% 27.77/4.18 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK15_skl,X0)|~sQ133_spl|~sQ166_spl)),
% 27.77/4.18 inference(forward_subsumption_resolution,[status(thm)],[f1724,f1517])).
% 27.77/4.18 fof(f1815,plain,(
% 27.77/4.18 ~subactivity_occurrence(sK15_skl,sK16_skl)|~sQ133_spl|~sQ166_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f1804,f203])).
% 27.77/4.18 fof(f1816,plain,(
% 27.77/4.18 $false|~sQ133_spl|~sQ166_spl),
% 27.77/4.18 inference(forward_subsumption_resolution,[status(thm)],[f1815,f204])).
% 27.77/4.18 fof(f1817,plain,(
% 27.77/4.18 ~sQ133_spl|~sQ166_spl),
% 27.77/4.18 inference(contradiction_clause,[status(thm)],[f1816])).
% 27.77/4.18 fof(f2047,plain,(
% 27.77/4.18 ![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)|~sQ149_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f1713,f180])).
% 27.77/4.18 fof(f2048,plain,(
% 27.77/4.18 ![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)|~sQ149_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f1713,f179])).
% 27.77/4.18 fof(f2222,definition,(
% 27.77/4.18 sQ224_spl <=> (leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f2223,plain,(
% 27.77/4.18 leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0))|~sQ224_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f2222])).
% 27.77/4.18 fof(f6873,plain,(
% 27.77/4.18 ~next_subocc(sK12_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)|~sQ149_spl|~sQ148_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f1718,f1585])).
% 27.77/4.18 fof(f12365,definition,(
% 27.77/4.18 sQ1222_spl <=> (occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ1222_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f12367,plain,(
% 27.77/4.18 ~occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0)|sQ1222_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f12365])).
% 27.77/4.18 fof(f12374,plain,(
% 27.77/4.18 $false|~sQ149_spl|sQ1222_spl),
% 27.77/4.18 inference(forward_subsumption_resolution,[status(thm)],[f12367,f1713])).
% 27.77/4.18 fof(f12375,plain,(
% 27.77/4.18 ~sQ149_spl|sQ1222_spl),
% 27.77/4.18 inference(contradiction_clause,[status(thm)],[f12374])).
% 27.77/4.18 fof(f19520,plain,(
% 27.77/4.18 ~occurrence_of(sK2_skl(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),tptp0)|~sQ224_spl|~sQ149_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f2223,f1719])).
% 27.77/4.18 fof(f19524,plain,(
% 27.77/4.18 ~sQ1222_spl|~sQ224_spl|~sQ149_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f19520,f12365,f2222,f1589])).
% 27.77/4.18 fof(f19526,plain,(
% 27.77/4.18 ~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)|~sQ149_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f2047,f1712])).
% 27.77/4.18 fof(f19531,definition,(
% 27.77/4.18 sQ1766_spl <=> (next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ1766_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f19532,plain,(
% 27.77/4.18 next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)|~sQ1766_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f19531])).
% 27.77/4.18 fof(f19534,plain,(
% 27.77/4.18 ~sQ129_spl|sQ224_spl|sQ1766_spl|~sQ149_spl),
% 27.77/4.18 inference(split_clause,[status(thm)],[f19526,f1430,f2222,f19531,f1589])).
% 27.77/4.18 fof(f19559,plain,(
% 27.77/4.18 min_precedes(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)|~sQ1766_spl),
% 27.77/4.18 inference(resolution,[status(thm)],[f19532,f157])).
% 27.77/4.18 fof(f19567,plain,(
% 27.77/4.18 ![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)|~sQ1766_spl)),
% 27.77/4.18 inference(resolution,[status(thm)],[f19559,f185])).
% 27.77/4.18 fof(f19597,definition,(
% 27.77/4.18 sQ1769_spl <=> (sK12_skl(sK12_skl(sK15_skl))=sK13_skl(sK15_skl))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ1769_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f19598,plain,(
% 27.77/4.18 sK12_skl(sK12_skl(sK15_skl))=sK13_skl(sK15_skl)|~sQ1769_spl),
% 27.77/4.18 inference(component_clause,[status(thm)],[f19597])).
% 27.77/4.18 fof(f19600,definition,(
% 27.77/4.18 sQ1770_spl <=> (sK12_skl(sK12_skl(sK15_skl))=sK14_skl(sK15_skl))),
% 27.77/4.18 introduced(definition,[new_symbols(definition,[sQ1770_spl])],[split_symbol_definition])).
% 27.77/4.18 fof(f19601,plain,(
% 27.77/4.18 sK12_skl(sK12_skl(sK15_skl))=sK14_skl(sK15_skl)|~sQ1770_spl),
% 27.77/4.21 inference(component_clause,[status(thm)],[f19600])).
% 27.77/4.21 fof(f19603,plain,(
% 27.77/4.21 sQ166_spl|~sQ14_spl|sQ1769_spl|sQ1770_spl|~sQ1766_spl),
% 27.77/4.21 inference(split_clause,[status(thm)],[f19567,f1723,f308,f19597,f19600,f19531])).
% 27.77/4.21 fof(f19670,plain,(
% 27.77/4.21 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)|~sQ1770_spl|~sQ1766_spl),
% 27.77/4.21 inference(forward_demodulation,[status(thm)],[f19601,f19532])).
% 27.77/4.21 fof(f19671,plain,(
% 27.77/4.21 $false|~sQ149_spl|~sQ148_spl|~sQ1770_spl|~sQ1766_spl),
% 27.77/4.21 inference(forward_subsumption_resolution,[status(thm)],[f19670,f6873])).
% 27.77/4.21 fof(f19672,plain,(
% 27.77/4.21 ~sQ149_spl|~sQ148_spl|~sQ1770_spl|~sQ1766_spl),
% 27.77/4.21 inference(contradiction_clause,[status(thm)],[f19671])).
% 27.77/4.21 fof(f19719,plain,(
% 27.77/4.21 $false|sQ127_spl),
% 27.77/4.21 inference(forward_subsumption_resolution,[status(thm)],[f1425,f191])).
% 27.77/4.21 fof(f19720,plain,(
% 27.77/4.21 sQ127_spl),
% 27.77/4.21 inference(contradiction_clause,[status(thm)],[f19719])).
% 27.77/4.21 fof(f20238,plain,(
% 27.77/4.21 $false|sQ118_spl),
% 27.77/4.21 inference(forward_subsumption_resolution,[status(thm)],[f1374,f188])).
% 27.77/4.21 fof(f20239,plain,(
% 27.77/4.21 sQ118_spl),
% 27.77/4.21 inference(contradiction_clause,[status(thm)],[f20238])).
% 27.77/4.21 fof(f20676,plain,(
% 27.77/4.21 ~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)|~sQ149_spl),
% 27.77/4.21 inference(resolution,[status(thm)],[f2048,f1712])).
% 27.77/4.21 fof(f20678,definition,(
% 27.77/4.21 sQ1863_spl <=> (occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3))),
% 27.77/4.21 introduced(definition,[new_symbols(definition,[sQ1863_spl])],[split_symbol_definition])).
% 27.77/4.21 fof(f20679,plain,(
% 27.77/4.21 occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3)|~sQ1863_spl),
% 27.77/4.21 inference(component_clause,[status(thm)],[f20678])).
% 27.77/4.21 fof(f20681,plain,(
% 27.77/4.21 ~sQ129_spl|sQ224_spl|sQ1863_spl|~sQ149_spl),
% 27.77/4.21 inference(split_clause,[status(thm)],[f20676,f1430,f2222,f20678,f1589])).
% 27.77/4.21 fof(f20682,plain,(
% 27.77/4.21 occurrence_of(sK13_skl(sK15_skl),tptp3)|~sQ1769_spl|~sQ1863_spl),
% 27.77/4.21 inference(forward_demodulation,[status(thm)],[f19598,f20679])).
% 27.77/4.21 fof(f20705,plain,(
% 27.77/4.21 tptp3=tptp4|~sQ1769_spl|~sQ1863_spl|~sQ113_spl),
% 27.77/4.21 inference(resolution,[status(thm)],[f20682,f1355])).
% 27.77/4.21 fof(f20721,plain,(
% 27.77/4.21 $false|~sQ1769_spl|~sQ1863_spl|~sQ113_spl),
% 27.77/4.21 inference(forward_subsumption_resolution,[status(thm)],[f20705,f192])).
% 27.77/4.21 fof(f20722,plain,(
% 27.77/4.21 ~sQ1769_spl|~sQ1863_spl|~sQ113_spl),
% 27.77/4.21 inference(contradiction_clause,[status(thm)],[f20721])).
% 27.77/4.21 fof(f20723,plain,(
% 27.77/4.21 $false),
% 27.77/4.21 inference(sat_refutation,[status(thm)],[f344,f357,f1340,f1345,f1433,f1471,f1587,f1592,f1817,f12375,f19524,f19534,f19603,f19672,f19720,f20239,f20681,f20722])).
% 27.77/4.21 % SZS output end CNFRefutation for theBenchmark.p
% 16.44/4.27 % Elapsed time: 3.701211 seconds
% 16.44/4.27 % CPU time: 28.870920 seconds
% 16.44/4.27 % Total memory used: 249.436 MB
% 16.44/4.27 % Net memory used: 239.919 MB
%------------------------------------------------------------------------------