%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU280+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 : 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 02:22:12 PM UTC 2026
% Result : Theorem 0.16s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU280+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.16/0.42 % Computer : n020.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 06:07:48 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.46 % Refutation found
% 0.16/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.46 fof(f1,conjecture,(
% 0.16/0.46 (! [A] :(? [B] :(! [C] :( in(C,B)<=> ( in(C,A)& ordinal(C) ) ) )))),
% 0.16/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.46 fof(f2,negated_conjecture,(
% 0.16/0.46 ~((! [A] :(? [B] :(! [C] :( in(C,B)<=> ( in(C,A)& ordinal(C) ) ) ))))),
% 0.16/0.46 inference(negated_conjecture,[status(cth)],[f1])).
% 0.16/0.46 fof(f7,axiom,(
% 0.16/0.46 (! [A] :( (! [B,C,D] :( ( B = C& ordinal(C)& B = D& ordinal(D) )=> C = D ))=> (? [B] :(! [C] :( in(C,B)<=> (? [D] :( in(D,A)& D = C& ordinal(C) ) )) ))) )),
% 0.16/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.46 fof(f8,plain,(
% 0.16/0.46 (?[A]: ![B]: ?[C]: (in(C,B)<~>(in(C,A)&ordinal(C))))),
% 0.16/0.46 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/0.46 fof(f9,plain,(
% 0.16/0.46 ?[A]: ![B]: ?[C]: ((in(C,B)|(in(C,A)&ordinal(C)))&(~in(C,B)|(~in(C,A)|~ordinal(C))))),
% 0.16/0.46 inference(NNF_transformation,[status(thm)],[f8])).
% 0.16/0.46 fof(f10,plain,(
% 0.16/0.46 ![B]: ((in(sK1_skl(B),B)|(in(sK1_skl(B),sK0_skl)&ordinal(sK1_skl(B))))&(~in(sK1_skl(B),B)|(~in(sK1_skl(B),sK0_skl)|~ordinal(sK1_skl(B)))))),
% 0.16/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(C,sK1_skl(B))],[f9])).
% 0.16/0.46 fof(f11,plain,(
% 0.16/0.46 ![X0]: (in(sK1_skl(X0),X0)|in(sK1_skl(X0),sK0_skl))),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.16/0.46 fof(f12,plain,(
% 0.16/0.46 ![X0]: (in(sK1_skl(X0),X0)|ordinal(sK1_skl(X0)))),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.16/0.46 fof(f13,plain,(
% 0.16/0.46 ![X0]: (~in(sK1_skl(X0),X0)|~in(sK1_skl(X0),sK0_skl)|~ordinal(sK1_skl(X0)))),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f10])).
% 0.16/0.46 fof(f25,plain,(
% 0.16/0.46 ![A]: ((?[B,C,D]: ((((B=C&ordinal(C))&B=D)&ordinal(D))&~C=D))|(?[B]: ![C]: (in(C,B)<=>(?[D]: ((in(D,A)&D=C)&ordinal(C))))))),
% 0.16/0.46 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.16/0.46 fof(f26,definition,(
% 0.16/0.46 ![B,C,D]: (sP0_prd(D,C,B)<=>((((B=C&ordinal(C))&B=D)&ordinal(D))&~C=D))),
% 0.16/0.46 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.16/0.46 fof(f27,plain,(
% 0.16/0.46 ![A]: ((?[B,C,D]: sP0_prd(D,C,B))|(?[B]: ![C]: (in(C,B)<=>(?[D]: ((in(D,A)&D=C)&ordinal(C))))))),
% 0.16/0.46 inference(formula_renaming,[status(thm)],[f25,f26])).
% 0.16/0.46 fof(f28,plain,(
% 0.16/0.46 ![A]: ((?[B,C,D]: sP0_prd(D,C,B))|(?[B]: ![C]: ((~in(C,B)|(?[D]: ((in(D,A)&D=C)&ordinal(C))))&(in(C,B)|(![D]: ((~in(D,A)|~D=C)|~ordinal(C)))))))),
% 0.16/0.46 inference(NNF_transformation,[status(thm)],[f27])).
% 0.16/0.46 fof(f29,plain,(
% 0.16/0.46 (?[B,C,D]: sP0_prd(D,C,B))|(![A]: ?[B]: ((![C]: (~in(C,B)|((?[D]: (in(D,A)&D=C))&ordinal(C))))&(![C]: (in(C,B)|((![D]: (~in(D,A)|~D=C))|~ordinal(C))))))),
% 0.16/0.46 inference(miniscoping,[status(thm)],[f28])).
% 0.16/0.46 fof(f30,plain,(
% 0.16/0.46 sP0_prd(sK5_skl,sK4_skl,sK3_skl)|(![A]: ((![C]: (~in(C,sK6_skl(A))|((in(sK7_skl(C,A),A)&sK7_skl(C,A)=C)&ordinal(C))))&(![C]: (in(C,sK6_skl(A))|((![D]: (~in(D,A)|~D=C))|~ordinal(C))))))),
% 0.16/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(B,sK3_skl),skolemize(C,sK4_skl),skolemize(D,sK5_skl),skolemize(B,sK6_skl(A)),skolemize(D,sK7_skl(C,A))],[f29])).
% 0.16/0.46 fof(f31,plain,(
% 0.16/0.46 ![X0,X1]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl)|~in(X0,sK6_skl(X1))|in(sK7_skl(X0,X1),X1))),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f30])).
% 0.16/0.46 fof(f32,plain,(
% 0.16/0.46 ![X0,X1]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl)|~in(X0,sK6_skl(X1))|sK7_skl(X0,X1)=X0)),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f30])).
% 0.16/0.46 fof(f33,plain,(
% 0.16/0.46 ![X0,X1]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl)|~in(X0,sK6_skl(X1))|ordinal(X0))),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f30])).
% 0.16/0.46 fof(f34,plain,(
% 0.16/0.46 ![X0,X1,X2]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl)|in(X0,sK6_skl(X1))|~in(X2,X1)|~X2=X0|~ordinal(X0))),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f30])).
% 0.16/0.46 fof(f35,plain,(
% 0.16/0.46 ![B,C,D]: ((~sP0_prd(D,C,B)|((((B=C&ordinal(C))&B=D)&ordinal(D))&~C=D))&(sP0_prd(D,C,B)|((((~B=C|~ordinal(C))|~B=D)|~ordinal(D))|C=D)))),
% 0.16/0.46 inference(NNF_transformation,[status(thm)],[f26])).
% 0.16/0.46 fof(f36,plain,(
% 0.16/0.46 (![B,C,D]: (~sP0_prd(D,C,B)|((((B=C&ordinal(C))&B=D)&ordinal(D))&~C=D)))&(![B,C,D]: (sP0_prd(D,C,B)|((((~B=C|~ordinal(C))|~B=D)|~ordinal(D))|C=D)))),
% 0.16/0.46 inference(miniscoping,[status(thm)],[f35])).
% 0.16/0.47 fof(f37,plain,(
% 0.16/0.47 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|X2=X1)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f36])).
% 0.16/0.47 fof(f39,plain,(
% 0.16/0.47 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|X2=X0)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f36])).
% 0.16/0.47 fof(f41,plain,(
% 0.16/0.47 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~X1=X0)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f36])).
% 0.16/0.47 fof(f43,definition,(
% 0.16/0.47 sQ0_spl <=> (sP0_prd(sK5_skl,sK4_skl,sK3_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f44,plain,(
% 0.16/0.47 sP0_prd(sK5_skl,sK4_skl,sK3_skl)|~sQ0_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f43])).
% 0.16/0.47 fof(f46,definition,(
% 0.16/0.47 ![X0,X1]: (sQ1_spl <=> (~in(X0,sK6_skl(X1))|in(sK7_skl(X0,X1),X1)))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f47,plain,(
% 0.16/0.47 ![X0,X1]: (~in(X0,sK6_skl(X1))|in(sK7_skl(X0,X1),X1)|~sQ1_spl)),
% 0.16/0.47 inference(component_clause,[status(thm)],[f46])).
% 0.16/0.47 fof(f49,plain,(
% 0.16/0.47 sQ0_spl|sQ1_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f31,f43,f46])).
% 0.16/0.47 fof(f50,definition,(
% 0.16/0.47 ![X0,X1]: (sQ2_spl <=> (~in(X0,sK6_skl(X1))|sK7_skl(X0,X1)=X0))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f51,plain,(
% 0.16/0.47 ![X0,X1]: (~in(X0,sK6_skl(X1))|sK7_skl(X0,X1)=X0|~sQ2_spl)),
% 0.16/0.47 inference(component_clause,[status(thm)],[f50])).
% 0.16/0.47 fof(f53,plain,(
% 0.16/0.47 sQ0_spl|sQ2_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f32,f43,f50])).
% 0.16/0.47 fof(f54,definition,(
% 0.16/0.47 ![X0,X1]: (sQ3_spl <=> (~in(X0,sK6_skl(X1))|ordinal(X0)))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f55,plain,(
% 0.16/0.47 ![X0,X1]: (~in(X0,sK6_skl(X1))|ordinal(X0)|~sQ3_spl)),
% 0.16/0.47 inference(component_clause,[status(thm)],[f54])).
% 0.16/0.47 fof(f57,plain,(
% 0.16/0.47 sQ0_spl|sQ3_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f33,f43,f54])).
% 0.16/0.47 fof(f58,definition,(
% 0.16/0.47 ![X0,X1,X2]: (sQ4_spl <=> (in(X0,sK6_skl(X1))|~in(X2,X1)|~X2=X0|~ordinal(X0)))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f59,plain,(
% 0.16/0.47 ![X0,X1,X2]: (in(X0,sK6_skl(X1))|~in(X2,X1)|~X2=X0|~ordinal(X0)|~sQ4_spl)),
% 0.16/0.47 inference(component_clause,[status(thm)],[f58])).
% 0.16/0.47 fof(f61,plain,(
% 0.16/0.47 sQ0_spl|sQ4_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f34,f43,f58])).
% 0.16/0.47 fof(f62,plain,(
% 0.16/0.47 ![X0,X1]: (~sP0_prd(X0,X0,X1))),
% 0.16/0.47 inference(destructive_equality_resolution,[status(thm)],[f41])).
% 0.16/0.47 fof(f102,plain,(
% 0.16/0.47 sK3_skl=sK5_skl|~sQ0_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f44,f39])).
% 0.16/0.47 fof(f104,plain,(
% 0.16/0.47 sK3_skl=sK4_skl|~sQ0_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f44,f37])).
% 0.16/0.47 fof(f105,plain,(
% 0.16/0.47 sP0_prd(sK3_skl,sK4_skl,sK3_skl)|~sQ0_spl),
% 0.16/0.47 inference(backward_demodulation,[status(thm)],[f102,f44])).
% 0.16/0.47 fof(f108,plain,(
% 0.16/0.47 sP0_prd(sK3_skl,sK3_skl,sK3_skl)|~sQ0_spl),
% 0.16/0.47 inference(forward_demodulation,[status(thm)],[f104,f105])).
% 0.16/0.47 fof(f109,plain,(
% 0.16/0.47 $false|~sQ0_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f108,f62])).
% 0.16/0.47 fof(f110,plain,(
% 0.16/0.47 ~sQ0_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f109])).
% 0.16/0.47 fof(f111,plain,(
% 0.16/0.47 ![X0,X1]: (in(X0,sK6_skl(X1))|~in(X0,X1)|~ordinal(X0)|~sQ4_spl)),
% 0.16/0.47 inference(destructive_equality_resolution,[status(thm)],[f59])).
% 0.16/0.47 fof(f124,plain,(
% 0.16/0.47 ![X0]: (ordinal(sK1_skl(sK6_skl(X0)))|ordinal(sK1_skl(sK6_skl(X0)))|~sQ3_spl)),
% 0.16/0.47 inference(resolution,[status(thm)],[f55,f12])).
% 0.16/0.47 fof(f125,plain,(
% 0.16/0.47 ![X0]: (ordinal(sK1_skl(sK6_skl(X0)))|~sQ3_spl)),
% 0.16/0.47 inference(duplicate_literals_removal,[status(thm)],[f124])).
% 0.16/0.47 fof(f137,plain,(
% 0.16/0.47 ![X0]: (in(sK1_skl(X0),sK6_skl(sK0_skl))|~ordinal(sK1_skl(X0))|in(sK1_skl(X0),X0)|~sQ4_spl)),
% 0.16/0.47 inference(resolution,[status(thm)],[f111,f11])).
% 0.16/0.47 fof(f146,plain,(
% 0.16/0.47 ![X0]: (in(sK1_skl(X0),sK6_skl(sK0_skl))|in(sK1_skl(X0),X0)|~sQ4_spl)),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f137,f12])).
% 0.16/0.47 fof(f152,plain,(
% 0.16/0.47 sK7_skl(sK1_skl(sK6_skl(sK0_skl)),sK0_skl)=sK1_skl(sK6_skl(sK0_skl))|~sQ4_spl|~sQ2_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f146,f51])).
% 0.16/0.47 fof(f156,plain,(
% 0.16/0.47 in(sK7_skl(sK1_skl(sK6_skl(sK0_skl)),sK0_skl),sK0_skl)|~sQ4_spl|~sQ1_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f146,f47])).
% 0.16/0.47 fof(f169,plain,(
% 0.16/0.47 in(sK1_skl(sK6_skl(sK0_skl)),sK0_skl)|~sQ2_spl|~sQ4_spl|~sQ1_spl),
% 0.16/0.47 inference(forward_demodulation,[status(thm)],[f152,f156])).
% 0.16/0.47 fof(f173,definition,(
% 0.16/0.47 sQ11_spl <=> (ordinal(sK1_skl(sK6_skl(sK0_skl))))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f175,plain,(
% 0.16/0.47 ~ordinal(sK1_skl(sK6_skl(sK0_skl)))|sQ11_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f173])).
% 0.16/0.47 fof(f187,plain,(
% 0.16/0.47 ~in(sK1_skl(sK6_skl(sK0_skl)),sK6_skl(sK0_skl))|~ordinal(sK1_skl(sK6_skl(sK0_skl)))|~sQ2_spl|~sQ4_spl|~sQ1_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f169,f13])).
% 0.16/0.47 fof(f188,plain,(
% 0.16/0.47 in(sK1_skl(sK6_skl(sK0_skl)),sK6_skl(sK0_skl))|~ordinal(sK1_skl(sK6_skl(sK0_skl)))|~sQ2_spl|~sQ1_spl|~sQ4_spl),
% 0.16/0.47 inference(resolution,[status(thm)],[f169,f111])).
% 0.16/0.47 fof(f190,definition,(
% 0.16/0.47 sQ12_spl <=> (in(sK1_skl(sK6_skl(sK0_skl)),sK6_skl(sK0_skl)))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f193,plain,(
% 0.16/0.47 ~sQ12_spl|~sQ11_spl|~sQ2_spl|~sQ4_spl|~sQ1_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f187,f190,f173,f50,f58,f46])).
% 0.16/0.47 fof(f194,plain,(
% 0.16/0.47 sQ12_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl),
% 0.16/0.47 inference(split_clause,[status(thm)],[f188,f190,f173,f50,f46,f58])).
% 0.16/0.47 fof(f195,plain,(
% 0.16/0.47 $false|~sQ3_spl|sQ11_spl),
% 0.16/0.47 inference(forward_subsumption_resolution,[status(thm)],[f175,f125])).
% 0.16/0.47 fof(f196,plain,(
% 0.16/0.47 ~sQ3_spl|sQ11_spl),
% 0.16/0.47 inference(contradiction_clause,[status(thm)],[f195])).
% 0.16/0.47 fof(f197,plain,(
% 0.16/0.47 $false),
% 0.16/0.47 inference(sat_refutation,[status(thm)],[f49,f53,f57,f61,f110,f193,f194,f196])).
% 0.16/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.50 % Elapsed time: 0.062469 seconds
% 0.16/0.50 % CPU time: 0.183103 seconds
% 0.16/0.50 % Total memory used: 53.653 MB
% 0.16/0.50 % Net memory used: 53.428 MB
%------------------------------------------------------------------------------