%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU238+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 02:22:06 PM UTC 2026
% Result : Theorem 18.39s 2.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU238+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n002.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 06:05:01 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 18.39/2.84 % Refutation found
% 18.39/2.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.39/2.84 % SZS output start CNFRefutation for theBenchmark
% 18.39/2.84 fof(f1,axiom,(
% 18.39/2.84 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f12,axiom,(
% 18.39/2.84 (! [A,B] :( proper_subset(A,B)<=> ( subset(A,B)& A != B ) ) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f20,axiom,(
% 18.39/2.84 (! [A] :( ordinal(A)=> ( ~ empty(succ(A))& epsilon_transitive(succ(A))& epsilon_connected(succ(A))& ordinal(succ(A)) ) ) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f38,axiom,(
% 18.39/2.84 (! [A,B] :( ( ordinal(A)& ordinal(B) )=> ( ordinal_subset(A,B)<=> subset(A,B) ) ) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f41,axiom,(
% 18.39/2.84 (! [A] : in(A,succ(A)) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f44,axiom,(
% 18.39/2.84 (! [A] :( epsilon_transitive(A)=> (! [B] :( ordinal(B)=> ( proper_subset(A,B)=> in(A,B) ) ) )) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f46,axiom,(
% 18.39/2.84 (! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ( in(A,B)<=> ordinal_subset(succ(A),B) ) ) )) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f48,axiom,(
% 18.39/2.84 (! [A] :( ordinal(A)=> ( being_limit_ordinal(A)<=> (! [B] :( ordinal(B)=> ( in(B,A)=> in(succ(B),A) ) ) )) ) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f49,conjecture,(
% 18.39/2.84 (! [A] :( ordinal(A)=> ( ~ ( ~ being_limit_ordinal(A)& (! [B] :( ordinal(B)=> A != succ(B) ) ))& ~ ( (? [B] :( ordinal(B)& A = succ(B) ))& being_limit_ordinal(A) ) ) ) )),
% 18.39/2.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.39/2.84 fof(f50,negated_conjecture,(
% 18.39/2.84 ~((! [A] :( ordinal(A)=> ( ~ ( ~ being_limit_ordinal(A)& (! [B] :( ordinal(B)=> A != succ(B) ) ))& ~ ( (? [B] :( ordinal(B)& A = succ(B) ))& being_limit_ordinal(A) ) ) ) ))),
% 18.39/2.84 inference(negated_conjecture,[status(cth)],[f49])).
% 18.39/2.84 fof(f56,plain,(
% 18.39/2.84 ![A,B]: (~in(A,B)|~in(B,A))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 18.39/2.84 fof(f57,plain,(
% 18.39/2.84 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f56])).
% 18.39/2.84 fof(f81,plain,(
% 18.39/2.84 ![A,B]: ((~proper_subset(A,B)|(subset(A,B)&~A=B))&(proper_subset(A,B)|(~subset(A,B)|A=B)))),
% 18.39/2.84 inference(NNF_transformation,[status(thm)],[f12])).
% 18.39/2.84 fof(f82,plain,(
% 18.39/2.84 (![A,B]: (~proper_subset(A,B)|(subset(A,B)&~A=B)))&(![A,B]: (proper_subset(A,B)|(~subset(A,B)|A=B)))),
% 18.39/2.84 inference(miniscoping,[status(thm)],[f81])).
% 18.39/2.84 fof(f85,plain,(
% 18.39/2.84 ![X0,X1]: (proper_subset(X0,X1)|~subset(X0,X1)|X0=X1)),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f82])).
% 18.39/2.84 fof(f106,plain,(
% 18.39/2.84 ![A]: (~ordinal(A)|(((~empty(succ(A))&epsilon_transitive(succ(A)))&epsilon_connected(succ(A)))&ordinal(succ(A))))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 18.39/2.84 fof(f108,plain,(
% 18.39/2.84 ![X0]: (~ordinal(X0)|epsilon_transitive(succ(X0)))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f106])).
% 18.39/2.84 fof(f110,plain,(
% 18.39/2.84 ![X0]: (~ordinal(X0)|ordinal(succ(X0)))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f106])).
% 18.39/2.84 fof(f169,plain,(
% 18.39/2.84 ![A,B]: ((~ordinal(A)|~ordinal(B))|(ordinal_subset(A,B)<=>subset(A,B)))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 18.39/2.84 fof(f170,plain,(
% 18.39/2.84 ![A,B]: ((~ordinal(A)|~ordinal(B))|((~ordinal_subset(A,B)|subset(A,B))&(ordinal_subset(A,B)|~subset(A,B))))),
% 18.39/2.84 inference(NNF_transformation,[status(thm)],[f169])).
% 18.39/2.84 fof(f171,plain,(
% 18.39/2.84 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|~ordinal_subset(X0,X1)|subset(X0,X1))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f170])).
% 18.39/2.84 fof(f178,plain,(
% 18.39/2.84 ![X0]: (in(X0,succ(X0)))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f41])).
% 18.39/2.84 fof(f182,plain,(
% 18.39/2.84 ![A]: (~epsilon_transitive(A)|(![B]: (~ordinal(B)|(~proper_subset(A,B)|in(A,B)))))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 18.39/2.84 fof(f183,plain,(
% 18.39/2.84 ![X0,X1]: (~epsilon_transitive(X0)|~ordinal(X1)|~proper_subset(X0,X1)|in(X0,X1))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f182])).
% 18.39/2.84 fof(f186,plain,(
% 18.39/2.84 ![A]: (~ordinal(A)|(![B]: (~ordinal(B)|(in(A,B)<=>ordinal_subset(succ(A),B)))))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 18.39/2.84 fof(f187,plain,(
% 18.39/2.84 ![A]: (~ordinal(A)|(![B]: (~ordinal(B)|((~in(A,B)|ordinal_subset(succ(A),B))&(in(A,B)|~ordinal_subset(succ(A),B))))))),
% 18.39/2.84 inference(NNF_transformation,[status(thm)],[f186])).
% 18.39/2.84 fof(f188,plain,(
% 18.39/2.84 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|~in(X0,X1)|ordinal_subset(succ(X0),X1))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f187])).
% 18.39/2.84 fof(f194,plain,(
% 18.39/2.84 ![A]: (~ordinal(A)|(being_limit_ordinal(A)<=>(![B]: (~ordinal(B)|(~in(B,A)|in(succ(B),A))))))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 18.39/2.84 fof(f195,plain,(
% 18.39/2.84 ![A]: (~ordinal(A)|((~being_limit_ordinal(A)|(![B]: (~ordinal(B)|(~in(B,A)|in(succ(B),A)))))&(being_limit_ordinal(A)|(?[B]: (ordinal(B)&(in(B,A)&~in(succ(B),A)))))))),
% 18.39/2.84 inference(NNF_transformation,[status(thm)],[f194])).
% 18.39/2.84 fof(f196,plain,(
% 18.39/2.84 ![A]: (~ordinal(A)|((~being_limit_ordinal(A)|(![B]: (~ordinal(B)|(~in(B,A)|in(succ(B),A)))))&(being_limit_ordinal(A)|(ordinal(sK14_skl(A))&(in(sK14_skl(A),A)&~in(succ(sK14_skl(A)),A))))))),
% 18.39/2.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(B,sK14_skl(A))],[f195])).
% 18.39/2.84 fof(f197,plain,(
% 18.39/2.84 ![X0,X1]: (~ordinal(X0)|~being_limit_ordinal(X0)|~ordinal(X1)|~in(X1,X0)|in(succ(X1),X0))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f196])).
% 18.39/2.84 fof(f198,plain,(
% 18.39/2.84 ![X0]: (~ordinal(X0)|being_limit_ordinal(X0)|ordinal(sK14_skl(X0)))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f196])).
% 18.39/2.84 fof(f199,plain,(
% 18.39/2.84 ![X0]: (~ordinal(X0)|being_limit_ordinal(X0)|in(sK14_skl(X0),X0))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f196])).
% 18.39/2.84 fof(f200,plain,(
% 18.39/2.84 ![X0]: (~ordinal(X0)|being_limit_ordinal(X0)|~in(succ(sK14_skl(X0)),X0))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f196])).
% 18.39/2.84 fof(f201,plain,(
% 18.39/2.84 (?[A]: (ordinal(A)&((~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B))))|((?[B]: (ordinal(B)&A=succ(B)))&being_limit_ordinal(A)))))),
% 18.39/2.84 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 18.39/2.84 fof(f202,definition,(
% 18.39/2.84 ![A]: (sP0_prd(A)<=>(~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B)))))),
% 18.39/2.84 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 18.39/2.84 fof(f203,plain,(
% 18.39/2.84 ?[A]: (ordinal(A)&(sP0_prd(A)|((?[B]: (ordinal(B)&A=succ(B)))&being_limit_ordinal(A))))),
% 18.39/2.84 inference(formula_renaming,[status(thm)],[f201,f202])).
% 18.39/2.84 fof(f204,plain,(
% 18.39/2.84 (ordinal(sK15_skl)&(sP0_prd(sK15_skl)|((ordinal(sK16_skl)&sK15_skl=succ(sK16_skl))&being_limit_ordinal(sK15_skl))))),
% 18.39/2.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(A,sK15_skl),skolemize(B,sK16_skl)],[f203])).
% 18.39/2.84 fof(f205,plain,(
% 18.39/2.84 ordinal(sK15_skl)),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f204])).
% 18.39/2.84 fof(f206,plain,(
% 18.39/2.84 sP0_prd(sK15_skl)|ordinal(sK16_skl)),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f204])).
% 18.39/2.84 fof(f207,plain,(
% 18.39/2.84 sP0_prd(sK15_skl)|sK15_skl=succ(sK16_skl)),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f204])).
% 18.39/2.84 fof(f208,plain,(
% 18.39/2.84 sP0_prd(sK15_skl)|being_limit_ordinal(sK15_skl)),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f204])).
% 18.39/2.84 fof(f223,plain,(
% 18.39/2.84 ![A]: ((~sP0_prd(A)|(~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B)))))&(sP0_prd(A)|(being_limit_ordinal(A)|(?[B]: (ordinal(B)&A=succ(B))))))),
% 18.39/2.84 inference(NNF_transformation,[status(thm)],[f202])).
% 18.39/2.84 fof(f224,plain,(
% 18.39/2.84 (![A]: (~sP0_prd(A)|(~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B))))))&(![A]: (sP0_prd(A)|(being_limit_ordinal(A)|(?[B]: (ordinal(B)&A=succ(B))))))),
% 18.39/2.84 inference(miniscoping,[status(thm)],[f223])).
% 18.39/2.84 fof(f225,plain,(
% 18.39/2.84 (![A]: (~sP0_prd(A)|(~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B))))))&(![A]: (sP0_prd(A)|(being_limit_ordinal(A)|(ordinal(sK17_skl(A))&A=succ(sK17_skl(A))))))),
% 18.39/2.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(B,sK17_skl(A))],[f224])).
% 18.39/2.84 fof(f226,plain,(
% 18.39/2.84 ![X0]: (~sP0_prd(X0)|~being_limit_ordinal(X0))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f225])).
% 18.39/2.84 fof(f227,plain,(
% 18.39/2.84 ![X0,X1]: (~sP0_prd(X0)|~ordinal(X1)|~X0=succ(X1))),
% 18.39/2.84 inference(cnf_transformation,[status(thm)],[f225])).
% 18.39/2.84 fof(f231,plain,(
% 18.39/2.84 ordinal(sK16_skl)|~being_limit_ordinal(sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f206,f226])).
% 18.39/2.84 fof(f233,plain,(
% 18.39/2.84 sK15_skl=succ(sK16_skl)|~being_limit_ordinal(sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f207,f226])).
% 18.39/2.84 fof(f235,plain,(
% 18.39/2.84 ![X0]: (~ordinal(X0)|~sK15_skl=succ(X0)|being_limit_ordinal(sK15_skl))),
% 18.39/2.84 inference(resolution,[status(thm)],[f227,f208])).
% 18.39/2.84 fof(f249,plain,(
% 18.39/2.84 ![X0]: (~ordinal(succ(X0))|~being_limit_ordinal(succ(X0))|~ordinal(X0)|in(succ(X0),succ(X0)))),
% 18.39/2.84 inference(resolution,[status(thm)],[f197,f178])).
% 18.39/2.84 fof(f250,plain,(
% 18.39/2.84 ![X0]: (~being_limit_ordinal(succ(X0))|~ordinal(X0)|in(succ(X0),succ(X0)))),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f249,f110])).
% 18.39/2.84 fof(f1177,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|ordinal(sK14_skl(sK15_skl))),
% 18.39/2.84 inference(resolution,[status(thm)],[f198,f205])).
% 18.39/2.84 fof(f1246,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|in(sK14_skl(sK15_skl),sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f199,f205])).
% 18.39/2.84 fof(f1254,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|epsilon_transitive(succ(sK14_skl(sK15_skl)))),
% 18.39/2.84 inference(resolution,[status(thm)],[f1177,f108])).
% 18.39/2.84 fof(f1263,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~sK15_skl=succ(sK14_skl(sK15_skl))|being_limit_ordinal(sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f1177,f235])).
% 18.39/2.84 fof(f1264,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|ordinal(succ(sK14_skl(sK15_skl)))),
% 18.39/2.84 inference(resolution,[status(thm)],[f1177,f110])).
% 18.39/2.84 fof(f1267,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~sK15_skl=succ(sK14_skl(sK15_skl))),
% 18.39/2.84 inference(duplicate_literals_removal,[status(thm)],[f1263])).
% 18.39/2.84 fof(f1312,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(sK14_skl(sK15_skl))|~ordinal(sK15_skl)|ordinal_subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f1246,f188])).
% 18.39/2.84 fof(f1317,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(sK15_skl)|ordinal_subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f1312,f198])).
% 18.39/2.84 fof(f8809,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|ordinal_subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f1317,f205])).
% 18.39/2.84 fof(f8811,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(succ(sK14_skl(sK15_skl)))|~ordinal(sK15_skl)|subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f8809,f171])).
% 18.39/2.84 fof(f8812,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(sK15_skl)|subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f8811,f1264])).
% 18.39/2.84 fof(f12384,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f8812,f205])).
% 18.39/2.84 fof(f12387,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|proper_subset(succ(sK14_skl(sK15_skl)),sK15_skl)|succ(sK14_skl(sK15_skl))=sK15_skl),
% 18.39/2.84 inference(resolution,[status(thm)],[f12384,f85])).
% 18.39/2.84 fof(f12388,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|proper_subset(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f12387,f1267])).
% 18.39/2.84 fof(f12389,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~epsilon_transitive(succ(sK14_skl(sK15_skl)))|~ordinal(sK15_skl)|in(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f12388,f183])).
% 18.39/2.84 fof(f12392,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(sK15_skl)|in(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f12389,f1254])).
% 18.39/2.84 fof(f12874,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|in(succ(sK14_skl(sK15_skl)),sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f12392,f205])).
% 18.39/2.84 fof(f12875,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(sK15_skl)|being_limit_ordinal(sK15_skl)),
% 18.39/2.84 inference(resolution,[status(thm)],[f12874,f200])).
% 18.39/2.84 fof(f12883,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)|~ordinal(sK15_skl)),
% 18.39/2.84 inference(duplicate_literals_removal,[status(thm)],[f12875])).
% 18.39/2.84 fof(f12884,plain,(
% 18.39/2.84 being_limit_ordinal(sK15_skl)),
% 18.39/2.84 inference(forward_subsumption_resolution,[status(thm)],[f12883,f205])).
% 18.39/2.84 fof(f12886,plain,(
% 18.39/2.84 sK15_skl=succ(sK16_skl)),
% 18.39/2.84 inference(backward_subsumption_resolution,[status(thm)],[f233,f12884])).
% 18.39/2.84 fof(f12887,plain,(
% 18.39/2.84 ordinal(sK16_skl)),
% 18.39/2.87 inference(backward_subsumption_resolution,[status(thm)],[f231,f12884])).
% 18.39/2.87 fof(f12918,plain,(
% 18.39/2.87 ~being_limit_ordinal(sK15_skl)|~ordinal(sK16_skl)|in(succ(sK16_skl),succ(sK16_skl))),
% 18.39/2.87 inference(paramodulation,[status(thm)],[f12886,f250])).
% 18.39/2.87 fof(f12922,plain,(
% 18.39/2.87 ~being_limit_ordinal(sK15_skl)|~ordinal(sK16_skl)|in(sK15_skl,succ(sK16_skl))),
% 18.39/2.87 inference(forward_demodulation,[status(thm)],[f12886,f12918])).
% 18.39/2.87 fof(f12923,plain,(
% 18.39/2.87 ~being_limit_ordinal(sK15_skl)|~ordinal(sK16_skl)|in(sK15_skl,sK15_skl)),
% 18.39/2.87 inference(forward_demodulation,[status(thm)],[f12886,f12922])).
% 18.39/2.87 fof(f12924,plain,(
% 18.39/2.87 ~ordinal(sK16_skl)|in(sK15_skl,sK15_skl)),
% 18.39/2.87 inference(forward_subsumption_resolution,[status(thm)],[f12923,f12884])).
% 18.39/2.87 fof(f12996,plain,(
% 18.39/2.87 in(sK15_skl,sK15_skl)),
% 18.39/2.87 inference(forward_subsumption_resolution,[status(thm)],[f12924,f12887])).
% 18.39/2.87 fof(f13002,plain,(
% 18.39/2.87 ~in(sK15_skl,sK15_skl)),
% 18.39/2.87 inference(resolution,[status(thm)],[f12996,f57])).
% 18.39/2.87 fof(f13006,plain,(
% 18.39/2.87 $false),
% 18.39/2.87 inference(forward_subsumption_resolution,[status(thm)],[f13002,f12996])).
% 18.39/2.87 % SZS output end CNFRefutation for theBenchmark.p
% 18.39/2.89 % Elapsed time: 2.436549 seconds
% 18.39/2.89 % CPU time: 18.842170 seconds
% 18.39/2.89 % Total memory used: 238.859 MB
% 18.39/2.89 % Net memory used: 230.400 MB
%------------------------------------------------------------------------------