%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU234+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:05 PM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU234+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 06:04:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.41 fof(f6,axiom,(
% 0.13/0.41 (! [A] :( ( epsilon_transitive(A)& epsilon_connected(A) )=> ordinal(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f8,axiom,(
% 0.13/0.41 (! [A] :( epsilon_transitive(A)<=> (! [B] :( in(B,A)=> subset(B,A) ) )) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f9,axiom,(
% 0.13/0.41 (! [A] :( epsilon_connected(A)<=> (! [B,C] :~ ( in(B,A)& in(C,A)& ~ in(B,C)& B != C& ~ in(C,B) ) )) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f33,axiom,(
% 0.13/0.41 (! [A] :( ordinal(A)=> (! [B] :( ordinal(B)=> ~ ( ~ in(A,B)& A != B& ~ in(B,A) ) ) )) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f35,conjecture,(
% 0.13/0.41 (! [A] :( (! [B] :( in(B,A)=> ( ordinal(B)& subset(B,A) ) ))=> ordinal(A) ) )),
% 0.13/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f36,negated_conjecture,(
% 0.13/0.41 ~((! [A] :( (! [B] :( in(B,A)=> ( ordinal(B)& subset(B,A) ) ))=> ordinal(A) ) ))),
% 0.13/0.41 inference(negated_conjecture,[status(cth)],[f35])).
% 0.13/0.41 fof(f56,plain,(
% 0.13/0.41 ![A]: ((~epsilon_transitive(A)|~epsilon_connected(A))|ordinal(A))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.13/0.41 fof(f57,plain,(
% 0.13/0.41 ![X0]: (~epsilon_transitive(X0)|~epsilon_connected(X0)|ordinal(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.41 fof(f62,plain,(
% 0.13/0.41 ![A]: (epsilon_transitive(A)<=>(![B]: (~in(B,A)|subset(B,A))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.13/0.41 fof(f63,plain,(
% 0.13/0.41 ![A]: ((~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A))))&(epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f62])).
% 0.13/0.41 fof(f64,plain,(
% 0.13/0.41 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f63])).
% 0.13/0.41 fof(f65,plain,(
% 0.13/0.41 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(in(sK0_skl(A),A)&~subset(sK0_skl(A),A))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f64])).
% 0.13/0.41 fof(f67,plain,(
% 0.13/0.41 ![X0]: (epsilon_transitive(X0)|in(sK0_skl(X0),X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f65])).
% 0.13/0.41 fof(f68,plain,(
% 0.13/0.41 ![X0]: (epsilon_transitive(X0)|~subset(sK0_skl(X0),X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f65])).
% 0.13/0.41 fof(f69,plain,(
% 0.13/0.41 ![A]: (epsilon_connected(A)<=>(![B,C]: ((((~in(B,A)|~in(C,A))|in(B,C))|B=C)|in(C,B))))),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.13/0.41 fof(f70,plain,(
% 0.13/0.41 ![A]: ((~epsilon_connected(A)|(![B,C]: ((((~in(B,A)|~in(C,A))|in(B,C))|B=C)|in(C,B))))&(epsilon_connected(A)|(?[B,C]: ((((in(B,A)&in(C,A))&~in(B,C))&~B=C)&~in(C,B)))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f69])).
% 0.13/0.41 fof(f71,plain,(
% 0.13/0.41 (![A]: (~epsilon_connected(A)|(![B,C]: ((((~in(B,A)|~in(C,A))|in(B,C))|B=C)|in(C,B)))))&(![A]: (epsilon_connected(A)|(?[B,C]: ((((in(B,A)&in(C,A))&~in(B,C))&~B=C)&~in(C,B)))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f70])).
% 0.13/0.41 fof(f72,plain,(
% 0.13/0.41 (![A]: (~epsilon_connected(A)|(![B,C]: ((((~in(B,A)|~in(C,A))|in(B,C))|B=C)|in(C,B)))))&(![A]: (epsilon_connected(A)|((((in(sK1_skl(A),A)&in(sK2_skl(A),A))&~in(sK1_skl(A),sK2_skl(A)))&~sK1_skl(A)=sK2_skl(A))&~in(sK2_skl(A),sK1_skl(A)))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B,sK1_skl(A)),skolemize(C,sK2_skl(A))],[f71])).
% 0.13/0.41 fof(f74,plain,(
% 0.13/0.41 ![X0]: (epsilon_connected(X0)|in(sK1_skl(X0),X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.41 fof(f75,plain,(
% 0.13/0.41 ![X0]: (epsilon_connected(X0)|in(sK2_skl(X0),X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.41 fof(f76,plain,(
% 0.13/0.41 ![X0]: (epsilon_connected(X0)|~in(sK1_skl(X0),sK2_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.41 fof(f77,plain,(
% 0.13/0.41 ![X0]: (epsilon_connected(X0)|~sK1_skl(X0)=sK2_skl(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.41 fof(f78,plain,(
% 0.13/0.41 ![X0]: (epsilon_connected(X0)|~in(sK2_skl(X0),sK1_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.42 fof(f149,plain,(
% 0.13/0.42 ![A]: (~ordinal(A)|(![B]: (~ordinal(B)|((in(A,B)|A=B)|in(B,A)))))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.13/0.42 fof(f150,plain,(
% 0.13/0.42 ![X0,X1]: (~ordinal(X0)|~ordinal(X1)|in(X0,X1)|X0=X1|in(X1,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f149])).
% 0.13/0.42 fof(f153,plain,(
% 0.13/0.42 (?[A]: ((![B]: (~in(B,A)|(ordinal(B)&subset(B,A))))&~ordinal(A)))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.13/0.42 fof(f154,plain,(
% 0.13/0.42 ((![B]: (~in(B,sK16_skl)|(ordinal(B)&subset(B,sK16_skl))))&~ordinal(sK16_skl))),
% 0.13/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f153])).
% 0.13/0.42 fof(f155,plain,(
% 0.13/0.42 ![X0]: (~in(X0,sK16_skl)|ordinal(X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f154])).
% 0.13/0.42 fof(f156,plain,(
% 0.13/0.42 ![X0]: (~in(X0,sK16_skl)|subset(X0,sK16_skl))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f154])).
% 0.13/0.42 fof(f157,plain,(
% 0.13/0.42 ~ordinal(sK16_skl)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f154])).
% 0.13/0.42 fof(f198,plain,(
% 0.13/0.42 ~epsilon_transitive(sK16_skl)|~epsilon_connected(sK16_skl)),
% 0.13/0.42 inference(resolution,[status(thm)],[f57,f157])).
% 0.13/0.42 fof(f209,plain,(
% 0.13/0.42 epsilon_transitive(sK16_skl)|subset(sK0_skl(sK16_skl),sK16_skl)),
% 0.13/0.42 inference(resolution,[status(thm)],[f67,f156])).
% 0.13/0.42 fof(f212,plain,(
% 0.13/0.42 ~epsilon_connected(sK16_skl)),
% 0.13/0.42 inference(backward_subsumption_resolution,[status(thm)],[f198,f213])).
% 0.13/0.42 fof(f213,plain,(
% 0.13/0.42 epsilon_transitive(sK16_skl)),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f209,f68])).
% 0.13/0.42 fof(f215,plain,(
% 0.13/0.42 epsilon_connected(sK16_skl)|ordinal(sK1_skl(sK16_skl))),
% 0.13/0.42 inference(resolution,[status(thm)],[f74,f155])).
% 0.13/0.42 fof(f218,plain,(
% 0.13/0.42 ordinal(sK1_skl(sK16_skl))),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f215,f212])).
% 0.13/0.42 fof(f220,plain,(
% 0.13/0.42 epsilon_connected(sK16_skl)|ordinal(sK2_skl(sK16_skl))),
% 0.13/0.42 inference(resolution,[status(thm)],[f75,f155])).
% 0.13/0.42 fof(f223,plain,(
% 0.13/0.42 ordinal(sK2_skl(sK16_skl))),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f220,f212])).
% 0.13/0.42 fof(f228,plain,(
% 0.13/0.42 ![X0]: (~ordinal(X0)|in(X0,sK1_skl(sK16_skl))|X0=sK1_skl(sK16_skl)|in(sK1_skl(sK16_skl),X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f218,f150])).
% 0.13/0.42 fof(f410,plain,(
% 0.13/0.42 in(sK2_skl(sK16_skl),sK1_skl(sK16_skl))|sK2_skl(sK16_skl)=sK1_skl(sK16_skl)|in(sK1_skl(sK16_skl),sK2_skl(sK16_skl))),
% 0.13/0.42 inference(resolution,[status(thm)],[f228,f223])).
% 0.13/0.42 fof(f473,plain,(
% 0.13/0.42 sK2_skl(sK16_skl)=sK1_skl(sK16_skl)|in(sK1_skl(sK16_skl),sK2_skl(sK16_skl))|epsilon_connected(sK16_skl)),
% 0.13/0.42 inference(resolution,[status(thm)],[f410,f78])).
% 0.13/0.42 fof(f476,plain,(
% 0.13/0.42 in(sK1_skl(sK16_skl),sK2_skl(sK16_skl))|epsilon_connected(sK16_skl)),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f473,f77])).
% 0.13/0.42 fof(f556,plain,(
% 0.13/0.42 epsilon_connected(sK16_skl)|epsilon_connected(sK16_skl)),
% 0.13/0.42 inference(resolution,[status(thm)],[f476,f76])).
% 0.13/0.42 fof(f561,plain,(
% 0.13/0.42 epsilon_connected(sK16_skl)),
% 0.13/0.42 inference(duplicate_literals_removal,[status(thm)],[f556])).
% 0.13/0.42 fof(f562,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f561,f212])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.069199 seconds
% 0.13/0.43 % CPU time: 0.315570 seconds
% 0.13/0.43 % Total memory used: 85.487 MB
% 0.13/0.43 % Net memory used: 85.126 MB
%------------------------------------------------------------------------------