%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO005+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 : n005.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:22 PM UTC 2026
% Result : Theorem 56.29s 7.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO005+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 03:41:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 56.29/7.58 % Refutation found
% 56.29/7.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.29/7.58 % SZS output start CNFRefutation for theBenchmark
% 56.29/7.58 fof(f4,axiom,(
% 56.29/7.58 (! [X11,X12,X13,X14] :( ( occurrence_of(X13,X14)& ~ atomic(X14)& leaf_occ(X11,X13)& leaf_occ(X12,X13) )=> X11 = X12 ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f5,axiom,(
% 56.29/7.58 (! [X15,X16,X17] :( next_subocc(X15,X16,X17)<=> ( min_precedes(X15,X16,X17)& ~ (? [X18] :( min_precedes(X15,X18,X17)& min_precedes(X18,X16,X17) ) )) ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f11,axiom,(
% 56.29/7.58 (! [X32,X33] :( root_occ(X32,X33)<=> (? [X34] :( occurrence_of(X33,X34)& subactivity_occurrence(X32,X33)& root(X32,X34) ) )) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f13,axiom,(
% 56.29/7.58 (! [X38,X39] :( root(X38,X39)=> legal(X38) ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f14,axiom,(
% 56.29/7.58 (! [X40,X41] :( occurrence_of(X40,X41)=> ( arboreal(X40)<=> atomic(X41) ) ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f18,axiom,(
% 56.29/7.58 (! [X51] :( legal(X51)=> arboreal(X51) ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f21,axiom,(
% 56.29/7.58 (! [X56,X57,X58] :( ( occurrence_of(X56,X58)& root_occ(X57,X56) )=> ~ (? [X59] : min_precedes(X59,X57,X58) )) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f22,axiom,(
% 56.29/7.58 (! [X60,X61,X62] :( ( occurrence_of(X60,X62)& leaf_occ(X61,X60) )=> ~ (? [X63] : min_precedes(X61,X63,X62) )) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f23,axiom,(
% 56.29/7.58 (! [X64,X65,X66] :( ( occurrence_of(X64,X65)& occurrence_of(X64,X66) )=> X65 = X66 ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f25,axiom,(
% 56.29/7.58 (! [X70,X71,X72] :( min_precedes(X71,X72,X70)=> (? [X73] :( occurrence_of(X73,X70)& subactivity_occurrence(X71,X73)& subactivity_occurrence(X72,X73) ) )) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f33,axiom,(
% 56.29/7.58 (! [X95] :( occurrence_of(X95,tptp0)=> (? [X96,X97] :( occurrence_of(X96,tptp4)& root_occ(X96,X95)& ( occurrence_of(X97,tptp3)| occurrence_of(X97,tptp2) )& leaf_occ(X97,X95)& next_subocc(X96,X97,tptp0) ) )) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f35,axiom,(
% 56.29/7.58 ~ atomic(tptp0) ),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f39,axiom,(
% 56.29/7.58 atomic(tptp1) ),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f43,axiom,(
% 56.29/7.58 tptp1 != tptp3 ),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f44,axiom,(
% 56.29/7.58 tptp1 != tptp2 ),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f46,axiom,(
% 56.29/7.58 (! [X98,X99] :( ( occurrence_of(X99,tptp0)& subactivity_occurrence(X98,X99)& arboreal(X98)& ~ leaf_occ(X98,X99) )=> root_occ(X98,X99) ) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f47,axiom,(
% 56.29/7.58 (! [X100,X101] :( ( occurrence_of(X101,tptp0)& subactivity_occurrence(X100,X101)& arboreal(X100)& ~ leaf_occ(X100,X101) )=> (? [X102] :( occurrence_of(X102,tptp1)& next_subocc(X100,X102,tptp0) ) )) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f48,conjecture,(
% 56.29/7.58 ~ (? [X103] : occurrence_of(X103,tptp0) )),
% 56.29/7.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.29/7.58 fof(f49,negated_conjecture,(
% 56.29/7.58 ~(~ (? [X103] : occurrence_of(X103,tptp0) ))),
% 56.29/7.58 inference(negated_conjecture,[status(cth)],[f48])).
% 56.29/7.58 fof(f59,plain,(
% 56.29/7.58 ![X11,X12,X13,X14]: ((((~occurrence_of(X13,X14)|atomic(X14))|~leaf_occ(X11,X13))|~leaf_occ(X12,X13))|X11=X12)),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 56.29/7.58 fof(f60,plain,(
% 56.29/7.58 ![X11,X12]: ((![X13]: (((![X14]: (~occurrence_of(X13,X14)|atomic(X14)))|~leaf_occ(X11,X13))|~leaf_occ(X12,X13)))|X11=X12)),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f59])).
% 56.29/7.58 fof(f61,plain,(
% 56.29/7.58 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|atomic(X1)|~leaf_occ(X2,X0)|~leaf_occ(X3,X0)|X2=X3)),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f60])).
% 56.29/7.58 fof(f62,plain,(
% 56.29/7.58 ![X15,X16,X17]: (next_subocc(X15,X16,X17)<=>(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 56.29/7.58 fof(f63,plain,(
% 56.29/7.58 ![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))))))),
% 56.29/7.58 inference(NNF_transformation,[status(thm)],[f62])).
% 56.29/7.58 fof(f64,plain,(
% 56.29/7.58 (![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))))))),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f63])).
% 56.29/7.58 fof(f65,plain,(
% 56.29/7.58 (![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)))))),
% 56.29/7.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f64])).
% 56.29/7.58 fof(f66,plain,(
% 56.29/7.58 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f65])).
% 56.29/7.58 fof(f87,plain,(
% 56.29/7.58 ![X32,X33]: ((~root_occ(X32,X33)|(?[X34]: ((occurrence_of(X33,X34)&subactivity_occurrence(X32,X33))&root(X32,X34))))&(root_occ(X32,X33)|(![X34]: ((~occurrence_of(X33,X34)|~subactivity_occurrence(X32,X33))|~root(X32,X34)))))),
% 56.29/7.58 inference(NNF_transformation,[status(thm)],[f11])).
% 56.29/7.58 fof(f88,plain,(
% 56.29/7.58 (![X32,X33]: (~root_occ(X32,X33)|(?[X34]: ((occurrence_of(X33,X34)&subactivity_occurrence(X32,X33))&root(X32,X34)))))&(![X32,X33]: (root_occ(X32,X33)|(![X34]: ((~occurrence_of(X33,X34)|~subactivity_occurrence(X32,X33))|~root(X32,X34)))))),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f87])).
% 56.29/7.58 fof(f89,plain,(
% 56.29/7.58 (![X32,X33]: (~root_occ(X32,X33)|((occurrence_of(X33,sK1_skl(X33,X32))&subactivity_occurrence(X32,X33))&root(X32,sK1_skl(X33,X32)))))&(![X32,X33]: (root_occ(X32,X33)|(![X34]: ((~occurrence_of(X33,X34)|~subactivity_occurrence(X32,X33))|~root(X32,X34)))))),
% 56.29/7.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X34,sK1_skl(X33,X32))],[f88])).
% 56.29/7.58 fof(f90,plain,(
% 56.29/7.58 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK1_skl(X1,X0)))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f89])).
% 56.29/7.58 fof(f91,plain,(
% 56.29/7.58 ![X0,X1]: (~root_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f89])).
% 56.29/7.58 fof(f92,plain,(
% 56.29/7.58 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK1_skl(X1,X0)))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f89])).
% 56.29/7.58 fof(f101,plain,(
% 56.29/7.58 ![X38,X39]: (~root(X38,X39)|legal(X38))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 56.29/7.58 fof(f102,plain,(
% 56.29/7.58 ![X38]: ((![X39]: ~root(X38,X39))|legal(X38))),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f101])).
% 56.29/7.58 fof(f103,plain,(
% 56.29/7.58 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f102])).
% 56.29/7.58 fof(f104,plain,(
% 56.29/7.58 ![X40,X41]: (~occurrence_of(X40,X41)|(arboreal(X40)<=>atomic(X41)))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 56.29/7.58 fof(f105,plain,(
% 56.29/7.58 ![X40,X41]: (~occurrence_of(X40,X41)|((~arboreal(X40)|atomic(X41))&(arboreal(X40)|~atomic(X41))))),
% 56.29/7.58 inference(NNF_transformation,[status(thm)],[f104])).
% 56.29/7.58 fof(f107,plain,(
% 56.29/7.58 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f105])).
% 56.29/7.58 fof(f125,plain,(
% 56.29/7.58 ![X51]: (~legal(X51)|arboreal(X51))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 56.29/7.58 fof(f126,plain,(
% 56.29/7.58 ![X0]: (~legal(X0)|arboreal(X0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f125])).
% 56.29/7.58 fof(f134,plain,(
% 56.29/7.58 ![X56,X57,X58]: ((~occurrence_of(X56,X58)|~root_occ(X57,X56))|(![X59]: ~min_precedes(X59,X57,X58)))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 56.29/7.58 fof(f135,plain,(
% 56.29/7.58 ![X57,X58]: ((![X56]: (~occurrence_of(X56,X58)|~root_occ(X57,X56)))|(![X59]: ~min_precedes(X59,X57,X58)))),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f134])).
% 56.29/7.58 fof(f136,plain,(
% 56.29/7.58 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~min_precedes(X3,X2,X1))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f135])).
% 56.29/7.58 fof(f137,plain,(
% 56.29/7.58 ![X60,X61,X62]: ((~occurrence_of(X60,X62)|~leaf_occ(X61,X60))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 56.29/7.58 fof(f138,plain,(
% 56.29/7.58 ![X61,X62]: ((![X60]: (~occurrence_of(X60,X62)|~leaf_occ(X61,X60)))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f137])).
% 56.29/7.58 fof(f139,plain,(
% 56.29/7.58 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f138])).
% 56.29/7.58 fof(f140,plain,(
% 56.29/7.58 ![X64,X65,X66]: ((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 56.29/7.58 fof(f141,plain,(
% 56.29/7.58 ![X65,X66]: ((![X64]: (~occurrence_of(X64,X65)|~occurrence_of(X64,X66)))|X65=X66)),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f140])).
% 56.29/7.58 fof(f142,plain,(
% 56.29/7.58 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f141])).
% 56.29/7.58 fof(f147,plain,(
% 56.29/7.58 ![X70,X71,X72]: (~min_precedes(X71,X72,X70)|(?[X73]: ((occurrence_of(X73,X70)&subactivity_occurrence(X71,X73))&subactivity_occurrence(X72,X73))))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 56.29/7.58 fof(f148,plain,(
% 56.29/7.58 ![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))))),
% 56.29/7.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X73,sK8_skl(X72,X71,X70))],[f147])).
% 56.29/7.58 fof(f149,plain,(
% 56.29/7.58 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK8_skl(X1,X0,X2),X2))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f148])).
% 56.29/7.58 fof(f151,plain,(
% 56.29/7.58 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK8_skl(X1,X0,X2)))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f148])).
% 56.29/7.58 fof(f179,plain,(
% 56.29/7.58 ![X95]: (~occurrence_of(X95,tptp0)|(?[X96,X97]: ((((occurrence_of(X96,tptp4)&root_occ(X96,X95))&(occurrence_of(X97,tptp3)|occurrence_of(X97,tptp2)))&leaf_occ(X97,X95))&next_subocc(X96,X97,tptp0))))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 56.29/7.58 fof(f180,plain,(
% 56.29/7.58 ![X95]: (~occurrence_of(X95,tptp0)|((((occurrence_of(sK14_skl(X95),tptp4)&root_occ(sK14_skl(X95),X95))&(occurrence_of(sK15_skl(X95),tptp3)|occurrence_of(sK15_skl(X95),tptp2)))&leaf_occ(sK15_skl(X95),X95))&next_subocc(sK14_skl(X95),sK15_skl(X95),tptp0)))),
% 56.29/7.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(X96,sK14_skl(X95)),skolemize(X97,sK15_skl(X95))],[f179])).
% 56.29/7.58 fof(f182,plain,(
% 56.29/7.58 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK14_skl(X0),X0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f180])).
% 56.29/7.58 fof(f183,plain,(
% 56.29/7.58 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK15_skl(X0),tptp3)|occurrence_of(sK15_skl(X0),tptp2))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f180])).
% 56.29/7.58 fof(f184,plain,(
% 56.29/7.58 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK15_skl(X0),X0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f180])).
% 56.29/7.58 fof(f185,plain,(
% 56.29/7.58 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK14_skl(X0),sK15_skl(X0),tptp0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f180])).
% 56.29/7.58 fof(f187,plain,(
% 56.29/7.58 ~atomic(tptp0)),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f35])).
% 56.29/7.58 fof(f191,plain,(
% 56.29/7.58 atomic(tptp1)),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f39])).
% 56.29/7.58 fof(f195,plain,(
% 56.29/7.58 ~tptp1=tptp3),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f43])).
% 56.29/7.58 fof(f196,plain,(
% 56.29/7.58 ~tptp1=tptp2),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f44])).
% 56.29/7.58 fof(f198,plain,(
% 56.29/7.58 ![X98,X99]: ((((~occurrence_of(X99,tptp0)|~subactivity_occurrence(X98,X99))|~arboreal(X98))|leaf_occ(X98,X99))|root_occ(X98,X99))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 56.29/7.58 fof(f199,plain,(
% 56.29/7.58 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|root_occ(X1,X0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f198])).
% 56.29/7.58 fof(f200,plain,(
% 56.29/7.58 ![X100,X101]: ((((~occurrence_of(X101,tptp0)|~subactivity_occurrence(X100,X101))|~arboreal(X100))|leaf_occ(X100,X101))|(?[X102]: (occurrence_of(X102,tptp1)&next_subocc(X100,X102,tptp0))))),
% 56.29/7.58 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 56.29/7.58 fof(f201,plain,(
% 56.29/7.58 ![X100]: ((![X101]: (((~occurrence_of(X101,tptp0)|~subactivity_occurrence(X100,X101))|~arboreal(X100))|leaf_occ(X100,X101)))|(?[X102]: (occurrence_of(X102,tptp1)&next_subocc(X100,X102,tptp0))))),
% 56.29/7.58 inference(miniscoping,[status(thm)],[f200])).
% 56.29/7.58 fof(f202,plain,(
% 56.29/7.58 ![X100]: ((![X101]: (((~occurrence_of(X101,tptp0)|~subactivity_occurrence(X100,X101))|~arboreal(X100))|leaf_occ(X100,X101)))|(occurrence_of(sK16_skl(X100),tptp1)&next_subocc(X100,sK16_skl(X100),tptp0)))),
% 56.29/7.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(X102,sK16_skl(X100))],[f201])).
% 56.29/7.58 fof(f203,plain,(
% 56.29/7.58 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp1))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f202])).
% 56.29/7.58 fof(f204,plain,(
% 56.29/7.58 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK16_skl(X1),tptp0))),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f202])).
% 56.29/7.58 fof(f205,plain,(
% 56.29/7.58 occurrence_of(sK17_skl,tptp0)),
% 56.29/7.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X103,sK17_skl)],[f49])).
% 56.29/7.58 fof(f206,plain,(
% 56.29/7.58 occurrence_of(sK17_skl,tptp0)),
% 56.29/7.58 inference(cnf_transformation,[status(thm)],[f205])).
% 56.29/7.58 fof(f208,plain,(
% 56.29/7.58 ![X0]: (~occurrence_of(sK17_skl,X0)|tptp0=X0)),
% 56.29/7.58 inference(resolution,[status(thm)],[f142,f206])).
% 56.29/7.58 fof(f242,plain,(
% 56.29/7.58 root_occ(sK14_skl(sK17_skl),sK17_skl)),
% 56.29/7.58 inference(resolution,[status(thm)],[f182,f206])).
% 56.29/7.58 fof(f247,plain,(
% 56.29/7.58 root(sK14_skl(sK17_skl),sK1_skl(sK17_skl,sK14_skl(sK17_skl)))),
% 56.29/7.58 inference(resolution,[status(thm)],[f242,f92])).
% 56.29/7.58 fof(f248,plain,(
% 56.29/7.58 occurrence_of(sK17_skl,sK1_skl(sK17_skl,sK14_skl(sK17_skl)))),
% 56.29/7.58 inference(resolution,[status(thm)],[f242,f90])).
% 56.29/7.58 fof(f249,plain,(
% 56.29/7.58 subactivity_occurrence(sK14_skl(sK17_skl),sK17_skl)),
% 56.29/7.58 inference(resolution,[status(thm)],[f242,f91])).
% 56.29/7.58 fof(f289,plain,(
% 56.29/7.58 ![X0,X1]: (~leaf_occ(X0,sK17_skl)|~min_precedes(X0,X1,tptp0))),
% 56.29/7.58 inference(resolution,[status(thm)],[f139,f206])).
% 56.29/7.58 fof(f292,plain,(
% 56.29/7.58 tptp0=sK1_skl(sK17_skl,sK14_skl(sK17_skl))),
% 56.29/7.58 inference(resolution,[status(thm)],[f248,f208])).
% 56.29/7.58 fof(f311,plain,(
% 56.29/7.58 root(sK14_skl(sK17_skl),tptp0)),
% 56.29/7.58 inference(forward_demodulation,[status(thm)],[f292,f247])).
% 56.29/7.58 fof(f316,plain,(
% 56.29/7.58 legal(sK14_skl(sK17_skl))),
% 56.29/7.58 inference(resolution,[status(thm)],[f311,f103])).
% 56.29/7.58 fof(f317,plain,(
% 56.29/7.58 arboreal(sK14_skl(sK17_skl))),
% 56.29/7.58 inference(resolution,[status(thm)],[f316,f126])).
% 56.29/7.58 fof(f615,plain,(
% 56.29/7.58 next_subocc(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 56.29/7.58 inference(resolution,[status(thm)],[f185,f206])).
% 56.29/7.58 fof(f625,plain,(
% 56.29/7.58 ~occurrence_of(sK17_skl,tptp0)|~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK17_skl)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1)),
% 56.29/7.58 inference(resolution,[status(thm)],[f203,f249])).
% 56.29/7.58 fof(f626,plain,(
% 56.29/7.58 ~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK17_skl)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f625,f206])).
% 56.29/7.58 fof(f630,plain,(
% 56.29/7.58 min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 56.29/7.58 inference(resolution,[status(thm)],[f615,f66])).
% 56.29/7.58 fof(f633,plain,(
% 56.29/7.58 ~leaf_occ(sK14_skl(sK17_skl),sK17_skl)),
% 56.29/7.58 inference(resolution,[status(thm)],[f630,f289])).
% 56.29/7.58 fof(f676,plain,(
% 56.29/7.58 ~occurrence_of(sK17_skl,tptp0)|~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK17_skl)|next_subocc(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 56.29/7.58 inference(resolution,[status(thm)],[f204,f249])).
% 56.29/7.58 fof(f677,plain,(
% 56.29/7.58 ~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK17_skl)|next_subocc(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f676,f206])).
% 56.29/7.58 fof(f1134,plain,(
% 56.29/7.58 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f626,f317])).
% 56.29/7.58 fof(f1142,plain,(
% 56.29/7.58 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|arboreal(sK16_skl(sK14_skl(sK17_skl)))|~atomic(tptp1)),
% 56.29/7.58 inference(resolution,[status(thm)],[f1134,f107])).
% 56.29/7.58 fof(f1150,plain,(
% 56.29/7.58 ![X0]: (leaf_occ(sK14_skl(sK17_skl),sK17_skl)|~occurrence_of(sK16_skl(sK14_skl(sK17_skl)),X0)|X0=tptp1)),
% 56.29/7.58 inference(resolution,[status(thm)],[f1134,f142])).
% 56.29/7.58 fof(f1158,plain,(
% 56.29/7.58 arboreal(sK16_skl(sK14_skl(sK17_skl)))|~atomic(tptp1)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f1142,f633])).
% 56.29/7.58 fof(f1163,plain,(
% 56.29/7.58 ![X0]: (~occurrence_of(sK16_skl(sK14_skl(sK17_skl)),X0)|X0=tptp1)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f1150,f633])).
% 56.29/7.58 fof(f1187,plain,(
% 56.29/7.58 arboreal(sK16_skl(sK14_skl(sK17_skl)))),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f1158,f191])).
% 56.29/7.58 fof(f1301,plain,(
% 56.29/7.58 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|next_subocc(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f677,f317])).
% 56.29/7.58 fof(f1305,plain,(
% 56.29/7.58 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 56.29/7.58 inference(resolution,[status(thm)],[f1301,f66])).
% 56.29/7.58 fof(f1307,plain,(
% 56.29/7.58 min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f1305,f633])).
% 56.29/7.58 fof(f1319,plain,(
% 56.29/7.58 subactivity_occurrence(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 56.29/7.58 inference(resolution,[status(thm)],[f1307,f151])).
% 56.29/7.58 fof(f1321,plain,(
% 56.29/7.58 occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0)),
% 56.29/7.58 inference(resolution,[status(thm)],[f1307,f149])).
% 56.29/7.58 fof(f1860,plain,(
% 56.29/7.58 occurrence_of(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp3)|occurrence_of(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp2)),
% 56.29/7.58 inference(resolution,[status(thm)],[f1321,f183])).
% 56.29/7.58 fof(f1862,plain,(
% 56.29/7.58 leaf_occ(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 56.29/7.58 inference(resolution,[status(thm)],[f1321,f184])).
% 56.29/7.58 fof(f1868,plain,(
% 56.29/7.58 ![X0,X1]: (~root_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|~min_precedes(X1,X0,tptp0))),
% 56.29/7.58 inference(resolution,[status(thm)],[f1321,f136])).
% 56.29/7.58 fof(f1876,plain,(
% 56.29/7.58 ![X0,X1]: (atomic(tptp0)|~leaf_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|~leaf_occ(X1,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|X0=X1)),
% 56.29/7.58 inference(resolution,[status(thm)],[f1321,f61])).
% 56.29/7.58 fof(f1885,plain,(
% 56.29/7.58 ![X0,X1]: (~leaf_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|~leaf_occ(X1,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|X0=X1)),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f1876,f187])).
% 56.29/7.58 fof(f2969,plain,(
% 56.29/7.58 ~occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0)|~arboreal(sK16_skl(sK14_skl(sK17_skl)))|leaf_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|root_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 56.29/7.58 inference(resolution,[status(thm)],[f1319,f199])).
% 56.29/7.58 fof(f2980,plain,(
% 56.29/7.58 ~arboreal(sK16_skl(sK14_skl(sK17_skl)))|leaf_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|root_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f2969,f1321])).
% 56.29/7.58 fof(f4094,plain,(
% 56.29/7.58 ~root_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 56.29/7.58 inference(resolution,[status(thm)],[f1868,f1307])).
% 56.29/7.58 fof(f13231,plain,(
% 56.29/7.58 leaf_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|root_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 56.29/7.58 inference(forward_subsumption_resolution,[status(thm)],[f2980,f1187])).
% 56.29/7.65 fof(f13236,plain,(
% 56.29/7.65 ![X0]: (root_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|~leaf_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|X0=sK16_skl(sK14_skl(sK17_skl)))),
% 56.29/7.65 inference(resolution,[status(thm)],[f13231,f1885])).
% 56.29/7.65 fof(f13251,plain,(
% 56.29/7.65 ![X0]: (~leaf_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|X0=sK16_skl(sK14_skl(sK17_skl)))),
% 56.29/7.65 inference(forward_subsumption_resolution,[status(thm)],[f13236,f4094])).
% 56.29/7.65 fof(f14197,plain,(
% 56.29/7.65 sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))=sK16_skl(sK14_skl(sK17_skl))),
% 56.29/7.65 inference(resolution,[status(thm)],[f13251,f1862])).
% 56.29/7.65 fof(f14272,plain,(
% 56.29/7.65 occurrence_of(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp3)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp2)),
% 56.29/7.65 inference(backward_demodulation,[status(thm)],[f14197,f1860])).
% 56.29/7.65 fof(f14278,plain,(
% 56.29/7.65 occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp3)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp2)),
% 56.29/7.65 inference(forward_demodulation,[status(thm)],[f14197,f14272])).
% 56.29/7.65 fof(f14446,plain,(
% 56.29/7.65 occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp3)|tptp2=tptp1),
% 56.29/7.65 inference(resolution,[status(thm)],[f14278,f1163])).
% 56.29/7.65 fof(f14474,plain,(
% 56.29/7.65 occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp3)),
% 56.29/7.65 inference(forward_subsumption_resolution,[status(thm)],[f14446,f196])).
% 56.29/7.65 fof(f14478,plain,(
% 56.29/7.65 tptp3=tptp1),
% 56.29/7.65 inference(resolution,[status(thm)],[f14474,f1163])).
% 56.29/7.65 fof(f14510,plain,(
% 56.29/7.65 $false),
% 56.29/7.65 inference(forward_subsumption_resolution,[status(thm)],[f14478,f195])).
% 56.29/7.65 % SZS output end CNFRefutation for theBenchmark.p
% 56.29/7.66 % Elapsed time: 7.284085 seconds
% 56.29/7.66 % CPU time: 57.186877 seconds
% 56.29/7.66 % Total memory used: 296.854 MB
% 56.29/7.66 % Net memory used: 283.015 MB
%------------------------------------------------------------------------------