%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO009+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 : 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:23 PM UTC 2026
% Result : Theorem 0.10s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO009+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:44:01 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.44 % Refutation found
% 0.10/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.44 fof(f19,axiom,(
% 0.10/0.44 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f20,axiom,(
% 0.10/0.44 (! [X58,X59] :( root_occ(X58,X59)<=> (? [X60] :( occurrence_of(X59,X60)& subactivity_occurrence(X58,X59)& root(X58,X60) ) )) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f24,axiom,(
% 0.10/0.44 (! [X68,X69,X70] :( min_precedes(X68,X69,X70)=> (? [X71] :( root(X71,X70)& min_precedes(X71,X69,X70) ) )) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f27,axiom,(
% 0.10/0.44 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f28,axiom,(
% 0.10/0.44 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f30,axiom,(
% 0.10/0.44 (! [X90,X91,X92,X93] :( ( occurrence_of(X92,X93)& root_occ(X90,X92)& root_occ(X91,X92) )=> X90 = X91 ) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f33,axiom,(
% 0.10/0.44 (! [X101] :( occurrence_of(X101,tptp0)=> (? [X102,X103,X104] :( occurrence_of(X102,tptp3)& root_occ(X102,X101)& occurrence_of(X103,tptp4)& next_subocc(X102,X103,tptp0)& ( occurrence_of(X104,tptp2)| occurrence_of(X104,tptp1) )& next_subocc(X103,X104,tptp0)& leaf_occ(X104,X101) ) )) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f46,conjecture,(
% 0.10/0.44 (! [X105] :( occurrence_of(X105,tptp0)=> (? [X106,X107] :( occurrence_of(X106,tptp3)& root_occ(X106,X105)& ( occurrence_of(X107,tptp2)| occurrence_of(X107,tptp1) )& min_precedes(X106,X107,tptp0)& leaf_occ(X107,X105) ) )) )),
% 0.10/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f47,negated_conjecture,(
% 0.10/0.44 ~((! [X105] :( occurrence_of(X105,tptp0)=> (? [X106,X107] :( occurrence_of(X106,tptp3)& root_occ(X106,X105)& ( occurrence_of(X107,tptp2)| occurrence_of(X107,tptp1) )& min_precedes(X106,X107,tptp0)& leaf_occ(X107,X105) ) )) ))),
% 0.10/0.44 inference(negated_conjecture,[status(cth)],[f46])).
% 0.10/0.44 fof(f117,plain,(
% 0.10/0.44 ![X55,X56]: ((~leaf_occ(X55,X56)|(?[X57]: ((occurrence_of(X56,X57)&subactivity_occurrence(X55,X56))&leaf(X55,X57))))&(leaf_occ(X55,X56)|(![X57]: ((~occurrence_of(X56,X57)|~subactivity_occurrence(X55,X56))|~leaf(X55,X57)))))),
% 0.10/0.44 inference(NNF_transformation,[status(thm)],[f19])).
% 0.10/0.44 fof(f118,plain,(
% 0.10/0.44 (![X55,X56]: (~leaf_occ(X55,X56)|(?[X57]: ((occurrence_of(X56,X57)&subactivity_occurrence(X55,X56))&leaf(X55,X57)))))&(![X55,X56]: (leaf_occ(X55,X56)|(![X57]: ((~occurrence_of(X56,X57)|~subactivity_occurrence(X55,X56))|~leaf(X55,X57)))))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f117])).
% 0.10/0.44 fof(f119,plain,(
% 0.10/0.44 (![X55,X56]: (~leaf_occ(X55,X56)|((occurrence_of(X56,sK8_skl(X56,X55))&subactivity_occurrence(X55,X56))&leaf(X55,sK8_skl(X56,X55)))))&(![X55,X56]: (leaf_occ(X55,X56)|(![X57]: ((~occurrence_of(X56,X57)|~subactivity_occurrence(X55,X56))|~leaf(X55,X57)))))),
% 0.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f118])).
% 0.10/0.44 fof(f121,plain,(
% 0.10/0.44 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f119])).
% 0.10/0.44 fof(f124,plain,(
% 0.10/0.44 ![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.10/0.44 inference(NNF_transformation,[status(thm)],[f20])).
% 0.10/0.44 fof(f125,plain,(
% 0.10/0.44 (![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.10/0.44 inference(miniscoping,[status(thm)],[f124])).
% 0.10/0.44 fof(f126,plain,(
% 0.10/0.44 (![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.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f125])).
% 0.10/0.44 fof(f130,plain,(
% 0.10/0.44 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f126])).
% 0.10/0.44 fof(f141,plain,(
% 0.10/0.44 ![X68,X69,X70]: (~min_precedes(X68,X69,X70)|(?[X71]: (root(X71,X70)&min_precedes(X71,X69,X70))))),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.10/0.44 fof(f142,plain,(
% 0.10/0.44 ![X69,X70]: ((![X68]: ~min_precedes(X68,X69,X70))|(?[X71]: (root(X71,X70)&min_precedes(X71,X69,X70))))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f141])).
% 0.10/0.44 fof(f143,plain,(
% 0.10/0.44 ![X69,X70]: ((![X68]: ~min_precedes(X68,X69,X70))|(root(sK10_skl(X70,X69),X70)&min_precedes(sK10_skl(X70,X69),X69,X70)))),
% 0.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X71,sK10_skl(X70,X69))],[f142])).
% 0.10/0.44 fof(f144,plain,(
% 0.10/0.44 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|root(sK10_skl(X2,X1),X2))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f143])).
% 0.10/0.44 fof(f145,plain,(
% 0.10/0.44 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK10_skl(X2,X1),X1,X2))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f143])).
% 0.10/0.44 fof(f153,plain,(
% 0.10/0.44 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.10/0.44 fof(f154,plain,(
% 0.10/0.44 ![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))))))),
% 0.10/0.44 inference(NNF_transformation,[status(thm)],[f153])).
% 0.10/0.44 fof(f155,plain,(
% 0.10/0.44 (![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))))))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f154])).
% 0.10/0.44 fof(f156,plain,(
% 0.10/0.44 (![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)))))),
% 0.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f155])).
% 0.10/0.44 fof(f157,plain,(
% 0.10/0.44 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f156])).
% 0.10/0.44 fof(f161,plain,(
% 0.10/0.44 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.10/0.44 fof(f162,plain,(
% 0.10/0.44 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f161])).
% 0.10/0.44 fof(f163,plain,(
% 0.10/0.44 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f162])).
% 0.10/0.44 fof(f167,plain,(
% 0.10/0.44 ![X90,X91,X92,X93]: (((~occurrence_of(X92,X93)|~root_occ(X90,X92))|~root_occ(X91,X92))|X90=X91)),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.10/0.44 fof(f168,plain,(
% 0.10/0.44 ![X90,X91]: ((![X92]: (((![X93]: ~occurrence_of(X92,X93))|~root_occ(X90,X92))|~root_occ(X91,X92)))|X90=X91)),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f167])).
% 0.10/0.44 fof(f169,plain,(
% 0.10/0.44 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f168])).
% 0.10/0.44 fof(f176,plain,(
% 0.10/0.44 ![X101]: (~occurrence_of(X101,tptp0)|(?[X102,X103,X104]: ((((((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&next_subocc(X102,X103,tptp0))&(occurrence_of(X104,tptp2)|occurrence_of(X104,tptp1)))&next_subocc(X103,X104,tptp0))&leaf_occ(X104,X101))))),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.10/0.44 fof(f177,plain,(
% 0.10/0.44 ![X101]: (~occurrence_of(X101,tptp0)|(?[X104]: ((?[X103]: (((?[X102]: (((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&next_subocc(X102,X103,tptp0)))&(occurrence_of(X104,tptp2)|occurrence_of(X104,tptp1)))&next_subocc(X103,X104,tptp0)))&leaf_occ(X104,X101))))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f176])).
% 0.10/0.44 fof(f178,plain,(
% 0.10/0.44 ![X101]: (~occurrence_of(X101,tptp0)|((((((occurrence_of(sK14_skl(X101),tptp3)&root_occ(sK14_skl(X101),X101))&occurrence_of(sK13_skl(X101),tptp4))&next_subocc(sK14_skl(X101),sK13_skl(X101),tptp0))&(occurrence_of(sK12_skl(X101),tptp2)|occurrence_of(sK12_skl(X101),tptp1)))&next_subocc(sK13_skl(X101),sK12_skl(X101),tptp0))&leaf_occ(sK12_skl(X101),X101)))),
% 0.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X104,sK12_skl(X101)),skolemize(X103,sK13_skl(X101)),skolemize(X102,sK14_skl(X101))],[f177])).
% 0.10/0.44 fof(f179,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK14_skl(X0),tptp3))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f178])).
% 0.10/0.44 fof(f180,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK14_skl(X0),X0))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f178])).
% 0.10/0.44 fof(f183,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK12_skl(X0),tptp2)|occurrence_of(sK12_skl(X0),tptp1))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f178])).
% 0.10/0.44 fof(f184,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK13_skl(X0),sK12_skl(X0),tptp0))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f178])).
% 0.10/0.44 fof(f185,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK12_skl(X0),X0))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f178])).
% 0.10/0.44 fof(f198,plain,(
% 0.10/0.44 (?[X105]: (occurrence_of(X105,tptp0)&(![X106,X107]: ((((~occurrence_of(X106,tptp3)|~root_occ(X106,X105))|(~occurrence_of(X107,tptp2)&~occurrence_of(X107,tptp1)))|~min_precedes(X106,X107,tptp0))|~leaf_occ(X107,X105)))))),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.10/0.44 fof(f199,plain,(
% 0.10/0.44 ?[X105]: (occurrence_of(X105,tptp0)&(![X107]: ((![X106]: (((~occurrence_of(X106,tptp3)|~root_occ(X106,X105))|(~occurrence_of(X107,tptp2)&~occurrence_of(X107,tptp1)))|~min_precedes(X106,X107,tptp0)))|~leaf_occ(X107,X105))))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f198])).
% 0.10/0.44 fof(f200,plain,(
% 0.10/0.44 (occurrence_of(sK15_skl,tptp0)&(![X107]: ((![X106]: (((~occurrence_of(X106,tptp3)|~root_occ(X106,sK15_skl))|(~occurrence_of(X107,tptp2)&~occurrence_of(X107,tptp1)))|~min_precedes(X106,X107,tptp0)))|~leaf_occ(X107,sK15_skl))))),
% 0.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X105,sK15_skl)],[f199])).
% 0.10/0.44 fof(f201,plain,(
% 0.10/0.44 occurrence_of(sK15_skl,tptp0)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f200])).
% 0.10/0.44 fof(f202,plain,(
% 0.10/0.44 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK15_skl)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0)|~leaf_occ(X1,sK15_skl))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f200])).
% 0.10/0.44 fof(f203,plain,(
% 0.10/0.44 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK15_skl)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0)|~leaf_occ(X1,sK15_skl))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f200])).
% 0.10/0.44 fof(f211,plain,(
% 0.10/0.44 ![X0,X1]: (~root_occ(X0,sK15_skl)|~root_occ(X1,sK15_skl)|X0=X1)),
% 0.10/0.44 inference(resolution,[status(thm)],[f169,f201])).
% 0.10/0.44 fof(f304,plain,(
% 0.10/0.44 root_occ(sK14_skl(sK15_skl),sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f180,f201])).
% 0.10/0.44 fof(f305,plain,(
% 0.10/0.44 ![X0]: (~root_occ(X0,sK15_skl)|X0=sK14_skl(sK15_skl))),
% 0.10/0.44 inference(resolution,[status(thm)],[f304,f211])).
% 0.10/0.44 fof(f316,plain,(
% 0.10/0.44 leaf_occ(sK12_skl(sK15_skl),sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f185,f201])).
% 0.10/0.44 fof(f323,plain,(
% 0.10/0.44 subactivity_occurrence(sK12_skl(sK15_skl),sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f316,f121])).
% 0.10/0.44 fof(f424,plain,(
% 0.10/0.44 occurrence_of(sK14_skl(sK15_skl),tptp3)),
% 0.10/0.44 inference(resolution,[status(thm)],[f179,f201])).
% 0.10/0.44 fof(f426,plain,(
% 0.10/0.44 ![X0]: (~root_occ(sK14_skl(sK15_skl),sK15_skl)|~occurrence_of(X0,tptp1)|~min_precedes(sK14_skl(sK15_skl),X0,tptp0)|~leaf_occ(X0,sK15_skl))),
% 0.10/0.44 inference(resolution,[status(thm)],[f424,f203])).
% 0.10/0.44 fof(f427,plain,(
% 0.10/0.44 ![X0]: (~root_occ(sK14_skl(sK15_skl),sK15_skl)|~occurrence_of(X0,tptp2)|~min_precedes(sK14_skl(sK15_skl),X0,tptp0)|~leaf_occ(X0,sK15_skl))),
% 0.10/0.44 inference(resolution,[status(thm)],[f424,f202])).
% 0.10/0.44 fof(f439,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp1)|~min_precedes(sK14_skl(sK15_skl),X0,tptp0)|~leaf_occ(X0,sK15_skl))),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f426,f304])).
% 0.10/0.44 fof(f440,plain,(
% 0.10/0.44 ![X0]: (~occurrence_of(X0,tptp2)|~min_precedes(sK14_skl(sK15_skl),X0,tptp0)|~leaf_occ(X0,sK15_skl))),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f427,f304])).
% 0.10/0.44 fof(f590,plain,(
% 0.10/0.44 ![X0]: (root_occ(X0,sK15_skl)|~subactivity_occurrence(X0,sK15_skl)|~root(X0,tptp0))),
% 0.10/0.44 inference(resolution,[status(thm)],[f130,f201])).
% 0.10/0.44 fof(f682,plain,(
% 0.10/0.44 next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 0.10/0.44 inference(resolution,[status(thm)],[f184,f201])).
% 0.10/0.44 fof(f683,plain,(
% 0.10/0.44 min_precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 0.10/0.44 inference(resolution,[status(thm)],[f682,f157])).
% 0.10/0.44 fof(f695,plain,(
% 0.10/0.44 min_precedes(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
% 0.10/0.44 inference(resolution,[status(thm)],[f683,f145])).
% 0.10/0.44 fof(f696,plain,(
% 0.10/0.44 root(sK10_skl(tptp0,sK12_skl(sK15_skl)),tptp0)),
% 0.10/0.44 inference(resolution,[status(thm)],[f683,f144])).
% 0.10/0.44 fof(f734,plain,(
% 0.10/0.44 ![X0,X1]: (~min_precedes(X0,X1,tptp0)|~subactivity_occurrence(X1,sK15_skl)|subactivity_occurrence(X0,sK15_skl))),
% 0.10/0.44 inference(resolution,[status(thm)],[f163,f201])).
% 0.10/0.44 fof(f746,plain,(
% 0.10/0.44 ![X0]: (~min_precedes(X0,sK12_skl(sK15_skl),tptp0)|subactivity_occurrence(X0,sK15_skl))),
% 0.10/0.44 inference(resolution,[status(thm)],[f734,f323])).
% 0.10/0.44 fof(f866,plain,(
% 0.10/0.44 occurrence_of(sK12_skl(sK15_skl),tptp2)|occurrence_of(sK12_skl(sK15_skl),tptp1)),
% 0.10/0.44 inference(resolution,[status(thm)],[f183,f201])).
% 0.10/0.44 fof(f923,plain,(
% 0.10/0.44 subactivity_occurrence(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f695,f746])).
% 0.10/0.44 fof(f937,plain,(
% 0.10/0.44 root_occ(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl)|~root(sK10_skl(tptp0,sK12_skl(sK15_skl)),tptp0)),
% 0.10/0.44 inference(resolution,[status(thm)],[f923,f590])).
% 0.10/0.44 fof(f944,plain,(
% 0.10/0.44 root_occ(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl)),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f937,f696])).
% 0.10/0.44 fof(f947,plain,(
% 0.10/0.44 sK10_skl(tptp0,sK12_skl(sK15_skl))=sK14_skl(sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f944,f305])).
% 0.10/0.44 fof(f957,plain,(
% 0.10/0.44 min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 0.10/0.44 inference(backward_demodulation,[status(thm)],[f947,f695])).
% 0.10/0.44 fof(f963,plain,(
% 0.10/0.44 ~occurrence_of(sK12_skl(sK15_skl),tptp2)|~leaf_occ(sK12_skl(sK15_skl),sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f957,f440])).
% 0.10/0.44 fof(f964,plain,(
% 0.10/0.44 ~occurrence_of(sK12_skl(sK15_skl),tptp1)|~leaf_occ(sK12_skl(sK15_skl),sK15_skl)),
% 0.10/0.44 inference(resolution,[status(thm)],[f957,f439])).
% 0.10/0.44 fof(f978,plain,(
% 0.10/0.44 ~occurrence_of(sK12_skl(sK15_skl),tptp2)),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f963,f316])).
% 0.10/0.44 fof(f979,plain,(
% 0.10/0.44 ~occurrence_of(sK12_skl(sK15_skl),tptp1)),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f964,f316])).
% 0.10/0.44 fof(f982,plain,(
% 0.10/0.44 occurrence_of(sK12_skl(sK15_skl),tptp1)),
% 0.10/0.44 inference(backward_subsumption_resolution,[status(thm)],[f866,f978])).
% 0.10/0.44 fof(f984,plain,(
% 0.10/0.44 $false),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f982,f979])).
% 0.10/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.46 % Elapsed time: 0.093433 seconds
% 0.10/0.46 % CPU time: 0.481744 seconds
% 0.10/0.46 % Total memory used: 91.709 MB
% 0.10/0.46 % Net memory used: 91.170 MB
%------------------------------------------------------------------------------