%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO012+3 : 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 : n008.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:24 PM UTC 2026
% Result : Theorem 0.13s 6.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO012+3 : 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/5.36 % Computer : n008.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Mon Sep 21 03:43:15 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 0.13/6.02 % Refutation found
% 0.13/6.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/6.02 % SZS output start CNFRefutation for theBenchmark
% 0.13/6.02 fof(f1,axiom,(
% 0.13/6.02 (! [X0,X1] :( occurrence_of(X1,X0)=> ( activity(X0)& activity_occurrence(X1) ) ) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f2,axiom,(
% 0.13/6.02 (! [X2] :( activity_occurrence(X2)=> (? [X3] :( activity(X3)& occurrence_of(X2,X3) ) )) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f3,axiom,(
% 0.13/6.02 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f14,axiom,(
% 0.13/6.02 (! [X31,X32,X33] :( min_precedes(X31,X32,X33)=> (? [X34] :( root(X34,X33)& min_precedes(X34,X32,X33) ) )) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f26,axiom,(
% 0.13/6.02 (! [X69,X70,X71] :( min_precedes(X70,X71,X69)=> (? [X72] :( occurrence_of(X72,X69)& subactivity_occurrence(X70,X72)& subactivity_occurrence(X71,X72) ) )) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f30,axiom,(
% 0.13/6.02 (! [X83,X84,X85,X86] :( ( min_precedes(X83,X84,X85)& occurrence_of(X86,X85)& subactivity_occurrence(X84,X86) )=> subactivity_occurrence(X83,X86) ) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f34,axiom,(
% 0.13/6.02 (! [X99,X100] :( root_occ(X99,X100)<=> (? [X101] :( occurrence_of(X100,X101)& subactivity_occurrence(X99,X100)& root(X99,X101) ) )) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f36,axiom,(
% 0.13/6.02 (! [X105,X106,X107,X108] :( ( occurrence_of(X107,X108)& root_occ(X105,X107)& root_occ(X106,X107) )=> X105 = X106 ) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f50,axiom,(
% 0.13/6.02 (! [X161] :( occurrence_of(X161,tptp0)=> (? [X162,X163,X164] :( occurrence_of(X162,tptp3)& root_occ(X162,X161)& occurrence_of(X163,tptp4)& min_precedes(X162,X163,tptp0)& ( occurrence_of(X164,tptp2)| occurrence_of(X164,tptp1) )& min_precedes(X163,X164,tptp0)& (! [X165] :( min_precedes(X162,X165,tptp0)=> ( X165 = X163| X165 = X164 ) ) )) )) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f62,axiom,(
% 0.13/6.02 tptp2 != tptp1 ),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f63,conjecture,(
% 0.13/6.02 (! [X166] :( occurrence_of(X166,tptp0)=> (? [X167,X168] :( occurrence_of(X167,tptp3)& root_occ(X167,X166)& ( occurrence_of(X168,tptp2)| occurrence_of(X168,tptp1) )& min_precedes(X167,X168,tptp0) ) )) )),
% 0.13/6.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/6.02 fof(f64,negated_conjecture,(
% 0.13/6.02 ~((! [X166] :( occurrence_of(X166,tptp0)=> (? [X167,X168] :( occurrence_of(X167,tptp3)& root_occ(X167,X166)& ( occurrence_of(X168,tptp2)| occurrence_of(X168,tptp1) )& min_precedes(X167,X168,tptp0) ) )) ))),
% 0.13/6.02 inference(negated_conjecture,[status(cth)],[f63])).
% 0.13/6.02 fof(f65,plain,(
% 0.13/6.02 ![X0,X1]: (~occurrence_of(X1,X0)|(activity(X0)&activity_occurrence(X1)))),
% 0.13/6.02 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.13/6.02 fof(f67,plain,(
% 0.13/6.02 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 0.13/6.02 inference(cnf_transformation,[status(thm)],[f65])).
% 0.13/6.02 fof(f68,plain,(
% 0.13/6.02 ![X2]: (~activity_occurrence(X2)|(?[X3]: (activity(X3)&occurrence_of(X2,X3))))),
% 0.13/6.02 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/6.02 fof(f69,plain,(
% 0.13/6.02 ![X2]: (~activity_occurrence(X2)|(activity(sK0_skl(X2))&occurrence_of(X2,sK0_skl(X2))))),
% 0.13/6.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X3,sK0_skl(X2))],[f68])).
% 0.13/6.02 fof(f71,plain,(
% 0.13/6.02 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK0_skl(X0)))),
% 0.13/6.02 inference(cnf_transformation,[status(thm)],[f69])).
% 0.13/6.02 fof(f72,plain,(
% 0.13/6.02 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 0.13/6.02 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.13/6.02 fof(f73,plain,(
% 0.13/6.02 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 0.13/6.02 inference(miniscoping,[status(thm)],[f72])).
% 0.13/6.02 fof(f74,plain,(
% 0.13/6.02 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.13/6.02 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/6.02 fof(f110,plain,(
% 0.13/6.02 ![X31,X32,X33]: (~min_precedes(X31,X32,X33)|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 0.13/6.02 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.13/6.02 fof(f111,plain,(
% 0.13/6.02 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 0.13/6.02 inference(miniscoping,[status(thm)],[f110])).
% 0.13/6.02 fof(f112,plain,(
% 0.13/6.02 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(root(sK4_skl(X33,X32),X33)&min_precedes(sK4_skl(X33,X32),X32,X33)))),
% 0.13/6.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X34,sK4_skl(X33,X32))],[f111])).
% 0.13/6.02 fof(f113,plain,(
% 0.13/6.02 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|root(sK4_skl(X2,X1),X2))),
% 0.13/6.02 inference(cnf_transformation,[status(thm)],[f112])).
% 0.13/6.02 fof(f114,plain,(
% 0.13/6.02 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK4_skl(X2,X1),X1,X2))),
% 0.13/6.02 inference(cnf_transformation,[status(thm)],[f112])).
% 0.13/6.02 fof(f161,plain,(
% 0.13/6.02 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|(?[X72]: ((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))))),
% 0.13/6.02 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.13/6.02 fof(f162,plain,(
% 0.13/6.03 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|((occurrence_of(sK9_skl(X71,X70,X69),X69)&subactivity_occurrence(X70,sK9_skl(X71,X70,X69)))&subactivity_occurrence(X71,sK9_skl(X71,X70,X69))))),
% 0.13/6.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f161])).
% 0.13/6.03 fof(f163,plain,(
% 0.13/6.03 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK9_skl(X1,X0,X2),X2))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f162])).
% 0.13/6.03 fof(f164,plain,(
% 0.13/6.03 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK9_skl(X1,X0,X2)))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f162])).
% 0.13/6.03 fof(f165,plain,(
% 0.13/6.03 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK9_skl(X1,X0,X2)))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f162])).
% 0.13/6.03 fof(f177,plain,(
% 0.13/6.03 ![X83,X84,X85,X86]: (((~min_precedes(X83,X84,X85)|~occurrence_of(X86,X85))|~subactivity_occurrence(X84,X86))|subactivity_occurrence(X83,X86))),
% 0.13/6.03 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.13/6.03 fof(f178,plain,(
% 0.13/6.03 ![X83,X86]: ((![X84]: ((![X85]: (~min_precedes(X83,X84,X85)|~occurrence_of(X86,X85)))|~subactivity_occurrence(X84,X86)))|subactivity_occurrence(X83,X86))),
% 0.13/6.03 inference(miniscoping,[status(thm)],[f177])).
% 0.13/6.03 fof(f179,plain,(
% 0.13/6.03 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f178])).
% 0.13/6.03 fof(f191,plain,(
% 0.13/6.03 ![X99,X100]: ((~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101))))&(root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 0.13/6.03 inference(NNF_transformation,[status(thm)],[f34])).
% 0.13/6.03 fof(f192,plain,(
% 0.13/6.03 (![X99,X100]: (~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 0.13/6.03 inference(miniscoping,[status(thm)],[f191])).
% 0.13/6.03 fof(f193,plain,(
% 0.13/6.03 (![X99,X100]: (~root_occ(X99,X100)|((occurrence_of(X100,sK13_skl(X100,X99))&subactivity_occurrence(X99,X100))&root(X99,sK13_skl(X100,X99)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 0.13/6.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f192])).
% 0.13/6.03 fof(f194,plain,(
% 0.13/6.03 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK13_skl(X1,X0)))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/6.03 fof(f196,plain,(
% 0.13/6.03 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK13_skl(X1,X0)))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/6.03 fof(f197,plain,(
% 0.13/6.03 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/6.03 fof(f205,plain,(
% 0.13/6.03 ![X105,X106,X107,X108]: (((~occurrence_of(X107,X108)|~root_occ(X105,X107))|~root_occ(X106,X107))|X105=X106)),
% 0.13/6.03 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.13/6.03 fof(f206,plain,(
% 0.13/6.03 ![X105,X106]: ((![X107]: (((![X108]: ~occurrence_of(X107,X108))|~root_occ(X105,X107))|~root_occ(X106,X107)))|X105=X106)),
% 0.13/6.03 inference(miniscoping,[status(thm)],[f205])).
% 0.13/6.03 fof(f207,plain,(
% 0.13/6.03 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f206])).
% 0.13/6.03 fof(f249,plain,(
% 0.13/6.03 ![X161]: (~occurrence_of(X161,tptp0)|(?[X162,X163,X164]: ((((((occurrence_of(X162,tptp3)&root_occ(X162,X161))&occurrence_of(X163,tptp4))&min_precedes(X162,X163,tptp0))&(occurrence_of(X164,tptp2)|occurrence_of(X164,tptp1)))&min_precedes(X163,X164,tptp0))&(![X165]: (~min_precedes(X162,X165,tptp0)|(X165=X163|X165=X164))))))),
% 0.13/6.03 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.13/6.03 fof(f250,plain,(
% 0.13/6.03 ![X161]: (~occurrence_of(X161,tptp0)|((((((occurrence_of(sK16_skl(X161),tptp3)&root_occ(sK16_skl(X161),X161))&occurrence_of(sK17_skl(X161),tptp4))&min_precedes(sK16_skl(X161),sK17_skl(X161),tptp0))&(occurrence_of(sK18_skl(X161),tptp2)|occurrence_of(sK18_skl(X161),tptp1)))&min_precedes(sK17_skl(X161),sK18_skl(X161),tptp0))&(![X165]: (~min_precedes(sK16_skl(X161),X165,tptp0)|(X165=sK17_skl(X161)|X165=sK18_skl(X161))))))),
% 0.13/6.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X162,sK16_skl(X161)),skolemize(X163,sK17_skl(X161)),skolemize(X164,sK18_skl(X161))],[f249])).
% 0.13/6.03 fof(f251,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK16_skl(X0),tptp3))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f250])).
% 0.13/6.03 fof(f252,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK16_skl(X0),X0))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f250])).
% 0.13/6.03 fof(f254,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|min_precedes(sK16_skl(X0),sK17_skl(X0),tptp0))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f250])).
% 0.13/6.03 fof(f255,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK18_skl(X0),tptp2)|occurrence_of(sK18_skl(X0),tptp1))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f250])).
% 0.13/6.03 fof(f256,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|min_precedes(sK17_skl(X0),sK18_skl(X0),tptp0))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f250])).
% 0.13/6.03 fof(f269,plain,(
% 0.13/6.03 ~tptp2=tptp1),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/6.03 fof(f270,plain,(
% 0.13/6.03 (?[X166]: (occurrence_of(X166,tptp0)&(![X167,X168]: (((~occurrence_of(X167,tptp3)|~root_occ(X167,X166))|(~occurrence_of(X168,tptp2)&~occurrence_of(X168,tptp1)))|~min_precedes(X167,X168,tptp0)))))),
% 0.13/6.03 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.13/6.03 fof(f271,plain,(
% 0.13/6.03 (occurrence_of(sK19_skl,tptp0)&(![X167,X168]: (((~occurrence_of(X167,tptp3)|~root_occ(X167,sK19_skl))|(~occurrence_of(X168,tptp2)&~occurrence_of(X168,tptp1)))|~min_precedes(X167,X168,tptp0))))),
% 0.13/6.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(X166,sK19_skl)],[f270])).
% 0.13/6.03 fof(f272,plain,(
% 0.13/6.03 occurrence_of(sK19_skl,tptp0)),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f271])).
% 0.13/6.03 fof(f273,plain,(
% 0.13/6.03 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK19_skl)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f271])).
% 0.13/6.03 fof(f274,plain,(
% 0.13/6.03 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK19_skl)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0))),
% 0.13/6.03 inference(cnf_transformation,[status(thm)],[f271])).
% 0.13/6.03 fof(f275,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(sK19_skl,X0)|X0=tptp0)),
% 0.13/6.03 inference(resolution,[status(thm)],[f74,f272])).
% 0.13/6.03 fof(f297,plain,(
% 0.13/6.03 root_occ(sK16_skl(sK19_skl),sK19_skl)),
% 0.13/6.03 inference(resolution,[status(thm)],[f252,f272])).
% 0.13/6.03 fof(f299,plain,(
% 0.13/6.03 root(sK16_skl(sK19_skl),sK13_skl(sK19_skl,sK16_skl(sK19_skl)))),
% 0.13/6.03 inference(resolution,[status(thm)],[f297,f196])).
% 0.13/6.03 fof(f300,plain,(
% 0.13/6.03 occurrence_of(sK19_skl,sK13_skl(sK19_skl,sK16_skl(sK19_skl)))),
% 0.13/6.03 inference(resolution,[status(thm)],[f297,f194])).
% 0.13/6.03 fof(f308,plain,(
% 0.13/6.03 sK13_skl(sK19_skl,sK16_skl(sK19_skl))=tptp0),
% 0.13/6.03 inference(resolution,[status(thm)],[f300,f275])).
% 0.13/6.03 fof(f320,plain,(
% 0.13/6.03 root(sK16_skl(sK19_skl),tptp0)),
% 0.13/6.03 inference(backward_demodulation,[status(thm)],[f308,f299])).
% 0.13/6.03 fof(f342,plain,(
% 0.13/6.03 occurrence_of(sK16_skl(sK19_skl),tptp3)),
% 0.13/6.03 inference(resolution,[status(thm)],[f251,f272])).
% 0.13/6.03 fof(f642,plain,(
% 0.13/6.03 min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)),
% 0.13/6.03 inference(resolution,[status(thm)],[f254,f272])).
% 0.13/6.03 fof(f703,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK17_skl(sK19_skl),X0)|subactivity_occurrence(sK16_skl(sK19_skl),X0))),
% 0.13/6.03 inference(resolution,[status(thm)],[f179,f642])).
% 0.13/6.03 fof(f784,plain,(
% 0.13/6.03 min_precedes(sK17_skl(sK19_skl),sK18_skl(sK19_skl),tptp0)),
% 0.13/6.03 inference(resolution,[status(thm)],[f256,f272])).
% 0.13/6.03 fof(f795,plain,(
% 0.13/6.03 subactivity_occurrence(sK18_skl(sK19_skl),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.03 inference(resolution,[status(thm)],[f784,f165])).
% 0.13/6.03 fof(f796,plain,(
% 0.13/6.03 subactivity_occurrence(sK17_skl(sK19_skl),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.03 inference(resolution,[status(thm)],[f784,f164])).
% 0.13/6.03 fof(f797,plain,(
% 0.13/6.03 occurrence_of(sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0),tptp0)),
% 0.13/6.03 inference(resolution,[status(thm)],[f784,f163])).
% 0.13/6.03 fof(f799,plain,(
% 0.13/6.03 min_precedes(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK18_skl(sK19_skl),tptp0)),
% 0.13/6.03 inference(resolution,[status(thm)],[f784,f114])).
% 0.13/6.03 fof(f801,plain,(
% 0.13/6.03 root(sK4_skl(tptp0,sK18_skl(sK19_skl)),tptp0)),
% 0.13/6.03 inference(resolution,[status(thm)],[f784,f113])).
% 0.13/6.03 fof(f1183,plain,(
% 0.13/6.03 ![X0]: (root_occ(X0,sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|~subactivity_occurrence(X0,sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|~root(X0,tptp0))),
% 0.13/6.03 inference(resolution,[status(thm)],[f797,f197])).
% 0.13/6.03 fof(f1195,plain,(
% 0.13/6.03 ![X0,X1]: (~root_occ(X0,sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|~root_occ(X1,sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|X0=X1)),
% 0.13/6.03 inference(resolution,[status(thm)],[f797,f207])).
% 0.13/6.03 fof(f1204,plain,(
% 0.13/6.03 ~occurrence_of(sK4_skl(tptp0,sK18_skl(sK19_skl)),tptp3)|~root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp1)),
% 0.13/6.03 inference(resolution,[status(thm)],[f799,f274])).
% 0.13/6.03 fof(f1205,plain,(
% 0.13/6.03 ~occurrence_of(sK4_skl(tptp0,sK18_skl(sK19_skl)),tptp3)|~root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 0.13/6.03 inference(resolution,[status(thm)],[f799,f273])).
% 0.13/6.03 fof(f1206,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK18_skl(sK19_skl),X0)|subactivity_occurrence(sK4_skl(tptp0,sK18_skl(sK19_skl)),X0))),
% 0.13/6.03 inference(resolution,[status(thm)],[f799,f179])).
% 0.13/6.03 fof(f1359,plain,(
% 0.13/6.03 occurrence_of(sK18_skl(sK19_skl),tptp2)|occurrence_of(sK18_skl(sK19_skl),tptp1)),
% 0.13/6.03 inference(resolution,[status(thm)],[f255,f272])).
% 0.13/6.03 fof(f1381,plain,(
% 0.13/6.03 occurrence_of(sK18_skl(sK19_skl),tptp1)|activity_occurrence(sK18_skl(sK19_skl))),
% 0.13/6.03 inference(resolution,[status(thm)],[f1359,f67])).
% 0.13/6.03 fof(f1386,plain,(
% 0.13/6.03 activity_occurrence(sK18_skl(sK19_skl))),
% 0.13/6.03 inference(forward_subsumption_resolution,[status(thm)],[f1381,f67])).
% 0.13/6.03 fof(f1388,plain,(
% 0.13/6.03 occurrence_of(sK18_skl(sK19_skl),sK0_skl(sK18_skl(sK19_skl)))),
% 0.13/6.03 inference(resolution,[status(thm)],[f1386,f71])).
% 0.13/6.03 fof(f1434,plain,(
% 0.13/6.03 ![X0]: (~occurrence_of(sK18_skl(sK19_skl),X0)|X0=sK0_skl(sK18_skl(sK19_skl)))),
% 0.13/6.03 inference(resolution,[status(thm)],[f1388,f74])).
% 0.13/6.03 fof(f1442,plain,(
% 0.13/6.03 tptp2=sK0_skl(sK18_skl(sK19_skl))|occurrence_of(sK18_skl(sK19_skl),tptp1)),
% 0.13/6.03 inference(resolution,[status(thm)],[f1434,f1359])).
% 0.13/6.03 fof(f1449,plain,(
% 0.13/6.03 tptp2=sK0_skl(sK18_skl(sK19_skl))|tptp1=sK0_skl(sK18_skl(sK19_skl))),
% 0.13/6.03 inference(resolution,[status(thm)],[f1442,f1434])).
% 0.13/6.03 fof(f1477,plain,(
% 0.13/6.03 occurrence_of(sK18_skl(sK19_skl),tptp2)|tptp1=sK0_skl(sK18_skl(sK19_skl))),
% 0.13/6.03 inference(paramodulation,[status(thm)],[f1449,f1388])).
% 0.13/6.03 fof(f1578,plain,(
% 0.13/6.03 ~occurrence_of(sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0),tptp0)|subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.03 inference(resolution,[status(thm)],[f703,f796])).
% 0.13/6.03 fof(f1580,plain,(
% 0.13/6.03 subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.03 inference(forward_subsumption_resolution,[status(thm)],[f1578,f797])).
% 0.13/6.03 fof(f4463,plain,(
% 0.13/6.03 ~occurrence_of(sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0),tptp0)|subactivity_occurrence(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.05 inference(resolution,[status(thm)],[f1206,f795])).
% 0.13/6.05 fof(f4465,plain,(
% 0.13/6.05 subactivity_occurrence(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f4463,f797])).
% 0.13/6.05 fof(f6451,plain,(
% 0.13/6.05 root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|~root(sK4_skl(tptp0,sK18_skl(sK19_skl)),tptp0)),
% 0.13/6.05 inference(resolution,[status(thm)],[f1183,f4465])).
% 0.13/6.05 fof(f6454,plain,(
% 0.13/6.05 root_occ(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|~root(sK16_skl(sK19_skl),tptp0)),
% 0.13/6.05 inference(resolution,[status(thm)],[f1183,f1580])).
% 0.13/6.05 fof(f6455,plain,(
% 0.13/6.05 root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6451,f801])).
% 0.13/6.05 fof(f6456,plain,(
% 0.13/6.05 root_occ(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6454,f320])).
% 0.13/6.05 fof(f6627,plain,(
% 0.13/6.05 ![X0]: (~root_occ(X0,sK9_skl(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0))|X0=sK16_skl(sK19_skl))),
% 0.13/6.05 inference(resolution,[status(thm)],[f1195,f6456])).
% 0.13/6.05 fof(f6628,plain,(
% 0.13/6.05 sK4_skl(tptp0,sK18_skl(sK19_skl))=sK16_skl(sK19_skl)),
% 0.13/6.05 inference(resolution,[status(thm)],[f6627,f6455])).
% 0.13/6.05 fof(f6824,plain,(
% 0.13/6.05 ~occurrence_of(sK16_skl(sK19_skl),tptp3)|~root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp1)),
% 0.13/6.05 inference(forward_demodulation,[status(thm)],[f6628,f1204])).
% 0.13/6.05 fof(f6825,plain,(
% 0.13/6.05 ~occurrence_of(sK16_skl(sK19_skl),tptp3)|~root_occ(sK16_skl(sK19_skl),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp1)),
% 0.13/6.05 inference(forward_demodulation,[status(thm)],[f6628,f6824])).
% 0.13/6.05 fof(f6826,plain,(
% 0.13/6.05 ~root_occ(sK16_skl(sK19_skl),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp1)),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6825,f342])).
% 0.13/6.05 fof(f6827,plain,(
% 0.13/6.05 ~root_occ(sK16_skl(sK19_skl),sK19_skl)|tptp2=sK0_skl(sK18_skl(sK19_skl))),
% 0.13/6.05 inference(resolution,[status(thm)],[f6826,f1442])).
% 0.13/6.05 fof(f6829,plain,(
% 0.13/6.05 tptp2=sK0_skl(sK18_skl(sK19_skl))),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6827,f297])).
% 0.13/6.05 fof(f6831,plain,(
% 0.13/6.05 ~occurrence_of(sK16_skl(sK19_skl),tptp3)|~root_occ(sK4_skl(tptp0,sK18_skl(sK19_skl)),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 0.13/6.05 inference(forward_demodulation,[status(thm)],[f6628,f1205])).
% 0.13/6.05 fof(f6832,plain,(
% 0.13/6.05 ~occurrence_of(sK16_skl(sK19_skl),tptp3)|~root_occ(sK16_skl(sK19_skl),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 0.13/6.05 inference(forward_demodulation,[status(thm)],[f6628,f6831])).
% 0.13/6.05 fof(f6833,plain,(
% 0.13/6.05 ~root_occ(sK16_skl(sK19_skl),sK19_skl)|~occurrence_of(sK18_skl(sK19_skl),tptp2)),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6832,f342])).
% 0.13/6.05 fof(f6834,plain,(
% 0.13/6.05 ~root_occ(sK16_skl(sK19_skl),sK19_skl)|tptp1=sK0_skl(sK18_skl(sK19_skl))),
% 0.13/6.05 inference(resolution,[status(thm)],[f6833,f1477])).
% 0.13/6.05 fof(f6836,plain,(
% 0.13/6.05 tptp1=sK0_skl(sK18_skl(sK19_skl))),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6834,f297])).
% 0.13/6.05 fof(f6932,plain,(
% 0.13/6.05 tptp2=tptp1),
% 0.13/6.05 inference(backward_demodulation,[status(thm)],[f6836,f6829])).
% 0.13/6.05 fof(f6933,plain,(
% 0.13/6.05 $false),
% 0.13/6.05 inference(forward_subsumption_resolution,[status(thm)],[f6932,f269])).
% 0.13/6.05 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/6.06 % Elapsed time: 0.683462 seconds
% 0.13/6.06 % CPU time: 5.171663 seconds
% 0.13/6.06 % Total memory used: 152.890 MB
% 0.13/6.06 % Net memory used: 148.401 MB
%------------------------------------------------------------------------------