%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO014+2 : 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 : n006.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:25 PM UTC 2026
% Result : Theorem 0.15s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n006.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 03:42:27 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 0.15/0.46 % Refutation found
% 0.15/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.46 fof(f1,axiom,(
% 0.15/0.46 (! [X0,X1,X2,X3] :( ( min_precedes(X0,X1,X3)& min_precedes(X1,X2,X3) )=> min_precedes(X0,X2,X3) ) )),
% 0.15/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f5,axiom,(
% 0.15/0.46 (! [X15,X16,X17] :( next_subocc(X15,X16,X17)<=> ( min_precedes(X15,X16,X17)& ~ (? [X18] :( min_precedes(X15,X18,X17)& min_precedes(X18,X16,X17) ) )) ) )),
% 0.15/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f33,axiom,(
% 0.15/0.46 (! [X95,X96] :( ( occurrence_of(X96,tptp0)& subactivity_occurrence(X95,X96)& arboreal(X95)& ~ leaf_occ(X95,X96) )=> (? [X97,X98,X99] :( occurrence_of(X97,tptp3)& next_subocc(X95,X97,tptp0)& occurrence_of(X98,tptp4)& next_subocc(X97,X98,tptp0)& ( occurrence_of(X99,tptp2)| occurrence_of(X99,tptp1) )& next_subocc(X98,X99,tptp0)& leaf(X99,tptp0) ) )) )),
% 0.15/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f46,conjecture,(
% 0.15/0.46 (! [X100,X101] :( ( occurrence_of(X101,tptp0)& subactivity_occurrence(X100,X101)& arboreal(X100)& ~ leaf_occ(X100,X101) )=> (? [X102,X103] :( occurrence_of(X102,tptp3)& next_subocc(X100,X102,tptp0)& ( occurrence_of(X103,tptp2)| occurrence_of(X103,tptp1) )& min_precedes(X102,X103,tptp0)& leaf(X103,tptp0) ) )) )),
% 0.15/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.46 fof(f47,negated_conjecture,(
% 0.15/0.46 ~((! [X100,X101] :( ( occurrence_of(X101,tptp0)& subactivity_occurrence(X100,X101)& arboreal(X100)& ~ leaf_occ(X100,X101) )=> (? [X102,X103] :( occurrence_of(X102,tptp3)& next_subocc(X100,X102,tptp0)& ( occurrence_of(X103,tptp2)| occurrence_of(X103,tptp1) )& min_precedes(X102,X103,tptp0)& leaf(X103,tptp0) ) )) ))),
% 0.15/0.46 inference(negated_conjecture,[status(cth)],[f46])).
% 0.15/0.46 fof(f48,plain,(
% 0.15/0.46 ![X0,X1,X2,X3]: ((~min_precedes(X0,X1,X3)|~min_precedes(X1,X2,X3))|min_precedes(X0,X2,X3))),
% 0.15/0.46 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.15/0.46 fof(f49,plain,(
% 0.15/0.46 ![X0,X2,X3]: ((![X1]: (~min_precedes(X0,X1,X3)|~min_precedes(X1,X2,X3)))|min_precedes(X0,X2,X3))),
% 0.15/0.46 inference(miniscoping,[status(thm)],[f48])).
% 0.15/0.46 fof(f50,plain,(
% 0.15/0.46 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~min_precedes(X1,X3,X2)|min_precedes(X0,X3,X2))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/0.46 fof(f60,plain,(
% 0.15/0.46 ![X15,X16,X17]: (next_subocc(X15,X16,X17)<=>(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))),
% 0.15/0.46 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/0.46 fof(f61,plain,(
% 0.15/0.46 ![X15,X16,X17]: ((~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))&(next_subocc(X15,X16,X17)|(~min_precedes(X15,X16,X17)|(?[X18]: (min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))))),
% 0.15/0.46 inference(NNF_transformation,[status(thm)],[f60])).
% 0.15/0.46 fof(f62,plain,(
% 0.15/0.46 (![X15,X16,X17]: (~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17))))))&(![X15,X16,X17]: (next_subocc(X15,X16,X17)|(~min_precedes(X15,X16,X17)|(?[X18]: (min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))))),
% 0.15/0.46 inference(miniscoping,[status(thm)],[f61])).
% 0.15/0.46 fof(f63,plain,(
% 0.15/0.46 (![X15,X16,X17]: (~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17))))))&(![X15,X16,X17]: (next_subocc(X15,X16,X17)|(~min_precedes(X15,X16,X17)|(min_precedes(X15,sK0_skl(X17,X16,X15),X17)&min_precedes(sK0_skl(X17,X16,X15),X16,X17)))))),
% 0.15/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f62])).
% 0.15/0.46 fof(f64,plain,(
% 0.15/0.46 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f63])).
% 0.15/0.46 fof(f177,plain,(
% 0.15/0.46 ![X95,X96]: ((((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96))|(?[X97,X98,X99]: ((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&next_subocc(X98,X99,tptp0))&leaf(X99,tptp0))))),
% 0.15/0.46 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.15/0.46 fof(f178,plain,(
% 0.15/0.46 ![X95]: ((![X96]: (((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96)))|(?[X99]: ((?[X98]: (((?[X97]: (((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0)))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&next_subocc(X98,X99,tptp0)))&leaf(X99,tptp0))))),
% 0.15/0.46 inference(miniscoping,[status(thm)],[f177])).
% 0.15/0.46 fof(f179,plain,(
% 0.15/0.46 ![X95]: ((![X96]: (((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96)))|((((((occurrence_of(sK16_skl(X95),tptp3)&next_subocc(X95,sK16_skl(X95),tptp0))&occurrence_of(sK15_skl(X95),tptp4))&next_subocc(sK16_skl(X95),sK15_skl(X95),tptp0))&(occurrence_of(sK14_skl(X95),tptp2)|occurrence_of(sK14_skl(X95),tptp1)))&next_subocc(sK15_skl(X95),sK14_skl(X95),tptp0))&leaf(sK14_skl(X95),tptp0)))),
% 0.15/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X99,sK14_skl(X95)),skolemize(X98,sK15_skl(X95)),skolemize(X97,sK16_skl(X95))],[f178])).
% 0.15/0.46 fof(f180,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp3))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/0.46 fof(f181,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK16_skl(X1),tptp0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/0.46 fof(f183,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK16_skl(X1),sK15_skl(X1),tptp0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/0.46 fof(f184,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp2)|occurrence_of(sK14_skl(X1),tptp1))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/0.46 fof(f185,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK15_skl(X1),sK14_skl(X1),tptp0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/0.46 fof(f186,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|leaf(sK14_skl(X1),tptp0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f179])).
% 0.15/0.46 fof(f199,plain,(
% 0.15/0.46 (?[X100,X101]: ((((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&~leaf_occ(X100,X101))&(![X102,X103]: ((((~occurrence_of(X102,tptp3)|~next_subocc(X100,X102,tptp0))|(~occurrence_of(X103,tptp2)&~occurrence_of(X103,tptp1)))|~min_precedes(X102,X103,tptp0))|~leaf(X103,tptp0)))))),
% 0.15/0.46 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.15/0.46 fof(f200,plain,(
% 0.15/0.46 ?[X100]: ((?[X101]: (((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&~leaf_occ(X100,X101)))&(![X103]: ((![X102]: (((~occurrence_of(X102,tptp3)|~next_subocc(X100,X102,tptp0))|(~occurrence_of(X103,tptp2)&~occurrence_of(X103,tptp1)))|~min_precedes(X102,X103,tptp0)))|~leaf(X103,tptp0))))),
% 0.15/0.46 inference(miniscoping,[status(thm)],[f199])).
% 0.15/0.46 fof(f201,plain,(
% 0.15/0.46 ((((occurrence_of(sK18_skl,tptp0)&subactivity_occurrence(sK17_skl,sK18_skl))&arboreal(sK17_skl))&~leaf_occ(sK17_skl,sK18_skl))&(![X103]: ((![X102]: (((~occurrence_of(X102,tptp3)|~next_subocc(sK17_skl,X102,tptp0))|(~occurrence_of(X103,tptp2)&~occurrence_of(X103,tptp1)))|~min_precedes(X102,X103,tptp0)))|~leaf(X103,tptp0))))),
% 0.15/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(X100,sK17_skl),skolemize(X101,sK18_skl)],[f200])).
% 0.15/0.46 fof(f202,plain,(
% 0.15/0.46 occurrence_of(sK18_skl,tptp0)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/0.46 fof(f203,plain,(
% 0.15/0.46 subactivity_occurrence(sK17_skl,sK18_skl)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/0.46 fof(f204,plain,(
% 0.15/0.46 arboreal(sK17_skl)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/0.46 fof(f205,plain,(
% 0.15/0.46 ~leaf_occ(sK17_skl,sK18_skl)),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/0.46 fof(f206,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp3)|~next_subocc(sK17_skl,X0,tptp0)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0)|~leaf(X1,tptp0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/0.46 fof(f207,plain,(
% 0.15/0.46 ![X0,X1]: (~occurrence_of(X0,tptp3)|~next_subocc(sK17_skl,X0,tptp0)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0)|~leaf(X1,tptp0))),
% 0.15/0.46 inference(cnf_transformation,[status(thm)],[f201])).
% 0.15/0.46 fof(f232,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)),
% 0.15/0.46 inference(resolution,[status(thm)],[f203,f185])).
% 0.15/0.46 fof(f233,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK14_skl(sK17_skl),tptp2)|occurrence_of(sK14_skl(sK17_skl),tptp1)),
% 0.15/0.46 inference(resolution,[status(thm)],[f203,f184])).
% 0.15/0.46 fof(f234,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 0.15/0.46 inference(resolution,[status(thm)],[f203,f183])).
% 0.15/0.46 fof(f235,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0)),
% 0.15/0.46 inference(resolution,[status(thm)],[f203,f181])).
% 0.15/0.46 fof(f236,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|leaf(sK14_skl(sK17_skl),tptp0)),
% 0.15/0.46 inference(resolution,[status(thm)],[f203,f186])).
% 0.15/0.46 fof(f238,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK16_skl(sK17_skl),tptp3)),
% 0.15/0.46 inference(resolution,[status(thm)],[f203,f180])).
% 0.15/0.46 fof(f243,definition,(
% 0.15/0.46 sQ3_spl <=> (occurrence_of(sK18_skl,tptp0))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f245,plain,(
% 0.15/0.46 ~occurrence_of(sK18_skl,tptp0)|sQ3_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f243])).
% 0.15/0.46 fof(f246,definition,(
% 0.15/0.46 sQ4_spl <=> (arboreal(sK17_skl))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f248,plain,(
% 0.15/0.46 ~arboreal(sK17_skl)|sQ4_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f246])).
% 0.15/0.46 fof(f249,definition,(
% 0.15/0.46 sQ5_spl <=> (leaf_occ(sK17_skl,sK18_skl))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f250,plain,(
% 0.15/0.46 leaf_occ(sK17_skl,sK18_skl)|~sQ5_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f249])).
% 0.15/0.46 fof(f252,definition,(
% 0.15/0.46 sQ6_spl <=> (next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f253,plain,(
% 0.15/0.46 next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)|~sQ6_spl),
% 0.15/0.46 inference(component_clause,[status(thm)],[f252])).
% 0.15/0.46 fof(f255,plain,(
% 0.15/0.46 ~sQ3_spl|~sQ4_spl|sQ5_spl|sQ6_spl),
% 0.15/0.46 inference(split_clause,[status(thm)],[f232,f243,f246,f249,f252])).
% 0.15/0.46 fof(f256,definition,(
% 0.15/0.46 sQ7_spl <=> (occurrence_of(sK14_skl(sK17_skl),tptp2))),
% 0.15/0.46 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.46 fof(f259,definition,(
% 0.15/0.47 sQ8_spl <=> (occurrence_of(sK14_skl(sK17_skl),tptp1))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f262,plain,(
% 0.15/0.47 ~sQ3_spl|~sQ4_spl|sQ5_spl|sQ7_spl|sQ8_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f233,f243,f246,f249,f256,f259])).
% 0.15/0.47 fof(f263,definition,(
% 0.15/0.47 sQ9_spl <=> (next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f264,plain,(
% 0.15/0.47 next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)|~sQ9_spl),
% 0.15/0.47 inference(component_clause,[status(thm)],[f263])).
% 0.15/0.47 fof(f266,plain,(
% 0.15/0.47 ~sQ3_spl|~sQ4_spl|sQ5_spl|sQ9_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f234,f243,f246,f249,f263])).
% 0.15/0.47 fof(f267,definition,(
% 0.15/0.47 sQ10_spl <=> (next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f268,plain,(
% 0.15/0.47 next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0)|~sQ10_spl),
% 0.15/0.47 inference(component_clause,[status(thm)],[f267])).
% 0.15/0.47 fof(f270,plain,(
% 0.15/0.47 ~sQ3_spl|~sQ4_spl|sQ5_spl|sQ10_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f235,f243,f246,f249,f267])).
% 0.15/0.47 fof(f271,definition,(
% 0.15/0.47 sQ11_spl <=> (leaf(sK14_skl(sK17_skl),tptp0))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f274,plain,(
% 0.15/0.47 ~sQ3_spl|~sQ4_spl|sQ5_spl|sQ11_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f236,f243,f246,f249,f271])).
% 0.15/0.47 fof(f279,definition,(
% 0.15/0.47 sQ13_spl <=> (occurrence_of(sK16_skl(sK17_skl),tptp3))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f282,plain,(
% 0.15/0.47 ~sQ3_spl|~sQ4_spl|sQ5_spl|sQ13_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f238,f243,f246,f249,f279])).
% 0.15/0.47 fof(f296,plain,(
% 0.15/0.47 $false|sQ4_spl),
% 0.15/0.47 inference(forward_subsumption_resolution,[status(thm)],[f248,f204])).
% 0.15/0.47 fof(f297,plain,(
% 0.15/0.47 sQ4_spl),
% 0.15/0.47 inference(contradiction_clause,[status(thm)],[f296])).
% 0.15/0.47 fof(f298,plain,(
% 0.15/0.47 $false|~sQ5_spl),
% 0.15/0.47 inference(forward_subsumption_resolution,[status(thm)],[f250,f205])).
% 0.15/0.47 fof(f299,plain,(
% 0.15/0.47 ~sQ5_spl),
% 0.15/0.47 inference(contradiction_clause,[status(thm)],[f298])).
% 0.15/0.47 fof(f301,plain,(
% 0.15/0.47 $false|sQ3_spl),
% 0.15/0.47 inference(forward_subsumption_resolution,[status(thm)],[f245,f202])).
% 0.15/0.47 fof(f302,plain,(
% 0.15/0.47 sQ3_spl),
% 0.15/0.47 inference(contradiction_clause,[status(thm)],[f301])).
% 0.15/0.47 fof(f535,plain,(
% 0.15/0.47 ![X0]: (~occurrence_of(sK16_skl(sK17_skl),tptp3)|~occurrence_of(X0,tptp2)|~min_precedes(sK16_skl(sK17_skl),X0,tptp0)|~leaf(X0,tptp0)|~sQ10_spl)),
% 0.15/0.47 inference(resolution,[status(thm)],[f206,f268])).
% 0.15/0.47 fof(f536,definition,(
% 0.15/0.47 ![X0]: (sQ67_spl <=> (~occurrence_of(X0,tptp2)|~min_precedes(sK16_skl(sK17_skl),X0,tptp0)|~leaf(X0,tptp0)))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f537,plain,(
% 0.15/0.47 ![X0]: (~occurrence_of(X0,tptp2)|~min_precedes(sK16_skl(sK17_skl),X0,tptp0)|~leaf(X0,tptp0)|~sQ67_spl)),
% 0.15/0.47 inference(component_clause,[status(thm)],[f536])).
% 0.15/0.47 fof(f539,plain,(
% 0.15/0.47 ~sQ13_spl|sQ67_spl|~sQ10_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f535,f279,f536,f267])).
% 0.15/0.47 fof(f540,plain,(
% 0.15/0.47 ![X0]: (~occurrence_of(sK16_skl(sK17_skl),tptp3)|~occurrence_of(X0,tptp1)|~min_precedes(sK16_skl(sK17_skl),X0,tptp0)|~leaf(X0,tptp0)|~sQ10_spl)),
% 0.15/0.47 inference(resolution,[status(thm)],[f207,f268])).
% 0.15/0.47 fof(f541,definition,(
% 0.15/0.47 ![X0]: (sQ68_spl <=> (~occurrence_of(X0,tptp1)|~min_precedes(sK16_skl(sK17_skl),X0,tptp0)|~leaf(X0,tptp0)))),
% 0.15/0.47 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.15/0.47 fof(f542,plain,(
% 0.15/0.47 ![X0]: (~occurrence_of(X0,tptp1)|~min_precedes(sK16_skl(sK17_skl),X0,tptp0)|~leaf(X0,tptp0)|~sQ68_spl)),
% 0.15/0.47 inference(component_clause,[status(thm)],[f541])).
% 0.15/0.47 fof(f544,plain,(
% 0.15/0.47 ~sQ13_spl|sQ68_spl|~sQ10_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f540,f279,f541,f267])).
% 0.15/0.47 fof(f546,plain,(
% 0.15/0.47 min_precedes(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)|~sQ6_spl),
% 0.15/0.47 inference(resolution,[status(thm)],[f253,f64])).
% 0.15/0.47 fof(f548,plain,(
% 0.15/0.47 min_precedes(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)|~sQ9_spl),
% 0.15/0.47 inference(resolution,[status(thm)],[f264,f64])).
% 0.15/0.47 fof(f642,plain,(
% 0.15/0.47 ![X0]: (~min_precedes(X0,sK15_skl(sK17_skl),tptp0)|min_precedes(X0,sK14_skl(sK17_skl),tptp0)|~sQ6_spl)),
% 0.15/0.47 inference(resolution,[status(thm)],[f546,f50])).
% 0.15/0.47 fof(f978,plain,(
% 0.15/0.47 min_precedes(sK16_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)|~sQ6_spl|~sQ9_spl),
% 0.15/0.47 inference(resolution,[status(thm)],[f642,f548])).
% 0.15/0.47 fof(f1311,plain,(
% 0.15/0.47 ~occurrence_of(sK14_skl(sK17_skl),tptp1)|~leaf(sK14_skl(sK17_skl),tptp0)|~sQ6_spl|~sQ9_spl|~sQ68_spl),
% 0.15/0.47 inference(resolution,[status(thm)],[f978,f542])).
% 0.15/0.47 fof(f1312,plain,(
% 0.15/0.47 ~occurrence_of(sK14_skl(sK17_skl),tptp2)|~leaf(sK14_skl(sK17_skl),tptp0)|~sQ6_spl|~sQ9_spl|~sQ67_spl),
% 0.15/0.47 inference(resolution,[status(thm)],[f978,f537])).
% 0.15/0.47 fof(f1319,plain,(
% 0.15/0.47 ~sQ8_spl|~sQ11_spl|~sQ6_spl|~sQ9_spl|~sQ68_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f1311,f259,f271,f252,f263,f541])).
% 0.15/0.47 fof(f1320,plain,(
% 0.15/0.47 ~sQ7_spl|~sQ11_spl|~sQ6_spl|~sQ9_spl|~sQ67_spl),
% 0.15/0.47 inference(split_clause,[status(thm)],[f1312,f256,f271,f252,f263,f536])).
% 0.15/0.47 fof(f1333,plain,(
% 0.15/0.47 $false),
% 0.15/0.47 inference(sat_refutation,[status(thm)],[f255,f262,f266,f270,f274,f282,f297,f299,f302,f539,f544,f1319,f1320])).
% 0.15/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.50 % Elapsed time: 0.120613 seconds
% 0.15/0.50 % CPU time: 0.692185 seconds
% 0.15/0.50 % Total memory used: 88.668 MB
% 0.15/0.50 % Net memory used: 88.309 MB
%------------------------------------------------------------------------------