%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM405+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:42:49 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM405+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n018.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 02:29:28 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f26,axiom,(
% 0.09/0.39 (! [A] :(? [B] :(! [C] :( in(C,B)<=> ( in(C,A)& ordinal(C) ) ) )))),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f29,axiom,(
% 0.09/0.39 (! [A] :~ (! [B] :( in(B,A)<=> ordinal(B) ) ))),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f30,conjecture,(
% 0.09/0.39 (! [A] :~ (! [B] :( ordinal(B)=> in(B,A) ) ))),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f31,negated_conjecture,(
% 0.09/0.39 ~((! [A] :~ (! [B] :( ordinal(B)=> in(B,A) ) )))),
% 0.09/0.39 inference(negated_conjecture,[status(cth)],[f30])).
% 0.09/0.39 fof(f119,plain,(
% 0.09/0.39 ![A]: ?[B]: ![C]: ((~in(C,B)|(in(C,A)&ordinal(C)))&(in(C,B)|(~in(C,A)|~ordinal(C))))),
% 0.09/0.39 inference(NNF_transformation,[status(thm)],[f26])).
% 0.09/0.39 fof(f120,plain,(
% 0.09/0.39 ![A]: ?[B]: ((![C]: (~in(C,B)|(in(C,A)&ordinal(C))))&(![C]: (in(C,B)|(~in(C,A)|~ordinal(C)))))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f119])).
% 0.09/0.39 fof(f121,plain,(
% 0.09/0.39 ![A]: ((![C]: (~in(C,sK14_skl(A))|(in(C,A)&ordinal(C))))&(![C]: (in(C,sK14_skl(A))|(~in(C,A)|~ordinal(C)))))),
% 0.09/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(B,sK14_skl(A))],[f120])).
% 0.09/0.40 fof(f123,plain,(
% 0.09/0.40 ![X0,X1]: (~in(X0,sK14_skl(X1))|ordinal(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f121])).
% 0.09/0.40 fof(f124,plain,(
% 0.09/0.40 ![X0,X1]: (in(X0,sK14_skl(X1))|~in(X0,X1)|~ordinal(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f121])).
% 0.09/0.40 fof(f129,plain,(
% 0.09/0.40 ![A]: (?[B]: (in(B,A)<~>ordinal(B)))),
% 0.09/0.40 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.09/0.40 fof(f130,plain,(
% 0.09/0.40 ![A]: ?[B]: ((in(B,A)|ordinal(B))&(~in(B,A)|~ordinal(B)))),
% 0.09/0.40 inference(NNF_transformation,[status(thm)],[f129])).
% 0.09/0.40 fof(f131,plain,(
% 0.09/0.40 ![A]: ((in(sK15_skl(A),A)|ordinal(sK15_skl(A)))&(~in(sK15_skl(A),A)|~ordinal(sK15_skl(A))))),
% 0.09/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(B,sK15_skl(A))],[f130])).
% 0.09/0.40 fof(f132,plain,(
% 0.09/0.40 ![X0]: (in(sK15_skl(X0),X0)|ordinal(sK15_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f131])).
% 0.09/0.40 fof(f133,plain,(
% 0.09/0.40 ![X0]: (~in(sK15_skl(X0),X0)|~ordinal(sK15_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f131])).
% 0.09/0.40 fof(f134,plain,(
% 0.09/0.40 (?[A]: ![B]: (~ordinal(B)|in(B,A)))),
% 0.09/0.40 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.09/0.40 fof(f135,plain,(
% 0.09/0.40 ![B]: (~ordinal(B)|in(B,sK16_skl))),
% 0.09/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f134])).
% 0.09/0.40 fof(f136,plain,(
% 0.09/0.40 ![X0]: (~ordinal(X0)|in(X0,sK16_skl))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f135])).
% 0.09/0.40 fof(f250,plain,(
% 0.09/0.40 ![X0]: (in(X0,sK14_skl(sK16_skl))|~ordinal(X0)|~ordinal(X0))),
% 0.09/0.40 inference(resolution,[status(thm)],[f124,f136])).
% 0.09/0.40 fof(f251,plain,(
% 0.09/0.40 ![X0]: (in(X0,sK14_skl(sK16_skl))|~ordinal(X0))),
% 0.09/0.40 inference(duplicate_literals_removal,[status(thm)],[f250])).
% 0.09/0.40 fof(f315,plain,(
% 0.09/0.40 ![X0]: (ordinal(sK15_skl(sK14_skl(X0)))|ordinal(sK15_skl(sK14_skl(X0))))),
% 0.09/0.40 inference(resolution,[status(thm)],[f132,f123])).
% 0.09/0.40 fof(f321,plain,(
% 0.09/0.40 ![X0]: (ordinal(sK15_skl(sK14_skl(X0))))),
% 0.09/0.40 inference(duplicate_literals_removal,[status(thm)],[f315])).
% 0.09/0.40 fof(f353,plain,(
% 0.09/0.40 ![X0]: (~in(sK15_skl(sK14_skl(X0)),sK14_skl(X0)))),
% 0.09/0.40 inference(resolution,[status(thm)],[f321,f133])).
% 0.09/0.40 fof(f354,plain,(
% 0.09/0.40 ![X0]: (in(sK15_skl(sK14_skl(X0)),sK14_skl(sK16_skl)))),
% 0.09/0.40 inference(resolution,[status(thm)],[f321,f251])).
% 0.09/0.40 fof(f367,plain,(
% 0.09/0.40 $false),
% 0.09/0.40 inference(resolution,[status(thm)],[f354,f353])).
% 0.09/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.066869 seconds
% 0.14/0.42 % CPU time: 0.107711 seconds
% 0.14/0.42 % Total memory used: 13.247 MB
% 0.14/0.42 % Net memory used: 13.214 MB
%------------------------------------------------------------------------------