%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO016+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:26 PM UTC 2026
% Result : Theorem 7.56s 6.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PRO016+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.04/5.31 % Computer : n012.cluster.edu
% 0.04/5.31 % Model : x86_64 x86_64
% 0.04/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.31 % Memory : 8046.5625MB
% 0.04/5.31 % OS : Linux 6.8.0-71-generic
% 0.04/5.31 % CPULimit : 300
% 0.04/5.31 % WCLimit : 300
% 0.04/5.31 % DateTime : Mon Sep 21 03:43:30 UTC 2026
% 0.04/5.31 % CPUTime :
% 0.04/5.32 % Drodi V4.1.1
% 7.56/6.32 % Refutation found
% 7.56/6.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.56/6.32 % SZS output start CNFRefutation for theBenchmark
% 7.56/6.32 fof(f10,axiom,(
% 7.56/6.32 (! [X31,X32,X33] :( ( occurrence_of(X31,X33)& leaf_occ(X32,X31) )=> ~ (? [X34] : min_precedes(X32,X34,X33) )) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f19,axiom,(
% 7.56/6.32 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f22,axiom,(
% 7.56/6.32 (! [X63,X64] :( precedes(X63,X64)<=> ( earlier(X63,X64)& legal(X64) ) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f25,axiom,(
% 7.56/6.32 (! [X72,X73,X74] :( min_precedes(X72,X73,X74)=> precedes(X72,X73) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f26,axiom,(
% 7.56/6.32 (! [X75,X76,X77] :( next_subocc(X75,X76,X77)=> ( arboreal(X75)& arboreal(X76) ) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f27,axiom,(
% 7.56/6.32 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f28,axiom,(
% 7.56/6.32 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f29,axiom,(
% 7.56/6.32 (! [X86,X87,X88,X89] :( ( occurrence_of(X88,X89)& ~ atomic(X89)& leaf_occ(X86,X88)& leaf_occ(X87,X88) )=> X86 = X87 ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f31,axiom,(
% 7.56/6.32 (! [X94,X95,X96] :( ( earlier(X94,X95)& earlier(X95,X96) )=> earlier(X94,X96) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f32,axiom,(
% 7.56/6.32 (! [X97,X98,X99,X100] :( ( min_precedes(X97,X98,X100)& min_precedes(X97,X99,X100)& precedes(X98,X99) )=> min_precedes(X98,X99,X100) ) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f33,axiom,(
% 7.56/6.32 (! [X101,X102] :( ( occurrence_of(X102,tptp0)& subactivity_occurrence(X101,X102)& arboreal(X101)& ~ leaf_occ(X101,X102) )=> (? [X103,X104,X105] :( occurrence_of(X103,tptp3)& next_subocc(X101,X103,tptp0)& occurrence_of(X104,tptp4)& next_subocc(X103,X104,tptp0)& ( occurrence_of(X105,tptp1)| occurrence_of(X105,tptp2) )& next_subocc(X104,X105,tptp0)& leaf_occ(X105,X102) ) )) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f35,axiom,(
% 7.56/6.32 ~ atomic(tptp0) ),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f46,conjecture,(
% 7.56/6.32 (! [X106,X107] :( ( occurrence_of(X107,tptp0)& subactivity_occurrence(X106,X107)& arboreal(X106)& ~ leaf_occ(X106,X107) )=> (? [X108,X109] :( occurrence_of(X108,tptp3)& next_subocc(X106,X108,tptp0)& ( occurrence_of(X109,tptp1)| occurrence_of(X109,tptp2) )& min_precedes(X108,X109,tptp0)& leaf_occ(X109,X107)& ( occurrence_of(X109,tptp1)=> ~ (? [X110] :( occurrence_of(X110,tptp2)& min_precedes(X108,X110,tptp0) ) ))& ( occurrence_of(X109,tptp2)=> ~ (? [X111] :( occurrence_of(X111,tptp1)& min_precedes(X108,X111,tptp0) ) )) ) )) )),
% 7.56/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.56/6.32 fof(f47,negated_conjecture,(
% 7.56/6.32 ~((! [X106,X107] :( ( occurrence_of(X107,tptp0)& subactivity_occurrence(X106,X107)& arboreal(X106)& ~ leaf_occ(X106,X107) )=> (? [X108,X109] :( occurrence_of(X108,tptp3)& next_subocc(X106,X108,tptp0)& ( occurrence_of(X109,tptp1)| occurrence_of(X109,tptp2) )& min_precedes(X108,X109,tptp0)& leaf_occ(X109,X107)& ( occurrence_of(X109,tptp1)=> ~ (? [X110] :( occurrence_of(X110,tptp2)& min_precedes(X108,X110,tptp0) ) ))& ( occurrence_of(X109,tptp2)=> ~ (? [X111] :( occurrence_of(X111,tptp1)& min_precedes(X108,X111,tptp0) ) )) ) )) ))),
% 7.56/6.32 inference(negated_conjecture,[status(cth)],[f46])).
% 7.56/6.32 fof(f80,plain,(
% 7.56/6.32 ![X31,X32,X33]: ((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 7.56/6.32 fof(f81,plain,(
% 7.56/6.32 ![X32,X33]: ((![X31]: (~occurrence_of(X31,X33)|~leaf_occ(X32,X31)))|(![X34]: ~min_precedes(X32,X34,X33)))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f80])).
% 7.56/6.32 fof(f82,plain,(
% 7.56/6.32 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f81])).
% 7.56/6.32 fof(f117,plain,(
% 7.56/6.32 ![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)))))),
% 7.56/6.32 inference(NNF_transformation,[status(thm)],[f19])).
% 7.56/6.32 fof(f118,plain,(
% 7.56/6.32 (![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)))))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f117])).
% 7.56/6.32 fof(f119,plain,(
% 7.56/6.32 (![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)))))),
% 7.56/6.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f118])).
% 7.56/6.32 fof(f121,plain,(
% 7.56/6.32 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f119])).
% 7.56/6.32 fof(f133,plain,(
% 7.56/6.32 ![X63,X64]: ((~precedes(X63,X64)|(earlier(X63,X64)&legal(X64)))&(precedes(X63,X64)|(~earlier(X63,X64)|~legal(X64))))),
% 7.56/6.32 inference(NNF_transformation,[status(thm)],[f22])).
% 7.56/6.32 fof(f134,plain,(
% 7.56/6.32 (![X63,X64]: (~precedes(X63,X64)|(earlier(X63,X64)&legal(X64))))&(![X63,X64]: (precedes(X63,X64)|(~earlier(X63,X64)|~legal(X64))))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f133])).
% 7.56/6.32 fof(f135,plain,(
% 7.56/6.32 ![X0,X1]: (~precedes(X0,X1)|earlier(X0,X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f134])).
% 7.56/6.32 fof(f136,plain,(
% 7.56/6.32 ![X0,X1]: (~precedes(X0,X1)|legal(X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f134])).
% 7.56/6.32 fof(f137,plain,(
% 7.56/6.32 ![X0,X1]: (precedes(X0,X1)|~earlier(X0,X1)|~legal(X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f134])).
% 7.56/6.32 fof(f146,plain,(
% 7.56/6.32 ![X72,X73,X74]: (~min_precedes(X72,X73,X74)|precedes(X72,X73))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 7.56/6.32 fof(f147,plain,(
% 7.56/6.32 ![X72,X73]: ((![X74]: ~min_precedes(X72,X73,X74))|precedes(X72,X73))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f146])).
% 7.56/6.32 fof(f148,plain,(
% 7.56/6.32 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|precedes(X0,X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f147])).
% 7.56/6.32 fof(f149,plain,(
% 7.56/6.32 ![X75,X76,X77]: (~next_subocc(X75,X76,X77)|(arboreal(X75)&arboreal(X76)))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 7.56/6.32 fof(f150,plain,(
% 7.56/6.32 ![X75,X76]: ((![X77]: ~next_subocc(X75,X76,X77))|(arboreal(X75)&arboreal(X76)))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f149])).
% 7.56/6.32 fof(f152,plain,(
% 7.56/6.32 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|arboreal(X1))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f150])).
% 7.56/6.32 fof(f153,plain,(
% 7.56/6.32 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 7.56/6.32 fof(f154,plain,(
% 7.56/6.32 ![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))))))),
% 7.56/6.32 inference(NNF_transformation,[status(thm)],[f153])).
% 7.56/6.32 fof(f155,plain,(
% 7.56/6.32 (![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))))))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f154])).
% 7.56/6.32 fof(f156,plain,(
% 7.56/6.32 (![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)))))),
% 7.56/6.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f155])).
% 7.56/6.32 fof(f157,plain,(
% 7.56/6.32 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f156])).
% 7.56/6.32 fof(f158,plain,(
% 7.56/6.32 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f156])).
% 7.56/6.32 fof(f161,plain,(
% 7.56/6.32 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 7.56/6.32 fof(f162,plain,(
% 7.56/6.32 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f161])).
% 7.56/6.32 fof(f163,plain,(
% 7.56/6.32 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f162])).
% 7.56/6.32 fof(f164,plain,(
% 7.56/6.32 ![X86,X87,X88,X89]: ((((~occurrence_of(X88,X89)|atomic(X89))|~leaf_occ(X86,X88))|~leaf_occ(X87,X88))|X86=X87)),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 7.56/6.32 fof(f165,plain,(
% 7.56/6.32 ![X86,X87]: ((![X88]: (((![X89]: (~occurrence_of(X88,X89)|atomic(X89)))|~leaf_occ(X86,X88))|~leaf_occ(X87,X88)))|X86=X87)),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f164])).
% 7.56/6.32 fof(f166,plain,(
% 7.56/6.32 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|atomic(X1)|~leaf_occ(X2,X0)|~leaf_occ(X3,X0)|X2=X3)),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f165])).
% 7.56/6.32 fof(f170,plain,(
% 7.56/6.32 ![X94,X95,X96]: ((~earlier(X94,X95)|~earlier(X95,X96))|earlier(X94,X96))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 7.56/6.32 fof(f171,plain,(
% 7.56/6.32 ![X94,X96]: ((![X95]: (~earlier(X94,X95)|~earlier(X95,X96)))|earlier(X94,X96))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f170])).
% 7.56/6.32 fof(f172,plain,(
% 7.56/6.32 ![X0,X1,X2]: (~earlier(X0,X1)|~earlier(X1,X2)|earlier(X0,X2))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f171])).
% 7.56/6.32 fof(f173,plain,(
% 7.56/6.32 ![X97,X98,X99,X100]: (((~min_precedes(X97,X98,X100)|~min_precedes(X97,X99,X100))|~precedes(X98,X99))|min_precedes(X98,X99,X100))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 7.56/6.32 fof(f174,plain,(
% 7.56/6.32 ![X98,X99,X100]: (((![X97]: (~min_precedes(X97,X98,X100)|~min_precedes(X97,X99,X100)))|~precedes(X98,X99))|min_precedes(X98,X99,X100))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f173])).
% 7.56/6.32 fof(f175,plain,(
% 7.56/6.32 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~min_precedes(X0,X3,X2)|~precedes(X1,X3)|min_precedes(X1,X3,X2))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f174])).
% 7.56/6.32 fof(f176,plain,(
% 7.56/6.32 ![X101,X102]: ((((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102))|(?[X103,X104,X105]: ((((((occurrence_of(X103,tptp3)&next_subocc(X101,X103,tptp0))&occurrence_of(X104,tptp4))&next_subocc(X103,X104,tptp0))&(occurrence_of(X105,tptp1)|occurrence_of(X105,tptp2)))&next_subocc(X104,X105,tptp0))&leaf_occ(X105,X102))))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 7.56/6.32 fof(f177,plain,(
% 7.56/6.32 ![X101,X102]: ((((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102))|(?[X105]: ((?[X104]: (((?[X103]: (((occurrence_of(X103,tptp3)&next_subocc(X101,X103,tptp0))&occurrence_of(X104,tptp4))&next_subocc(X103,X104,tptp0)))&(occurrence_of(X105,tptp1)|occurrence_of(X105,tptp2)))&next_subocc(X104,X105,tptp0)))&leaf_occ(X105,X102))))),
% 7.56/6.32 inference(miniscoping,[status(thm)],[f176])).
% 7.56/6.32 fof(f178,plain,(
% 7.56/6.32 ![X101,X102]: ((((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102))|((((((occurrence_of(sK14_skl(X102,X101),tptp3)&next_subocc(X101,sK14_skl(X102,X101),tptp0))&occurrence_of(sK13_skl(X102,X101),tptp4))&next_subocc(sK14_skl(X102,X101),sK13_skl(X102,X101),tptp0))&(occurrence_of(sK12_skl(X102,X101),tptp1)|occurrence_of(sK12_skl(X102,X101),tptp2)))&next_subocc(sK13_skl(X102,X101),sK12_skl(X102,X101),tptp0))&leaf_occ(sK12_skl(X102,X101),X102)))),
% 7.56/6.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X105,sK12_skl(X102,X101)),skolemize(X104,sK13_skl(X102,X101)),skolemize(X103,sK14_skl(X102,X101))],[f177])).
% 7.56/6.32 fof(f180,plain,(
% 7.56/6.32 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X0,X1),tptp0))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f178])).
% 7.56/6.32 fof(f182,plain,(
% 7.56/6.32 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK14_skl(X0,X1),sK13_skl(X0,X1),tptp0))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f178])).
% 7.56/6.32 fof(f184,plain,(
% 7.56/6.32 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK13_skl(X0,X1),sK12_skl(X0,X1),tptp0))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f178])).
% 7.56/6.32 fof(f185,plain,(
% 7.56/6.32 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|leaf_occ(sK12_skl(X0,X1),X0))),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f178])).
% 7.56/6.32 fof(f187,plain,(
% 7.56/6.32 ~atomic(tptp0)),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f35])).
% 7.56/6.32 fof(f198,plain,(
% 7.56/6.32 (?[X106,X107]: ((((occurrence_of(X107,tptp0)&subactivity_occurrence(X106,X107))&arboreal(X106))&~leaf_occ(X106,X107))&(![X108,X109]: ((((((~occurrence_of(X108,tptp3)|~next_subocc(X106,X108,tptp0))|(~occurrence_of(X109,tptp1)&~occurrence_of(X109,tptp2)))|~min_precedes(X108,X109,tptp0))|~leaf_occ(X109,X107))|(occurrence_of(X109,tptp1)&(?[X110]: (occurrence_of(X110,tptp2)&min_precedes(X108,X110,tptp0)))))|(occurrence_of(X109,tptp2)&(?[X111]: (occurrence_of(X111,tptp1)&min_precedes(X108,X111,tptp0))))))))),
% 7.56/6.32 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 7.56/6.32 fof(f199,definition,(
% 7.56/6.32 ![X109]: (sP0_prd(X109)<=>(~occurrence_of(X109,tptp1)&~occurrence_of(X109,tptp2)))),
% 7.56/6.32 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 7.56/6.32 fof(f200,definition,(
% 7.56/6.32 ![X108,X109]: (sP1_prd(X109,X108)<=>(occurrence_of(X109,tptp1)&(?[X110]: (occurrence_of(X110,tptp2)&min_precedes(X108,X110,tptp0)))))),
% 7.56/6.32 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 7.56/6.32 fof(f201,plain,(
% 7.56/6.32 ?[X106,X107]: ((((occurrence_of(X107,tptp0)&subactivity_occurrence(X106,X107))&arboreal(X106))&~leaf_occ(X106,X107))&(![X108,X109]: ((((((~occurrence_of(X108,tptp3)|~next_subocc(X106,X108,tptp0))|sP0_prd(X109))|~min_precedes(X108,X109,tptp0))|~leaf_occ(X109,X107))|sP1_prd(X109,X108))|(occurrence_of(X109,tptp2)&(?[X111]: (occurrence_of(X111,tptp1)&min_precedes(X108,X111,tptp0)))))))),
% 7.56/6.32 inference(formula_renaming,[status(thm)],[f198,f200,f199])).
% 7.56/6.32 fof(f202,plain,(
% 7.56/6.32 ((((occurrence_of(sK16_skl,tptp0)&subactivity_occurrence(sK15_skl,sK16_skl))&arboreal(sK15_skl))&~leaf_occ(sK15_skl,sK16_skl))&(![X108,X109]: ((((((~occurrence_of(X108,tptp3)|~next_subocc(sK15_skl,X108,tptp0))|sP0_prd(X109))|~min_precedes(X108,X109,tptp0))|~leaf_occ(X109,sK16_skl))|sP1_prd(X109,X108))|(occurrence_of(X109,tptp2)&(occurrence_of(sK17_skl(X109,X108),tptp1)&min_precedes(X108,sK17_skl(X109,X108),tptp0))))))),
% 7.56/6.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X106,sK15_skl),skolemize(X107,sK16_skl),skolemize(X111,sK17_skl(X109,X108))],[f201])).
% 7.56/6.32 fof(f203,plain,(
% 7.56/6.32 occurrence_of(sK16_skl,tptp0)),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f202])).
% 7.56/6.32 fof(f204,plain,(
% 7.56/6.32 subactivity_occurrence(sK15_skl,sK16_skl)),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f202])).
% 7.56/6.32 fof(f205,plain,(
% 7.56/6.32 arboreal(sK15_skl)),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f202])).
% 7.56/6.32 fof(f206,plain,(
% 7.56/6.32 ~leaf_occ(sK15_skl,sK16_skl)),
% 7.56/6.32 inference(cnf_transformation,[status(thm)],[f202])).
% 7.56/6.32 fof(f240,plain,(
% 7.56/6.32 ![X0,X1]: (~leaf_occ(X0,sK16_skl)|~min_precedes(X0,X1,tptp0))),
% 7.56/6.32 inference(resolution,[status(thm)],[f82,f203])).
% 7.56/6.32 fof(f245,plain,(
% 7.56/6.32 ![X0,X1]: (~min_precedes(X0,X1,tptp0)|~subactivity_occurrence(X1,sK16_skl)|subactivity_occurrence(X0,sK16_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f163,f203])).
% 7.56/6.32 fof(f471,plain,(
% 7.56/6.32 ![X0,X1]: (atomic(tptp0)|~leaf_occ(X0,sK16_skl)|~leaf_occ(X1,sK16_skl)|X0=X1)),
% 7.56/6.32 inference(resolution,[status(thm)],[f166,f203])).
% 7.56/6.32 fof(f474,plain,(
% 7.56/6.32 ![X0,X1]: (~leaf_occ(X0,sK16_skl)|~leaf_occ(X1,sK16_skl)|X0=X1)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f471,f187])).
% 7.56/6.32 fof(f518,plain,(
% 7.56/6.32 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(X0,sK14_skl(sK16_skl,X0),tptp0))),
% 7.56/6.32 inference(resolution,[status(thm)],[f180,f203])).
% 7.56/6.32 fof(f528,plain,(
% 7.56/6.32 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(sK14_skl(sK16_skl,X0),sK13_skl(sK16_skl,X0),tptp0))),
% 7.56/6.32 inference(resolution,[status(thm)],[f182,f203])).
% 7.56/6.32 fof(f530,plain,(
% 7.56/6.32 ~occurrence_of(sK16_skl,tptp0)|~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK14_skl(sK16_skl,sK15_skl),sK13_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f182,f204])).
% 7.56/6.32 fof(f532,plain,(
% 7.56/6.32 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK14_skl(sK16_skl,sK15_skl),sK13_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f530,f203])).
% 7.56/6.32 fof(f638,plain,(
% 7.56/6.32 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(sK13_skl(sK16_skl,X0),sK12_skl(sK16_skl,X0),tptp0))),
% 7.56/6.32 inference(resolution,[status(thm)],[f184,f203])).
% 7.56/6.32 fof(f640,plain,(
% 7.56/6.32 ~occurrence_of(sK16_skl,tptp0)|~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f184,f204])).
% 7.56/6.32 fof(f642,plain,(
% 7.56/6.32 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f640,f203])).
% 7.56/6.32 fof(f643,plain,(
% 7.56/6.32 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|leaf_occ(sK12_skl(sK16_skl,X0),sK16_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f185,f203])).
% 7.56/6.32 fof(f645,plain,(
% 7.56/6.32 ~occurrence_of(sK16_skl,tptp0)|~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|leaf_occ(sK12_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(resolution,[status(thm)],[f185,f204])).
% 7.56/6.32 fof(f647,plain,(
% 7.56/6.32 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|leaf_occ(sK12_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f645,f203])).
% 7.56/6.32 fof(f806,plain,(
% 7.56/6.32 leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK14_skl(sK16_skl,sK15_skl),sK13_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f532,f205])).
% 7.56/6.32 fof(f809,plain,(
% 7.56/6.32 leaf_occ(sK15_skl,sK16_skl)|arboreal(sK13_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f806,f152])).
% 7.56/6.32 fof(f813,plain,(
% 7.56/6.32 arboreal(sK13_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f809,f206])).
% 7.56/6.32 fof(f873,plain,(
% 7.56/6.32 leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f642,f205])).
% 7.56/6.32 fof(f874,plain,(
% 7.56/6.32 ![X0]: (leaf_occ(sK15_skl,sK16_skl)|~min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0)|~min_precedes(X0,sK12_skl(sK16_skl,sK15_skl),tptp0))),
% 7.56/6.32 inference(resolution,[status(thm)],[f873,f158])).
% 7.56/6.32 fof(f875,plain,(
% 7.56/6.32 leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f873,f157])).
% 7.56/6.32 fof(f878,plain,(
% 7.56/6.32 ![X0]: (~min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0)|~min_precedes(X0,sK12_skl(sK16_skl,sK15_skl),tptp0))),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f874,f206])).
% 7.56/6.32 fof(f879,plain,(
% 7.56/6.32 min_precedes(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f875,f206])).
% 7.56/6.32 fof(f890,plain,(
% 7.56/6.32 leaf_occ(sK15_skl,sK16_skl)|leaf_occ(sK12_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f647,f205])).
% 7.56/6.32 fof(f893,plain,(
% 7.56/6.32 ![X0]: (leaf_occ(sK15_skl,sK16_skl)|~leaf_occ(X0,sK16_skl)|X0=sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f890,f474])).
% 7.56/6.32 fof(f909,plain,(
% 7.56/6.32 leaf_occ(sK15_skl,sK16_skl)|subactivity_occurrence(sK12_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(resolution,[status(thm)],[f890,f121])).
% 7.56/6.32 fof(f913,plain,(
% 7.56/6.32 ![X0]: (~leaf_occ(X0,sK16_skl)|X0=sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f893,f206])).
% 7.56/6.32 fof(f926,plain,(
% 7.56/6.32 subactivity_occurrence(sK12_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f909,f206])).
% 7.56/6.32 fof(f1447,plain,(
% 7.56/6.32 ~subactivity_occurrence(sK12_skl(sK16_skl,sK15_skl),sK16_skl)|subactivity_occurrence(sK13_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(resolution,[status(thm)],[f879,f245])).
% 7.56/6.32 fof(f1450,plain,(
% 7.56/6.32 ~leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(resolution,[status(thm)],[f879,f240])).
% 7.56/6.32 fof(f1456,plain,(
% 7.56/6.32 ![X0]: (~min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0)|~precedes(X0,sK12_skl(sK16_skl,sK15_skl))|min_precedes(X0,sK12_skl(sK16_skl,sK15_skl),tptp0))),
% 7.56/6.32 inference(resolution,[status(thm)],[f879,f175])).
% 7.56/6.32 fof(f1464,plain,(
% 7.56/6.32 precedes(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f879,f148])).
% 7.56/6.32 fof(f1476,plain,(
% 7.56/6.32 subactivity_occurrence(sK13_skl(sK16_skl,sK15_skl),sK16_skl)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1447,f926])).
% 7.56/6.32 fof(f1482,plain,(
% 7.56/6.32 ~arboreal(sK13_skl(sK16_skl,sK15_skl))|leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|leaf_occ(sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK16_skl)),
% 7.56/6.32 inference(resolution,[status(thm)],[f1476,f643])).
% 7.56/6.32 fof(f1483,plain,(
% 7.56/6.32 ~arboreal(sK13_skl(sK16_skl,sK15_skl))|leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f1476,f638])).
% 7.56/6.32 fof(f1485,plain,(
% 7.56/6.32 ~arboreal(sK13_skl(sK16_skl,sK15_skl))|leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f1476,f528])).
% 7.56/6.32 fof(f1487,plain,(
% 7.56/6.32 ~arboreal(sK13_skl(sK16_skl,sK15_skl))|leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f1476,f518])).
% 7.56/6.32 fof(f1537,plain,(
% 7.56/6.32 leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|leaf_occ(sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK16_skl)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1482,f813])).
% 7.56/6.32 fof(f1538,plain,(
% 7.56/6.32 leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1483,f813])).
% 7.56/6.32 fof(f1540,plain,(
% 7.56/6.32 leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1485,f813])).
% 7.56/6.32 fof(f1542,plain,(
% 7.56/6.32 leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1487,f813])).
% 7.56/6.32 fof(f1582,plain,(
% 7.56/6.32 legal(sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f1464,f136])).
% 7.56/6.32 fof(f5833,plain,(
% 7.56/6.32 ![X0]: (~min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0)|~precedes(X0,sK12_skl(sK16_skl,sK15_skl)))),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1456,f878])).
% 7.56/6.32 fof(f7124,plain,(
% 7.56/6.32 leaf_occ(sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK16_skl)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1537,f1450])).
% 7.56/6.32 fof(f7140,plain,(
% 7.56/6.32 sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl))=sK12_skl(sK16_skl,sK15_skl)),
% 7.56/6.32 inference(resolution,[status(thm)],[f7124,f913])).
% 7.56/6.32 fof(f10589,plain,(
% 7.56/6.32 leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)|next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_demodulation,[status(thm)],[f7140,f1538])).
% 7.56/6.32 fof(f10590,plain,(
% 7.56/6.32 next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f10589,f1450])).
% 7.56/6.32 fof(f10592,plain,(
% 7.56/6.32 min_precedes(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f10590,f157])).
% 7.56/6.32 fof(f10624,plain,(
% 7.56/6.32 precedes(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f10592,f148])).
% 7.56/6.32 fof(f10762,plain,(
% 7.56/6.32 earlier(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f10624,f135])).
% 7.56/6.32 fof(f10764,plain,(
% 7.56/6.32 next_subocc(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1540,f1450])).
% 7.56/6.32 fof(f10766,plain,(
% 7.56/6.32 min_precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f10764,f157])).
% 7.56/6.32 fof(f10769,plain,(
% 7.56/6.32 next_subocc(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f1542,f1450])).
% 7.56/6.32 fof(f10771,plain,(
% 7.56/6.32 min_precedes(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)),
% 7.56/6.32 inference(resolution,[status(thm)],[f10769,f157])).
% 7.56/6.32 fof(f10774,plain,(
% 7.56/6.32 ![X0]: (~earlier(X0,sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)))|earlier(X0,sK12_skl(sK16_skl,sK15_skl)))),
% 7.56/6.32 inference(resolution,[status(thm)],[f10762,f172])).
% 7.56/6.32 fof(f10781,plain,(
% 7.56/6.32 ~precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f10771,f5833])).
% 7.56/6.32 fof(f11138,plain,(
% 7.56/6.32 precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)))),
% 7.56/6.32 inference(resolution,[status(thm)],[f10766,f148])).
% 7.56/6.32 fof(f11338,plain,(
% 7.56/6.32 earlier(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)))),
% 7.56/6.32 inference(resolution,[status(thm)],[f11138,f135])).
% 7.56/6.32 fof(f11346,plain,(
% 7.56/6.32 earlier(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f11338,f10774])).
% 7.56/6.32 fof(f11396,plain,(
% 7.56/6.32 precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))|~legal(sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(resolution,[status(thm)],[f11346,f137])).
% 7.56/6.32 fof(f11399,plain,(
% 7.56/6.32 ~legal(sK12_skl(sK16_skl,sK15_skl))),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f11396,f10781])).
% 7.56/6.32 fof(f11400,plain,(
% 7.56/6.32 $false),
% 7.56/6.32 inference(forward_subsumption_resolution,[status(thm)],[f11399,f1582])).
% 7.56/6.32 % SZS output end CNFRefutation for theBenchmark.p
% 7.56/6.33 % Elapsed time: 1.016978 seconds
% 7.56/6.33 % CPU time: 7.918017 seconds
% 7.56/6.33 % Total memory used: 215.277 MB
% 7.56/6.33 % Net memory used: 207.386 MB
%------------------------------------------------------------------------------