%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO004+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 : n003.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 15.45s 12.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO004+2 : 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.10/10.72 % Computer : n003.cluster.edu
% 0.10/10.72 % Model : x86_64 x86_64
% 0.10/10.72 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.72 % Memory : 8046.5625MB
% 0.10/10.72 % OS : Linux 6.8.0-71-generic
% 0.10/10.72 % CPULimit : 300
% 0.10/10.72 % WCLimit : 300
% 0.10/10.72 % DateTime : Mon Sep 21 03:42:41 UTC 2026
% 0.10/10.72 % CPUTime :
% 0.10/10.73 % Drodi V4.1.1
% 15.45/12.81 % Refutation found
% 15.45/12.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.45/12.81 % SZS output start CNFRefutation for theBenchmark
% 15.45/12.81 fof(f4,axiom,(
% 15.45/12.81 (! [X11,X12,X13,X14] :( ( occurrence_of(X13,X14)& ~ atomic(X14)& leaf_occ(X11,X13)& leaf_occ(X12,X13) )=> X11 = X12 ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f5,axiom,(
% 15.45/12.81 (! [X15,X16,X17] :( next_subocc(X15,X16,X17)<=> ( min_precedes(X15,X16,X17)& ~ (? [X18] :( min_precedes(X15,X18,X17)& min_precedes(X18,X16,X17) ) )) ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f6,axiom,(
% 15.45/12.81 (! [X19,X20,X21] :( next_subocc(X19,X20,X21)=> ( arboreal(X19)& arboreal(X20) ) ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f11,axiom,(
% 15.45/12.81 (! [X32,X33] :( root_occ(X32,X33)<=> (? [X34] :( occurrence_of(X33,X34)& subactivity_occurrence(X32,X33)& root(X32,X34) ) )) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f13,axiom,(
% 15.45/12.81 (! [X38,X39] :( root(X38,X39)=> legal(X38) ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f18,axiom,(
% 15.45/12.81 (! [X51] :( legal(X51)=> arboreal(X51) ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f21,axiom,(
% 15.45/12.81 (! [X56,X57,X58] :( ( occurrence_of(X56,X58)& root_occ(X57,X56) )=> ~ (? [X59] : min_precedes(X59,X57,X58) )) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f22,axiom,(
% 15.45/12.81 (! [X60,X61,X62] :( ( occurrence_of(X60,X62)& leaf_occ(X61,X60) )=> ~ (? [X63] : min_precedes(X61,X63,X62) )) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f23,axiom,(
% 15.45/12.81 (! [X64,X65,X66] :( ( occurrence_of(X64,X65)& occurrence_of(X64,X66) )=> X65 = X66 ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f25,axiom,(
% 15.45/12.81 (! [X70,X71,X72] :( min_precedes(X71,X72,X70)=> (? [X73] :( occurrence_of(X73,X70)& subactivity_occurrence(X71,X73)& subactivity_occurrence(X72,X73) ) )) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f33,axiom,(
% 15.45/12.81 (! [X95] :( occurrence_of(X95,tptp0)=> (? [X96,X97] :( occurrence_of(X96,tptp4)& root_occ(X96,X95)& occurrence_of(X97,tptp3)& leaf_occ(X97,X95)& next_subocc(X96,X97,tptp0) ) )) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f35,axiom,(
% 15.45/12.81 ~ atomic(tptp0) ),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f43,axiom,(
% 15.45/12.81 tptp1 != tptp3 ),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f46,axiom,(
% 15.45/12.81 (! [X98,X99] :( ( occurrence_of(X99,tptp0)& subactivity_occurrence(X98,X99)& arboreal(X98)& ~ leaf_occ(X98,X99) )=> root_occ(X98,X99) ) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f48,axiom,(
% 15.45/12.81 (! [X102,X103] :( ( occurrence_of(X103,tptp0)& subactivity_occurrence(X102,X103)& arboreal(X102)& ~ leaf_occ(X102,X103) )=> (? [X104] :( occurrence_of(X104,tptp1)& next_subocc(X102,X104,tptp0) ) )) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f49,conjecture,(
% 15.45/12.81 ~ (? [X105] : occurrence_of(X105,tptp0) )),
% 15.45/12.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 15.45/12.81 fof(f50,negated_conjecture,(
% 15.45/12.81 ~(~ (? [X105] : occurrence_of(X105,tptp0) ))),
% 15.45/12.81 inference(negated_conjecture,[status(cth)],[f49])).
% 15.45/12.81 fof(f60,plain,(
% 15.45/12.81 ![X11,X12,X13,X14]: ((((~occurrence_of(X13,X14)|atomic(X14))|~leaf_occ(X11,X13))|~leaf_occ(X12,X13))|X11=X12)),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 15.45/12.81 fof(f61,plain,(
% 15.45/12.81 ![X11,X12]: ((![X13]: (((![X14]: (~occurrence_of(X13,X14)|atomic(X14)))|~leaf_occ(X11,X13))|~leaf_occ(X12,X13)))|X11=X12)),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f60])).
% 15.45/12.81 fof(f62,plain,(
% 15.45/12.81 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|atomic(X1)|~leaf_occ(X2,X0)|~leaf_occ(X3,X0)|X2=X3)),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f61])).
% 15.45/12.81 fof(f63,plain,(
% 15.45/12.81 ![X15,X16,X17]: (next_subocc(X15,X16,X17)<=>(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 15.45/12.81 fof(f64,plain,(
% 15.45/12.81 ![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))))))),
% 15.45/12.81 inference(NNF_transformation,[status(thm)],[f63])).
% 15.45/12.81 fof(f65,plain,(
% 15.45/12.81 (![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))))))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f64])).
% 15.45/12.81 fof(f66,plain,(
% 15.45/12.81 (![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)))))),
% 15.45/12.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f65])).
% 15.45/12.81 fof(f67,plain,(
% 15.45/12.81 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f66])).
% 15.45/12.81 fof(f71,plain,(
% 15.45/12.81 ![X19,X20,X21]: (~next_subocc(X19,X20,X21)|(arboreal(X19)&arboreal(X20)))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 15.45/12.81 fof(f72,plain,(
% 15.45/12.81 ![X19,X20]: ((![X21]: ~next_subocc(X19,X20,X21))|(arboreal(X19)&arboreal(X20)))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f71])).
% 15.45/12.81 fof(f74,plain,(
% 15.45/12.81 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|arboreal(X1))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f72])).
% 15.45/12.81 fof(f88,plain,(
% 15.45/12.81 ![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)))))),
% 15.45/12.81 inference(NNF_transformation,[status(thm)],[f11])).
% 15.45/12.81 fof(f89,plain,(
% 15.45/12.81 (![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)))))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f88])).
% 15.45/12.81 fof(f90,plain,(
% 15.45/12.81 (![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)))))),
% 15.45/12.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X34,sK1_skl(X33,X32))],[f89])).
% 15.45/12.81 fof(f91,plain,(
% 15.45/12.81 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK1_skl(X1,X0)))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f90])).
% 15.45/12.81 fof(f92,plain,(
% 15.45/12.81 ![X0,X1]: (~root_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f90])).
% 15.45/12.81 fof(f93,plain,(
% 15.45/12.81 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK1_skl(X1,X0)))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f90])).
% 15.45/12.81 fof(f102,plain,(
% 15.45/12.81 ![X38,X39]: (~root(X38,X39)|legal(X38))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 15.45/12.81 fof(f103,plain,(
% 15.45/12.81 ![X38]: ((![X39]: ~root(X38,X39))|legal(X38))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f102])).
% 15.45/12.81 fof(f104,plain,(
% 15.45/12.81 ![X0,X1]: (~root(X0,X1)|legal(X0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f103])).
% 15.45/12.81 fof(f126,plain,(
% 15.45/12.81 ![X51]: (~legal(X51)|arboreal(X51))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 15.45/12.81 fof(f127,plain,(
% 15.45/12.81 ![X0]: (~legal(X0)|arboreal(X0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f126])).
% 15.45/12.81 fof(f135,plain,(
% 15.45/12.81 ![X56,X57,X58]: ((~occurrence_of(X56,X58)|~root_occ(X57,X56))|(![X59]: ~min_precedes(X59,X57,X58)))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 15.45/12.81 fof(f136,plain,(
% 15.45/12.81 ![X57,X58]: ((![X56]: (~occurrence_of(X56,X58)|~root_occ(X57,X56)))|(![X59]: ~min_precedes(X59,X57,X58)))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f135])).
% 15.45/12.81 fof(f137,plain,(
% 15.45/12.81 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~min_precedes(X3,X2,X1))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f136])).
% 15.45/12.81 fof(f138,plain,(
% 15.45/12.81 ![X60,X61,X62]: ((~occurrence_of(X60,X62)|~leaf_occ(X61,X60))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 15.45/12.81 fof(f139,plain,(
% 15.45/12.81 ![X61,X62]: ((![X60]: (~occurrence_of(X60,X62)|~leaf_occ(X61,X60)))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f138])).
% 15.45/12.81 fof(f140,plain,(
% 15.45/12.81 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f139])).
% 15.45/12.81 fof(f141,plain,(
% 15.45/12.81 ![X64,X65,X66]: ((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 15.45/12.81 fof(f142,plain,(
% 15.45/12.81 ![X65,X66]: ((![X64]: (~occurrence_of(X64,X65)|~occurrence_of(X64,X66)))|X65=X66)),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f141])).
% 15.45/12.81 fof(f143,plain,(
% 15.45/12.81 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f142])).
% 15.45/12.81 fof(f148,plain,(
% 15.45/12.81 ![X70,X71,X72]: (~min_precedes(X71,X72,X70)|(?[X73]: ((occurrence_of(X73,X70)&subactivity_occurrence(X71,X73))&subactivity_occurrence(X72,X73))))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 15.45/12.81 fof(f149,plain,(
% 15.45/12.81 ![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))))),
% 15.45/12.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X73,sK8_skl(X72,X71,X70))],[f148])).
% 15.45/12.81 fof(f150,plain,(
% 15.45/12.81 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK8_skl(X1,X0,X2),X2))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f149])).
% 15.45/12.81 fof(f152,plain,(
% 15.45/12.81 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK8_skl(X1,X0,X2)))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f149])).
% 15.45/12.81 fof(f180,plain,(
% 15.45/12.81 ![X95]: (~occurrence_of(X95,tptp0)|(?[X96,X97]: ((((occurrence_of(X96,tptp4)&root_occ(X96,X95))&occurrence_of(X97,tptp3))&leaf_occ(X97,X95))&next_subocc(X96,X97,tptp0))))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 15.45/12.81 fof(f181,plain,(
% 15.45/12.81 ![X95]: (~occurrence_of(X95,tptp0)|((((occurrence_of(sK14_skl(X95),tptp4)&root_occ(sK14_skl(X95),X95))&occurrence_of(sK15_skl(X95),tptp3))&leaf_occ(sK15_skl(X95),X95))&next_subocc(sK14_skl(X95),sK15_skl(X95),tptp0)))),
% 15.45/12.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(X96,sK14_skl(X95)),skolemize(X97,sK15_skl(X95))],[f180])).
% 15.45/12.81 fof(f183,plain,(
% 15.45/12.81 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK14_skl(X0),X0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f181])).
% 15.45/12.81 fof(f184,plain,(
% 15.45/12.81 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK15_skl(X0),tptp3))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f181])).
% 15.45/12.81 fof(f185,plain,(
% 15.45/12.81 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK15_skl(X0),X0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f181])).
% 15.45/12.81 fof(f186,plain,(
% 15.45/12.81 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK14_skl(X0),sK15_skl(X0),tptp0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f181])).
% 15.45/12.81 fof(f188,plain,(
% 15.45/12.81 ~atomic(tptp0)),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f35])).
% 15.45/12.81 fof(f196,plain,(
% 15.45/12.81 ~tptp1=tptp3),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f43])).
% 15.45/12.81 fof(f199,plain,(
% 15.45/12.81 ![X98,X99]: ((((~occurrence_of(X99,tptp0)|~subactivity_occurrence(X98,X99))|~arboreal(X98))|leaf_occ(X98,X99))|root_occ(X98,X99))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 15.45/12.81 fof(f200,plain,(
% 15.45/12.81 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|root_occ(X1,X0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f199])).
% 15.45/12.81 fof(f203,plain,(
% 15.45/12.81 ![X102,X103]: ((((~occurrence_of(X103,tptp0)|~subactivity_occurrence(X102,X103))|~arboreal(X102))|leaf_occ(X102,X103))|(?[X104]: (occurrence_of(X104,tptp1)&next_subocc(X102,X104,tptp0))))),
% 15.45/12.81 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 15.45/12.81 fof(f204,plain,(
% 15.45/12.81 ![X102]: ((![X103]: (((~occurrence_of(X103,tptp0)|~subactivity_occurrence(X102,X103))|~arboreal(X102))|leaf_occ(X102,X103)))|(?[X104]: (occurrence_of(X104,tptp1)&next_subocc(X102,X104,tptp0))))),
% 15.45/12.81 inference(miniscoping,[status(thm)],[f203])).
% 15.45/12.81 fof(f205,plain,(
% 15.45/12.81 ![X102]: ((![X103]: (((~occurrence_of(X103,tptp0)|~subactivity_occurrence(X102,X103))|~arboreal(X102))|leaf_occ(X102,X103)))|(occurrence_of(sK16_skl(X102),tptp1)&next_subocc(X102,sK16_skl(X102),tptp0)))),
% 15.45/12.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(X104,sK16_skl(X102))],[f204])).
% 15.45/12.81 fof(f206,plain,(
% 15.45/12.81 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp1))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f205])).
% 15.45/12.81 fof(f207,plain,(
% 15.45/12.81 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK16_skl(X1),tptp0))),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f205])).
% 15.45/12.81 fof(f208,plain,(
% 15.45/12.81 occurrence_of(sK17_skl,tptp0)),
% 15.45/12.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X105,sK17_skl)],[f50])).
% 15.45/12.81 fof(f209,plain,(
% 15.45/12.81 occurrence_of(sK17_skl,tptp0)),
% 15.45/12.81 inference(cnf_transformation,[status(thm)],[f208])).
% 15.45/12.81 fof(f211,plain,(
% 15.45/12.81 ![X0]: (~occurrence_of(sK17_skl,X0)|tptp0=X0)),
% 15.45/12.81 inference(resolution,[status(thm)],[f143,f209])).
% 15.45/12.81 fof(f245,plain,(
% 15.45/12.81 root_occ(sK14_skl(sK17_skl),sK17_skl)),
% 15.45/12.81 inference(resolution,[status(thm)],[f183,f209])).
% 15.45/12.81 fof(f250,plain,(
% 15.45/12.81 root(sK14_skl(sK17_skl),sK1_skl(sK17_skl,sK14_skl(sK17_skl)))),
% 15.45/12.81 inference(resolution,[status(thm)],[f245,f93])).
% 15.45/12.81 fof(f251,plain,(
% 15.45/12.81 occurrence_of(sK17_skl,sK1_skl(sK17_skl,sK14_skl(sK17_skl)))),
% 15.45/12.81 inference(resolution,[status(thm)],[f245,f91])).
% 15.45/12.81 fof(f252,plain,(
% 15.45/12.81 subactivity_occurrence(sK14_skl(sK17_skl),sK17_skl)),
% 15.45/12.81 inference(resolution,[status(thm)],[f245,f92])).
% 15.45/12.81 fof(f292,plain,(
% 15.45/12.81 ![X0,X1]: (~leaf_occ(X0,sK17_skl)|~min_precedes(X0,X1,tptp0))),
% 15.45/12.81 inference(resolution,[status(thm)],[f140,f209])).
% 15.45/12.81 fof(f295,plain,(
% 15.45/12.81 tptp0=sK1_skl(sK17_skl,sK14_skl(sK17_skl))),
% 15.45/12.81 inference(resolution,[status(thm)],[f251,f211])).
% 15.45/12.81 fof(f314,plain,(
% 15.45/12.81 root(sK14_skl(sK17_skl),tptp0)),
% 15.45/12.81 inference(forward_demodulation,[status(thm)],[f295,f250])).
% 15.45/12.81 fof(f319,plain,(
% 15.45/12.81 legal(sK14_skl(sK17_skl))),
% 15.45/12.81 inference(resolution,[status(thm)],[f314,f104])).
% 15.45/12.81 fof(f320,plain,(
% 15.45/12.81 arboreal(sK14_skl(sK17_skl))),
% 15.45/12.81 inference(resolution,[status(thm)],[f319,f127])).
% 15.45/12.81 fof(f563,plain,(
% 15.45/12.81 next_subocc(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 15.45/12.81 inference(resolution,[status(thm)],[f186,f209])).
% 15.45/12.81 fof(f595,plain,(
% 15.45/12.81 min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 15.45/12.81 inference(resolution,[status(thm)],[f563,f67])).
% 15.45/12.81 fof(f618,plain,(
% 15.45/12.81 ~leaf_occ(sK14_skl(sK17_skl),sK17_skl)),
% 15.45/12.81 inference(resolution,[status(thm)],[f595,f292])).
% 15.45/12.81 fof(f648,plain,(
% 15.45/12.81 ~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)),
% 15.45/12.81 inference(resolution,[status(thm)],[f206,f252])).
% 15.45/12.81 fof(f649,plain,(
% 15.45/12.81 ~arboreal(sK14_skl(sK17_skl))|leaf_occ(sK14_skl(sK17_skl),sK17_skl)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f648,f209])).
% 15.45/12.81 fof(f654,plain,(
% 15.45/12.81 ~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)),
% 15.45/12.81 inference(resolution,[status(thm)],[f207,f252])).
% 15.45/12.81 fof(f655,plain,(
% 15.45/12.81 ~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)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f654,f209])).
% 15.45/12.81 fof(f1178,plain,(
% 15.45/12.81 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f649,f320])).
% 15.45/12.81 fof(f1194,plain,(
% 15.45/12.81 ![X0]: (leaf_occ(sK14_skl(sK17_skl),sK17_skl)|~occurrence_of(sK16_skl(sK14_skl(sK17_skl)),X0)|X0=tptp1)),
% 15.45/12.81 inference(resolution,[status(thm)],[f1178,f143])).
% 15.45/12.81 fof(f1207,plain,(
% 15.45/12.81 ![X0]: (~occurrence_of(sK16_skl(sK14_skl(sK17_skl)),X0)|X0=tptp1)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f1194,f618])).
% 15.45/12.81 fof(f1216,plain,(
% 15.45/12.81 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|next_subocc(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f655,f320])).
% 15.45/12.81 fof(f1217,plain,(
% 15.45/12.81 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|arboreal(sK16_skl(sK14_skl(sK17_skl)))),
% 15.45/12.81 inference(resolution,[status(thm)],[f1216,f74])).
% 15.45/12.81 fof(f1220,plain,(
% 15.45/12.81 leaf_occ(sK14_skl(sK17_skl),sK17_skl)|min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 15.45/12.81 inference(resolution,[status(thm)],[f1216,f67])).
% 15.45/12.81 fof(f1221,plain,(
% 15.45/12.81 arboreal(sK16_skl(sK14_skl(sK17_skl)))),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f1217,f618])).
% 15.45/12.81 fof(f1223,plain,(
% 15.45/12.81 min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f1220,f618])).
% 15.45/12.81 fof(f1247,plain,(
% 15.45/12.81 subactivity_occurrence(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 15.45/12.81 inference(resolution,[status(thm)],[f1223,f152])).
% 15.45/12.81 fof(f1249,plain,(
% 15.45/12.81 occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0)),
% 15.45/12.81 inference(resolution,[status(thm)],[f1223,f150])).
% 15.45/12.81 fof(f1906,plain,(
% 15.45/12.81 occurrence_of(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp3)),
% 15.45/12.81 inference(resolution,[status(thm)],[f1249,f184])).
% 15.45/12.81 fof(f1908,plain,(
% 15.45/12.81 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))),
% 15.45/12.81 inference(resolution,[status(thm)],[f1249,f185])).
% 15.45/12.81 fof(f1914,plain,(
% 15.45/12.81 ![X0,X1]: (~root_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|~min_precedes(X1,X0,tptp0))),
% 15.45/12.81 inference(resolution,[status(thm)],[f1249,f137])).
% 15.45/12.81 fof(f1922,plain,(
% 15.45/12.81 ![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)),
% 15.45/12.81 inference(resolution,[status(thm)],[f1249,f62])).
% 15.45/12.81 fof(f1931,plain,(
% 15.45/12.81 ![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)),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f1922,f188])).
% 15.45/12.81 fof(f3049,plain,(
% 15.45/12.81 ~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))),
% 15.45/12.81 inference(resolution,[status(thm)],[f1247,f200])).
% 15.45/12.81 fof(f3060,plain,(
% 15.45/12.81 ~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))),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f3049,f1249])).
% 15.45/12.81 fof(f3903,plain,(
% 15.45/12.81 ~root_occ(sK16_skl(sK14_skl(sK17_skl)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))),
% 15.45/12.81 inference(resolution,[status(thm)],[f1914,f1223])).
% 15.45/12.81 fof(f11535,plain,(
% 15.45/12.81 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))),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f3060,f1221])).
% 15.45/12.81 fof(f11540,plain,(
% 15.45/12.81 ![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)))),
% 15.45/12.81 inference(resolution,[status(thm)],[f11535,f1931])).
% 15.45/12.81 fof(f11555,plain,(
% 15.45/12.81 ![X0]: (~leaf_occ(X0,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))|X0=sK16_skl(sK14_skl(sK17_skl)))),
% 15.45/12.81 inference(forward_subsumption_resolution,[status(thm)],[f11540,f3903])).
% 15.45/12.81 fof(f12768,plain,(
% 15.45/12.81 sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))=sK16_skl(sK14_skl(sK17_skl))),
% 15.45/12.81 inference(resolution,[status(thm)],[f11555,f1908])).
% 15.45/12.81 fof(f12856,plain,(
% 15.45/12.81 occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp3)),
% 15.45/12.81 inference(backward_demodulation,[status(thm)],[f12768,f1906])).
% 12.32/12.86 fof(f12864,plain,(
% 12.32/12.86 tptp3=tptp1),
% 12.32/12.86 inference(resolution,[status(thm)],[f12856,f1207])).
% 12.32/12.86 fof(f12891,plain,(
% 12.32/12.86 $false),
% 12.32/12.86 inference(forward_subsumption_resolution,[status(thm)],[f12864,f196])).
% 12.32/12.86 % SZS output end CNFRefutation for theBenchmark.p
% 12.32/12.86 % Elapsed time: 2.122409 seconds
% 12.32/12.86 % CPU time: 16.577057 seconds
% 12.32/12.86 % Total memory used: 216.901 MB
% 12.32/12.86 % Net memory used: 207.466 MB
%------------------------------------------------------------------------------