%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO003+3 : 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 : n020.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:22 PM UTC 2026
% Result : Theorem 56.33s 12.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO003+3 : 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.08/5.36 % Computer : n020.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Mon Sep 21 03:41:37 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.38 % Drodi V4.1.1
% 56.33/12.58 % Refutation found
% 56.33/12.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.33/12.58 % SZS output start CNFRefutation for theBenchmark
% 56.33/12.58 fof(f3,axiom,(
% 56.33/12.58 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f23,axiom,(
% 56.33/12.58 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f26,axiom,(
% 56.33/12.58 (! [X69,X70,X71] :( min_precedes(X70,X71,X69)=> (? [X72] :( occurrence_of(X72,X69)& subactivity_occurrence(X70,X72)& subactivity_occurrence(X71,X72) ) )) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f28,axiom,(
% 56.33/12.58 (! [X76,X77] :( ( occurrence_of(X77,X76)& ~ atomic(X76) )=> (? [X78] :( root(X78,X76)& subactivity_occurrence(X78,X77) ) )) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f34,axiom,(
% 56.33/12.58 (! [X99,X100] :( root_occ(X99,X100)<=> (? [X101] :( occurrence_of(X100,X101)& subactivity_occurrence(X99,X100)& root(X99,X101) ) )) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f35,axiom,(
% 56.33/12.58 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f36,axiom,(
% 56.33/12.58 (! [X105,X106,X107,X108] :( ( occurrence_of(X107,X108)& root_occ(X105,X107)& root_occ(X106,X107) )=> X105 = X106 ) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f40,axiom,(
% 56.33/12.58 (! [X121,X122,X123,X124,X125] :( ( next_subocc(X121,X122,X124)& next_subocc(X121,X123,X124)& occurrence_of(X125,X124)& subactivity_occurrence(X123,X125)& subactivity_occurrence(X122,X125) )=> X122 = X123 ) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f50,axiom,(
% 56.33/12.58 (! [X161] :( occurrence_of(X161,tptp0)=> (? [X162,X163] :( occurrence_of(X162,tptp4)& root_occ(X162,X161)& occurrence_of(X163,tptp3)& leaf_occ(X163,X161)& next_subocc(X162,X163,tptp0) ) )) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f52,axiom,(
% 56.33/12.58 ~ atomic(tptp0) ),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f60,axiom,(
% 56.33/12.58 tptp1 != tptp3 ),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f63,axiom,(
% 56.33/12.58 (! [X164,X165] :( ( occurrence_of(X165,tptp0)& root_occ(X164,X165) )=> (? [X166] :( occurrence_of(X166,tptp1)& next_subocc(X164,X166,tptp0) ) )) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f64,conjecture,(
% 56.33/12.58 ~ (? [X167] : occurrence_of(X167,tptp0) )),
% 56.33/12.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.33/12.58 fof(f65,negated_conjecture,(
% 56.33/12.58 ~(~ (? [X167] : occurrence_of(X167,tptp0) ))),
% 56.33/12.58 inference(negated_conjecture,[status(cth)],[f64])).
% 56.33/12.58 fof(f73,plain,(
% 56.33/12.58 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 56.33/12.58 fof(f74,plain,(
% 56.33/12.58 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f73])).
% 56.33/12.58 fof(f75,plain,(
% 56.33/12.58 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f74])).
% 56.33/12.58 fof(f144,plain,(
% 56.33/12.58 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 56.33/12.58 fof(f145,plain,(
% 56.33/12.58 ![X60,X61,X62]: ((~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))&(next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 56.33/12.58 inference(NNF_transformation,[status(thm)],[f144])).
% 56.33/12.58 fof(f146,plain,(
% 56.33/12.58 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f145])).
% 56.33/12.58 fof(f147,plain,(
% 56.33/12.58 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(min_precedes(X60,sK7_skl(X62,X61,X60),X62)&min_precedes(sK7_skl(X62,X61,X60),X61,X62)))))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f146])).
% 56.33/12.58 fof(f148,plain,(
% 56.33/12.58 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f147])).
% 56.33/12.58 fof(f162,plain,(
% 56.33/12.58 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|(?[X72]: ((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))))),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 56.33/12.58 fof(f163,plain,(
% 56.33/12.58 ![X69,X70,X71]: (~min_precedes(X70,X71,X69)|((occurrence_of(sK9_skl(X71,X70,X69),X69)&subactivity_occurrence(X70,sK9_skl(X71,X70,X69)))&subactivity_occurrence(X71,sK9_skl(X71,X70,X69))))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f162])).
% 56.33/12.58 fof(f164,plain,(
% 56.33/12.58 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|occurrence_of(sK9_skl(X1,X0,X2),X2))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f163])).
% 56.33/12.58 fof(f165,plain,(
% 56.33/12.58 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X0,sK9_skl(X1,X0,X2)))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f163])).
% 56.33/12.58 fof(f166,plain,(
% 56.33/12.58 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|subactivity_occurrence(X1,sK9_skl(X1,X0,X2)))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f163])).
% 56.33/12.58 fof(f171,plain,(
% 56.33/12.58 ![X76,X77]: ((~occurrence_of(X77,X76)|atomic(X76))|(?[X78]: (root(X78,X76)&subactivity_occurrence(X78,X77))))),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 56.33/12.58 fof(f172,plain,(
% 56.33/12.58 ![X76,X77]: ((~occurrence_of(X77,X76)|atomic(X76))|(root(sK11_skl(X77,X76),X76)&subactivity_occurrence(sK11_skl(X77,X76),X77)))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X78,sK11_skl(X77,X76))],[f171])).
% 56.33/12.58 fof(f173,plain,(
% 56.33/12.58 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1)|root(sK11_skl(X0,X1),X1))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f172])).
% 56.33/12.58 fof(f174,plain,(
% 56.33/12.58 ![X0,X1]: (~occurrence_of(X0,X1)|atomic(X1)|subactivity_occurrence(sK11_skl(X0,X1),X0))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f172])).
% 56.33/12.58 fof(f192,plain,(
% 56.33/12.58 ![X99,X100]: ((~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101))))&(root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 56.33/12.58 inference(NNF_transformation,[status(thm)],[f34])).
% 56.33/12.58 fof(f193,plain,(
% 56.33/12.58 (![X99,X100]: (~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f192])).
% 56.33/12.58 fof(f194,plain,(
% 56.33/12.58 (![X99,X100]: (~root_occ(X99,X100)|((occurrence_of(X100,sK13_skl(X100,X99))&subactivity_occurrence(X99,X100))&root(X99,sK13_skl(X100,X99)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f193])).
% 56.33/12.58 fof(f198,plain,(
% 56.33/12.58 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f194])).
% 56.33/12.58 fof(f199,plain,(
% 56.33/12.58 ![X102,X103]: ((~leaf_occ(X102,X103)|(?[X104]: ((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104))))&(leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 56.33/12.58 inference(NNF_transformation,[status(thm)],[f35])).
% 56.33/12.58 fof(f200,plain,(
% 56.33/12.58 (![X102,X103]: (~leaf_occ(X102,X103)|(?[X104]: ((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104)))))&(![X102,X103]: (leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f199])).
% 56.33/12.58 fof(f201,plain,(
% 56.33/12.58 (![X102,X103]: (~leaf_occ(X102,X103)|((occurrence_of(X103,sK14_skl(X103,X102))&subactivity_occurrence(X102,X103))&leaf(X102,sK14_skl(X103,X102)))))&(![X102,X103]: (leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f200])).
% 56.33/12.58 fof(f203,plain,(
% 56.33/12.58 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f201])).
% 56.33/12.58 fof(f206,plain,(
% 56.33/12.58 ![X105,X106,X107,X108]: (((~occurrence_of(X107,X108)|~root_occ(X105,X107))|~root_occ(X106,X107))|X105=X106)),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 56.33/12.58 fof(f207,plain,(
% 56.33/12.58 ![X105,X106]: ((![X107]: (((![X108]: ~occurrence_of(X107,X108))|~root_occ(X105,X107))|~root_occ(X106,X107)))|X105=X106)),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f206])).
% 56.33/12.58 fof(f208,plain,(
% 56.33/12.58 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~root_occ(X2,X0)|~root_occ(X3,X0)|X2=X3)),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f207])).
% 56.33/12.58 fof(f218,plain,(
% 56.33/12.58 ![X121,X122,X123,X124,X125]: (((((~next_subocc(X121,X122,X124)|~next_subocc(X121,X123,X124))|~occurrence_of(X125,X124))|~subactivity_occurrence(X123,X125))|~subactivity_occurrence(X122,X125))|X122=X123)),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 56.33/12.58 fof(f219,plain,(
% 56.33/12.58 ![X122,X123]: ((![X125]: (((![X124]: ((![X121]: (~next_subocc(X121,X122,X124)|~next_subocc(X121,X123,X124)))|~occurrence_of(X125,X124)))|~subactivity_occurrence(X123,X125))|~subactivity_occurrence(X122,X125)))|X122=X123)),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f218])).
% 56.33/12.58 fof(f220,plain,(
% 56.33/12.58 ![X0,X1,X2,X3,X4]: (~next_subocc(X0,X1,X2)|~next_subocc(X0,X3,X2)|~occurrence_of(X4,X2)|~subactivity_occurrence(X3,X4)|~subactivity_occurrence(X1,X4)|X1=X3)),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f219])).
% 56.33/12.58 fof(f250,plain,(
% 56.33/12.58 ![X161]: (~occurrence_of(X161,tptp0)|(?[X162,X163]: ((((occurrence_of(X162,tptp4)&root_occ(X162,X161))&occurrence_of(X163,tptp3))&leaf_occ(X163,X161))&next_subocc(X162,X163,tptp0))))),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 56.33/12.58 fof(f251,plain,(
% 56.33/12.58 ![X161]: (~occurrence_of(X161,tptp0)|((((occurrence_of(sK16_skl(X161),tptp4)&root_occ(sK16_skl(X161),X161))&occurrence_of(sK17_skl(X161),tptp3))&leaf_occ(sK17_skl(X161),X161))&next_subocc(sK16_skl(X161),sK17_skl(X161),tptp0)))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(X162,sK16_skl(X161)),skolemize(X163,sK17_skl(X161))],[f250])).
% 56.33/12.58 fof(f253,plain,(
% 56.33/12.58 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK16_skl(X0),X0))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f251])).
% 56.33/12.58 fof(f254,plain,(
% 56.33/12.58 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK17_skl(X0),tptp3))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f251])).
% 56.33/12.58 fof(f255,plain,(
% 56.33/12.58 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK17_skl(X0),X0))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f251])).
% 56.33/12.58 fof(f256,plain,(
% 56.33/12.58 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK16_skl(X0),sK17_skl(X0),tptp0))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f251])).
% 56.33/12.58 fof(f258,plain,(
% 56.33/12.58 ~atomic(tptp0)),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f52])).
% 56.33/12.58 fof(f266,plain,(
% 56.33/12.58 ~tptp1=tptp3),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f60])).
% 56.33/12.58 fof(f269,plain,(
% 56.33/12.58 ![X164,X165]: ((~occurrence_of(X165,tptp0)|~root_occ(X164,X165))|(?[X166]: (occurrence_of(X166,tptp1)&next_subocc(X164,X166,tptp0))))),
% 56.33/12.58 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 56.33/12.58 fof(f270,plain,(
% 56.33/12.58 ![X164]: ((![X165]: (~occurrence_of(X165,tptp0)|~root_occ(X164,X165)))|(?[X166]: (occurrence_of(X166,tptp1)&next_subocc(X164,X166,tptp0))))),
% 56.33/12.58 inference(miniscoping,[status(thm)],[f269])).
% 56.33/12.58 fof(f271,plain,(
% 56.33/12.58 ![X164]: ((![X165]: (~occurrence_of(X165,tptp0)|~root_occ(X164,X165)))|(occurrence_of(sK18_skl(X164),tptp1)&next_subocc(X164,sK18_skl(X164),tptp0)))),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X166,sK18_skl(X164))],[f270])).
% 56.33/12.58 fof(f272,plain,(
% 56.33/12.58 ![X0,X1]: (~occurrence_of(X0,tptp0)|~root_occ(X1,X0)|occurrence_of(sK18_skl(X1),tptp1))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f271])).
% 56.33/12.58 fof(f273,plain,(
% 56.33/12.58 ![X0,X1]: (~occurrence_of(X0,tptp0)|~root_occ(X1,X0)|next_subocc(X1,sK18_skl(X1),tptp0))),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f271])).
% 56.33/12.58 fof(f274,plain,(
% 56.33/12.58 occurrence_of(sK19_skl,tptp0)),
% 56.33/12.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(X167,sK19_skl)],[f65])).
% 56.33/12.58 fof(f275,plain,(
% 56.33/12.58 occurrence_of(sK19_skl,tptp0)),
% 56.33/12.58 inference(cnf_transformation,[status(thm)],[f274])).
% 56.33/12.58 fof(f302,plain,(
% 56.33/12.58 root_occ(sK16_skl(sK19_skl),sK19_skl)),
% 56.33/12.58 inference(resolution,[status(thm)],[f253,f275])).
% 56.33/12.58 fof(f485,plain,(
% 56.33/12.58 atomic(tptp0)|root(sK11_skl(sK19_skl,tptp0),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f173,f275])).
% 56.33/12.58 fof(f486,plain,(
% 56.33/12.58 root(sK11_skl(sK19_skl,tptp0),tptp0)),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f485,f258])).
% 56.33/12.58 fof(f535,plain,(
% 56.33/12.58 atomic(tptp0)|subactivity_occurrence(sK11_skl(sK19_skl,tptp0),sK19_skl)),
% 56.33/12.58 inference(resolution,[status(thm)],[f174,f275])).
% 56.33/12.58 fof(f537,plain,(
% 56.33/12.58 subactivity_occurrence(sK11_skl(sK19_skl,tptp0),sK19_skl)),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f535,f258])).
% 56.33/12.58 fof(f709,plain,(
% 56.33/12.58 ![X0,X1]: (~root_occ(X0,sK19_skl)|~root_occ(X1,sK19_skl)|X0=X1)),
% 56.33/12.58 inference(resolution,[status(thm)],[f208,f275])).
% 56.33/12.58 fof(f714,plain,(
% 56.33/12.58 ![X0]: (~root_occ(X0,sK19_skl)|sK16_skl(sK19_skl)=X0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f709,f302])).
% 56.33/12.58 fof(f765,plain,(
% 56.33/12.58 ![X0]: (root_occ(X0,sK19_skl)|~subactivity_occurrence(X0,sK19_skl)|~root(X0,tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f198,f275])).
% 56.33/12.58 fof(f771,plain,(
% 56.33/12.58 ![X0]: (root_occ(sK11_skl(sK19_skl,tptp0),X0)|~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK11_skl(sK19_skl,tptp0),X0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f198,f486])).
% 56.33/12.58 fof(f955,plain,(
% 56.33/12.58 root_occ(sK11_skl(sK19_skl,tptp0),sK19_skl)|~root(sK11_skl(sK19_skl,tptp0),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f765,f537])).
% 56.33/12.58 fof(f958,plain,(
% 56.33/12.58 root_occ(sK11_skl(sK19_skl,tptp0),sK19_skl)),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f955,f486])).
% 56.33/12.58 fof(f959,plain,(
% 56.33/12.58 sK16_skl(sK19_skl)=sK11_skl(sK19_skl,tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f958,f714])).
% 56.33/12.58 fof(f1162,plain,(
% 56.33/12.58 ~occurrence_of(sK19_skl,tptp0)|occurrence_of(sK18_skl(sK16_skl(sK19_skl)),tptp1)),
% 56.33/12.58 inference(resolution,[status(thm)],[f272,f302])).
% 56.33/12.58 fof(f1163,plain,(
% 56.33/12.58 occurrence_of(sK18_skl(sK16_skl(sK19_skl)),tptp1)),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f1162,f275])).
% 56.33/12.58 fof(f1167,plain,(
% 56.33/12.58 ~occurrence_of(sK19_skl,tptp0)|next_subocc(sK16_skl(sK19_skl),sK18_skl(sK16_skl(sK19_skl)),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f273,f302])).
% 56.33/12.58 fof(f1168,plain,(
% 56.33/12.58 next_subocc(sK16_skl(sK19_skl),sK18_skl(sK16_skl(sK19_skl)),tptp0)),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f1167,f275])).
% 56.33/12.58 fof(f1209,plain,(
% 56.33/12.58 ![X0]: (~occurrence_of(sK18_skl(sK16_skl(sK19_skl)),X0)|X0=tptp1)),
% 56.33/12.58 inference(resolution,[status(thm)],[f1163,f75])).
% 56.33/12.58 fof(f1726,plain,(
% 56.33/12.58 ![X0,X1]: (~next_subocc(sK16_skl(sK19_skl),X0,tptp0)|~occurrence_of(X1,tptp0)|~subactivity_occurrence(sK18_skl(sK16_skl(sK19_skl)),X1)|~subactivity_occurrence(X0,X1)|X0=sK18_skl(sK16_skl(sK19_skl)))),
% 56.33/12.58 inference(resolution,[status(thm)],[f1168,f220])).
% 56.33/12.58 fof(f1734,plain,(
% 56.33/12.58 min_precedes(sK16_skl(sK19_skl),sK18_skl(sK16_skl(sK19_skl)),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f1168,f148])).
% 56.33/12.58 fof(f1880,plain,(
% 56.33/12.58 subactivity_occurrence(sK18_skl(sK16_skl(sK19_skl)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f1734,f166])).
% 56.33/12.58 fof(f1881,plain,(
% 56.33/12.58 subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f1734,f165])).
% 56.33/12.58 fof(f1882,plain,(
% 56.33/12.58 occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f1734,f164])).
% 56.33/12.58 fof(f1986,plain,(
% 56.33/12.58 ![X0]: (root_occ(sK16_skl(sK19_skl),X0)|~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK11_skl(sK19_skl,tptp0),X0))),
% 56.33/12.58 inference(forward_demodulation,[status(thm)],[f959,f771])).
% 56.33/12.58 fof(f1987,plain,(
% 56.33/12.58 ![X0]: (root_occ(sK16_skl(sK19_skl),X0)|~occurrence_of(X0,tptp0)|~subactivity_occurrence(sK16_skl(sK19_skl),X0))),
% 56.33/12.58 inference(forward_demodulation,[status(thm)],[f959,f1986])).
% 56.33/12.58 fof(f3058,plain,(
% 56.33/12.58 next_subocc(sK16_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f1882,f256])).
% 56.33/12.58 fof(f3061,plain,(
% 56.33/12.58 leaf_occ(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f1882,f255])).
% 56.33/12.58 fof(f3062,plain,(
% 56.33/12.58 root_occ(sK16_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f1882,f253])).
% 56.33/12.58 fof(f3086,plain,(
% 56.33/12.58 ![X0,X1]: (~root_occ(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))|~root_occ(X1,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))|X0=X1)),
% 56.33/12.58 inference(resolution,[status(thm)],[f1882,f208])).
% 56.33/12.58 fof(f4300,plain,(
% 56.33/12.58 root_occ(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))|~occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f1881,f1987])).
% 56.33/12.58 fof(f4323,plain,(
% 56.33/12.58 root_occ(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f4300,f1882])).
% 56.33/12.58 fof(f5990,plain,(
% 56.33/12.58 ![X0]: (~next_subocc(sK16_skl(sK19_skl),X0,tptp0)|~occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),tptp0)|~subactivity_occurrence(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))|X0=sK18_skl(sK16_skl(sK19_skl)))),
% 56.33/12.58 inference(resolution,[status(thm)],[f1880,f1726])).
% 56.33/12.58 fof(f6015,plain,(
% 56.33/12.58 ![X0]: (~next_subocc(sK16_skl(sK19_skl),X0,tptp0)|~subactivity_occurrence(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))|X0=sK18_skl(sK16_skl(sK19_skl)))),
% 56.33/12.58 inference(forward_subsumption_resolution,[status(thm)],[f5990,f1882])).
% 56.33/12.58 fof(f18174,plain,(
% 56.33/12.58 subactivity_occurrence(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f3061,f203])).
% 56.33/12.58 fof(f18658,plain,(
% 56.33/12.58 ![X0]: (~root_occ(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))|sK16_skl(sK19_skl)=X0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f3086,f4323])).
% 56.33/12.58 fof(f18663,plain,(
% 56.33/12.58 sK16_skl(sK19_skl)=sK16_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
% 56.33/12.58 inference(resolution,[status(thm)],[f18658,f3062])).
% 56.33/12.58 fof(f18945,plain,(
% 56.33/12.58 next_subocc(sK16_skl(sK19_skl),sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp0)),
% 56.33/12.58 inference(backward_demodulation,[status(thm)],[f18663,f3058])).
% 56.33/12.58 fof(f19116,plain,(
% 56.33/12.58 min_precedes(sK16_skl(sK19_skl),sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f18945,f148])).
% 56.33/12.58 fof(f19489,plain,(
% 56.33/12.58 occurrence_of(sK9_skl(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK16_skl(sK19_skl),tptp0),tptp0)),
% 56.33/12.58 inference(resolution,[status(thm)],[f19116,f164])).
% 56.33/12.58 fof(f22272,plain,(
% 56.33/12.58 occurrence_of(sK17_skl(sK9_skl(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK16_skl(sK19_skl),tptp0)),tptp3)),
% 56.33/12.58 inference(resolution,[status(thm)],[f19489,f254])).
% 56.33/12.58 fof(f34081,plain,(
% 56.33/12.58 ~next_subocc(sK16_skl(sK19_skl),sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp0)|sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))=sK18_skl(sK16_skl(sK19_skl))),
% 56.33/12.58 inference(resolution,[status(thm)],[f18174,f6015])).
% 56.33/12.58 fof(f34123,plain,(
% 56.33/12.58 sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))=sK18_skl(sK16_skl(sK19_skl))),
% 56.33/12.63 inference(forward_subsumption_resolution,[status(thm)],[f34081,f18945])).
% 56.33/12.63 fof(f34172,plain,(
% 56.33/12.63 occurrence_of(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp3)),
% 56.33/12.63 inference(backward_demodulation,[status(thm)],[f34123,f22272])).
% 56.33/12.63 fof(f34290,plain,(
% 56.33/12.63 occurrence_of(sK18_skl(sK16_skl(sK19_skl)),tptp3)),
% 56.33/12.63 inference(forward_demodulation,[status(thm)],[f34123,f34172])).
% 56.33/12.63 fof(f34318,plain,(
% 56.33/12.63 tptp3=tptp1),
% 56.33/12.63 inference(resolution,[status(thm)],[f34290,f1209])).
% 56.33/12.63 fof(f34432,plain,(
% 56.33/12.63 $false),
% 56.33/12.63 inference(forward_subsumption_resolution,[status(thm)],[f34318,f266])).
% 56.33/12.63 % SZS output end CNFRefutation for theBenchmark.p
% 7.36/12.67 % Elapsed time: 7.283805 seconds
% 7.36/12.67 % CPU time: 57.359720 seconds
% 7.36/12.67 % Total memory used: 376.755 MB
% 7.36/12.67 % Net memory used: 355.794 MB
%------------------------------------------------------------------------------