%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU238+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 5.07s 1.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU238+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n015.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 06:05:35 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 5.07/1.45 % Refutation found
% 5.07/1.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.07/1.45 % SZS output start CNFRefutation for theBenchmark
% 5.07/1.45 fof(f1,axiom,(
% 5.07/1.45 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f12,axiom,(
% 5.07/1.45 (! [A,B] :( proper_subset(A,B)<=> ( subset(A,B)& A != B ) ) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f26,axiom,(
% 5.07/1.45 (! [A] :( ordinal(A)=> ( ~ empty(succ(A))& epsilon_transitive(succ(A))& epsilon_connected(succ(A))& ordinal(succ(A)) ) ) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f43,axiom,(
% 5.07/1.45 (! [A,B] :( ( ordinal(A)& ordinal(B) )=> ( ordinal_subset(A,B)<=> subset(A,B) ) ) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f46,axiom,(
% 5.07/1.45 (! [A] : in(A,succ(A)) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f49,axiom,(
% 5.07/1.45 (! [A] :( epsilon_transitive(A)=> (! [B] :( ordinal(B)=> ( proper_subset(A,B)=> in(A,B) ) ) )) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f51,axiom,(
% 5.07/1.45 (! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ( in(A,B)<=> ordinal_subset(succ(A),B) ) ) )) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f53,axiom,(
% 5.07/1.45 (! [A] :( ordinal(A)=> ( being_limit_ordinal(A)<=> (! [B] :( ordinal(B)=> ( in(B,A)=> in(succ(B),A) ) ) )) ) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f54,conjecture,(
% 5.07/1.45 (! [A] :( ordinal(A)=> ( ~ ( ~ being_limit_ordinal(A)& (! [B] :( ordinal(B)=> A != succ(B) ) ))& ~ ( (? [B] :( ordinal(B)& A = succ(B) ))& being_limit_ordinal(A) ) ) ) )),
% 5.07/1.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.07/1.45 fof(f55,negated_conjecture,(
% 5.07/1.45 ~((! [A] :( ordinal(A)=> ( ~ ( ~ being_limit_ordinal(A)& (! [B] :( ordinal(B)=> A != succ(B) ) ))& ~ ( (? [B] :( ordinal(B)& A = succ(B) ))& being_limit_ordinal(A) ) ) ) ))),
% 5.07/1.45 inference(negated_conjecture,[status(cth)],[f54])).
% 5.07/1.45 fof(f61,plain,(
% 5.07/1.45 ![A,B]: (~in(A,B)|~in(B,A))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 5.07/1.45 fof(f62,plain,(
% 5.07/1.45 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f61])).
% 5.07/1.45 fof(f86,plain,(
% 5.07/1.45 ![A,B]: ((~proper_subset(A,B)|(subset(A,B)&~A=B))&(proper_subset(A,B)|(~subset(A,B)|A=B)))),
% 5.07/1.45 inference(NNF_transformation,[status(thm)],[f12])).
% 5.07/1.45 fof(f87,plain,(
% 5.07/1.45 (![A,B]: (~proper_subset(A,B)|(subset(A,B)&~A=B)))&(![A,B]: (proper_subset(A,B)|(~subset(A,B)|A=B)))),
% 5.07/1.45 inference(miniscoping,[status(thm)],[f86])).
% 5.07/1.45 fof(f90,plain,(
% 5.07/1.45 ![X0,X1]: (proper_subset(X0,X1)|~subset(X0,X1)|X0=X1)),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f87])).
% 5.07/1.45 fof(f111,plain,(
% 5.07/1.45 ![A]: (~ordinal(A)|(((~empty(succ(A))&epsilon_transitive(succ(A)))&epsilon_connected(succ(A)))&ordinal(succ(A))))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 5.07/1.45 fof(f113,plain,(
% 5.07/1.45 ![X0]: (~ordinal(X0)|epsilon_transitive(succ(X0)))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f111])).
% 5.07/1.45 fof(f115,plain,(
% 5.07/1.45 ![X0]: (~ordinal(X0)|ordinal(succ(X0)))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f111])).
% 5.07/1.45 fof(f170,plain,(
% 5.07/1.45 ![A,B]: ((~ordinal(A)|~ordinal(B))|(ordinal_subset(A,B)<=>subset(A,B)))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 5.07/1.45 fof(f171,plain,(
% 5.07/1.45 ![A,B]: ((~ordinal(A)|~ordinal(B))|((~ordinal_subset(A,B)|subset(A,B))&(ordinal_subset(A,B)|~subset(A,B))))),
% 5.07/1.45 inference(NNF_transformation,[status(thm)],[f170])).
% 5.07/1.45 fof(f172,plain,(
% 5.07/1.45 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|~ordinal_subset(X0,X1)|subset(X0,X1))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f171])).
% 5.07/1.45 fof(f179,plain,(
% 5.07/1.45 ![X0]: (in(X0,succ(X0)))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f46])).
% 5.07/1.45 fof(f183,plain,(
% 5.07/1.45 ![A]: (~epsilon_transitive(A)|(![B]: (~ordinal(B)|(~proper_subset(A,B)|in(A,B)))))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 5.07/1.45 fof(f184,plain,(
% 5.07/1.45 ![X0,X1]: (~epsilon_transitive(X0)|~ordinal(X1)|~proper_subset(X0,X1)|in(X0,X1))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f183])).
% 5.07/1.45 fof(f187,plain,(
% 5.07/1.45 ![A]: (~ordinal(A)|(![B]: (~ordinal(B)|(in(A,B)<=>ordinal_subset(succ(A),B)))))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 5.07/1.45 fof(f188,plain,(
% 5.07/1.45 ![A]: (~ordinal(A)|(![B]: (~ordinal(B)|((~in(A,B)|ordinal_subset(succ(A),B))&(in(A,B)|~ordinal_subset(succ(A),B))))))),
% 5.07/1.45 inference(NNF_transformation,[status(thm)],[f187])).
% 5.07/1.45 fof(f189,plain,(
% 5.07/1.45 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|~in(X0,X1)|ordinal_subset(succ(X0),X1))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f188])).
% 5.07/1.45 fof(f195,plain,(
% 5.07/1.45 ![A]: (~ordinal(A)|(being_limit_ordinal(A)<=>(![B]: (~ordinal(B)|(~in(B,A)|in(succ(B),A))))))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 5.07/1.45 fof(f196,plain,(
% 5.07/1.45 ![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)))))))),
% 5.07/1.45 inference(NNF_transformation,[status(thm)],[f195])).
% 5.07/1.45 fof(f197,plain,(
% 5.07/1.45 ![A]: (~ordinal(A)|((~being_limit_ordinal(A)|(![B]: (~ordinal(B)|(~in(B,A)|in(succ(B),A)))))&(being_limit_ordinal(A)|(ordinal(sK13_skl(A))&(in(sK13_skl(A),A)&~in(succ(sK13_skl(A)),A))))))),
% 5.07/1.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f196])).
% 5.07/1.45 fof(f198,plain,(
% 5.07/1.45 ![X0,X1]: (~ordinal(X0)|~being_limit_ordinal(X0)|~ordinal(X1)|~in(X1,X0)|in(succ(X1),X0))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f197])).
% 5.07/1.45 fof(f199,plain,(
% 5.07/1.45 ![X0]: (~ordinal(X0)|being_limit_ordinal(X0)|ordinal(sK13_skl(X0)))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f197])).
% 5.07/1.45 fof(f200,plain,(
% 5.07/1.45 ![X0]: (~ordinal(X0)|being_limit_ordinal(X0)|in(sK13_skl(X0),X0))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f197])).
% 5.07/1.45 fof(f201,plain,(
% 5.07/1.45 ![X0]: (~ordinal(X0)|being_limit_ordinal(X0)|~in(succ(sK13_skl(X0)),X0))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f197])).
% 5.07/1.45 fof(f202,plain,(
% 5.07/1.45 (?[A]: (ordinal(A)&((~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B))))|((?[B]: (ordinal(B)&A=succ(B)))&being_limit_ordinal(A)))))),
% 5.07/1.45 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 5.07/1.45 fof(f203,definition,(
% 5.07/1.45 ![A]: (sP0_prd(A)<=>(~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B)))))),
% 5.07/1.45 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 5.07/1.45 fof(f204,plain,(
% 5.07/1.45 ?[A]: (ordinal(A)&(sP0_prd(A)|((?[B]: (ordinal(B)&A=succ(B)))&being_limit_ordinal(A))))),
% 5.07/1.45 inference(formula_renaming,[status(thm)],[f202,f203])).
% 5.07/1.45 fof(f205,plain,(
% 5.07/1.45 (ordinal(sK14_skl)&(sP0_prd(sK14_skl)|((ordinal(sK15_skl)&sK14_skl=succ(sK15_skl))&being_limit_ordinal(sK14_skl))))),
% 5.07/1.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(A,sK14_skl),skolemize(B,sK15_skl)],[f204])).
% 5.07/1.45 fof(f206,plain,(
% 5.07/1.45 ordinal(sK14_skl)),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f205])).
% 5.07/1.45 fof(f207,plain,(
% 5.07/1.45 sP0_prd(sK14_skl)|ordinal(sK15_skl)),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f205])).
% 5.07/1.45 fof(f208,plain,(
% 5.07/1.45 sP0_prd(sK14_skl)|sK14_skl=succ(sK15_skl)),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f205])).
% 5.07/1.45 fof(f209,plain,(
% 5.07/1.45 sP0_prd(sK14_skl)|being_limit_ordinal(sK14_skl)),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f205])).
% 5.07/1.45 fof(f224,plain,(
% 5.07/1.45 ![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))))))),
% 5.07/1.45 inference(NNF_transformation,[status(thm)],[f203])).
% 5.07/1.45 fof(f225,plain,(
% 5.07/1.45 (![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))))))),
% 5.07/1.45 inference(miniscoping,[status(thm)],[f224])).
% 5.07/1.45 fof(f226,plain,(
% 5.07/1.45 (![A]: (~sP0_prd(A)|(~being_limit_ordinal(A)&(![B]: (~ordinal(B)|~A=succ(B))))))&(![A]: (sP0_prd(A)|(being_limit_ordinal(A)|(ordinal(sK16_skl(A))&A=succ(sK16_skl(A))))))),
% 5.07/1.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(B,sK16_skl(A))],[f225])).
% 5.07/1.45 fof(f227,plain,(
% 5.07/1.45 ![X0]: (~sP0_prd(X0)|~being_limit_ordinal(X0))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f226])).
% 5.07/1.45 fof(f228,plain,(
% 5.07/1.45 ![X0,X1]: (~sP0_prd(X0)|~ordinal(X1)|~X0=succ(X1))),
% 5.07/1.45 inference(cnf_transformation,[status(thm)],[f226])).
% 5.07/1.45 fof(f232,plain,(
% 5.07/1.45 ordinal(sK15_skl)|~being_limit_ordinal(sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f207,f227])).
% 5.07/1.45 fof(f234,plain,(
% 5.07/1.45 sK14_skl=succ(sK15_skl)|~being_limit_ordinal(sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f208,f227])).
% 5.07/1.45 fof(f236,plain,(
% 5.07/1.45 ![X0]: (~ordinal(X0)|~sK14_skl=succ(X0)|being_limit_ordinal(sK14_skl))),
% 5.07/1.45 inference(resolution,[status(thm)],[f228,f209])).
% 5.07/1.45 fof(f250,plain,(
% 5.07/1.45 ![X0]: (~ordinal(succ(X0))|~being_limit_ordinal(succ(X0))|~ordinal(X0)|in(succ(X0),succ(X0)))),
% 5.07/1.45 inference(resolution,[status(thm)],[f198,f179])).
% 5.07/1.45 fof(f251,plain,(
% 5.07/1.45 ![X0]: (~being_limit_ordinal(succ(X0))|~ordinal(X0)|in(succ(X0),succ(X0)))),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f250,f115])).
% 5.07/1.45 fof(f1116,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|ordinal(sK13_skl(sK14_skl))),
% 5.07/1.45 inference(resolution,[status(thm)],[f199,f206])).
% 5.07/1.45 fof(f1166,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|epsilon_transitive(succ(sK13_skl(sK14_skl)))),
% 5.07/1.45 inference(resolution,[status(thm)],[f1116,f113])).
% 5.07/1.45 fof(f1175,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~sK14_skl=succ(sK13_skl(sK14_skl))|being_limit_ordinal(sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f1116,f236])).
% 5.07/1.45 fof(f1176,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|ordinal(succ(sK13_skl(sK14_skl)))),
% 5.07/1.45 inference(resolution,[status(thm)],[f1116,f115])).
% 5.07/1.45 fof(f1179,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~sK14_skl=succ(sK13_skl(sK14_skl))),
% 5.07/1.45 inference(duplicate_literals_removal,[status(thm)],[f1175])).
% 5.07/1.45 fof(f1207,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|in(sK13_skl(sK14_skl),sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f200,f206])).
% 5.07/1.45 fof(f1268,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(sK13_skl(sK14_skl))|~ordinal(sK14_skl)|ordinal_subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f1207,f189])).
% 5.07/1.45 fof(f1273,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(sK14_skl)|ordinal_subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f1268,f199])).
% 5.07/1.45 fof(f6695,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|ordinal_subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f1273,f206])).
% 5.07/1.45 fof(f6697,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(succ(sK13_skl(sK14_skl)))|~ordinal(sK14_skl)|subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f6695,f172])).
% 5.07/1.45 fof(f6698,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(sK14_skl)|subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f6697,f1176])).
% 5.07/1.45 fof(f9384,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f6698,f206])).
% 5.07/1.45 fof(f9387,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|proper_subset(succ(sK13_skl(sK14_skl)),sK14_skl)|succ(sK13_skl(sK14_skl))=sK14_skl),
% 5.07/1.45 inference(resolution,[status(thm)],[f9384,f90])).
% 5.07/1.45 fof(f9388,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|proper_subset(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f9387,f1179])).
% 5.07/1.45 fof(f9389,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~epsilon_transitive(succ(sK13_skl(sK14_skl)))|~ordinal(sK14_skl)|in(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f9388,f184])).
% 5.07/1.45 fof(f9392,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(sK14_skl)|in(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f9389,f1166])).
% 5.07/1.45 fof(f9532,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|in(succ(sK13_skl(sK14_skl)),sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f9392,f206])).
% 5.07/1.45 fof(f9533,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(sK14_skl)|being_limit_ordinal(sK14_skl)),
% 5.07/1.45 inference(resolution,[status(thm)],[f9532,f201])).
% 5.07/1.45 fof(f9541,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)|~ordinal(sK14_skl)),
% 5.07/1.45 inference(duplicate_literals_removal,[status(thm)],[f9533])).
% 5.07/1.45 fof(f9542,plain,(
% 5.07/1.45 being_limit_ordinal(sK14_skl)),
% 5.07/1.45 inference(forward_subsumption_resolution,[status(thm)],[f9541,f206])).
% 5.07/1.45 fof(f9544,plain,(
% 5.07/1.45 sK14_skl=succ(sK15_skl)),
% 5.07/1.45 inference(backward_subsumption_resolution,[status(thm)],[f234,f9542])).
% 5.07/1.45 fof(f9545,plain,(
% 5.07/1.45 ordinal(sK15_skl)),
% 5.07/1.45 inference(backward_subsumption_resolution,[status(thm)],[f232,f9542])).
% 7.36/1.46 fof(f9604,plain,(
% 7.36/1.46 ~being_limit_ordinal(sK14_skl)|~ordinal(sK15_skl)|in(succ(sK15_skl),succ(sK15_skl))),
% 7.36/1.46 inference(paramodulation,[status(thm)],[f9544,f251])).
% 7.36/1.46 fof(f9609,plain,(
% 7.36/1.46 ~being_limit_ordinal(sK14_skl)|~ordinal(sK15_skl)|in(sK14_skl,succ(sK15_skl))),
% 7.36/1.46 inference(forward_demodulation,[status(thm)],[f9544,f9604])).
% 7.36/1.46 fof(f9610,plain,(
% 7.36/1.46 ~being_limit_ordinal(sK14_skl)|~ordinal(sK15_skl)|in(sK14_skl,sK14_skl)),
% 7.36/1.46 inference(forward_demodulation,[status(thm)],[f9544,f9609])).
% 7.36/1.46 fof(f9611,plain,(
% 7.36/1.46 ~ordinal(sK15_skl)|in(sK14_skl,sK14_skl)),
% 7.36/1.46 inference(forward_subsumption_resolution,[status(thm)],[f9610,f9542])).
% 7.36/1.46 fof(f9683,plain,(
% 7.36/1.46 in(sK14_skl,sK14_skl)),
% 7.36/1.46 inference(forward_subsumption_resolution,[status(thm)],[f9611,f9545])).
% 7.36/1.46 fof(f9689,plain,(
% 7.36/1.46 ~in(sK14_skl,sK14_skl)),
% 7.36/1.46 inference(resolution,[status(thm)],[f9683,f62])).
% 7.36/1.46 fof(f9693,plain,(
% 7.36/1.46 $false),
% 7.36/1.46 inference(forward_subsumption_resolution,[status(thm)],[f9689,f9683])).
% 7.36/1.46 % SZS output end CNFRefutation for theBenchmark.p
% 7.36/1.49 % Elapsed time: 1.031801 seconds
% 7.36/1.49 % CPU time: 7.822809 seconds
% 7.36/1.49 % Total memory used: 179.753 MB
% 7.36/1.49 % Net memory used: 174.368 MB
%------------------------------------------------------------------------------