%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO014+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 : n005.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 5.57s 1.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO014+4 : 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/0.36 % Computer : n005.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:42:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 5.57/1.15 % Refutation found
% 5.57/1.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.57/1.15 % SZS output start CNFRefutation for theBenchmark
% 5.57/1.15 fof(f3,axiom,(
% 5.57/1.15 (! [X8,X9,X10,X11] :( ( occurrence_of(X9,X8)& subactivity_occurrence(X10,X9)& leaf_occ(X11,X9)& arboreal(X10)& ~ min_precedes(X10,X11,X8) )=> X11 = X10 ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f4,axiom,(
% 5.57/1.15 (! [X12,X13] :( occurrence_of(X13,X12)=> ( activity(X12)& activity_occurrence(X13) ) ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f8,axiom,(
% 5.57/1.15 (! [X25,X26] :( ( leaf(X25,X26)& ~ atomic(X26) )=> (? [X27] :( occurrence_of(X27,X26)& leaf_occ(X25,X27) ) )) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f9,axiom,(
% 5.57/1.15 (! [X28,X29,X30] :( ( occurrence_of(X28,X29)& occurrence_of(X28,X30) )=> X29 = X30 ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f13,axiom,(
% 5.57/1.15 (! [X41] :( activity_occurrence(X41)=> (? [X42] :( activity(X42)& occurrence_of(X41,X42) ) )) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f19,axiom,(
% 5.57/1.15 (! [X55,X56] :( leaf_occ(X55,X56)<=> (? [X57] :( occurrence_of(X56,X57)& subactivity_occurrence(X55,X56)& leaf(X55,X57) ) )) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f21,axiom,(
% 5.57/1.15 (! [X61,X62] :( earlier(X61,X62)=> ~ earlier(X62,X61) ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f22,axiom,(
% 5.57/1.15 (! [X63,X64] :( precedes(X63,X64)<=> ( earlier(X63,X64)& legal(X64) ) ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f25,axiom,(
% 5.57/1.15 (! [X72,X73,X74] :( min_precedes(X72,X73,X74)=> precedes(X72,X73) ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f27,axiom,(
% 5.57/1.15 (! [X78,X79,X80] :( next_subocc(X78,X79,X80)<=> ( min_precedes(X78,X79,X80)& ~ (? [X81] :( min_precedes(X78,X81,X80)& min_precedes(X81,X79,X80) ) )) ) )),
% 5.57/1.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.15 fof(f28,axiom,(
% 5.57/1.15 (! [X82,X83,X84,X85] :( ( min_precedes(X82,X83,X84)& occurrence_of(X85,X84)& subactivity_occurrence(X83,X85) )=> subactivity_occurrence(X82,X85) ) )),
% 5.57/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.16 fof(f31,axiom,(
% 5.57/1.16 (! [X94,X95,X96] :( ( earlier(X94,X95)& earlier(X95,X96) )=> earlier(X94,X96) ) )),
% 5.57/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.16 fof(f32,axiom,(
% 5.57/1.16 (! [X97,X98,X99,X100] :( ( min_precedes(X97,X98,X100)& min_precedes(X97,X99,X100)& precedes(X98,X99) )=> min_precedes(X98,X99,X100) ) )),
% 5.57/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.16 fof(f33,axiom,(
% 5.57/1.16 (! [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,tptp2)| occurrence_of(X105,tptp1) )& next_subocc(X104,X105,tptp0)& leaf(X105,tptp0) ) )) )),
% 5.57/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.16 fof(f35,axiom,(
% 5.57/1.16 ~ atomic(tptp0) ),
% 5.57/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.16 fof(f46,conjecture,(
% 5.57/1.16 (! [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,tptp2)| occurrence_of(X109,tptp1) )& min_precedes(X108,X109,tptp0)& leaf(X109,tptp0) ) )) )),
% 5.57/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.57/1.16 fof(f47,negated_conjecture,(
% 5.57/1.16 ~((! [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,tptp2)| occurrence_of(X109,tptp1) )& min_precedes(X108,X109,tptp0)& leaf(X109,tptp0) ) )) ))),
% 5.57/1.16 inference(negated_conjecture,[status(cth)],[f46])).
% 5.57/1.16 fof(f55,plain,(
% 5.57/1.16 ![X8,X9,X10,X11]: (((((~occurrence_of(X9,X8)|~subactivity_occurrence(X10,X9))|~leaf_occ(X11,X9))|~arboreal(X10))|min_precedes(X10,X11,X8))|X11=X10)),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 5.57/1.16 fof(f56,plain,(
% 5.57/1.16 ![X10,X11]: ((![X8]: (((![X9]: ((~occurrence_of(X9,X8)|~subactivity_occurrence(X10,X9))|~leaf_occ(X11,X9)))|~arboreal(X10))|min_precedes(X10,X11,X8)))|X11=X10)),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f55])).
% 5.57/1.16 fof(f57,plain,(
% 5.57/1.16 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~subactivity_occurrence(X2,X0)|~leaf_occ(X3,X0)|~arboreal(X2)|min_precedes(X2,X3,X1)|X3=X2)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f56])).
% 5.57/1.16 fof(f58,plain,(
% 5.57/1.16 ![X12,X13]: (~occurrence_of(X13,X12)|(activity(X12)&activity_occurrence(X13)))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 5.57/1.16 fof(f60,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f58])).
% 5.57/1.16 fof(f73,plain,(
% 5.57/1.16 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(?[X27]: (occurrence_of(X27,X26)&leaf_occ(X25,X27))))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 5.57/1.16 fof(f74,plain,(
% 5.57/1.16 ![X25,X26]: ((~leaf(X25,X26)|atomic(X26))|(occurrence_of(sK3_skl(X26,X25),X26)&leaf_occ(X25,sK3_skl(X26,X25))))),
% 5.57/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X27,sK3_skl(X26,X25))],[f73])).
% 5.57/1.16 fof(f75,plain,(
% 5.57/1.16 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|occurrence_of(sK3_skl(X1,X0),X1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f74])).
% 5.57/1.16 fof(f76,plain,(
% 5.57/1.16 ![X0,X1]: (~leaf(X0,X1)|atomic(X1)|leaf_occ(X0,sK3_skl(X1,X0)))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f74])).
% 5.57/1.16 fof(f77,plain,(
% 5.57/1.16 ![X28,X29,X30]: ((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 5.57/1.16 fof(f78,plain,(
% 5.57/1.16 ![X29,X30]: ((![X28]: (~occurrence_of(X28,X29)|~occurrence_of(X28,X30)))|X29=X30)),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f77])).
% 5.57/1.16 fof(f79,plain,(
% 5.57/1.16 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f78])).
% 5.57/1.16 fof(f89,plain,(
% 5.57/1.16 ![X41]: (~activity_occurrence(X41)|(?[X42]: (activity(X42)&occurrence_of(X41,X42))))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 5.57/1.16 fof(f90,plain,(
% 5.57/1.16 ![X41]: (~activity_occurrence(X41)|(activity(sK4_skl(X41))&occurrence_of(X41,sK4_skl(X41))))),
% 5.57/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f89])).
% 5.57/1.16 fof(f92,plain,(
% 5.57/1.16 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK4_skl(X0)))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f90])).
% 5.57/1.16 fof(f117,plain,(
% 5.57/1.16 ![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)))))),
% 5.57/1.16 inference(NNF_transformation,[status(thm)],[f19])).
% 5.57/1.16 fof(f118,plain,(
% 5.57/1.16 (![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)))))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f117])).
% 5.57/1.16 fof(f119,plain,(
% 5.57/1.16 (![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)))))),
% 5.57/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f118])).
% 5.57/1.16 fof(f121,plain,(
% 5.57/1.16 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f119])).
% 5.57/1.16 fof(f131,plain,(
% 5.57/1.16 ![X61,X62]: (~earlier(X61,X62)|~earlier(X62,X61))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 5.57/1.16 fof(f132,plain,(
% 5.57/1.16 ![X0,X1]: (~earlier(X0,X1)|~earlier(X1,X0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f131])).
% 5.57/1.16 fof(f133,plain,(
% 5.57/1.16 ![X63,X64]: ((~precedes(X63,X64)|(earlier(X63,X64)&legal(X64)))&(precedes(X63,X64)|(~earlier(X63,X64)|~legal(X64))))),
% 5.57/1.16 inference(NNF_transformation,[status(thm)],[f22])).
% 5.57/1.16 fof(f134,plain,(
% 5.57/1.16 (![X63,X64]: (~precedes(X63,X64)|(earlier(X63,X64)&legal(X64))))&(![X63,X64]: (precedes(X63,X64)|(~earlier(X63,X64)|~legal(X64))))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f133])).
% 5.57/1.16 fof(f135,plain,(
% 5.57/1.16 ![X0,X1]: (~precedes(X0,X1)|earlier(X0,X1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f134])).
% 5.57/1.16 fof(f136,plain,(
% 5.57/1.16 ![X0,X1]: (~precedes(X0,X1)|legal(X1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f134])).
% 5.57/1.16 fof(f137,plain,(
% 5.57/1.16 ![X0,X1]: (precedes(X0,X1)|~earlier(X0,X1)|~legal(X1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f134])).
% 5.57/1.16 fof(f146,plain,(
% 5.57/1.16 ![X72,X73,X74]: (~min_precedes(X72,X73,X74)|precedes(X72,X73))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 5.57/1.16 fof(f147,plain,(
% 5.57/1.16 ![X72,X73]: ((![X74]: ~min_precedes(X72,X73,X74))|precedes(X72,X73))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f146])).
% 5.57/1.16 fof(f148,plain,(
% 5.57/1.16 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|precedes(X0,X1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f147])).
% 5.57/1.16 fof(f153,plain,(
% 5.57/1.16 ![X78,X79,X80]: (next_subocc(X78,X79,X80)<=>(min_precedes(X78,X79,X80)&(![X81]: (~min_precedes(X78,X81,X80)|~min_precedes(X81,X79,X80)))))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 5.57/1.16 fof(f154,plain,(
% 5.57/1.16 ![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))))))),
% 5.57/1.16 inference(NNF_transformation,[status(thm)],[f153])).
% 5.57/1.16 fof(f155,plain,(
% 5.57/1.16 (![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))))))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f154])).
% 5.57/1.16 fof(f156,plain,(
% 5.57/1.16 (![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)))))),
% 5.57/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f155])).
% 5.57/1.16 fof(f157,plain,(
% 5.57/1.16 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f156])).
% 5.57/1.16 fof(f158,plain,(
% 5.57/1.16 ![X0,X1,X2,X3]: (~next_subocc(X0,X1,X2)|~min_precedes(X0,X3,X2)|~min_precedes(X3,X1,X2))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f156])).
% 5.57/1.16 fof(f159,plain,(
% 5.57/1.16 ![X0,X1,X2]: (next_subocc(X0,X1,X2)|~min_precedes(X0,X1,X2)|min_precedes(X0,sK11_skl(X2,X1,X0),X2))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f156])).
% 5.57/1.16 fof(f160,plain,(
% 5.57/1.16 ![X0,X1,X2]: (next_subocc(X0,X1,X2)|~min_precedes(X0,X1,X2)|min_precedes(sK11_skl(X2,X1,X0),X1,X2))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f156])).
% 5.57/1.16 fof(f161,plain,(
% 5.57/1.16 ![X82,X83,X84,X85]: (((~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84))|~subactivity_occurrence(X83,X85))|subactivity_occurrence(X82,X85))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 5.57/1.16 fof(f162,plain,(
% 5.57/1.16 ![X82,X85]: ((![X83]: ((![X84]: (~min_precedes(X82,X83,X84)|~occurrence_of(X85,X84)))|~subactivity_occurrence(X83,X85)))|subactivity_occurrence(X82,X85))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f161])).
% 5.57/1.16 fof(f163,plain,(
% 5.57/1.16 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~occurrence_of(X3,X2)|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X0,X3))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f162])).
% 5.57/1.16 fof(f170,plain,(
% 5.57/1.16 ![X94,X95,X96]: ((~earlier(X94,X95)|~earlier(X95,X96))|earlier(X94,X96))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 5.57/1.16 fof(f171,plain,(
% 5.57/1.16 ![X94,X96]: ((![X95]: (~earlier(X94,X95)|~earlier(X95,X96)))|earlier(X94,X96))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f170])).
% 5.57/1.16 fof(f172,plain,(
% 5.57/1.16 ![X0,X1,X2]: (~earlier(X0,X1)|~earlier(X1,X2)|earlier(X0,X2))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f171])).
% 5.57/1.16 fof(f173,plain,(
% 5.57/1.16 ![X97,X98,X99,X100]: (((~min_precedes(X97,X98,X100)|~min_precedes(X97,X99,X100))|~precedes(X98,X99))|min_precedes(X98,X99,X100))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 5.57/1.16 fof(f174,plain,(
% 5.57/1.16 ![X98,X99,X100]: (((![X97]: (~min_precedes(X97,X98,X100)|~min_precedes(X97,X99,X100)))|~precedes(X98,X99))|min_precedes(X98,X99,X100))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f173])).
% 5.57/1.16 fof(f175,plain,(
% 5.57/1.16 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~min_precedes(X0,X3,X2)|~precedes(X1,X3)|min_precedes(X1,X3,X2))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f174])).
% 5.57/1.16 fof(f176,plain,(
% 5.57/1.16 ![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,tptp2)|occurrence_of(X105,tptp1)))&next_subocc(X104,X105,tptp0))&leaf(X105,tptp0))))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 5.57/1.16 fof(f177,plain,(
% 5.57/1.16 ![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,tptp2)|occurrence_of(X105,tptp1)))&next_subocc(X104,X105,tptp0)))&leaf(X105,tptp0))))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f176])).
% 5.57/1.16 fof(f178,plain,(
% 5.57/1.16 ![X101]: ((![X102]: (((~occurrence_of(X102,tptp0)|~subactivity_occurrence(X101,X102))|~arboreal(X101))|leaf_occ(X101,X102)))|((((((occurrence_of(sK14_skl(X101),tptp3)&next_subocc(X101,sK14_skl(X101),tptp0))&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(sK12_skl(X101),tptp0)))),
% 5.57/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X105,sK12_skl(X101)),skolemize(X104,sK13_skl(X101)),skolemize(X103,sK14_skl(X101))],[f177])).
% 5.57/1.16 fof(f179,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp3))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 5.57/1.16 fof(f180,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 5.57/1.16 fof(f182,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK14_skl(X1),sK13_skl(X1),tptp0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 5.57/1.16 fof(f183,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK12_skl(X1),tptp2)|occurrence_of(sK12_skl(X1),tptp1))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 5.57/1.16 fof(f184,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(sK13_skl(X1),sK12_skl(X1),tptp0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 5.57/1.16 fof(f185,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|leaf(sK12_skl(X1),tptp0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f178])).
% 5.57/1.16 fof(f187,plain,(
% 5.57/1.16 ~atomic(tptp0)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f35])).
% 5.57/1.16 fof(f198,plain,(
% 5.57/1.16 (?[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,tptp2)&~occurrence_of(X109,tptp1)))|~min_precedes(X108,X109,tptp0))|~leaf(X109,tptp0)))))),
% 5.57/1.16 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 5.57/1.16 fof(f199,plain,(
% 5.57/1.16 ?[X106]: ((?[X107]: (((occurrence_of(X107,tptp0)&subactivity_occurrence(X106,X107))&arboreal(X106))&~leaf_occ(X106,X107)))&(![X109]: ((![X108]: (((~occurrence_of(X108,tptp3)|~next_subocc(X106,X108,tptp0))|(~occurrence_of(X109,tptp2)&~occurrence_of(X109,tptp1)))|~min_precedes(X108,X109,tptp0)))|~leaf(X109,tptp0))))),
% 5.57/1.16 inference(miniscoping,[status(thm)],[f198])).
% 5.57/1.16 fof(f200,plain,(
% 5.57/1.16 ((((occurrence_of(sK16_skl,tptp0)&subactivity_occurrence(sK15_skl,sK16_skl))&arboreal(sK15_skl))&~leaf_occ(sK15_skl,sK16_skl))&(![X109]: ((![X108]: (((~occurrence_of(X108,tptp3)|~next_subocc(sK15_skl,X108,tptp0))|(~occurrence_of(X109,tptp2)&~occurrence_of(X109,tptp1)))|~min_precedes(X108,X109,tptp0)))|~leaf(X109,tptp0))))),
% 5.57/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(X106,sK15_skl),skolemize(X107,sK16_skl)],[f199])).
% 5.57/1.16 fof(f201,plain,(
% 5.57/1.16 occurrence_of(sK16_skl,tptp0)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 5.57/1.16 fof(f202,plain,(
% 5.57/1.16 subactivity_occurrence(sK15_skl,sK16_skl)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 5.57/1.16 fof(f203,plain,(
% 5.57/1.16 arboreal(sK15_skl)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 5.57/1.16 fof(f204,plain,(
% 5.57/1.16 ~leaf_occ(sK15_skl,sK16_skl)),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 5.57/1.16 fof(f205,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0)|~leaf(X1,tptp0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 5.57/1.16 fof(f206,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0)|~leaf(X1,tptp0))),
% 5.57/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 5.57/1.16 fof(f321,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|occurrence_of(sK14_skl(X0),tptp3))),
% 5.57/1.16 inference(resolution,[status(thm)],[f179,f201])).
% 5.57/1.16 fof(f322,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(X0,sK14_skl(X0),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f180,f201])).
% 5.57/1.16 fof(f327,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK14_skl(sK15_skl),tptp3)),
% 5.57/1.16 inference(resolution,[status(thm)],[f321,f202])).
% 5.57/1.16 fof(f329,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK14_skl(sK15_skl),tptp3)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f327,f203])).
% 5.57/1.16 fof(f333,plain,(
% 5.57/1.16 ![X0]: (leaf_occ(sK15_skl,sK16_skl)|~occurrence_of(sK14_skl(sK15_skl),X0)|X0=tptp3)),
% 5.57/1.16 inference(resolution,[status(thm)],[f329,f79])).
% 5.57/1.16 fof(f334,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|activity_occurrence(sK14_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f329,f60])).
% 5.57/1.16 fof(f337,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(sK14_skl(sK15_skl),X0)|X0=tptp3)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f333,f204])).
% 5.57/1.16 fof(f338,plain,(
% 5.57/1.16 activity_occurrence(sK14_skl(sK15_skl))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f334,f204])).
% 5.57/1.16 fof(f340,plain,(
% 5.57/1.16 occurrence_of(sK14_skl(sK15_skl),sK4_skl(sK14_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f338,f92])).
% 5.57/1.16 fof(f349,plain,(
% 5.57/1.16 sK4_skl(sK14_skl(sK15_skl))=tptp3),
% 5.57/1.16 inference(resolution,[status(thm)],[f340,f337])).
% 5.57/1.16 fof(f356,plain,(
% 5.57/1.16 occurrence_of(sK14_skl(sK15_skl),tptp3)),
% 5.57/1.16 inference(backward_demodulation,[status(thm)],[f349,f340])).
% 5.57/1.16 fof(f367,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f322,f202])).
% 5.57/1.16 fof(f369,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f367,f203])).
% 5.57/1.16 fof(f428,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(sK14_skl(X0),sK13_skl(X0),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f182,f201])).
% 5.57/1.16 fof(f429,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|occurrence_of(sK12_skl(X0),tptp2)|occurrence_of(sK12_skl(X0),tptp1))),
% 5.57/1.16 inference(resolution,[status(thm)],[f183,f201])).
% 5.57/1.16 fof(f430,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|next_subocc(sK13_skl(X0),sK12_skl(X0),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f184,f201])).
% 5.57/1.16 fof(f433,plain,(
% 5.57/1.16 ![X0]: (leaf_occ(sK15_skl,sK16_skl)|~min_precedes(sK15_skl,X0,tptp0)|~min_precedes(X0,sK14_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f369,f158])).
% 5.57/1.16 fof(f434,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK15_skl,sK14_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f369,f157])).
% 5.57/1.16 fof(f439,plain,(
% 5.57/1.16 ![X0]: (~min_precedes(sK15_skl,X0,tptp0)|~min_precedes(X0,sK14_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f433,f204])).
% 5.57/1.16 fof(f440,plain,(
% 5.57/1.16 min_precedes(sK15_skl,sK14_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f434,f204])).
% 5.57/1.16 fof(f441,plain,(
% 5.57/1.16 next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)|min_precedes(sK11_skl(tptp0,sK14_skl(sK15_skl),sK15_skl),sK14_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f440,f160])).
% 5.57/1.16 fof(f442,plain,(
% 5.57/1.16 next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)|min_precedes(sK15_skl,sK11_skl(tptp0,sK14_skl(sK15_skl),sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f440,f159])).
% 5.57/1.16 fof(f449,plain,(
% 5.57/1.16 precedes(sK15_skl,sK14_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f440,f148])).
% 5.57/1.16 fof(f451,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK14_skl(sK15_skl),X0)|subactivity_occurrence(sK15_skl,X0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f440,f163])).
% 5.57/1.16 fof(f453,plain,(
% 5.57/1.16 earlier(sK15_skl,sK14_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f449,f135])).
% 5.57/1.16 fof(f458,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f428,f202])).
% 5.57/1.16 fof(f460,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f458,f203])).
% 5.57/1.16 fof(f477,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK12_skl(sK15_skl),tptp2)|occurrence_of(sK12_skl(sK15_skl),tptp1)),
% 5.57/1.16 inference(resolution,[status(thm)],[f429,f202])).
% 5.57/1.16 fof(f479,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK12_skl(sK15_skl),tptp2)|occurrence_of(sK12_skl(sK15_skl),tptp1)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f477,f203])).
% 5.57/1.16 fof(f481,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f430,f202])).
% 5.57/1.16 fof(f483,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f481,f203])).
% 5.57/1.16 fof(f523,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK16_skl)|~arboreal(X0)|leaf_occ(X0,sK16_skl)|leaf(sK12_skl(X0),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f185,f201])).
% 5.57/1.16 fof(f541,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f460,f157])).
% 5.57/1.16 fof(f545,plain,(
% 5.57/1.16 min_precedes(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f541,f204])).
% 5.57/1.16 fof(f547,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|leaf_occ(sK15_skl,sK16_skl)|leaf(sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f523,f202])).
% 5.57/1.16 fof(f549,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|leaf(sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f547,f203])).
% 5.57/1.16 fof(f558,plain,(
% 5.57/1.16 precedes(sK14_skl(sK15_skl),sK13_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f545,f148])).
% 5.57/1.16 fof(f560,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK13_skl(sK15_skl),X0)|subactivity_occurrence(sK14_skl(sK15_skl),X0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f545,f163])).
% 5.57/1.16 fof(f562,plain,(
% 5.57/1.16 earlier(sK14_skl(sK15_skl),sK13_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f558,f135])).
% 5.57/1.16 fof(f586,plain,(
% 5.57/1.16 ![X0]: (leaf_occ(sK15_skl,sK16_skl)|~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~occurrence_of(sK12_skl(sK15_skl),tptp1)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f549,f206])).
% 5.57/1.16 fof(f587,plain,(
% 5.57/1.16 ![X0]: (leaf_occ(sK15_skl,sK16_skl)|~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~occurrence_of(sK12_skl(sK15_skl),tptp2)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f549,f205])).
% 5.57/1.16 fof(f589,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|atomic(tptp0)|leaf_occ(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f549,f76])).
% 5.57/1.16 fof(f590,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|atomic(tptp0)|occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f549,f75])).
% 5.57/1.16 fof(f593,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~occurrence_of(sK12_skl(sK15_skl),tptp1)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f586,f204])).
% 5.57/1.16 fof(f594,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~occurrence_of(sK12_skl(sK15_skl),tptp2)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f587,f204])).
% 5.57/1.16 fof(f596,plain,(
% 5.57/1.16 atomic(tptp0)|leaf_occ(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f589,f204])).
% 5.57/1.16 fof(f597,plain,(
% 5.57/1.16 atomic(tptp0)|occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f590,f204])).
% 5.57/1.16 fof(f679,plain,(
% 5.57/1.16 ![X0]: (atomic(tptp0)|~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),X0)|X0=tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f597,f79])).
% 5.57/1.16 fof(f680,plain,(
% 5.57/1.16 atomic(tptp0)|activity_occurrence(sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f597,f60])).
% 5.57/1.16 fof(f697,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),X0)|X0=tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f679,f187])).
% 5.57/1.16 fof(f698,plain,(
% 5.57/1.16 activity_occurrence(sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f680,f187])).
% 5.57/1.16 fof(f699,plain,(
% 5.57/1.16 occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),sK4_skl(sK3_skl(tptp0,sK12_skl(sK15_skl))))),
% 5.57/1.16 inference(resolution,[status(thm)],[f698,f92])).
% 5.57/1.16 fof(f788,plain,(
% 5.57/1.16 leaf_occ(sK15_skl,sK16_skl)|min_precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f483,f157])).
% 5.57/1.16 fof(f792,plain,(
% 5.57/1.16 min_precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f788,f204])).
% 5.57/1.16 fof(f807,plain,(
% 5.57/1.16 precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f792,f148])).
% 5.57/1.16 fof(f809,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK12_skl(sK15_skl),X0)|subactivity_occurrence(sK13_skl(sK15_skl),X0))),
% 5.57/1.16 inference(resolution,[status(thm)],[f792,f163])).
% 5.57/1.16 fof(f820,plain,(
% 5.57/1.16 earlier(sK13_skl(sK15_skl),sK12_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f807,f135])).
% 5.57/1.16 fof(f821,plain,(
% 5.57/1.16 legal(sK12_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f807,f136])).
% 5.57/1.16 fof(f822,plain,(
% 5.57/1.16 ![X0]: (precedes(X0,sK12_skl(sK15_skl))|~earlier(X0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f821,f137])).
% 5.57/1.16 fof(f824,plain,(
% 5.57/1.16 ![X0]: (~earlier(X0,sK13_skl(sK15_skl))|earlier(X0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f820,f172])).
% 5.57/1.16 fof(f880,plain,(
% 5.57/1.16 earlier(sK14_skl(sK15_skl),sK12_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f824,f562])).
% 5.57/1.16 fof(f892,plain,(
% 5.57/1.16 precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f880,f822])).
% 5.57/1.16 fof(f894,plain,(
% 5.57/1.16 ~earlier(sK12_skl(sK15_skl),sK14_skl(sK15_skl))),
% 5.57/1.16 inference(resolution,[status(thm)],[f880,f132])).
% 5.57/1.16 fof(f895,plain,(
% 5.57/1.16 ![X0,X1]: (~min_precedes(X0,sK14_skl(sK15_skl),X1)|~min_precedes(X0,sK12_skl(sK15_skl),X1)|min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),X1))),
% 5.57/1.16 inference(resolution,[status(thm)],[f892,f175])).
% 5.57/1.16 fof(f948,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0)|leaf_occ(sK15_skl,sK16_skl)|occurrence_of(sK12_skl(sK15_skl),tptp2))),
% 5.57/1.16 inference(resolution,[status(thm)],[f593,f479])).
% 5.57/1.16 fof(f949,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0))),
% 5.57/1.16 inference(backward_subsumption_resolution,[status(thm)],[f594,f950])).
% 5.57/1.16 fof(f950,plain,(
% 5.57/1.16 ![X0]: (~occurrence_of(X0,tptp3)|~next_subocc(sK15_skl,X0,tptp0)|~min_precedes(X0,sK12_skl(sK15_skl),tptp0)|occurrence_of(sK12_skl(sK15_skl),tptp2))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f948,f204])).
% 5.57/1.16 fof(f983,plain,(
% 5.57/1.16 ![X0,X1]: (atomic(tptp0)|~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),X0)|~subactivity_occurrence(X1,sK3_skl(tptp0,sK12_skl(sK15_skl)))|~arboreal(X1)|min_precedes(X1,sK12_skl(sK15_skl),X0)|sK12_skl(sK15_skl)=X1)),
% 5.57/1.16 inference(resolution,[status(thm)],[f596,f57])).
% 5.57/1.16 fof(f984,plain,(
% 5.57/1.16 atomic(tptp0)|subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f596,f121])).
% 5.57/1.16 fof(f990,plain,(
% 5.57/1.16 ![X0,X1]: (~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),X0)|~subactivity_occurrence(X1,sK3_skl(tptp0,sK12_skl(sK15_skl)))|~arboreal(X1)|min_precedes(X1,sK12_skl(sK15_skl),X0)|sK12_skl(sK15_skl)=X1)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f983,f187])).
% 5.57/1.16 fof(f991,plain,(
% 5.57/1.16 subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f984,f187])).
% 5.57/1.16 fof(f1219,plain,(
% 5.57/1.16 ~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)|subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f809,f991])).
% 5.57/1.16 fof(f1277,plain,(
% 5.57/1.16 sK4_skl(sK3_skl(tptp0,sK12_skl(sK15_skl)))=tptp0),
% 5.57/1.16 inference(resolution,[status(thm)],[f699,f697])).
% 5.57/1.16 fof(f1287,plain,(
% 5.57/1.16 occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)),
% 5.57/1.16 inference(backward_demodulation,[status(thm)],[f1277,f699])).
% 5.57/1.16 fof(f1310,plain,(
% 5.57/1.16 subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(backward_subsumption_resolution,[status(thm)],[f1219,f1287])).
% 5.57/1.16 fof(f1352,plain,(
% 5.57/1.16 ~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)|subactivity_occurrence(sK14_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f1310,f560])).
% 5.57/1.16 fof(f1356,plain,(
% 5.57/1.16 subactivity_occurrence(sK14_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1352,f1287])).
% 5.57/1.16 fof(f1364,plain,(
% 5.57/1.16 ~occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)|subactivity_occurrence(sK15_skl,sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(resolution,[status(thm)],[f1356,f451])).
% 5.57/1.16 fof(f1368,plain,(
% 5.57/1.16 subactivity_occurrence(sK15_skl,sK3_skl(tptp0,sK12_skl(sK15_skl)))),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1364,f1287])).
% 5.57/1.16 fof(f1525,plain,(
% 5.57/1.16 next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)|~min_precedes(sK15_skl,sK11_skl(tptp0,sK14_skl(sK15_skl),sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f441,f439])).
% 5.57/1.16 fof(f1537,plain,(
% 5.57/1.16 next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1525,f442])).
% 5.57/1.16 fof(f1550,plain,(
% 5.57/1.16 ~occurrence_of(sK14_skl(sK15_skl),tptp3)|~min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f1537,f949])).
% 5.57/1.16 fof(f1557,plain,(
% 5.57/1.16 ~min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1550,f356])).
% 5.57/1.16 fof(f2126,plain,(
% 5.57/1.16 ![X0]: (~subactivity_occurrence(X0,sK3_skl(tptp0,sK12_skl(sK15_skl)))|~arboreal(X0)|min_precedes(X0,sK12_skl(sK15_skl),tptp0)|sK12_skl(sK15_skl)=X0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f990,f1287])).
% 5.57/1.16 fof(f2578,plain,(
% 5.57/1.16 ~min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)|min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(resolution,[status(thm)],[f895,f440])).
% 5.57/1.16 fof(f2581,plain,(
% 5.57/1.16 ~min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)),
% 5.57/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2578,f1557])).
% 5.57/1.16 fof(f2829,plain,(
% 5.57/1.16 ~arboreal(sK15_skl)|min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)|sK12_skl(sK15_skl)=sK15_skl),
% 5.57/1.16 inference(resolution,[status(thm)],[f2126,f1368])).
% 5.57/1.16 fof(f2834,plain,(
% 5.57/1.16 min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)|sK12_skl(sK15_skl)=sK15_skl),
% 5.57/1.18 inference(forward_subsumption_resolution,[status(thm)],[f2829,f203])).
% 5.57/1.18 fof(f2835,plain,(
% 5.57/1.18 sK12_skl(sK15_skl)=sK15_skl),
% 5.57/1.18 inference(resolution,[status(thm)],[f2834,f2581])).
% 5.57/1.18 fof(f3004,plain,(
% 5.57/1.18 ~earlier(sK15_skl,sK14_skl(sK15_skl))),
% 5.57/1.18 inference(backward_demodulation,[status(thm)],[f2835,f894])).
% 5.57/1.18 fof(f3423,plain,(
% 5.57/1.18 $false),
% 5.57/1.18 inference(forward_subsumption_resolution,[status(thm)],[f3004,f453])).
% 5.57/1.18 % SZS output end CNFRefutation for theBenchmark.p
% 5.57/1.19 % Elapsed time: 0.813019 seconds
% 5.57/1.19 % CPU time: 6.109914 seconds
% 5.57/1.19 % Total memory used: 169.702 MB
% 5.57/1.19 % Net memory used: 165.418 MB
%------------------------------------------------------------------------------