%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO017+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:59:26 PM UTC 2026
% Result : Theorem 12.96s 2.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO017+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n007.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 03:41:39 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 12.96/2.22 % Refutation found
% 12.96/2.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.96/2.22 % SZS output start CNFRefutation for theBenchmark
% 12.96/2.22 fof(f5,axiom,(
% 12.96/2.22 (! [X15,X16,X17] :( next_subocc(X15,X16,X17)<=> ( min_precedes(X15,X16,X17)& ~ (? [X18] :( min_precedes(X15,X18,X17)& min_precedes(X18,X16,X17) ) )) ) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f14,axiom,(
% 12.96/2.22 (! [X40,X41] :( occurrence_of(X40,X41)=> ( arboreal(X40)<=> atomic(X41) ) ) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f22,axiom,(
% 12.96/2.22 (! [X60,X61,X62] :( ( occurrence_of(X60,X62)& leaf_occ(X61,X60) )=> ~ (? [X63] : min_precedes(X61,X63,X62) )) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f23,axiom,(
% 12.96/2.22 (! [X64,X65,X66] :( ( occurrence_of(X64,X65)& occurrence_of(X64,X66) )=> X65 = X66 ) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f25,axiom,(
% 12.96/2.22 (! [X70,X71,X72] :( min_precedes(X71,X72,X70)=> (? [X73] :( occurrence_of(X73,X70)& subactivity_occurrence(X71,X73)& subactivity_occurrence(X72,X73) ) )) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f33,axiom,(
% 12.96/2.22 (! [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)& min_precedes(X97,X98,tptp0)& ( occurrence_of(X99,tptp2)| occurrence_of(X99,tptp1) )& min_precedes(X98,X99,tptp0)& (! [X100] :( min_precedes(X97,X100,tptp0)=> ( X100 = X98| X100 = X99 ) ) )) )) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f39,axiom,(
% 12.96/2.22 atomic(tptp3) ),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f40,axiom,(
% 12.96/2.22 tptp4 != tptp3 ),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f46,conjecture,(
% 12.96/2.22 (! [X101,X102] :( ( occurrence_of(X102,tptp0)& subactivity_occurrence(X101,X102)& arboreal(X101)& ~ leaf_occ(X101,X102) )=> (? [X103,X104] :( occurrence_of(X103,tptp3)& next_subocc(X101,X103,tptp0)& ( occurrence_of(X104,tptp2)| occurrence_of(X104,tptp1) )& min_precedes(X103,X104,tptp0)& leaf(X104,tptp0) ) )) )),
% 12.96/2.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.96/2.22 fof(f47,negated_conjecture,(
% 12.96/2.22 ~((! [X101,X102] :( ( occurrence_of(X102,tptp0)& subactivity_occurrence(X101,X102)& arboreal(X101)& ~ leaf_occ(X101,X102) )=> (? [X103,X104] :( occurrence_of(X103,tptp3)& next_subocc(X101,X103,tptp0)& ( occurrence_of(X104,tptp2)| occurrence_of(X104,tptp1) )& min_precedes(X103,X104,tptp0)& leaf(X104,tptp0) ) )) ))),
% 12.96/2.22 inference(negated_conjecture,[status(cth)],[f46])).
% 12.96/2.22 fof(f60,plain,(
% 12.96/2.22 ![X15,X16,X17]: (next_subocc(X15,X16,X17)<=>(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))),
% 12.96/2.22 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 12.96/2.22 fof(f61,plain,(
% 12.96/2.22 ![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))))))),
% 12.96/2.22 inference(NNF_transformation,[status(thm)],[f60])).
% 12.96/2.22 fof(f62,plain,(
% 12.96/2.22 (![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))))))),
% 12.96/2.22 inference(miniscoping,[status(thm)],[f61])).
% 12.96/2.22 fof(f63,plain,(
% 12.96/2.22 (![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)))))),
% 12.96/2.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f62])).
% 12.96/2.22 fof(f64,plain,(
% 12.96/2.22 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 12.96/2.22 inference(cnf_transformation,[status(thm)],[f63])).
% 12.96/2.22 fof(f65,plain,(
% 12.96/2.22 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f63])).
% 12.02/2.23 fof(f102,plain,(
% 12.02/2.23 ![X40,X41]: (~occurrence_of(X40,X41)|(arboreal(X40)<=>atomic(X41)))),
% 12.02/2.23 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 12.02/2.23 fof(f103,plain,(
% 12.02/2.23 ![X40,X41]: (~occurrence_of(X40,X41)|((~arboreal(X40)|atomic(X41))&(arboreal(X40)|~atomic(X41))))),
% 12.02/2.23 inference(NNF_transformation,[status(thm)],[f102])).
% 12.02/2.23 fof(f105,plain,(
% 12.02/2.23 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f103])).
% 12.02/2.23 fof(f135,plain,(
% 12.02/2.23 ![X60,X61,X62]: ((~occurrence_of(X60,X62)|~leaf_occ(X61,X60))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 12.02/2.23 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 12.02/2.23 fof(f136,plain,(
% 12.02/2.23 ![X61,X62]: ((![X60]: (~occurrence_of(X60,X62)|~leaf_occ(X61,X60)))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 12.02/2.23 inference(miniscoping,[status(thm)],[f135])).
% 12.02/2.23 fof(f137,plain,(
% 12.02/2.23 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f136])).
% 12.02/2.23 fof(f138,plain,(
% 12.02/2.23 ![X64,X65,X66]: ((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)),
% 12.02/2.23 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 12.02/2.23 fof(f139,plain,(
% 12.02/2.23 ![X65,X66]: ((![X64]: (~occurrence_of(X64,X65)|~occurrence_of(X64,X66)))|X65=X66)),
% 12.02/2.23 inference(miniscoping,[status(thm)],[f138])).
% 12.02/2.23 fof(f140,plain,(
% 12.02/2.23 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f139])).
% 12.02/2.23 fof(f145,plain,(
% 12.02/2.23 ![X70,X71,X72]: (~min_precedes(X71,X72,X70)|(?[X73]: ((occurrence_of(X73,X70)&subactivity_occurrence(X71,X73))&subactivity_occurrence(X72,X73))))),
% 12.02/2.23 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 12.02/2.23 fof(f146,plain,(
% 12.02/2.23 ![X70,X71,X72]: (~min_precedes(X71,X72,X70)|((occurrence_of(sK8_skl(X72,X71,X70),X70)&subactivity_occurrence(X71,sK8_skl(X72,X71,X70)))&subactivity_occurrence(X72,sK8_skl(X72,X71,X70))))),
% 12.02/2.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X73,sK8_skl(X72,X71,X70))],[f145])).
% 12.02/2.23 fof(f147,plain,(
% 12.02/2.23 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK8_skl(X1,X0,X2),X2))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f146])).
% 12.02/2.23 fof(f148,plain,(
% 12.02/2.23 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK8_skl(X1,X0,X2)))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f146])).
% 12.02/2.23 fof(f177,plain,(
% 12.02/2.23 ![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))&min_precedes(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&min_precedes(X98,X99,tptp0))&(![X100]: (~min_precedes(X97,X100,tptp0)|(X100=X98|X100=X99))))))),
% 12.02/2.23 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 12.02/2.23 fof(f178,plain,(
% 12.02/2.23 ![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))&min_precedes(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&min_precedes(X98,X99,tptp0))&(![X100]: (~min_precedes(X97,X100,tptp0)|(X100=X98|X100=X99))))))),
% 12.02/2.23 inference(miniscoping,[status(thm)],[f177])).
% 12.02/2.23 fof(f179,plain,(
% 12.02/2.23 ![X95]: ((![X96]: (((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96)))|((((((occurrence_of(sK14_skl(X95),tptp3)&next_subocc(X95,sK14_skl(X95),tptp0))&occurrence_of(sK15_skl(X95),tptp4))&min_precedes(sK14_skl(X95),sK15_skl(X95),tptp0))&(occurrence_of(sK16_skl(X95),tptp2)|occurrence_of(sK16_skl(X95),tptp1)))&min_precedes(sK15_skl(X95),sK16_skl(X95),tptp0))&(![X100]: (~min_precedes(sK14_skl(X95),X100,tptp0)|(X100=sK15_skl(X95)|X100=sK16_skl(X95))))))),
% 12.02/2.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X97,sK14_skl(X95)),skolemize(X98,sK15_skl(X95)),skolemize(X99,sK16_skl(X95))],[f178])).
% 12.02/2.23 fof(f180,plain,(
% 12.02/2.23 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp3))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f179])).
% 12.02/2.23 fof(f181,plain,(
% 12.02/2.23 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f179])).
% 12.02/2.23 fof(f182,plain,(
% 12.02/2.23 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK15_skl(X1),tptp4))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f179])).
% 12.02/2.23 fof(f183,plain,(
% 12.02/2.23 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK14_skl(X1),sK15_skl(X1),tptp0))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f179])).
% 12.02/2.23 fof(f185,plain,(
% 12.02/2.23 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK15_skl(X1),sK16_skl(X1),tptp0))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f179])).
% 12.02/2.23 fof(f186,plain,(
% 12.02/2.23 ![X0,X1,X2]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|~min_precedes(sK14_skl(X1),X2,tptp0)|X2=sK15_skl(X1)|X2=sK16_skl(X1))),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f179])).
% 12.02/2.23 fof(f192,plain,(
% 12.02/2.23 atomic(tptp3)),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f39])).
% 12.02/2.23 fof(f193,plain,(
% 12.02/2.23 ~tptp4=tptp3),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f40])).
% 12.02/2.23 fof(f199,plain,(
% 12.02/2.23 (?[X101,X102]: ((((occurrence_of(X102,tptp0)&subactivity_occurrence(X101,X102))&arboreal(X101))&~leaf_occ(X101,X102))&(![X103,X104]: ((((~occurrence_of(X103,tptp3)|~next_subocc(X101,X103,tptp0))|(~occurrence_of(X104,tptp2)&~occurrence_of(X104,tptp1)))|~min_precedes(X103,X104,tptp0))|~leaf(X104,tptp0)))))),
% 12.02/2.23 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 12.02/2.23 fof(f200,plain,(
% 12.02/2.23 ?[X101]: ((?[X102]: (((occurrence_of(X102,tptp0)&subactivity_occurrence(X101,X102))&arboreal(X101))&~leaf_occ(X101,X102)))&(![X104]: ((![X103]: (((~occurrence_of(X103,tptp3)|~next_subocc(X101,X103,tptp0))|(~occurrence_of(X104,tptp2)&~occurrence_of(X104,tptp1)))|~min_precedes(X103,X104,tptp0)))|~leaf(X104,tptp0))))),
% 12.02/2.23 inference(miniscoping,[status(thm)],[f199])).
% 12.02/2.23 fof(f201,plain,(
% 12.02/2.23 ((((occurrence_of(sK18_skl,tptp0)&subactivity_occurrence(sK17_skl,sK18_skl))&arboreal(sK17_skl))&~leaf_occ(sK17_skl,sK18_skl))&(![X104]: ((![X103]: (((~occurrence_of(X103,tptp3)|~next_subocc(sK17_skl,X103,tptp0))|(~occurrence_of(X104,tptp2)&~occurrence_of(X104,tptp1)))|~min_precedes(X103,X104,tptp0)))|~leaf(X104,tptp0))))),
% 12.02/2.23 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(X101,sK17_skl),skolemize(X102,sK18_skl)],[f200])).
% 12.02/2.23 fof(f202,plain,(
% 12.02/2.23 occurrence_of(sK18_skl,tptp0)),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f201])).
% 12.02/2.23 fof(f203,plain,(
% 12.02/2.23 subactivity_occurrence(sK17_skl,sK18_skl)),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f201])).
% 12.02/2.23 fof(f204,plain,(
% 12.02/2.23 arboreal(sK17_skl)),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f201])).
% 12.02/2.23 fof(f205,plain,(
% 12.02/2.23 ~leaf_occ(sK17_skl,sK18_skl)),
% 12.02/2.23 inference(cnf_transformation,[status(thm)],[f201])).
% 12.02/2.23 fof(f237,definition,(
% 12.02/2.23 sQ3_spl <=> (leaf_occ(sK17_skl,sK18_skl))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f238,plain,(
% 12.02/2.23 leaf_occ(sK17_skl,sK18_skl)|~sQ3_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f237])).
% 12.02/2.23 fof(f244,plain,(
% 12.02/2.23 $false|~sQ3_spl),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f238,f205])).
% 12.02/2.23 fof(f245,plain,(
% 12.02/2.23 ~sQ3_spl),
% 12.02/2.23 inference(contradiction_clause,[status(thm)],[f244])).
% 12.02/2.23 fof(f248,definition,(
% 12.02/2.23 sQ5_spl <=> (arboreal(sK17_skl))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f250,plain,(
% 12.02/2.23 ~arboreal(sK17_skl)|sQ5_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f248])).
% 12.02/2.23 fof(f255,plain,(
% 12.02/2.23 $false|sQ5_spl),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f250,f204])).
% 12.02/2.23 fof(f256,plain,(
% 12.02/2.23 sQ5_spl),
% 12.02/2.23 inference(contradiction_clause,[status(thm)],[f255])).
% 12.02/2.23 fof(f302,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK18_skl)|~arboreal(X0)|leaf_occ(X0,sK18_skl)|occurrence_of(sK14_skl(X0),tptp3))),
% 12.02/2.23 inference(resolution,[status(thm)],[f180,f202])).
% 12.02/2.23 fof(f303,plain,(
% 12.02/2.23 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK14_skl(sK17_skl),tptp3)),
% 12.02/2.23 inference(resolution,[status(thm)],[f302,f203])).
% 12.02/2.23 fof(f304,definition,(
% 12.02/2.23 sQ14_spl <=> (occurrence_of(sK14_skl(sK17_skl),tptp3))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f305,plain,(
% 12.02/2.23 occurrence_of(sK14_skl(sK17_skl),tptp3)|~sQ14_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f304])).
% 12.02/2.23 fof(f307,plain,(
% 12.02/2.23 ~sQ5_spl|sQ3_spl|sQ14_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f303,f248,f237,f304])).
% 12.02/2.23 fof(f312,plain,(
% 12.02/2.23 arboreal(sK14_skl(sK17_skl))|~atomic(tptp3)|~sQ14_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f305,f105])).
% 12.02/2.23 fof(f321,definition,(
% 12.02/2.23 sQ16_spl <=> (atomic(tptp3))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f323,plain,(
% 12.02/2.23 ~atomic(tptp3)|sQ16_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f321])).
% 12.02/2.23 fof(f325,definition,(
% 12.02/2.23 sQ17_spl <=> (arboreal(sK14_skl(sK17_skl)))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f328,plain,(
% 12.02/2.23 sQ17_spl|~sQ16_spl|~sQ14_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f312,f325,f321,f304])).
% 12.02/2.23 fof(f338,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK18_skl)|~arboreal(X0)|leaf_occ(X0,sK18_skl)|occurrence_of(sK15_skl(X0),tptp4))),
% 12.02/2.23 inference(resolution,[status(thm)],[f182,f202])).
% 12.02/2.23 fof(f339,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK18_skl)|~arboreal(X0)|leaf_occ(X0,sK18_skl)|next_subocc(X0,sK14_skl(X0),tptp0))),
% 12.02/2.23 inference(resolution,[status(thm)],[f181,f202])).
% 12.02/2.23 fof(f340,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK18_skl)|~arboreal(X0)|leaf_occ(X0,sK18_skl)|min_precedes(sK14_skl(X0),sK15_skl(X0),tptp0))),
% 12.02/2.23 inference(resolution,[status(thm)],[f183,f202])).
% 12.02/2.23 fof(f341,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK18_skl)|~arboreal(X0)|leaf_occ(X0,sK18_skl)|min_precedes(sK15_skl(X0),sK16_skl(X0),tptp0))),
% 12.02/2.23 inference(resolution,[status(thm)],[f185,f202])).
% 12.02/2.23 fof(f412,plain,(
% 12.02/2.23 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK15_skl(sK17_skl),tptp4)),
% 12.02/2.23 inference(resolution,[status(thm)],[f338,f203])).
% 12.02/2.23 fof(f413,definition,(
% 12.02/2.23 sQ24_spl <=> (occurrence_of(sK15_skl(sK17_skl),tptp4))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f414,plain,(
% 12.02/2.23 occurrence_of(sK15_skl(sK17_skl),tptp4)|~sQ24_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f413])).
% 12.02/2.23 fof(f416,plain,(
% 12.02/2.23 ~sQ5_spl|sQ3_spl|sQ24_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f412,f248,f237,f413])).
% 12.02/2.23 fof(f422,plain,(
% 12.02/2.23 ![X0]: (~occurrence_of(sK15_skl(sK17_skl),X0)|X0=tptp4|~sQ24_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f414,f140])).
% 12.02/2.23 fof(f450,plain,(
% 12.02/2.23 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|next_subocc(sK17_skl,sK14_skl(sK17_skl),tptp0)),
% 12.02/2.23 inference(resolution,[status(thm)],[f339,f203])).
% 12.02/2.23 fof(f451,definition,(
% 12.02/2.23 sQ29_spl <=> (next_subocc(sK17_skl,sK14_skl(sK17_skl),tptp0))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f452,plain,(
% 12.02/2.23 next_subocc(sK17_skl,sK14_skl(sK17_skl),tptp0)|~sQ29_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f451])).
% 12.02/2.23 fof(f454,plain,(
% 12.02/2.23 ~sQ5_spl|sQ3_spl|sQ29_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f450,f248,f237,f451])).
% 12.02/2.23 fof(f455,plain,(
% 12.02/2.23 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 12.02/2.23 inference(resolution,[status(thm)],[f340,f203])).
% 12.02/2.23 fof(f456,definition,(
% 12.02/2.23 sQ30_spl <=> (min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f457,plain,(
% 12.02/2.23 min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)|~sQ30_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f456])).
% 12.02/2.23 fof(f459,plain,(
% 12.02/2.23 ~sQ5_spl|sQ3_spl|sQ30_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f455,f248,f237,f456])).
% 12.02/2.23 fof(f460,plain,(
% 12.02/2.23 min_precedes(sK17_skl,sK14_skl(sK17_skl),tptp0)|~sQ29_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f452,f64])).
% 12.02/2.23 fof(f472,plain,(
% 12.02/2.23 subactivity_occurrence(sK17_skl,sK8_skl(sK14_skl(sK17_skl),sK17_skl,tptp0))|~sQ29_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f460,f148])).
% 12.02/2.23 fof(f473,plain,(
% 12.02/2.23 occurrence_of(sK8_skl(sK14_skl(sK17_skl),sK17_skl,tptp0),tptp0)|~sQ29_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f460,f147])).
% 12.02/2.23 fof(f478,plain,(
% 12.02/2.23 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK17_skl,X0)|~sQ29_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f460,f137])).
% 12.02/2.23 fof(f523,plain,(
% 12.02/2.23 subactivity_occurrence(sK14_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|~sQ30_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f457,f148])).
% 12.02/2.23 fof(f524,plain,(
% 12.02/2.23 occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)|~sQ30_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f457,f147])).
% 12.02/2.23 fof(f528,plain,(
% 12.02/2.23 ![X0]: (~next_subocc(sK14_skl(sK17_skl),X0,tptp0)|~min_precedes(sK15_skl(sK17_skl),X0,tptp0)|~sQ30_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f457,f65])).
% 12.02/2.23 fof(f529,plain,(
% 12.02/2.23 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK14_skl(sK17_skl),X0)|~sQ30_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f457,f137])).
% 12.02/2.23 fof(f636,plain,(
% 12.02/2.23 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)),
% 12.02/2.23 inference(resolution,[status(thm)],[f341,f203])).
% 12.02/2.23 fof(f637,definition,(
% 12.02/2.23 sQ54_spl <=> (min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f638,plain,(
% 12.02/2.23 min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)|~sQ54_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f637])).
% 12.02/2.23 fof(f640,plain,(
% 12.02/2.23 ~sQ5_spl|sQ3_spl|sQ54_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f636,f248,f237,f637])).
% 12.02/2.23 fof(f757,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|~arboreal(X0)|leaf_occ(X0,sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|next_subocc(X0,sK14_skl(X0),tptp0)|~sQ30_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f524,f181])).
% 12.02/2.23 fof(f759,plain,(
% 12.02/2.23 ![X0]: (~subactivity_occurrence(X0,sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|~arboreal(X0)|leaf_occ(X0,sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|occurrence_of(sK14_skl(X0),tptp3)|~sQ30_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f524,f180])).
% 12.02/2.23 fof(f1080,definition,(
% 12.02/2.23 ![X0]: (sQ103_spl <=> (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK17_skl,X0)|leaf_occ(sK17_skl,X0)))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f1081,plain,(
% 12.02/2.23 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK17_skl,X0)|leaf_occ(sK17_skl,X0)|~sQ103_spl)),
% 12.02/2.23 inference(component_clause,[status(thm)],[f1080])).
% 12.02/2.23 fof(f1152,plain,(
% 12.02/2.23 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK17_skl,X0)|~sQ29_spl|~sQ103_spl)),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f1081,f478])).
% 12.02/2.23 fof(f1160,plain,(
% 12.02/2.23 ~subactivity_occurrence(sK17_skl,sK8_skl(sK14_skl(sK17_skl),sK17_skl,tptp0))|~sQ103_spl|~sQ29_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f1152,f473])).
% 12.02/2.23 fof(f1162,plain,(
% 12.02/2.23 $false|~sQ103_spl|~sQ29_spl),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f1160,f472])).
% 12.02/2.23 fof(f1163,plain,(
% 12.02/2.23 ~sQ103_spl|~sQ29_spl),
% 12.02/2.23 inference(contradiction_clause,[status(thm)],[f1162])).
% 12.02/2.23 fof(f1270,plain,(
% 12.02/2.23 $false|sQ16_spl),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f323,f192])).
% 12.02/2.23 fof(f1271,plain,(
% 12.02/2.23 sQ16_spl),
% 12.02/2.23 inference(contradiction_clause,[status(thm)],[f1270])).
% 12.02/2.23 fof(f2249,plain,(
% 12.02/2.23 ~next_subocc(sK14_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)|~sQ30_spl|~sQ54_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f528,f638])).
% 12.02/2.23 fof(f2659,definition,(
% 12.02/2.23 sQ265_spl <=> (next_subocc(sK14_skl(sK17_skl),sK16_skl(sK17_skl),tptp0))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f2660,plain,(
% 12.02/2.23 next_subocc(sK14_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)|~sQ265_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f2659])).
% 12.02/2.23 fof(f2670,plain,(
% 12.02/2.23 $false|~sQ30_spl|~sQ54_spl|~sQ265_spl),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f2660,f2249])).
% 12.02/2.23 fof(f2671,plain,(
% 12.02/2.23 ~sQ30_spl|~sQ54_spl|~sQ265_spl),
% 12.02/2.23 inference(contradiction_clause,[status(thm)],[f2670])).
% 12.02/2.23 fof(f5121,definition,(
% 12.02/2.23 sQ508_spl <=> (leaf_occ(sK14_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ508_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f5122,plain,(
% 12.02/2.23 leaf_occ(sK14_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|~sQ508_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f5121])).
% 12.02/2.23 fof(f5144,plain,(
% 12.02/2.23 ~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)|~sQ508_spl|~sQ30_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f5122,f529])).
% 12.02/2.23 fof(f5148,plain,(
% 12.02/2.23 $false|~sQ508_spl|~sQ30_spl),
% 12.02/2.23 inference(forward_subsumption_resolution,[status(thm)],[f5144,f524])).
% 12.02/2.23 fof(f5149,plain,(
% 12.02/2.23 ~sQ508_spl|~sQ30_spl),
% 12.02/2.23 inference(contradiction_clause,[status(thm)],[f5148])).
% 12.02/2.23 fof(f5175,plain,(
% 12.02/2.23 ~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|next_subocc(sK14_skl(sK17_skl),sK14_skl(sK14_skl(sK17_skl)),tptp0)|~sQ30_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f757,f523])).
% 12.02/2.23 fof(f5180,definition,(
% 12.02/2.23 sQ515_spl <=> (next_subocc(sK14_skl(sK17_skl),sK14_skl(sK14_skl(sK17_skl)),tptp0))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ515_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f5181,plain,(
% 12.02/2.23 next_subocc(sK14_skl(sK17_skl),sK14_skl(sK14_skl(sK17_skl)),tptp0)|~sQ515_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f5180])).
% 12.02/2.23 fof(f5183,plain,(
% 12.02/2.23 ~sQ17_spl|sQ508_spl|sQ515_spl|~sQ30_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f5175,f325,f5121,f5180,f456])).
% 12.02/2.23 fof(f5195,plain,(
% 12.02/2.23 ~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|occurrence_of(sK14_skl(sK14_skl(sK17_skl)),tptp3)|~sQ30_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f759,f523])).
% 12.02/2.23 fof(f5200,definition,(
% 12.02/2.23 sQ519_spl <=> (occurrence_of(sK14_skl(sK14_skl(sK17_skl)),tptp3))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f5201,plain,(
% 12.02/2.23 occurrence_of(sK14_skl(sK14_skl(sK17_skl)),tptp3)|~sQ519_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f5200])).
% 12.02/2.23 fof(f5203,plain,(
% 12.02/2.23 ~sQ17_spl|sQ508_spl|sQ519_spl|~sQ30_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f5195,f325,f5121,f5200,f456])).
% 12.02/2.23 fof(f5340,plain,(
% 12.02/2.23 min_precedes(sK14_skl(sK17_skl),sK14_skl(sK14_skl(sK17_skl)),tptp0)|~sQ515_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f5181,f64])).
% 12.02/2.23 fof(f5360,plain,(
% 12.02/2.23 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK17_skl,X0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,X0)|sK14_skl(sK14_skl(sK17_skl))=sK15_skl(sK17_skl)|sK14_skl(sK14_skl(sK17_skl))=sK16_skl(sK17_skl)|~sQ515_spl)),
% 12.02/2.23 inference(resolution,[status(thm)],[f5340,f186])).
% 12.02/2.23 fof(f5381,definition,(
% 12.02/2.23 sQ543_spl <=> (sK14_skl(sK14_skl(sK17_skl))=sK15_skl(sK17_skl))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ543_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f5382,plain,(
% 12.02/2.23 sK14_skl(sK14_skl(sK17_skl))=sK15_skl(sK17_skl)|~sQ543_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f5381])).
% 12.02/2.23 fof(f5384,definition,(
% 12.02/2.23 sQ544_spl <=> (sK14_skl(sK14_skl(sK17_skl))=sK16_skl(sK17_skl))),
% 12.02/2.23 introduced(definition,[new_symbols(definition,[sQ544_spl])],[split_symbol_definition])).
% 12.02/2.23 fof(f5385,plain,(
% 12.02/2.23 sK14_skl(sK14_skl(sK17_skl))=sK16_skl(sK17_skl)|~sQ544_spl),
% 12.02/2.23 inference(component_clause,[status(thm)],[f5384])).
% 12.02/2.23 fof(f5387,plain,(
% 12.02/2.23 sQ103_spl|~sQ5_spl|sQ543_spl|sQ544_spl|~sQ515_spl),
% 12.02/2.23 inference(split_clause,[status(thm)],[f5360,f1080,f248,f5381,f5384,f5180])).
% 12.02/2.23 fof(f5413,plain,(
% 12.02/2.23 occurrence_of(sK15_skl(sK17_skl),tptp3)|~sQ543_spl|~sQ519_spl),
% 12.02/2.23 inference(backward_demodulation,[status(thm)],[f5382,f5201])).
% 12.02/2.23 fof(f5468,plain,(
% 12.02/2.23 next_subocc(sK14_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)|~sQ544_spl|~sQ515_spl),
% 12.02/2.23 inference(backward_demodulation,[status(thm)],[f5385,f5181])).
% 12.02/2.23 fof(f5522,plain,(
% 12.02/2.23 tptp3=tptp4|~sQ543_spl|~sQ519_spl|~sQ24_spl),
% 12.02/2.23 inference(resolution,[status(thm)],[f5413,f422])).
% 12.02/2.23 fof(f5536,plain,(
% 12.02/2.25 $false|~sQ543_spl|~sQ519_spl|~sQ24_spl),
% 12.02/2.25 inference(forward_subsumption_resolution,[status(thm)],[f5522,f193])).
% 12.02/2.25 fof(f5537,plain,(
% 12.02/2.25 ~sQ543_spl|~sQ519_spl|~sQ24_spl),
% 12.02/2.25 inference(contradiction_clause,[status(thm)],[f5536])).
% 12.02/2.25 fof(f5540,plain,(
% 12.02/2.25 sQ265_spl|~sQ544_spl|~sQ515_spl),
% 12.02/2.25 inference(split_clause,[status(thm)],[f5468,f2659,f5384,f5180])).
% 12.02/2.25 fof(f5587,plain,(
% 12.02/2.25 $false),
% 12.02/2.25 inference(sat_refutation,[status(thm)],[f245,f256,f307,f328,f416,f454,f459,f640,f1163,f1271,f2671,f5149,f5183,f5203,f5387,f5537,f5540])).
% 12.02/2.25 % SZS output end CNFRefutation for theBenchmark.p
% 12.02/2.27 % Elapsed time: 1.828314 seconds
% 12.02/2.27 % CPU time: 14.018461 seconds
% 12.02/2.27 % Total memory used: 150.442 MB
% 12.02/2.27 % Net memory used: 144.184 MB
%------------------------------------------------------------------------------