%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO003+4 : 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 : n011.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 10.66s 1.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO003+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n011.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 03:40:40 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 10.66/1.87 % Refutation found
% 10.66/1.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.66/1.87 % SZS output start CNFRefutation for theBenchmark
% 10.66/1.87 fof(f3,axiom,(
% 10.66/1.87 (! [X8,X9,X10,X11] :( ( occurrence_of(X9,X8)& subactivity_occurrence(X10,X9)& leaf_occ(X11,X9)& arboreal(X10)& ~ min_precedes(X10,X11,X8) )=> X11 = X10 ) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f4,axiom,(
% 10.66/1.87 (! [X12,X13] :( occurrence_of(X13,X12)=> ( activity(X12)& activity_occurrence(X13) ) ) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f7,axiom,(
% 10.66/1.87 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f9,axiom,(
% 10.66/1.87 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f13,axiom,(
% 10.66/1.87 (! [X41] :( activity_occurrence(X41)=> (? [X42] :( activity(X42)& occurrence_of(X41,X42) ) )) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f17,axiom,(
% 10.66/1.87 (! [X51,X52] :( occurrence_of(X51,X52)=> ( arboreal(X51)<=> atomic(X52) ) ) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f20,axiom,(
% 10.66/1.87 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f27,axiom,(
% 10.66/1.87 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f30,axiom,(
% 10.66/1.87 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f33,axiom,(
% 10.66/1.87 (! [X101] :( occurrence_of(X101,tptp0)=> (? [X102,X103] :( occurrence_of(X102,tptp4)& root_occ(X102,X101)& occurrence_of(X103,tptp3)& leaf_occ(X103,X101)& next_subocc(X102,X103,tptp0) ) )) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f39,axiom,(
% 10.66/1.87 atomic(tptp1) ),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f43,axiom,(
% 10.66/1.87 tptp1 != tptp3 ),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f46,axiom,(
% 10.66/1.87 (! [X104,X105] :( ( occurrence_of(X105,tptp0)& root_occ(X104,X105) )=> (? [X106] :( occurrence_of(X106,tptp1)& next_subocc(X104,X106,tptp0) ) )) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f47,conjecture,(
% 10.66/1.87 ~ (? [X107] : occurrence_of(X107,tptp0) )),
% 10.66/1.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.66/1.87 fof(f48,negated_conjecture,(
% 10.66/1.87 ~(~ (? [X107] : occurrence_of(X107,tptp0) ))),
% 10.66/1.87 inference(negated_conjecture,[status(cth)],[f47])).
% 10.66/1.87 fof(f56,plain,(
% 10.66/1.87 ![X8,X9,X10,X11]: (((((~occurrence_of(X9,X8)|~subactivity_occurrence(X10,X9))|~leaf_occ(X11,X9))|~arboreal(X10))|min_precedes(X10,X11,X8))|X11=X10)),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 10.66/1.87 fof(f57,plain,(
% 10.66/1.87 ![X10,X11]: ((![X8]: (((![X9]: ((~occurrence_of(X9,X8)|~subactivity_occurrence(X10,X9))|~leaf_occ(X11,X9)))|~arboreal(X10))|min_precedes(X10,X11,X8)))|X11=X10)),
% 10.66/1.87 inference(miniscoping,[status(thm)],[f56])).
% 10.66/1.87 fof(f58,plain,(
% 10.66/1.87 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~subactivity_occurrence(X2,X0)|~leaf_occ(X3,X0)|~arboreal(X2)|min_precedes(X2,X3,X1)|X3=X2)),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f57])).
% 10.66/1.87 fof(f59,plain,(
% 10.66/1.87 ![X12,X13]: (~occurrence_of(X13,X12)|(activity(X12)&activity_occurrence(X13)))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 10.66/1.87 fof(f61,plain,(
% 10.66/1.87 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f59])).
% 10.66/1.87 fof(f69,plain,(
% 10.66/1.87 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 10.66/1.87 fof(f70,plain,(
% 10.66/1.87 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|((occurrence_of(sK2_skl(X23,X22,X21),X21)&subactivity_occurrence(X22,sK2_skl(X23,X22,X21)))&subactivity_occurrence(X23,sK2_skl(X23,X22,X21))))),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f69])).
% 10.66/1.87 fof(f71,plain,(
% 10.66/1.87 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f70])).
% 10.66/1.87 fof(f72,plain,(
% 10.66/1.87 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f70])).
% 10.66/1.87 fof(f73,plain,(
% 10.66/1.87 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK2_skl(X1,X0,X2)))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f70])).
% 10.66/1.87 fof(f78,plain,(
% 10.66/1.87 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 10.66/1.87 fof(f79,plain,(
% 10.66/1.87 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 10.66/1.87 inference(miniscoping,[status(thm)],[f78])).
% 10.66/1.87 fof(f80,plain,(
% 10.66/1.87 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f79])).
% 10.66/1.87 fof(f90,plain,(
% 10.66/1.87 ![X41]: (~activity_occurrence(X41)|(?[X42]: (activity(X42)&occurrence_of(X41,X42))))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 10.66/1.87 fof(f91,plain,(
% 10.66/1.87 ![X41]: (~activity_occurrence(X41)|(activity(sK4_skl(X41))&occurrence_of(X41,sK4_skl(X41))))),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f90])).
% 10.66/1.87 fof(f93,plain,(
% 10.66/1.87 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK4_skl(X0)))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f91])).
% 10.66/1.87 fof(f111,plain,(
% 10.66/1.87 ![X51,X52]: (~occurrence_of(X51,X52)|(arboreal(X51)<=>atomic(X52)))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 10.66/1.87 fof(f112,plain,(
% 10.66/1.87 ![X51,X52]: (~occurrence_of(X51,X52)|((~arboreal(X51)|atomic(X52))&(arboreal(X51)|~atomic(X52))))),
% 10.66/1.87 inference(NNF_transformation,[status(thm)],[f111])).
% 10.66/1.87 fof(f114,plain,(
% 10.66/1.87 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f112])).
% 10.66/1.87 fof(f125,plain,(
% 10.66/1.87 ![X58,X59]: ((~root_occ(X58,X59)|(?[X60]: ((occurrence_of(X59,X60)&subactivity_occurrence(X58,X59))&root(X58,X60))))&(root_occ(X58,X59)|(![X60]: ((~occurrence_of(X59,X60)|~subactivity_occurrence(X58,X59))|~root(X58,X60)))))),
% 10.66/1.87 inference(NNF_transformation,[status(thm)],[f20])).
% 10.66/1.87 fof(f126,plain,(
% 10.66/1.87 (![X58,X59]: (~root_occ(X58,X59)|(?[X60]: ((occurrence_of(X59,X60)&subactivity_occurrence(X58,X59))&root(X58,X60)))))&(![X58,X59]: (root_occ(X58,X59)|(![X60]: ((~occurrence_of(X59,X60)|~subactivity_occurrence(X58,X59))|~root(X58,X60)))))),
% 10.66/1.87 inference(miniscoping,[status(thm)],[f125])).
% 10.66/1.87 fof(f127,plain,(
% 10.66/1.87 (![X58,X59]: (~root_occ(X58,X59)|((occurrence_of(X59,sK9_skl(X59,X58))&subactivity_occurrence(X58,X59))&root(X58,sK9_skl(X59,X58)))))&(![X58,X59]: (root_occ(X58,X59)|(![X60]: ((~occurrence_of(X59,X60)|~subactivity_occurrence(X58,X59))|~root(X58,X60)))))),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f126])).
% 10.66/1.87 fof(f128,plain,(
% 10.66/1.87 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK9_skl(X1,X0)))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f127])).
% 10.66/1.87 fof(f130,plain,(
% 10.66/1.87 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK9_skl(X1,X0)))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f127])).
% 10.66/1.87 fof(f131,plain,(
% 10.66/1.87 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f127])).
% 10.66/1.87 fof(f154,plain,(
% 10.66/1.87 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 10.66/1.87 fof(f155,plain,(
% 10.66/1.87 ![X78,X79,X80]: ((~next_subocc(X78,X79,X80)|(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))&(next_subocc(X78,X79,X80)|(~min_precedes(X78,X79,X80)|(?[X81]: (min_precedes(X78,X81,X80)&min_precedes(X81,X79,X80))))))),
% 10.66/1.87 inference(NNF_transformation,[status(thm)],[f154])).
% 10.66/1.87 fof(f156,plain,(
% 10.66/1.87 (![X78,X79,X80]: (~next_subocc(X78,X79,X80)|(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80))))))&(![X78,X79,X80]: (next_subocc(X78,X79,X80)|(~min_precedes(X78,X79,X80)|(?[X81]: (min_precedes(X78,X81,X80)&min_precedes(X81,X79,X80))))))),
% 10.66/1.87 inference(miniscoping,[status(thm)],[f155])).
% 10.66/1.87 fof(f157,plain,(
% 10.66/1.87 (![X78,X79,X80]: (~next_subocc(X78,X79,X80)|(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80))))))&(![X78,X79,X80]: (next_subocc(X78,X79,X80)|(~min_precedes(X78,X79,X80)|(min_precedes(X78,sK11_skl(X80,X79,X78),X80)&min_precedes(sK11_skl(X80,X79,X78),X79,X80)))))),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f156])).
% 10.66/1.87 fof(f158,plain,(
% 10.66/1.87 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f157])).
% 10.66/1.87 fof(f159,plain,(
% 10.66/1.87 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f157])).
% 10.66/1.87 fof(f168,plain,(
% 10.66/1.87 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 10.66/1.87 fof(f169,plain,(
% 10.66/1.87 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 10.66/1.87 inference(miniscoping,[status(thm)],[f168])).
% 10.66/1.87 fof(f170,plain,(
% 10.66/1.87 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f169])).
% 10.66/1.87 fof(f177,plain,(
% 10.66/1.87 ![X101]: (~occurrence_of(X101,tptp0)|(?[X102,X103]: ((((occurrence_of(X102,tptp4)&root_occ(X102,X101))&occurrence_of(X103,tptp3))&leaf_occ(X103,X101))&next_subocc(X102,X103,tptp0))))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 10.66/1.87 fof(f178,plain,(
% 10.66/1.87 ![X101]: (~occurrence_of(X101,tptp0)|((((occurrence_of(sK12_skl(X101),tptp4)&root_occ(sK12_skl(X101),X101))&occurrence_of(sK13_skl(X101),tptp3))&leaf_occ(sK13_skl(X101),X101))&next_subocc(sK12_skl(X101),sK13_skl(X101),tptp0)))),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f177])).
% 10.66/1.87 fof(f180,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK12_skl(X0),X0))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f178])).
% 10.66/1.87 fof(f181,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK13_skl(X0),tptp3))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f178])).
% 10.66/1.87 fof(f182,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK13_skl(X0),X0))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f178])).
% 10.66/1.87 fof(f183,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f178])).
% 10.66/1.87 fof(f189,plain,(
% 10.66/1.87 atomic(tptp1)),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f39])).
% 10.66/1.87 fof(f193,plain,(
% 10.66/1.87 ~tptp1=tptp3),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f43])).
% 10.66/1.87 fof(f196,plain,(
% 10.66/1.87 ![X104,X105]: ((~occurrence_of(X105,tptp0)|~root_occ(X104,X105))|(?[X106]: (occurrence_of(X106,tptp1)&next_subocc(X104,X106,tptp0))))),
% 10.66/1.87 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 10.66/1.87 fof(f197,plain,(
% 10.66/1.87 ![X104]: ((![X105]: (~occurrence_of(X105,tptp0)|~root_occ(X104,X105)))|(?[X106]: (occurrence_of(X106,tptp1)&next_subocc(X104,X106,tptp0))))),
% 10.66/1.87 inference(miniscoping,[status(thm)],[f196])).
% 10.66/1.87 fof(f198,plain,(
% 10.66/1.87 ![X104]: ((![X105]: (~occurrence_of(X105,tptp0)|~root_occ(X104,X105)))|(occurrence_of(sK14_skl(X104),tptp1)&next_subocc(X104,sK14_skl(X104),tptp0)))),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X106,sK14_skl(X104))],[f197])).
% 10.66/1.87 fof(f199,plain,(
% 10.66/1.87 ![X0,X1]: (~occurrence_of(X0,tptp0)|~root_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp1))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f198])).
% 10.66/1.87 fof(f200,plain,(
% 10.66/1.87 ![X0,X1]: (~occurrence_of(X0,tptp0)|~root_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f198])).
% 10.66/1.87 fof(f201,plain,(
% 10.66/1.87 occurrence_of(sK15_skl,tptp0)),
% 10.66/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X107,sK15_skl)],[f48])).
% 10.66/1.87 fof(f202,plain,(
% 10.66/1.87 occurrence_of(sK15_skl,tptp0)),
% 10.66/1.87 inference(cnf_transformation,[status(thm)],[f201])).
% 10.66/1.87 fof(f203,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(sK15_skl,X0)|X0=tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f80,f202])).
% 10.66/1.87 fof(f282,plain,(
% 10.66/1.87 root_occ(sK12_skl(sK15_skl),sK15_skl)),
% 10.66/1.87 inference(resolution,[status(thm)],[f180,f202])).
% 10.66/1.87 fof(f283,plain,(
% 10.66/1.87 root(sK12_skl(sK15_skl),sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 10.66/1.87 inference(resolution,[status(thm)],[f282,f130])).
% 10.66/1.87 fof(f284,plain,(
% 10.66/1.87 occurrence_of(sK15_skl,sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 10.66/1.87 inference(resolution,[status(thm)],[f282,f128])).
% 10.66/1.87 fof(f308,plain,(
% 10.66/1.87 sK9_skl(sK15_skl,sK12_skl(sK15_skl))=tptp0),
% 10.66/1.87 inference(resolution,[status(thm)],[f284,f203])).
% 10.66/1.87 fof(f333,plain,(
% 10.66/1.87 root(sK12_skl(sK15_skl),tptp0)),
% 10.66/1.87 inference(forward_demodulation,[status(thm)],[f308,f283])).
% 10.66/1.87 fof(f630,plain,(
% 10.66/1.87 ![X0]: (~root_occ(X0,sK15_skl)|occurrence_of(sK14_skl(X0),tptp1))),
% 10.66/1.87 inference(resolution,[status(thm)],[f199,f202])).
% 10.66/1.87 fof(f631,plain,(
% 10.66/1.87 occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)),
% 10.66/1.87 inference(resolution,[status(thm)],[f630,f282])).
% 10.66/1.87 fof(f636,plain,(
% 10.66/1.87 arboreal(sK14_skl(sK12_skl(sK15_skl)))|~atomic(tptp1)),
% 10.66/1.87 inference(resolution,[status(thm)],[f631,f114])).
% 10.66/1.87 fof(f640,plain,(
% 10.66/1.87 activity_occurrence(sK14_skl(sK12_skl(sK15_skl)))),
% 10.66/1.87 inference(resolution,[status(thm)],[f631,f61])).
% 10.66/1.87 fof(f644,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(sK14_skl(sK12_skl(sK15_skl)),X0)|X0=tptp1)),
% 10.66/1.87 inference(resolution,[status(thm)],[f631,f80])).
% 10.66/1.87 fof(f646,plain,(
% 10.66/1.87 arboreal(sK14_skl(sK12_skl(sK15_skl)))),
% 10.66/1.87 inference(forward_subsumption_resolution,[status(thm)],[f636,f189])).
% 10.66/1.87 fof(f647,plain,(
% 10.66/1.87 occurrence_of(sK14_skl(sK12_skl(sK15_skl)),sK4_skl(sK14_skl(sK12_skl(sK15_skl))))),
% 10.66/1.87 inference(resolution,[status(thm)],[f640,f93])).
% 10.66/1.87 fof(f728,plain,(
% 10.66/1.87 sK4_skl(sK14_skl(sK12_skl(sK15_skl)))=tptp1),
% 10.66/1.87 inference(resolution,[status(thm)],[f647,f644])).
% 10.66/1.87 fof(f752,plain,(
% 10.66/1.87 ![X0]: (~root_occ(X0,sK15_skl)|next_subocc(X0,sK14_skl(X0),tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f200,f202])).
% 10.66/1.87 fof(f753,plain,(
% 10.66/1.87 next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f752,f282])).
% 10.66/1.87 fof(f754,plain,(
% 10.66/1.87 min_precedes(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f753,f158])).
% 10.66/1.87 fof(f762,plain,(
% 10.66/1.87 ![X0]: (~next_subocc(sK12_skl(sK15_skl),X0,tptp0)|~min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f754,f159])).
% 10.66/1.87 fof(f768,plain,(
% 10.66/1.87 subactivity_occurrence(sK14_skl(sK12_skl(sK15_skl)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f754,f73])).
% 10.66/1.87 fof(f769,plain,(
% 10.66/1.87 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f754,f72])).
% 10.66/1.87 fof(f770,plain,(
% 10.66/1.87 occurrence_of(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0),tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f754,f71])).
% 10.66/1.87 fof(f840,plain,(
% 10.66/1.87 next_subocc(sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f183])).
% 10.66/1.87 fof(f841,plain,(
% 10.66/1.87 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp3)),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f181])).
% 10.66/1.87 fof(f843,plain,(
% 10.66/1.87 leaf_occ(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f182])).
% 10.66/1.87 fof(f844,plain,(
% 10.66/1.87 root_occ(sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f180])).
% 10.66/1.87 fof(f846,plain,(
% 10.66/1.87 ![X0]: (root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~subactivity_occurrence(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~root(X0,tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f131])).
% 10.66/1.87 fof(f848,plain,(
% 10.66/1.87 ![X0,X1]: (~root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~root_occ(X1,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|X0=X1)),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f170])).
% 10.66/1.87 fof(f853,plain,(
% 10.66/1.87 ![X0,X1]: (~subactivity_occurrence(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~leaf_occ(X1,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~arboreal(X0)|min_precedes(X0,X1,tptp0)|X1=X0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f770,f58])).
% 10.66/1.87 fof(f1046,plain,(
% 10.66/1.87 activity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 10.66/1.87 inference(resolution,[status(thm)],[f841,f61])).
% 10.66/1.87 fof(f1050,plain,(
% 10.66/1.87 ![X0]: (~occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),X0)|X0=tptp3)),
% 10.66/1.87 inference(resolution,[status(thm)],[f841,f80])).
% 10.66/1.87 fof(f1053,plain,(
% 10.66/1.87 occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))))),
% 10.66/1.87 inference(resolution,[status(thm)],[f1046,f93])).
% 10.66/1.87 fof(f3269,plain,(
% 10.66/1.87 ![X0]: (~root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|X0=sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
% 10.66/1.87 inference(resolution,[status(thm)],[f848,f844])).
% 10.66/1.87 fof(f3326,plain,(
% 10.66/1.87 sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))=tptp3),
% 10.66/1.87 inference(resolution,[status(thm)],[f1053,f1050])).
% 10.66/1.87 fof(f3848,plain,(
% 10.66/1.87 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~root(sK12_skl(sK15_skl),tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f846,f769])).
% 10.66/1.87 fof(f3851,plain,(
% 10.66/1.87 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 10.66/1.87 inference(forward_subsumption_resolution,[status(thm)],[f3848,f333])).
% 10.66/1.87 fof(f3852,plain,(
% 10.66/1.87 sK12_skl(sK15_skl)=sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
% 10.66/1.87 inference(resolution,[status(thm)],[f3851,f3269])).
% 10.66/1.87 fof(f3868,plain,(
% 10.66/1.87 next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 10.66/1.87 inference(backward_demodulation,[status(thm)],[f3852,f840])).
% 10.66/1.87 fof(f4161,plain,(
% 10.66/1.87 ![X0]: (~leaf_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|~arboreal(sK14_skl(sK12_skl(sK15_skl)))|min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0)|X0=sK14_skl(sK12_skl(sK15_skl)))),
% 10.66/1.87 inference(resolution,[status(thm)],[f853,f768])).
% 10.66/1.87 fof(f4165,plain,(
% 10.66/1.87 ![X0]: (~leaf_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))|min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0)|X0=sK14_skl(sK12_skl(sK15_skl)))),
% 10.66/1.87 inference(forward_subsumption_resolution,[status(thm)],[f4161,f646])).
% 10.66/1.87 fof(f4235,plain,(
% 10.66/1.87 min_precedes(sK14_skl(sK12_skl(sK15_skl)),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)|sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))),
% 10.66/1.87 inference(resolution,[status(thm)],[f4165,f843])).
% 10.66/1.87 fof(f6249,plain,(
% 10.66/1.87 sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))|~next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)),
% 10.66/1.87 inference(resolution,[status(thm)],[f4235,f762])).
% 10.66/1.87 fof(f6268,plain,(
% 10.66/1.87 sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))=sK14_skl(sK12_skl(sK15_skl))),
% 10.66/1.87 inference(forward_subsumption_resolution,[status(thm)],[f6249,f3868])).
% 10.66/1.87 fof(f6318,plain,(
% 10.66/1.87 sK4_skl(sK14_skl(sK12_skl(sK15_skl)))=tptp3),
% 10.66/1.87 inference(backward_demodulation,[status(thm)],[f6268,f3326])).
% 10.66/1.87 fof(f6356,plain,(
% 10.66/1.87 tptp1=tptp3),
% 10.66/1.87 inference(forward_demodulation,[status(thm)],[f728,f6318])).
% 10.66/1.87 fof(f6357,plain,(
% 10.66/1.87 $false),
% 10.66/1.87 inference(forward_subsumption_resolution,[status(thm)],[f6356,f193])).
% 10.66/1.87 % SZS output end CNFRefutation for theBenchmark.p
% 3.09/1.92 % Elapsed time: 1.466294 seconds
% 3.09/1.92 % CPU time: 11.239219 seconds
% 3.09/1.92 % Total memory used: 184.776 MB
% 3.09/1.92 % Net memory used: 179.064 MB
%------------------------------------------------------------------------------