%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU284+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 : n001.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:13 PM UTC 2026
% Result : Theorem 0.17s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU284+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.17/0.42 % Computer : n001.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 06:13:13 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.51 % Refutation found
% 0.17/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.51 fof(f1,conjecture,(
% 0.17/0.51 (! [A] :(? [B] :( relation(B)& function(B)& relation_dom(B) = A& (! [C] :( in(C,A)=> apply(B,C) = singleton(C) ) )) ))),
% 0.17/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.51 fof(f2,negated_conjecture,(
% 0.17/0.51 ~((! [A] :(? [B] :( relation(B)& function(B)& relation_dom(B) = A& (! [C] :( in(C,A)=> apply(B,C) = singleton(C) ) )) )))),
% 0.17/0.51 inference(negated_conjecture,[status(cth)],[f1])).
% 0.17/0.51 fof(f8,axiom,(
% 0.17/0.51 (! [A] :( ( (! [B,C,D] :( ( in(B,A)& C = singleton(B)& D = singleton(B) )=> C = D ))& (! [B] :~ ( in(B,A)& (! [C] : C != singleton(B) )) ))=> (? [B] :( relation(B)& function(B)& relation_dom(B) = A& (! [C] :( in(C,A)=> apply(B,C) = singleton(C) ) )) )) )),
% 0.17/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.51 fof(f9,axiom,(
% 0.17/0.51 (! [A] :( empty(A)=> function(A) ) )),
% 0.17/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.51 fof(f14,axiom,(
% 0.17/0.51 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.17/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.51 fof(f29,plain,(
% 0.17/0.51 (?[A]: ![B]: (((~relation(B)|~function(B))|~relation_dom(B)=A)|(?[C]: (in(C,A)&~apply(B,C)=singleton(C)))))),
% 0.17/0.51 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.17/0.51 fof(f30,plain,(
% 0.17/0.51 ![B]: (((~relation(B)|~function(B))|~relation_dom(B)=sK0_skl)|(in(sK1_skl(B),sK0_skl)&~apply(B,sK1_skl(B))=singleton(sK1_skl(B))))),
% 0.17/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(C,sK1_skl(B))],[f29])).
% 0.17/0.51 fof(f31,plain,(
% 0.17/0.51 ![X0]: (~relation(X0)|~function(X0)|~relation_dom(X0)=sK0_skl|in(sK1_skl(X0),sK0_skl))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f30])).
% 0.17/0.51 fof(f32,plain,(
% 0.17/0.51 ![X0]: (~relation(X0)|~function(X0)|~relation_dom(X0)=sK0_skl|~apply(X0,sK1_skl(X0))=singleton(sK1_skl(X0)))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f30])).
% 0.17/0.51 fof(f38,plain,(
% 0.17/0.51 ![A]: (((?[B,C,D]: (((in(B,A)&C=singleton(B))&D=singleton(B))&~C=D))|(?[B]: (in(B,A)&(![C]: ~C=singleton(B)))))|(?[B]: (((relation(B)&function(B))&relation_dom(B)=A)&(![C]: (~in(C,A)|apply(B,C)=singleton(C))))))),
% 0.17/0.51 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.17/0.51 fof(f39,definition,(
% 0.17/0.51 ![A]: (sP0_prd(A)<=>((?[B,C,D]: (((in(B,A)&C=singleton(B))&D=singleton(B))&~C=D))|(?[B]: (in(B,A)&(![C]: ~C=singleton(B))))))),
% 0.17/0.51 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.17/0.51 fof(f40,plain,(
% 0.17/0.51 ![A]: (sP0_prd(A)|(?[B]: (((relation(B)&function(B))&relation_dom(B)=A)&(![C]: (~in(C,A)|apply(B,C)=singleton(C))))))),
% 0.17/0.51 inference(formula_renaming,[status(thm)],[f38,f39])).
% 0.17/0.51 fof(f41,plain,(
% 0.17/0.51 ![A]: (sP0_prd(A)|(((relation(sK3_skl(A))&function(sK3_skl(A)))&relation_dom(sK3_skl(A))=A)&(![C]: (~in(C,A)|apply(sK3_skl(A),C)=singleton(C)))))),
% 0.17/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl(A))],[f40])).
% 0.17/0.51 fof(f42,plain,(
% 0.17/0.51 ![X0]: (sP0_prd(X0)|relation(sK3_skl(X0)))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f41])).
% 0.17/0.51 fof(f43,plain,(
% 0.17/0.51 ![X0]: (sP0_prd(X0)|function(sK3_skl(X0)))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f41])).
% 0.17/0.51 fof(f44,plain,(
% 0.17/0.51 ![X0]: (sP0_prd(X0)|relation_dom(sK3_skl(X0))=X0)),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f41])).
% 0.17/0.51 fof(f45,plain,(
% 0.17/0.51 ![X0,X1]: (sP0_prd(X0)|~in(X1,X0)|apply(sK3_skl(X0),X1)=singleton(X1))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f41])).
% 0.17/0.51 fof(f46,plain,(
% 0.17/0.51 ![A]: (~empty(A)|function(A))),
% 0.17/0.51 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.17/0.51 fof(f47,plain,(
% 0.17/0.51 ![X0]: (~empty(X0)|function(X0))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f46])).
% 0.17/0.51 fof(f52,plain,(
% 0.17/0.51 empty(empty_set)),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f14])).
% 0.17/0.51 fof(f88,definition,(
% 0.17/0.51 ![A,B,C,D]: (sP1_prd(D,C,B,A)<=>(((in(B,A)&C=singleton(B))&D=singleton(B))&~C=D))),
% 0.17/0.51 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.17/0.51 fof(f89,plain,(
% 0.17/0.51 ![A]: (sP0_prd(A)<=>((?[B,C,D]: sP1_prd(D,C,B,A))|(?[B]: (in(B,A)&(![C]: ~C=singleton(B))))))),
% 0.17/0.51 inference(formula_renaming,[status(thm)],[f39,f88])).
% 0.17/0.51 fof(f90,plain,(
% 0.17/0.51 ![A]: ((~sP0_prd(A)|((?[B,C,D]: sP1_prd(D,C,B,A))|(?[B]: (in(B,A)&(![C]: ~C=singleton(B))))))&(sP0_prd(A)|((![B,C,D]: ~sP1_prd(D,C,B,A))&(![B]: (~in(B,A)|(?[C]: C=singleton(B)))))))),
% 0.17/0.51 inference(NNF_transformation,[status(thm)],[f89])).
% 0.17/0.51 fof(f91,plain,(
% 0.17/0.51 (![A]: (~sP0_prd(A)|((?[B,C,D]: sP1_prd(D,C,B,A))|(?[B]: (in(B,A)&(![C]: ~C=singleton(B)))))))&(![A]: (sP0_prd(A)|((![B,C,D]: ~sP1_prd(D,C,B,A))&(![B]: (~in(B,A)|(?[C]: C=singleton(B)))))))),
% 0.17/0.51 inference(miniscoping,[status(thm)],[f90])).
% 0.17/0.51 fof(f92,plain,(
% 0.17/0.51 (![A]: (~sP0_prd(A)|(sP1_prd(sK12_skl(A),sK11_skl(A),sK10_skl(A),A)|(in(sK13_skl(A),A)&(![C]: ~C=singleton(sK13_skl(A)))))))&(![A]: (sP0_prd(A)|((![B,C,D]: ~sP1_prd(D,C,B,A))&(![B]: (~in(B,A)|sK14_skl(B,A)=singleton(B))))))),
% 0.17/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(B,sK10_skl(A)),skolemize(C,sK11_skl(A)),skolemize(D,sK12_skl(A)),skolemize(B,sK13_skl(A)),skolemize(C,sK14_skl(B,A))],[f91])).
% 0.17/0.51 fof(f94,plain,(
% 0.17/0.51 ![X0,X1]: (~sP0_prd(X0)|sP1_prd(sK12_skl(X0),sK11_skl(X0),sK10_skl(X0),X0)|~X1=singleton(sK13_skl(X0)))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f92])).
% 0.17/0.51 fof(f97,plain,(
% 0.17/0.51 ![A,B,C,D]: ((~sP1_prd(D,C,B,A)|(((in(B,A)&C=singleton(B))&D=singleton(B))&~C=D))&(sP1_prd(D,C,B,A)|(((~in(B,A)|~C=singleton(B))|~D=singleton(B))|C=D)))),
% 0.17/0.51 inference(NNF_transformation,[status(thm)],[f88])).
% 0.17/0.51 fof(f98,plain,(
% 0.17/0.51 (![A,B,C,D]: (~sP1_prd(D,C,B,A)|(((in(B,A)&C=singleton(B))&D=singleton(B))&~C=D)))&(![A,B,C,D]: (sP1_prd(D,C,B,A)|(((~in(B,A)|~C=singleton(B))|~D=singleton(B))|C=D)))),
% 0.17/0.51 inference(miniscoping,[status(thm)],[f97])).
% 0.17/0.51 fof(f100,plain,(
% 0.17/0.51 ![X0,X1,X2,X3]: (~sP1_prd(X0,X1,X2,X3)|X1=singleton(X2))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f98])).
% 0.17/0.51 fof(f101,plain,(
% 0.17/0.51 ![X0,X1,X2,X3]: (~sP1_prd(X0,X1,X2,X3)|X0=singleton(X2))),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f98])).
% 0.17/0.51 fof(f102,plain,(
% 0.17/0.51 ![X0,X1,X2,X3]: (~sP1_prd(X0,X1,X2,X3)|~X1=X0)),
% 0.17/0.51 inference(cnf_transformation,[status(thm)],[f98])).
% 0.17/0.51 fof(f104,plain,(
% 0.17/0.51 ![X0]: (~sP0_prd(X0)|sP1_prd(sK12_skl(X0),sK11_skl(X0),sK10_skl(X0),X0))),
% 0.17/0.51 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 0.17/0.51 fof(f105,plain,(
% 0.17/0.51 ![X0,X1,X2]: (~sP1_prd(X0,X0,X1,X2))),
% 0.17/0.51 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 0.17/0.51 fof(f112,plain,(
% 0.17/0.51 function(empty_set)),
% 0.17/0.51 inference(resolution,[status(thm)],[f52,f47])).
% 0.17/0.51 fof(f164,definition,(
% 0.17/0.51 sQ2_spl <=> (function(empty_set))),
% 0.17/0.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.17/0.51 fof(f166,plain,(
% 0.17/0.51 ~function(empty_set)|sQ2_spl),
% 0.17/0.51 inference(component_clause,[status(thm)],[f164])).
% 0.17/0.51 fof(f180,definition,(
% 0.17/0.51 sQ5_spl <=> (sP0_prd(sK0_skl))),
% 0.17/0.51 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.17/0.51 fof(f181,plain,(
% 0.17/0.51 sP0_prd(sK0_skl)|~sQ5_spl),
% 0.17/0.51 inference(component_clause,[status(thm)],[f180])).
% 0.17/0.51 fof(f182,plain,(
% 0.17/0.51 ~sP0_prd(sK0_skl)|sQ5_spl),
% 0.17/0.51 inference(component_clause,[status(thm)],[f180])).
% 0.17/0.51 fof(f187,plain,(
% 0.17/0.51 sP1_prd(sK12_skl(sK0_skl),sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK0_skl)|~sQ5_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f181,f104])).
% 0.17/0.51 fof(f190,plain,(
% 0.17/0.51 sK12_skl(sK0_skl)=singleton(sK10_skl(sK0_skl))|~sQ5_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f187,f101])).
% 0.17/0.51 fof(f191,plain,(
% 0.17/0.51 sK11_skl(sK0_skl)=singleton(sK10_skl(sK0_skl))|~sQ5_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f187,f100])).
% 0.17/0.51 fof(f192,plain,(
% 0.17/0.51 sK12_skl(sK0_skl)=sK11_skl(sK0_skl)|~sQ5_spl),
% 0.17/0.51 inference(backward_demodulation,[status(thm)],[f191,f190])).
% 0.17/0.51 fof(f193,plain,(
% 0.17/0.51 sP1_prd(sK11_skl(sK0_skl),sK11_skl(sK0_skl),sK10_skl(sK0_skl),sK0_skl)|~sQ5_spl),
% 0.17/0.51 inference(backward_demodulation,[status(thm)],[f192,f187])).
% 0.17/0.51 fof(f194,plain,(
% 0.17/0.51 $false|~sQ5_spl),
% 0.17/0.51 inference(forward_subsumption_resolution,[status(thm)],[f193,f105])).
% 0.17/0.51 fof(f195,plain,(
% 0.17/0.51 ~sQ5_spl),
% 0.17/0.51 inference(contradiction_clause,[status(thm)],[f194])).
% 0.17/0.51 fof(f196,plain,(
% 0.17/0.51 relation_dom(sK3_skl(sK0_skl))=sK0_skl|sQ5_spl),
% 0.17/0.51 inference(resolution,[status(thm)],[f182,f44])).
% 0.17/0.51 fof(f197,plain,(
% 0.17/0.51 ~relation(sK3_skl(sK0_skl))|~function(sK3_skl(sK0_skl))|in(sK1_skl(sK3_skl(sK0_skl)),sK0_skl)|sQ5_spl),
% 0.17/0.52 inference(resolution,[status(thm)],[f196,f31])).
% 0.17/0.52 fof(f200,definition,(
% 0.17/0.52 sQ7_spl <=> (relation(sK3_skl(sK0_skl)))),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.17/0.52 fof(f202,plain,(
% 0.17/0.52 ~relation(sK3_skl(sK0_skl))|sQ7_spl),
% 0.17/0.52 inference(component_clause,[status(thm)],[f200])).
% 0.17/0.52 fof(f203,definition,(
% 0.17/0.52 sQ8_spl <=> (function(sK3_skl(sK0_skl)))),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.17/0.52 fof(f205,plain,(
% 0.17/0.52 ~function(sK3_skl(sK0_skl))|sQ8_spl),
% 0.17/0.52 inference(component_clause,[status(thm)],[f203])).
% 0.17/0.52 fof(f206,definition,(
% 0.17/0.52 sQ9_spl <=> (in(sK1_skl(sK3_skl(sK0_skl)),sK0_skl))),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.17/0.52 fof(f207,plain,(
% 0.17/0.52 in(sK1_skl(sK3_skl(sK0_skl)),sK0_skl)|~sQ9_spl),
% 0.17/0.52 inference(component_clause,[status(thm)],[f206])).
% 0.17/0.52 fof(f209,plain,(
% 0.17/0.52 ~sQ7_spl|~sQ8_spl|sQ9_spl|sQ5_spl),
% 0.17/0.52 inference(split_clause,[status(thm)],[f197,f200,f203,f206,f180])).
% 0.17/0.52 fof(f221,plain,(
% 0.17/0.52 sP0_prd(sK0_skl)|sQ7_spl),
% 0.17/0.52 inference(resolution,[status(thm)],[f202,f42])).
% 0.17/0.52 fof(f222,plain,(
% 0.17/0.52 sQ5_spl|sQ7_spl),
% 0.17/0.52 inference(split_clause,[status(thm)],[f221,f180,f200])).
% 0.17/0.52 fof(f247,plain,(
% 0.17/0.52 $false|sQ2_spl),
% 0.17/0.52 inference(forward_subsumption_resolution,[status(thm)],[f166,f112])).
% 0.17/0.52 fof(f248,plain,(
% 0.17/0.52 sQ2_spl),
% 0.17/0.52 inference(contradiction_clause,[status(thm)],[f247])).
% 0.17/0.52 fof(f277,plain,(
% 0.17/0.52 sP0_prd(sK0_skl)|apply(sK3_skl(sK0_skl),sK1_skl(sK3_skl(sK0_skl)))=singleton(sK1_skl(sK3_skl(sK0_skl)))|~sQ9_spl),
% 0.17/0.52 inference(resolution,[status(thm)],[f207,f45])).
% 0.17/0.52 fof(f280,definition,(
% 0.17/0.52 sQ13_spl <=> (apply(sK3_skl(sK0_skl),sK1_skl(sK3_skl(sK0_skl)))=singleton(sK1_skl(sK3_skl(sK0_skl))))),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.17/0.52 fof(f281,plain,(
% 0.17/0.52 apply(sK3_skl(sK0_skl),sK1_skl(sK3_skl(sK0_skl)))=singleton(sK1_skl(sK3_skl(sK0_skl)))|~sQ13_spl),
% 0.17/0.52 inference(component_clause,[status(thm)],[f280])).
% 0.17/0.52 fof(f283,plain,(
% 0.17/0.52 sQ5_spl|sQ13_spl|~sQ9_spl),
% 0.17/0.52 inference(split_clause,[status(thm)],[f277,f180,f280,f206])).
% 0.17/0.52 fof(f284,plain,(
% 0.17/0.52 ~relation(sK3_skl(sK0_skl))|~function(sK3_skl(sK0_skl))|~relation_dom(sK3_skl(sK0_skl))=sK0_skl|~sQ13_spl),
% 0.17/0.52 inference(resolution,[status(thm)],[f281,f32])).
% 0.17/0.52 fof(f286,definition,(
% 0.17/0.52 sQ14_spl <=> (relation_dom(sK3_skl(sK0_skl))=sK0_skl)),
% 0.17/0.52 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.17/0.52 fof(f288,plain,(
% 0.17/0.52 ~relation_dom(sK3_skl(sK0_skl))=sK0_skl|sQ14_spl),
% 0.17/0.52 inference(component_clause,[status(thm)],[f286])).
% 0.17/0.52 fof(f289,plain,(
% 0.17/0.52 ~sQ7_spl|~sQ8_spl|~sQ14_spl|~sQ13_spl),
% 0.17/0.52 inference(split_clause,[status(thm)],[f284,f200,f203,f286,f280])).
% 0.17/0.52 fof(f294,plain,(
% 0.17/0.52 sP0_prd(sK0_skl)|sQ8_spl),
% 0.17/0.52 inference(resolution,[status(thm)],[f205,f43])).
% 0.17/0.52 fof(f295,plain,(
% 0.17/0.52 sQ5_spl|sQ8_spl),
% 0.17/0.52 inference(split_clause,[status(thm)],[f294,f180,f203])).
% 0.17/0.52 fof(f296,plain,(
% 0.17/0.52 ~sK0_skl=sK0_skl|sQ5_spl|sQ14_spl),
% 0.17/0.52 inference(forward_demodulation,[status(thm)],[f196,f288])).
% 0.17/0.52 fof(f297,plain,(
% 0.17/0.52 $false|sQ5_spl|sQ14_spl),
% 0.17/0.52 inference(trivial_equality_resolution,[status(thm)],[f296])).
% 0.17/0.52 fof(f298,plain,(
% 0.17/0.52 sQ5_spl|sQ14_spl),
% 0.17/0.52 inference(contradiction_clause,[status(thm)],[f297])).
% 0.17/0.52 fof(f299,plain,(
% 0.17/0.52 $false),
% 0.17/0.52 inference(sat_refutation,[status(thm)],[f195,f209,f222,f248,f283,f289,f295,f298])).
% 0.17/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.53 % Elapsed time: 0.089554 seconds
% 0.17/0.53 % CPU time: 0.448604 seconds
% 0.17/0.53 % Total memory used: 84.122 MB
% 0.17/0.53 % Net memory used: 83.554 MB
%------------------------------------------------------------------------------