%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO018+2 : 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 : n006.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 14.45s 2.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO018+2 : 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.54 % Computer : n006.cluster.edu
% 0.10/0.54 % Model : x86_64 x86_64
% 0.10/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.54 % Memory : 8046.5625MB
% 0.10/0.54 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.54 % WCLimit : 300
% 0.10/0.54 % DateTime : Mon Sep 21 03:43:28 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.14/0.56 % Drodi V4.1.1
% 14.45/2.43 % Refutation found
% 14.45/2.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.45/2.43 % SZS output start CNFRefutation for theBenchmark
% 14.45/2.43 fof(f1,axiom,(
% 14.45/2.43 (! [X0,X1,X2,X3] :( ( min_precedes(X0,X1,X3)& min_precedes(X1,X2,X3) )=> min_precedes(X0,X2,X3) ) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f5,axiom,(
% 14.45/2.43 (! [X15,X16,X17] :( next_subocc(X15,X16,X17)<=> ( min_precedes(X15,X16,X17)& ~ (? [X18] :( min_precedes(X15,X18,X17)& min_precedes(X18,X16,X17) ) )) ) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f14,axiom,(
% 14.45/2.43 (! [X40,X41] :( occurrence_of(X40,X41)=> ( arboreal(X40)<=> atomic(X41) ) ) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f19,axiom,(
% 14.45/2.43 (! [X52] :( activity_occurrence(X52)=> (? [X53] :( activity(X53)& occurrence_of(X52,X53) ) )) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f22,axiom,(
% 14.45/2.43 (! [X60,X61,X62] :( ( occurrence_of(X60,X62)& leaf_occ(X61,X60) )=> ~ (? [X63] : min_precedes(X61,X63,X62) )) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f23,axiom,(
% 14.45/2.43 (! [X64,X65,X66] :( ( occurrence_of(X64,X65)& occurrence_of(X64,X66) )=> X65 = X66 ) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f25,axiom,(
% 14.45/2.43 (! [X70,X71,X72] :( min_precedes(X71,X72,X70)=> (? [X73] :( occurrence_of(X73,X70)& subactivity_occurrence(X71,X73)& subactivity_occurrence(X72,X73) ) )) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f30,axiom,(
% 14.45/2.43 (! [X89,X90] :( occurrence_of(X90,X89)=> ( activity(X89)& activity_occurrence(X90) ) ) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f33,axiom,(
% 14.45/2.43 (! [X95,X96] :( ( occurrence_of(X96,tptp0)& subactivity_occurrence(X95,X96)& arboreal(X95)& ~ leaf_occ(X95,X96) )=> (? [X97,X98,X99] :( occurrence_of(X97,tptp3)& next_subocc(X95,X97,tptp0)& occurrence_of(X98,tptp4)& min_precedes(X97,X98,tptp0)& ( occurrence_of(X99,tptp1)| occurrence_of(X99,tptp2) )& min_precedes(X98,X99,tptp0)& (! [X100] :( min_precedes(X97,X100,tptp0)=> ( X100 = X98| X100 = X99 ) ) )) )) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f36,axiom,(
% 14.45/2.43 atomic(tptp4) ),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f40,axiom,(
% 14.45/2.43 tptp4 != tptp3 ),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f43,axiom,(
% 14.45/2.43 tptp3 != tptp1 ),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f44,axiom,(
% 14.45/2.43 tptp3 != tptp2 ),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f46,conjecture,(
% 14.45/2.43 (! [X101,X102] :( ( occurrence_of(X102,tptp0)& subactivity_occurrence(X101,X102)& arboreal(X101)& ~ leaf_occ(X101,X102) )=> (? [X103,X104] :( occurrence_of(X103,tptp3)& next_subocc(X101,X103,tptp0)& ( occurrence_of(X104,tptp1)| occurrence_of(X104,tptp2) )& min_precedes(X103,X104,tptp0)& leaf_occ(X104,X102)& ( occurrence_of(X104,tptp1)=> ~ (? [X105] :( occurrence_of(X105,tptp2)& min_precedes(X103,X105,tptp0) ) ))& ( occurrence_of(X104,tptp2)=> ~ (? [X106] :( occurrence_of(X106,tptp1)& min_precedes(X103,X106,tptp0) ) )) ) )) )),
% 14.45/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.45/2.43 fof(f47,negated_conjecture,(
% 14.45/2.43 ~((! [X101,X102] :( ( occurrence_of(X102,tptp0)& subactivity_occurrence(X101,X102)& arboreal(X101)& ~ leaf_occ(X101,X102) )=> (? [X103,X104] :( occurrence_of(X103,tptp3)& next_subocc(X101,X103,tptp0)& ( occurrence_of(X104,tptp1)| occurrence_of(X104,tptp2) )& min_precedes(X103,X104,tptp0)& leaf_occ(X104,X102)& ( occurrence_of(X104,tptp1)=> ~ (? [X105] :( occurrence_of(X105,tptp2)& min_precedes(X103,X105,tptp0) ) ))& ( occurrence_of(X104,tptp2)=> ~ (? [X106] :( occurrence_of(X106,tptp1)& min_precedes(X103,X106,tptp0) ) )) ) )) ))),
% 14.45/2.43 inference(negated_conjecture,[status(cth)],[f46])).
% 14.45/2.43 fof(f48,plain,(
% 14.45/2.43 ![X0,X1,X2,X3]: ((~min_precedes(X0,X1,X3)|~min_precedes(X1,X2,X3))|min_precedes(X0,X2,X3))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 14.45/2.43 fof(f49,plain,(
% 14.45/2.43 ![X0,X2,X3]: ((![X1]: (~min_precedes(X0,X1,X3)|~min_precedes(X1,X2,X3)))|min_precedes(X0,X2,X3))),
% 14.45/2.43 inference(miniscoping,[status(thm)],[f48])).
% 14.45/2.43 fof(f50,plain,(
% 14.45/2.43 ![X0,X1,X2,X3]: (~min_precedes(X0,X1,X2)|~min_precedes(X1,X3,X2)|min_precedes(X0,X3,X2))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f49])).
% 14.45/2.43 fof(f60,plain,(
% 14.45/2.43 ![X15,X16,X17]: (next_subocc(X15,X16,X17)<=>(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 14.45/2.43 fof(f61,plain,(
% 14.45/2.43 ![X15,X16,X17]: ((~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))&(next_subocc(X15,X16,X17)|(~min_precedes(X15,X16,X17)|(?[X18]: (min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))))),
% 14.45/2.43 inference(NNF_transformation,[status(thm)],[f60])).
% 14.45/2.43 fof(f62,plain,(
% 14.45/2.43 (![X15,X16,X17]: (~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17))))))&(![X15,X16,X17]: (next_subocc(X15,X16,X17)|(~min_precedes(X15,X16,X17)|(?[X18]: (min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))))),
% 14.45/2.43 inference(miniscoping,[status(thm)],[f61])).
% 14.45/2.43 fof(f63,plain,(
% 14.45/2.43 (![X15,X16,X17]: (~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]: (~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17))))))&(![X15,X16,X17]: (next_subocc(X15,X16,X17)|(~min_precedes(X15,X16,X17)|(min_precedes(X15,sK0_skl(X17,X16,X15),X17)&min_precedes(sK0_skl(X17,X16,X15),X16,X17)))))),
% 14.45/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f62])).
% 14.45/2.43 fof(f64,plain,(
% 14.45/2.43 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f63])).
% 14.45/2.43 fof(f102,plain,(
% 14.45/2.43 ![X40,X41]: (~occurrence_of(X40,X41)|(arboreal(X40)<=>atomic(X41)))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 14.45/2.43 fof(f103,plain,(
% 14.45/2.43 ![X40,X41]: (~occurrence_of(X40,X41)|((~arboreal(X40)|atomic(X41))&(arboreal(X40)|~atomic(X41))))),
% 14.45/2.43 inference(NNF_transformation,[status(thm)],[f102])).
% 14.45/2.43 fof(f105,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f103])).
% 14.45/2.43 fof(f125,plain,(
% 14.45/2.43 ![X52]: (~activity_occurrence(X52)|(?[X53]: (activity(X53)&occurrence_of(X52,X53))))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 14.45/2.43 fof(f126,plain,(
% 14.45/2.43 ![X52]: (~activity_occurrence(X52)|(activity(sK6_skl(X52))&occurrence_of(X52,sK6_skl(X52))))),
% 14.45/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(X53,sK6_skl(X52))],[f125])).
% 14.45/2.43 fof(f128,plain,(
% 14.45/2.43 ![X0]: (~activity_occurrence(X0)|occurrence_of(X0,sK6_skl(X0)))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f126])).
% 14.45/2.43 fof(f135,plain,(
% 14.45/2.43 ![X60,X61,X62]: ((~occurrence_of(X60,X62)|~leaf_occ(X61,X60))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 14.45/2.43 fof(f136,plain,(
% 14.45/2.43 ![X61,X62]: ((![X60]: (~occurrence_of(X60,X62)|~leaf_occ(X61,X60)))|(![X63]: ~min_precedes(X61,X63,X62)))),
% 14.45/2.43 inference(miniscoping,[status(thm)],[f135])).
% 14.45/2.43 fof(f137,plain,(
% 14.45/2.43 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~leaf_occ(X2,X0)|~min_precedes(X2,X3,X1))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f136])).
% 14.45/2.43 fof(f138,plain,(
% 14.45/2.43 ![X64,X65,X66]: ((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 14.45/2.43 fof(f139,plain,(
% 14.45/2.43 ![X65,X66]: ((![X64]: (~occurrence_of(X64,X65)|~occurrence_of(X64,X66)))|X65=X66)),
% 14.45/2.43 inference(miniscoping,[status(thm)],[f138])).
% 14.45/2.43 fof(f140,plain,(
% 14.45/2.43 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f139])).
% 14.45/2.43 fof(f145,plain,(
% 14.45/2.43 ![X70,X71,X72]: (~min_precedes(X71,X72,X70)|(?[X73]: ((occurrence_of(X73,X70)&subactivity_occurrence(X71,X73))&subactivity_occurrence(X72,X73))))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 14.45/2.43 fof(f146,plain,(
% 14.45/2.43 ![X70,X71,X72]: (~min_precedes(X71,X72,X70)|((occurrence_of(sK8_skl(X72,X71,X70),X70)&subactivity_occurrence(X71,sK8_skl(X72,X71,X70)))&subactivity_occurrence(X72,sK8_skl(X72,X71,X70))))),
% 14.45/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X73,sK8_skl(X72,X71,X70))],[f145])).
% 14.45/2.43 fof(f147,plain,(
% 14.45/2.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK8_skl(X1,X0,X2),X2))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f146])).
% 14.45/2.43 fof(f149,plain,(
% 14.45/2.43 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK8_skl(X1,X0,X2)))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f146])).
% 14.45/2.43 fof(f168,plain,(
% 14.45/2.43 ![X89,X90]: (~occurrence_of(X90,X89)|(activity(X89)&activity_occurrence(X90)))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 14.45/2.43 fof(f170,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,X1)|activity_occurrence(X0))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f168])).
% 14.45/2.43 fof(f177,plain,(
% 14.45/2.43 ![X95,X96]: ((((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96))|(?[X97,X98,X99]: ((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&min_precedes(X97,X98,tptp0))&(occurrence_of(X99,tptp1)|occurrence_of(X99,tptp2)))&min_precedes(X98,X99,tptp0))&(![X100]: (~min_precedes(X97,X100,tptp0)|(X100=X98|X100=X99))))))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 14.45/2.43 fof(f178,plain,(
% 14.45/2.43 ![X95]: ((![X96]: (((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96)))|(?[X97,X98,X99]: ((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&min_precedes(X97,X98,tptp0))&(occurrence_of(X99,tptp1)|occurrence_of(X99,tptp2)))&min_precedes(X98,X99,tptp0))&(![X100]: (~min_precedes(X97,X100,tptp0)|(X100=X98|X100=X99))))))),
% 14.45/2.43 inference(miniscoping,[status(thm)],[f177])).
% 14.45/2.43 fof(f179,plain,(
% 14.45/2.43 ![X95]: ((![X96]: (((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96)))|((((((occurrence_of(sK14_skl(X95),tptp3)&next_subocc(X95,sK14_skl(X95),tptp0))&occurrence_of(sK15_skl(X95),tptp4))&min_precedes(sK14_skl(X95),sK15_skl(X95),tptp0))&(occurrence_of(sK16_skl(X95),tptp1)|occurrence_of(sK16_skl(X95),tptp2)))&min_precedes(sK15_skl(X95),sK16_skl(X95),tptp0))&(![X100]: (~min_precedes(sK14_skl(X95),X100,tptp0)|(X100=sK15_skl(X95)|X100=sK16_skl(X95))))))),
% 14.45/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X97,sK14_skl(X95)),skolemize(X98,sK15_skl(X95)),skolemize(X99,sK16_skl(X95))],[f178])).
% 14.45/2.43 fof(f180,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK14_skl(X1),tptp3))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f181,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|next_subocc(X1,sK14_skl(X1),tptp0))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f182,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK15_skl(X1),tptp4))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f183,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK14_skl(X1),sK15_skl(X1),tptp0))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f184,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|occurrence_of(sK16_skl(X1),tptp1)|occurrence_of(sK16_skl(X1),tptp2))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f185,plain,(
% 14.45/2.43 ![X0,X1]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|min_precedes(sK15_skl(X1),sK16_skl(X1),tptp0))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f186,plain,(
% 14.45/2.43 ![X0,X1,X2]: (~occurrence_of(X0,tptp0)|~subactivity_occurrence(X1,X0)|~arboreal(X1)|leaf_occ(X1,X0)|~min_precedes(sK14_skl(X1),X2,tptp0)|X2=sK15_skl(X1)|X2=sK16_skl(X1))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f179])).
% 14.45/2.43 fof(f189,plain,(
% 14.45/2.43 atomic(tptp4)),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f36])).
% 14.45/2.43 fof(f193,plain,(
% 14.45/2.43 ~tptp4=tptp3),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f40])).
% 14.45/2.43 fof(f196,plain,(
% 14.45/2.43 ~tptp3=tptp1),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f43])).
% 14.45/2.43 fof(f197,plain,(
% 14.45/2.43 ~tptp3=tptp2),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f44])).
% 14.45/2.43 fof(f199,plain,(
% 14.45/2.43 (?[X101,X102]: ((((occurrence_of(X102,tptp0)&subactivity_occurrence(X101,X102))&arboreal(X101))&~leaf_occ(X101,X102))&(![X103,X104]: ((((((~occurrence_of(X103,tptp3)|~next_subocc(X101,X103,tptp0))|(~occurrence_of(X104,tptp1)&~occurrence_of(X104,tptp2)))|~min_precedes(X103,X104,tptp0))|~leaf_occ(X104,X102))|(occurrence_of(X104,tptp1)&(?[X105]: (occurrence_of(X105,tptp2)&min_precedes(X103,X105,tptp0)))))|(occurrence_of(X104,tptp2)&(?[X106]: (occurrence_of(X106,tptp1)&min_precedes(X103,X106,tptp0))))))))),
% 14.45/2.43 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 14.45/2.43 fof(f200,definition,(
% 14.45/2.43 ![X104]: (sP0_prd(X104)<=>(~occurrence_of(X104,tptp1)&~occurrence_of(X104,tptp2)))),
% 14.45/2.43 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 14.45/2.43 fof(f201,definition,(
% 14.45/2.43 ![X103,X104]: (sP1_prd(X104,X103)<=>(occurrence_of(X104,tptp1)&(?[X105]: (occurrence_of(X105,tptp2)&min_precedes(X103,X105,tptp0)))))),
% 14.45/2.43 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 14.45/2.43 fof(f202,plain,(
% 14.45/2.43 ?[X101,X102]: ((((occurrence_of(X102,tptp0)&subactivity_occurrence(X101,X102))&arboreal(X101))&~leaf_occ(X101,X102))&(![X103,X104]: ((((((~occurrence_of(X103,tptp3)|~next_subocc(X101,X103,tptp0))|sP0_prd(X104))|~min_precedes(X103,X104,tptp0))|~leaf_occ(X104,X102))|sP1_prd(X104,X103))|(occurrence_of(X104,tptp2)&(?[X106]: (occurrence_of(X106,tptp1)&min_precedes(X103,X106,tptp0)))))))),
% 14.45/2.43 inference(formula_renaming,[status(thm)],[f199,f201,f200])).
% 14.45/2.43 fof(f203,plain,(
% 14.45/2.43 ((((occurrence_of(sK18_skl,tptp0)&subactivity_occurrence(sK17_skl,sK18_skl))&arboreal(sK17_skl))&~leaf_occ(sK17_skl,sK18_skl))&(![X103,X104]: ((((((~occurrence_of(X103,tptp3)|~next_subocc(sK17_skl,X103,tptp0))|sP0_prd(X104))|~min_precedes(X103,X104,tptp0))|~leaf_occ(X104,sK18_skl))|sP1_prd(X104,X103))|(occurrence_of(X104,tptp2)&(occurrence_of(sK19_skl(X104,X103),tptp1)&min_precedes(X103,sK19_skl(X104,X103),tptp0))))))),
% 14.45/2.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(X101,sK17_skl),skolemize(X102,sK18_skl),skolemize(X106,sK19_skl(X104,X103))],[f202])).
% 14.45/2.43 fof(f204,plain,(
% 14.45/2.43 occurrence_of(sK18_skl,tptp0)),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f203])).
% 14.45/2.43 fof(f205,plain,(
% 14.45/2.43 subactivity_occurrence(sK17_skl,sK18_skl)),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f203])).
% 14.45/2.43 fof(f206,plain,(
% 14.45/2.43 arboreal(sK17_skl)),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f203])).
% 14.45/2.43 fof(f207,plain,(
% 14.45/2.43 ~leaf_occ(sK17_skl,sK18_skl)),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f203])).
% 14.45/2.43 fof(f211,plain,(
% 14.45/2.43 ![X104]: ((~sP0_prd(X104)|(~occurrence_of(X104,tptp1)&~occurrence_of(X104,tptp2)))&(sP0_prd(X104)|(occurrence_of(X104,tptp1)|occurrence_of(X104,tptp2))))),
% 14.45/2.43 inference(NNF_transformation,[status(thm)],[f200])).
% 14.45/2.43 fof(f212,plain,(
% 14.45/2.43 (![X104]: (~sP0_prd(X104)|(~occurrence_of(X104,tptp1)&~occurrence_of(X104,tptp2))))&(![X104]: (sP0_prd(X104)|(occurrence_of(X104,tptp1)|occurrence_of(X104,tptp2))))),
% 14.45/2.43 inference(miniscoping,[status(thm)],[f211])).
% 14.45/2.43 fof(f213,plain,(
% 14.45/2.43 ![X0]: (~sP0_prd(X0)|~occurrence_of(X0,tptp1))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f212])).
% 14.45/2.43 fof(f214,plain,(
% 14.45/2.43 ![X0]: (~sP0_prd(X0)|~occurrence_of(X0,tptp2))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f212])).
% 14.45/2.43 fof(f215,plain,(
% 14.45/2.43 ![X0]: (sP0_prd(X0)|occurrence_of(X0,tptp1)|occurrence_of(X0,tptp2))),
% 14.45/2.43 inference(cnf_transformation,[status(thm)],[f212])).
% 14.45/2.43 fof(f251,plain,(
% 14.45/2.43 ![X0,X1]: (sP0_prd(X0)|occurrence_of(X0,tptp1)|~occurrence_of(X0,X1)|X1=tptp2)),
% 14.45/2.43 inference(resolution,[status(thm)],[f215,f140])).
% 14.45/2.43 fof(f526,plain,(
% 14.45/2.43 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK15_skl(sK17_skl),tptp4)),
% 14.45/2.43 inference(resolution,[status(thm)],[f182,f205])).
% 14.45/2.43 fof(f528,plain,(
% 14.45/2.43 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK15_skl(sK17_skl),tptp4)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f526,f204])).
% 14.45/2.43 fof(f589,plain,(
% 14.45/2.43 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 14.45/2.43 inference(resolution,[status(thm)],[f183,f205])).
% 14.45/2.43 fof(f591,plain,(
% 14.45/2.43 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f589,f204])).
% 14.45/2.43 fof(f594,plain,(
% 14.45/2.43 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK16_skl(sK17_skl),tptp1)|occurrence_of(sK16_skl(sK17_skl),tptp2)),
% 14.45/2.43 inference(resolution,[status(thm)],[f184,f205])).
% 14.45/2.43 fof(f596,plain,(
% 14.45/2.43 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK16_skl(sK17_skl),tptp1)|occurrence_of(sK16_skl(sK17_skl),tptp2)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f594,f204])).
% 14.45/2.43 fof(f599,plain,(
% 14.45/2.43 ~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)),
% 14.45/2.43 inference(resolution,[status(thm)],[f185,f205])).
% 14.45/2.43 fof(f601,plain,(
% 14.45/2.43 ~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f599,f204])).
% 14.45/2.43 fof(f700,plain,(
% 14.45/2.43 ![X0]: (~occurrence_of(sK18_skl,tptp0)|~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|~min_precedes(sK14_skl(sK17_skl),X0,tptp0)|X0=sK15_skl(sK17_skl)|X0=sK16_skl(sK17_skl))),
% 14.45/2.43 inference(resolution,[status(thm)],[f186,f205])).
% 14.45/2.43 fof(f702,plain,(
% 14.45/2.43 ![X0]: (~arboreal(sK17_skl)|leaf_occ(sK17_skl,sK18_skl)|~min_precedes(sK14_skl(sK17_skl),X0,tptp0)|X0=sK15_skl(sK17_skl)|X0=sK16_skl(sK17_skl))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f700,f204])).
% 14.45/2.43 fof(f703,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK15_skl(sK17_skl),tptp4)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f528,f206])).
% 14.45/2.43 fof(f713,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|activity_occurrence(sK15_skl(sK17_skl))),
% 14.45/2.43 inference(resolution,[status(thm)],[f703,f170])).
% 14.45/2.43 fof(f716,plain,(
% 14.45/2.43 ![X0]: (leaf_occ(sK17_skl,sK18_skl)|~occurrence_of(sK15_skl(sK17_skl),X0)|X0=tptp4)),
% 14.45/2.43 inference(resolution,[status(thm)],[f703,f140])).
% 14.45/2.43 fof(f720,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|arboreal(sK15_skl(sK17_skl))|~atomic(tptp4)),
% 14.45/2.43 inference(resolution,[status(thm)],[f703,f105])).
% 14.45/2.43 fof(f731,plain,(
% 14.45/2.43 activity_occurrence(sK15_skl(sK17_skl))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f713,f207])).
% 14.45/2.43 fof(f733,plain,(
% 14.45/2.43 ![X0]: (~occurrence_of(sK15_skl(sK17_skl),X0)|X0=tptp4)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f716,f207])).
% 14.45/2.43 fof(f736,plain,(
% 14.45/2.43 arboreal(sK15_skl(sK17_skl))|~atomic(tptp4)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f720,f207])).
% 14.45/2.43 fof(f743,plain,(
% 14.45/2.43 occurrence_of(sK15_skl(sK17_skl),sK6_skl(sK15_skl(sK17_skl)))),
% 14.45/2.43 inference(resolution,[status(thm)],[f731,f128])).
% 14.45/2.43 fof(f745,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f591,f206])).
% 14.45/2.43 fof(f757,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|subactivity_occurrence(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))),
% 14.45/2.43 inference(resolution,[status(thm)],[f745,f149])).
% 14.45/2.43 fof(f759,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)),
% 14.45/2.43 inference(resolution,[status(thm)],[f745,f147])).
% 14.45/2.43 fof(f771,plain,(
% 14.45/2.43 ![X0]: (leaf_occ(sK17_skl,sK18_skl)|~min_precedes(sK15_skl(sK17_skl),X0,tptp0)|min_precedes(sK14_skl(sK17_skl),X0,tptp0))),
% 14.45/2.43 inference(resolution,[status(thm)],[f745,f50])).
% 14.45/2.43 fof(f782,plain,(
% 14.45/2.43 subactivity_occurrence(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f757,f207])).
% 14.45/2.43 fof(f784,plain,(
% 14.45/2.43 occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f759,f207])).
% 14.45/2.43 fof(f796,plain,(
% 14.45/2.43 ![X0]: (~min_precedes(sK15_skl(sK17_skl),X0,tptp0)|min_precedes(sK14_skl(sK17_skl),X0,tptp0))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f771,f207])).
% 14.45/2.43 fof(f807,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK16_skl(sK17_skl),tptp1)|occurrence_of(sK16_skl(sK17_skl),tptp2)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f596,f206])).
% 14.45/2.43 fof(f808,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|occurrence_of(sK16_skl(sK17_skl),tptp1)|~sP0_prd(sK16_skl(sK17_skl))),
% 14.45/2.43 inference(resolution,[status(thm)],[f807,f214])).
% 14.45/2.43 fof(f829,plain,(
% 14.45/2.43 occurrence_of(sK16_skl(sK17_skl),tptp1)|~sP0_prd(sK16_skl(sK17_skl))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f808,f207])).
% 14.45/2.43 fof(f851,plain,(
% 14.45/2.43 leaf_occ(sK17_skl,sK18_skl)|min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f601,f206])).
% 14.45/2.43 fof(f869,plain,(
% 14.45/2.43 ![X0]: (leaf_occ(sK17_skl,sK18_skl)|~occurrence_of(X0,tptp0)|~leaf_occ(sK15_skl(sK17_skl),X0))),
% 14.45/2.43 inference(resolution,[status(thm)],[f851,f137])).
% 14.45/2.43 fof(f894,plain,(
% 14.45/2.43 ![X0]: (~occurrence_of(X0,tptp0)|~leaf_occ(sK15_skl(sK17_skl),X0))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f869,f207])).
% 14.45/2.43 fof(f903,plain,(
% 14.45/2.43 ![X0]: (leaf_occ(sK17_skl,sK18_skl)|~min_precedes(sK14_skl(sK17_skl),X0,tptp0)|X0=sK15_skl(sK17_skl)|X0=sK16_skl(sK17_skl))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f702,f206])).
% 14.45/2.43 fof(f911,plain,(
% 14.45/2.43 arboreal(sK15_skl(sK17_skl))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f736,f189])).
% 14.45/2.43 fof(f952,plain,(
% 14.45/2.43 sK6_skl(sK15_skl(sK17_skl))=tptp4),
% 14.45/2.43 inference(resolution,[status(thm)],[f743,f733])).
% 14.45/2.43 fof(f1358,plain,(
% 14.45/2.43 ~sP0_prd(sK16_skl(sK17_skl))),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f829,f213])).
% 14.45/2.43 fof(f1690,plain,(
% 14.45/2.43 ~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)|~arboreal(sK15_skl(sK17_skl))|leaf_occ(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|next_subocc(sK15_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)),
% 14.45/2.43 inference(resolution,[status(thm)],[f782,f181])).
% 14.45/2.43 fof(f1691,plain,(
% 14.45/2.43 ~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)|~arboreal(sK15_skl(sK17_skl))|leaf_occ(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp3)),
% 14.45/2.43 inference(resolution,[status(thm)],[f782,f180])).
% 14.45/2.43 fof(f1713,plain,(
% 14.45/2.43 ~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)|leaf_occ(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|next_subocc(sK15_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f1690,f911])).
% 14.45/2.43 fof(f1714,plain,(
% 14.45/2.43 ~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)|leaf_occ(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp3)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f1691,f911])).
% 14.45/2.43 fof(f5624,plain,(
% 14.45/2.43 leaf_occ(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|next_subocc(sK15_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f1713,f784])).
% 14.45/2.43 fof(f5625,plain,(
% 14.45/2.43 next_subocc(sK15_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)|~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)),
% 14.45/2.43 inference(resolution,[status(thm)],[f5624,f894])).
% 14.45/2.43 fof(f5636,plain,(
% 14.45/2.43 next_subocc(sK15_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f5625,f784])).
% 14.45/2.43 fof(f5637,plain,(
% 14.45/2.43 leaf_occ(sK15_skl(sK17_skl),sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0))|occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp3)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f1714,f784])).
% 14.45/2.43 fof(f5638,plain,(
% 14.45/2.43 occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp3)|~occurrence_of(sK8_skl(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),tptp0)),
% 14.45/2.43 inference(resolution,[status(thm)],[f5637,f894])).
% 14.45/2.43 fof(f5649,plain,(
% 14.45/2.43 occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp3)),
% 14.45/2.43 inference(forward_subsumption_resolution,[status(thm)],[f5638,f784])).
% 14.45/2.43 fof(f5658,plain,(
% 14.45/2.43 sP0_prd(sK14_skl(sK15_skl(sK17_skl)))|occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp1)|tptp3=tptp2),
% 14.45/2.46 inference(resolution,[status(thm)],[f5649,f251])).
% 14.45/2.46 fof(f5663,plain,(
% 14.45/2.46 activity_occurrence(sK14_skl(sK15_skl(sK17_skl)))),
% 14.45/2.46 inference(resolution,[status(thm)],[f5649,f170])).
% 14.45/2.46 fof(f5666,plain,(
% 14.45/2.46 ![X0]: (~occurrence_of(sK14_skl(sK15_skl(sK17_skl)),X0)|X0=tptp3)),
% 14.45/2.46 inference(resolution,[status(thm)],[f5649,f140])).
% 14.45/2.46 fof(f5675,plain,(
% 14.45/2.46 sP0_prd(sK14_skl(sK15_skl(sK17_skl)))|occurrence_of(sK14_skl(sK15_skl(sK17_skl)),tptp1)),
% 14.45/2.46 inference(forward_subsumption_resolution,[status(thm)],[f5658,f197])).
% 14.45/2.46 fof(f5678,plain,(
% 14.45/2.46 occurrence_of(sK14_skl(sK15_skl(sK17_skl)),sK6_skl(sK14_skl(sK15_skl(sK17_skl))))),
% 14.45/2.46 inference(resolution,[status(thm)],[f5663,f128])).
% 14.45/2.46 fof(f5717,plain,(
% 14.45/2.46 min_precedes(sK15_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)),
% 14.45/2.46 inference(resolution,[status(thm)],[f5636,f64])).
% 14.45/2.46 fof(f5735,plain,(
% 14.45/2.46 min_precedes(sK14_skl(sK17_skl),sK14_skl(sK15_skl(sK17_skl)),tptp0)),
% 14.45/2.46 inference(resolution,[status(thm)],[f5717,f796])).
% 14.45/2.46 fof(f6012,plain,(
% 14.45/2.46 leaf_occ(sK17_skl,sK18_skl)|sK14_skl(sK15_skl(sK17_skl))=sK15_skl(sK17_skl)|sK14_skl(sK15_skl(sK17_skl))=sK16_skl(sK17_skl)),
% 14.45/2.46 inference(resolution,[status(thm)],[f5735,f903])).
% 14.45/2.46 fof(f6047,plain,(
% 14.45/2.46 sK14_skl(sK15_skl(sK17_skl))=sK15_skl(sK17_skl)|sK14_skl(sK15_skl(sK17_skl))=sK16_skl(sK17_skl)),
% 14.45/2.46 inference(forward_subsumption_resolution,[status(thm)],[f6012,f207])).
% 14.45/2.46 fof(f6850,plain,(
% 14.45/2.46 sK6_skl(sK14_skl(sK15_skl(sK17_skl)))=tptp3),
% 14.45/2.46 inference(resolution,[status(thm)],[f5678,f5666])).
% 14.45/2.46 fof(f8042,plain,(
% 14.45/2.46 sP0_prd(sK14_skl(sK15_skl(sK17_skl)))|tptp1=tptp3),
% 14.45/2.46 inference(resolution,[status(thm)],[f5675,f5666])).
% 14.45/2.46 fof(f8082,plain,(
% 14.45/2.46 sP0_prd(sK14_skl(sK15_skl(sK17_skl)))),
% 14.45/2.46 inference(forward_subsumption_resolution,[status(thm)],[f8042,f196])).
% 14.45/2.46 fof(f13600,plain,(
% 14.45/2.46 sP0_prd(sK16_skl(sK17_skl))|sK14_skl(sK15_skl(sK17_skl))=sK15_skl(sK17_skl)),
% 14.45/2.46 inference(paramodulation,[status(thm)],[f6047,f8082])).
% 14.45/2.46 fof(f13657,plain,(
% 14.45/2.46 sK14_skl(sK15_skl(sK17_skl))=sK15_skl(sK17_skl)),
% 14.45/2.46 inference(forward_subsumption_resolution,[status(thm)],[f13600,f1358])).
% 14.45/2.46 fof(f13743,plain,(
% 14.45/2.46 sK6_skl(sK15_skl(sK17_skl))=tptp3),
% 14.45/2.46 inference(backward_demodulation,[status(thm)],[f13657,f6850])).
% 14.45/2.46 fof(f13795,plain,(
% 14.45/2.46 tptp4=tptp3),
% 14.45/2.46 inference(forward_demodulation,[status(thm)],[f952,f13743])).
% 14.45/2.46 fof(f13796,plain,(
% 14.45/2.46 $false),
% 14.45/2.46 inference(forward_subsumption_resolution,[status(thm)],[f13795,f193])).
% 14.45/2.46 % SZS output end CNFRefutation for theBenchmark.p
% 1.12/2.52 % Elapsed time: 1.961865 seconds
% 1.12/2.52 % CPU time: 14.898369 seconds
% 1.12/2.52 % Total memory used: 183.864 MB
% 1.12/2.52 % Net memory used: 172.464 MB
%------------------------------------------------------------------------------