%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO012+4 : 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 : n012.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:25 PM UTC 2026
% Result : Theorem 0.14s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PRO012+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Mon Sep 21 03:42:23 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.30 % Drodi V4.1.1
% 0.14/0.43 % Refutation found
% 0.14/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.43 fof(f7,axiom,(
% 0.14/0.43 (! [X21,X22,X23] :( min_precedes(X22,X23,X21)=> (? [X24] :( occurrence_of(X24,X21)& subactivity_occurrence(X22,X24)& subactivity_occurrence(X23,X24) ) )) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f9,axiom,(
% 0.14/0.43 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f20,axiom,(
% 0.14/0.43 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f24,axiom,(
% 0.14/0.43 (! [X68,X69,X70] :( min_precedes(X68,X69,X70)=> (? [X71] :( root(X71,X70)& min_precedes(X71,X69,X70) ) )) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f28,axiom,(
% 0.14/0.43 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f30,axiom,(
% 0.14/0.43 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f33,axiom,(
% 0.14/0.43 (! [X101] :( occurrence_of(X101,tptp0)=> (? [X102,X103,X104] :( occurrence_of(X102,tptp3)& root_occ(X102,X101)& occurrence_of(X103,tptp4)& min_precedes(X102,X103,tptp0)& ( occurrence_of(X104,tptp2)| occurrence_of(X104,tptp1) )& min_precedes(X103,X104,tptp0)& (! [X105] :( min_precedes(X102,X105,tptp0)=> ( X105 = X103| X105 = X104 ) ) )) )) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f46,conjecture,(
% 0.14/0.43 (! [X106] :( occurrence_of(X106,tptp0)=> (? [X107,X108] :( occurrence_of(X107,tptp3)& root_occ(X107,X106)& ( occurrence_of(X108,tptp2)| occurrence_of(X108,tptp1) )& min_precedes(X107,X108,tptp0) ) )) )),
% 0.14/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.43 fof(f47,negated_conjecture,(
% 0.14/0.43 ~((! [X106] :( occurrence_of(X106,tptp0)=> (? [X107,X108] :( occurrence_of(X107,tptp3)& root_occ(X107,X106)& ( occurrence_of(X108,tptp2)| occurrence_of(X108,tptp1) )& min_precedes(X107,X108,tptp0) ) )) ))),
% 0.14/0.43 inference(negated_conjecture,[status(cth)],[f46])).
% 0.14/0.43 fof(f68,plain,(
% 0.14/0.43 ![X21,X22,X23]: (~min_precedes(X22,X23,X21)|(?[X24]: ((occurrence_of(X24,X21)&subactivity_occurrence(X22,X24))&subactivity_occurrence(X23,X24))))),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/0.43 fof(f69,plain,(
% 0.14/0.43 ![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))))),
% 0.14/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f68])).
% 0.14/0.43 fof(f70,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK2_skl(X1,X0,X2),X2))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.43 fof(f71,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK2_skl(X1,X0,X2)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.43 fof(f72,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK2_skl(X1,X0,X2)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.43 fof(f77,plain,(
% 0.14/0.43 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.43 fof(f78,plain,(
% 0.14/0.43 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f77])).
% 0.14/0.43 fof(f79,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f78])).
% 0.14/0.43 fof(f124,plain,(
% 0.14/0.43 ![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)))))),
% 0.14/0.43 inference(NNF_transformation,[status(thm)],[f20])).
% 0.14/0.43 fof(f125,plain,(
% 0.14/0.43 (![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)))))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f124])).
% 0.14/0.43 fof(f126,plain,(
% 0.14/0.43 (![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)))))),
% 0.14/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f125])).
% 0.14/0.43 fof(f127,plain,(
% 0.14/0.43 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK9_skl(X1,X0)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f126])).
% 0.14/0.43 fof(f129,plain,(
% 0.14/0.43 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK9_skl(X1,X0)))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f126])).
% 0.14/0.43 fof(f130,plain,(
% 0.14/0.43 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f126])).
% 0.14/0.43 fof(f141,plain,(
% 0.14/0.43 ![X68,X69,X70]: (~min_precedes(X68,X69,X70)|(?[X71]: (root(X71,X70)&min_precedes(X71,X69,X70))))),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.14/0.43 fof(f142,plain,(
% 0.14/0.43 ![X69,X70]: ((![X68]: ~min_precedes(X68,X69,X70))|(?[X71]: (root(X71,X70)&min_precedes(X71,X69,X70))))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f141])).
% 0.14/0.43 fof(f143,plain,(
% 0.14/0.43 ![X69,X70]: ((![X68]: ~min_precedes(X68,X69,X70))|(root(sK10_skl(X70,X69),X70)&min_precedes(sK10_skl(X70,X69),X69,X70)))),
% 0.14/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X71,sK10_skl(X70,X69))],[f142])).
% 0.14/0.43 fof(f144,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|root(sK10_skl(X2,X1),X2))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f143])).
% 0.14/0.43 fof(f145,plain,(
% 0.14/0.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK10_skl(X2,X1),X1,X2))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f143])).
% 0.14/0.43 fof(f161,plain,(
% 0.14/0.43 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.14/0.43 fof(f162,plain,(
% 0.14/0.43 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f161])).
% 0.14/0.43 fof(f163,plain,(
% 0.14/0.43 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f162])).
% 0.14/0.43 fof(f167,plain,(
% 0.14/0.43 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.14/0.43 fof(f168,plain,(
% 0.14/0.43 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 0.14/0.43 inference(miniscoping,[status(thm)],[f167])).
% 0.14/0.43 fof(f169,plain,(
% 0.14/0.43 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 0.14/0.43 inference(cnf_transformation,[status(thm)],[f168])).
% 0.14/0.43 fof(f176,plain,(
% 0.14/0.43 ![X101]: (~occurrence_of(X101,tptp0)|(?[X102,X103,X104]: ((((((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&min_precedes(X102,X103,tptp0))&(occurrence_of(X104,tptp2)|occurrence_of(X104,tptp1)))&min_precedes(X103,X104,tptp0))&(![X105]: (~min_precedes(X102,X105,tptp0)|(X105=X103|X105=X104))))))),
% 0.14/0.43 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.14/0.43 fof(f177,plain,(
% 0.14/0.43 ![X101]: (~occurrence_of(X101,tptp0)|((((((occurrence_of(sK12_skl(X101),tptp3)&root_occ(sK12_skl(X101),X101))&occurrence_of(sK13_skl(X101),tptp4))&min_precedes(sK12_skl(X101),sK13_skl(X101),tptp0))&(occurrence_of(sK14_skl(X101),tptp2)|occurrence_of(sK14_skl(X101),tptp1)))&min_precedes(sK13_skl(X101),sK14_skl(X101),tptp0))&(![X105]: (~min_precedes(sK12_skl(X101),X105,tptp0)|(X105=sK13_skl(X101)|X105=sK14_skl(X101))))))),
% 0.14/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101)),skolemize(X104,sK14_skl(X101))],[f176])).
% 0.14/0.44 fof(f178,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK12_skl(X0),tptp3))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f177])).
% 0.14/0.44 fof(f179,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK12_skl(X0),X0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f177])).
% 0.14/0.44 fof(f181,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|min_precedes(sK12_skl(X0),sK13_skl(X0),tptp0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f177])).
% 0.14/0.44 fof(f182,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK14_skl(X0),tptp2)|occurrence_of(sK14_skl(X0),tptp1))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f177])).
% 0.14/0.44 fof(f183,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|min_precedes(sK13_skl(X0),sK14_skl(X0),tptp0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f177])).
% 0.14/0.44 fof(f197,plain,(
% 0.14/0.44 (?[X106]: (occurrence_of(X106,tptp0)&(![X107,X108]: (((~occurrence_of(X107,tptp3)|~root_occ(X107,X106))|(~occurrence_of(X108,tptp2)&~occurrence_of(X108,tptp1)))|~min_precedes(X107,X108,tptp0)))))),
% 0.14/0.44 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.14/0.44 fof(f198,plain,(
% 0.14/0.44 (occurrence_of(sK15_skl,tptp0)&(![X107,X108]: (((~occurrence_of(X107,tptp3)|~root_occ(X107,sK15_skl))|(~occurrence_of(X108,tptp2)&~occurrence_of(X108,tptp1)))|~min_precedes(X107,X108,tptp0))))),
% 0.14/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X106,sK15_skl)],[f197])).
% 0.14/0.44 fof(f199,plain,(
% 0.14/0.44 occurrence_of(sK15_skl,tptp0)),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/0.44 fof(f200,plain,(
% 0.14/0.44 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK15_skl)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/0.44 fof(f201,plain,(
% 0.14/0.44 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK15_skl)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0))),
% 0.14/0.44 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/0.44 fof(f202,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(sK15_skl,X0)|X0=tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f79,f199])).
% 0.14/0.44 fof(f279,plain,(
% 0.14/0.44 root_occ(sK12_skl(sK15_skl),sK15_skl)),
% 0.14/0.44 inference(resolution,[status(thm)],[f179,f199])).
% 0.14/0.44 fof(f281,plain,(
% 0.14/0.44 root(sK12_skl(sK15_skl),sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f279,f129])).
% 0.14/0.44 fof(f282,plain,(
% 0.14/0.44 occurrence_of(sK15_skl,sK9_skl(sK15_skl,sK12_skl(sK15_skl)))),
% 0.14/0.44 inference(resolution,[status(thm)],[f279,f127])).
% 0.14/0.44 fof(f292,plain,(
% 0.14/0.44 occurrence_of(sK12_skl(sK15_skl),tptp3)),
% 0.14/0.44 inference(resolution,[status(thm)],[f178,f199])).
% 0.14/0.44 fof(f305,plain,(
% 0.14/0.44 sK9_skl(sK15_skl,sK12_skl(sK15_skl))=tptp0),
% 0.14/0.44 inference(resolution,[status(thm)],[f282,f202])).
% 0.14/0.44 fof(f319,plain,(
% 0.14/0.44 root(sK12_skl(sK15_skl),tptp0)),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f305,f281])).
% 0.14/0.44 fof(f443,plain,(
% 0.14/0.44 min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f181,f199])).
% 0.14/0.44 fof(f559,plain,(
% 0.14/0.44 min_precedes(sK13_skl(sK15_skl),sK14_skl(sK15_skl),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f183,f199])).
% 0.14/0.44 fof(f567,plain,(
% 0.14/0.44 min_precedes(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK14_skl(sK15_skl),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f559,f145])).
% 0.14/0.44 fof(f569,plain,(
% 0.14/0.44 subactivity_occurrence(sK14_skl(sK15_skl),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f559,f72])).
% 0.14/0.44 fof(f570,plain,(
% 0.14/0.44 root(sK10_skl(tptp0,sK14_skl(sK15_skl)),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f559,f144])).
% 0.14/0.44 fof(f571,plain,(
% 0.14/0.44 subactivity_occurrence(sK13_skl(sK15_skl),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f559,f71])).
% 0.14/0.44 fof(f572,plain,(
% 0.14/0.44 occurrence_of(sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f559,f70])).
% 0.14/0.44 fof(f593,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK13_skl(sK15_skl),X0)|subactivity_occurrence(sK12_skl(sK15_skl),X0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f163,f443])).
% 0.14/0.44 fof(f713,plain,(
% 0.14/0.44 ~occurrence_of(sK10_skl(tptp0,sK14_skl(sK15_skl)),tptp3)|~root_occ(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(resolution,[status(thm)],[f567,f201])).
% 0.14/0.44 fof(f714,plain,(
% 0.14/0.44 ~occurrence_of(sK10_skl(tptp0,sK14_skl(sK15_skl)),tptp3)|~root_occ(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp2)),
% 0.14/0.44 inference(resolution,[status(thm)],[f567,f200])).
% 0.14/0.44 fof(f715,plain,(
% 0.14/0.44 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK14_skl(sK15_skl),X0)|subactivity_occurrence(sK10_skl(tptp0,sK14_skl(sK15_skl)),X0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f567,f163])).
% 0.14/0.44 fof(f741,plain,(
% 0.14/0.44 occurrence_of(sK14_skl(sK15_skl),tptp2)|occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(resolution,[status(thm)],[f182,f199])).
% 0.14/0.44 fof(f755,plain,(
% 0.14/0.44 ![X0]: (root_occ(X0,sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|~subactivity_occurrence(X0,sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|~root(X0,tptp0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f572,f130])).
% 0.14/0.44 fof(f766,plain,(
% 0.14/0.44 ![X0,X1]: (~root_occ(X0,sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|~root_occ(X1,sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|X0=X1)),
% 0.14/0.44 inference(resolution,[status(thm)],[f572,f169])).
% 0.14/0.44 fof(f1086,plain,(
% 0.14/0.44 ~occurrence_of(sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),tptp0)|subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f593,f571])).
% 0.14/0.44 fof(f1088,plain,(
% 0.14/0.44 subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1086,f572])).
% 0.14/0.44 fof(f1581,plain,(
% 0.14/0.44 ~occurrence_of(sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),tptp0)|subactivity_occurrence(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(resolution,[status(thm)],[f715,f569])).
% 0.14/0.44 fof(f1583,plain,(
% 0.14/0.44 subactivity_occurrence(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1581,f572])).
% 0.14/0.44 fof(f2572,plain,(
% 0.14/0.44 root_occ(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|~root(sK10_skl(tptp0,sK14_skl(sK15_skl)),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f755,f1583])).
% 0.14/0.44 fof(f2575,plain,(
% 0.14/0.44 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|~root(sK12_skl(sK15_skl),tptp0)),
% 0.14/0.44 inference(resolution,[status(thm)],[f755,f1088])).
% 0.14/0.44 fof(f2576,plain,(
% 0.14/0.44 root_occ(sK10_skl(tptp0,sK14_skl(sK15_skl)),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2572,f570])).
% 0.14/0.44 fof(f2577,plain,(
% 0.14/0.44 root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2575,f319])).
% 0.14/0.44 fof(f2698,plain,(
% 0.14/0.44 ![X0]: (~root_occ(X0,sK2_skl(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0))|X0=sK12_skl(sK15_skl))),
% 0.14/0.44 inference(resolution,[status(thm)],[f766,f2577])).
% 0.14/0.44 fof(f2699,plain,(
% 0.14/0.44 sK10_skl(tptp0,sK14_skl(sK15_skl))=sK12_skl(sK15_skl)),
% 0.14/0.44 inference(resolution,[status(thm)],[f2698,f2576])).
% 0.14/0.44 fof(f2711,plain,(
% 0.14/0.44 ~occurrence_of(sK10_skl(tptp0,sK14_skl(sK15_skl)),tptp3)|~root_occ(sK12_skl(sK15_skl),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp2)),
% 0.14/0.44 inference(backward_demodulation,[status(thm)],[f2699,f714])).
% 0.14/0.44 fof(f2712,plain,(
% 0.14/0.44 ~occurrence_of(sK10_skl(tptp0,sK14_skl(sK15_skl)),tptp3)|~root_occ(sK12_skl(sK15_skl),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(backward_demodulation,[status(thm)],[f2699,f713])).
% 0.14/0.44 fof(f2779,plain,(
% 0.14/0.44 ~occurrence_of(sK12_skl(sK15_skl),tptp3)|~root_occ(sK12_skl(sK15_skl),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp2)),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f2699,f2711])).
% 0.14/0.44 fof(f2780,plain,(
% 0.14/0.44 ~root_occ(sK12_skl(sK15_skl),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp2)),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2779,f292])).
% 0.14/0.44 fof(f2781,plain,(
% 0.14/0.44 ~occurrence_of(sK12_skl(sK15_skl),tptp3)|~root_occ(sK12_skl(sK15_skl),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(forward_demodulation,[status(thm)],[f2699,f2712])).
% 0.14/0.44 fof(f2782,plain,(
% 0.14/0.44 ~root_occ(sK12_skl(sK15_skl),sK15_skl)|~occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2781,f292])).
% 0.14/0.44 fof(f2830,plain,(
% 0.14/0.44 occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(backward_subsumption_resolution,[status(thm)],[f741,f2831])).
% 0.14/0.44 fof(f2831,plain,(
% 0.14/0.44 ~occurrence_of(sK14_skl(sK15_skl),tptp2)),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2780,f279])).
% 0.14/0.44 fof(f2876,plain,(
% 0.14/0.44 ~occurrence_of(sK14_skl(sK15_skl),tptp1)),
% 0.14/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2782,f279])).
% 0.14/0.44 fof(f2877,plain,(
% 0.14/0.44 $false),
% 0.14/0.44 inference(backward_subsumption_resolution,[status(thm)],[f2830,f2876])).
% 0.14/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.46 % Elapsed time: 0.163649 seconds
% 0.14/0.46 % CPU time: 1.045949 seconds
% 0.14/0.46 % Total memory used: 113.207 MB
% 0.14/0.46 % Net memory used: 111.390 MB
%------------------------------------------------------------------------------