%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU217+2 : 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 : n004.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:01 PM UTC 2026
% Result : Theorem 0.15s 10.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU217+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/10.59 % Computer : n004.cluster.edu
% 0.11/10.59 % Model : x86_64 x86_64
% 0.11/10.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.59 % Memory : 8046.5625MB
% 0.11/10.59 % OS : Linux 6.8.0-71-generic
% 0.11/10.59 % CPULimit : 300
% 0.11/10.59 % WCLimit : 300
% 0.11/10.60 % DateTime : Mon Sep 21 05:59:16 UTC 2026
% 0.15/10.60 % CPUTime :
% 0.15/10.62 % Drodi V4.1.1
% 0.15/10.64 % Refutation found
% 0.15/10.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/10.64 % SZS output start CNFRefutation for theBenchmark
% 0.15/10.64 fof(f8,axiom,(
% 0.15/10.64 (! [A,B] :( relation(B)=> ( B = identity_relation(A)<=> (! [C,D] :( in(ordered_pair(C,D),B)<=> ( in(C,A)& C = D ) ) )) ) )),
% 0.15/10.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.64 fof(f27,axiom,(
% 0.15/10.64 (! [A] :( ( relation(A)& function(A) )=> (! [B,C] :( ( in(B,relation_dom(A))=> ( C = apply(A,B)<=> in(ordered_pair(B,C),A) ) )& ( ~ in(B,relation_dom(A))=> ( C = apply(A,B)<=> C = empty_set ) ) ) )) )),
% 0.15/10.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.64 fof(f62,axiom,(
% 0.15/10.64 (! [A] : relation(identity_relation(A)) )),
% 0.15/10.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.64 fof(f78,axiom,(
% 0.15/10.64 (! [A] :( relation(identity_relation(A))& function(identity_relation(A)) ) )),
% 0.15/10.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.64 fof(f165,conjecture,(
% 0.15/10.64 (! [A,B] :( in(B,A)=> apply(identity_relation(A),B) = B ) )),
% 0.15/10.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.64 fof(f166,negated_conjecture,(
% 0.15/10.64 ~((! [A,B] :( in(B,A)=> apply(identity_relation(A),B) = B ) ))),
% 0.15/10.64 inference(negated_conjecture,[status(cth)],[f165])).
% 0.15/10.64 fof(f206,lemma,(
% 0.15/10.64 (! [A] :( relation_dom(identity_relation(A)) = A& relation_rng(identity_relation(A)) = A ) )),
% 0.15/10.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/10.64 fof(f235,plain,(
% 0.15/10.64 ![A,B]: (~relation(B)|(B=identity_relation(A)<=>(![C,D]: (in(ordered_pair(C,D),B)<=>(in(C,A)&C=D)))))),
% 0.15/10.64 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.15/10.64 fof(f236,plain,(
% 0.15/10.64 ![A,B]: (~relation(B)|((~B=identity_relation(A)|(![C,D]: ((~in(ordered_pair(C,D),B)|(in(C,A)&C=D))&(in(ordered_pair(C,D),B)|(~in(C,A)|~C=D)))))&(B=identity_relation(A)|(?[C,D]: ((~in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))&(in(ordered_pair(C,D),B)|(in(C,A)&C=D)))))))),
% 0.15/10.64 inference(NNF_transformation,[status(thm)],[f235])).
% 0.15/10.64 fof(f237,plain,(
% 0.15/10.64 ![B]: (~relation(B)|((![A]: (~B=identity_relation(A)|((![C,D]: (~in(ordered_pair(C,D),B)|(in(C,A)&C=D)))&(![C,D]: (in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))))))&(![A]: (B=identity_relation(A)|(?[C,D]: ((~in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))&(in(ordered_pair(C,D),B)|(in(C,A)&C=D))))))))),
% 0.15/10.64 inference(miniscoping,[status(thm)],[f236])).
% 0.15/10.64 fof(f238,plain,(
% 0.15/10.64 ![B]: (~relation(B)|((![A]: (~B=identity_relation(A)|((![C,D]: (~in(ordered_pair(C,D),B)|(in(C,A)&C=D)))&(![C,D]: (in(ordered_pair(C,D),B)|(~in(C,A)|~C=D))))))&(![A]: (B=identity_relation(A)|((~in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B)|(~in(sK0_skl(A,B),A)|~sK0_skl(A,B)=sK1_skl(A,B)))&(in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B)|(in(sK0_skl(A,B),A)&sK0_skl(A,B)=sK1_skl(A,B))))))))),
% 0.15/10.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f237])).
% 0.15/10.64 fof(f241,plain,(
% 0.15/10.64 ![X0,X1,X2,X3]: (~relation(X0)|~X0=identity_relation(X1)|in(ordered_pair(X2,X3),X0)|~in(X2,X1)|~X2=X3)),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f238])).
% 0.15/10.64 fof(f392,plain,(
% 0.15/10.64 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|(C=apply(A,B)<=>in(ordered_pair(B,C),A)))&(in(B,relation_dom(A))|(C=apply(A,B)<=>C=empty_set)))))),
% 0.15/10.64 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.15/10.64 fof(f393,plain,(
% 0.15/10.64 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|((~C=apply(A,B)|in(ordered_pair(B,C),A))&(C=apply(A,B)|~in(ordered_pair(B,C),A))))&(in(B,relation_dom(A))|((~C=apply(A,B)|C=empty_set)&(C=apply(A,B)|~C=empty_set))))))),
% 0.15/10.64 inference(NNF_transformation,[status(thm)],[f392])).
% 0.15/10.64 fof(f394,plain,(
% 0.15/10.64 ![A]: ((~relation(A)|~function(A))|((![B]: (~in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|in(ordered_pair(B,C),A)))&(![C]: (C=apply(A,B)|~in(ordered_pair(B,C),A))))))&(![B]: (in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|C=empty_set))&(![C]: (C=apply(A,B)|~C=empty_set)))))))),
% 0.15/10.64 inference(miniscoping,[status(thm)],[f393])).
% 0.15/10.64 fof(f396,plain,(
% 0.15/10.64 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~in(X1,relation_dom(X0))|X2=apply(X0,X1)|~in(ordered_pair(X1,X2),X0))),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f394])).
% 0.15/10.64 fof(f483,plain,(
% 0.15/10.64 ![X0]: (relation(identity_relation(X0)))),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f62])).
% 0.15/10.64 fof(f512,plain,(
% 0.15/10.64 (![A]: relation(identity_relation(A)))&(![A]: function(identity_relation(A)))),
% 0.15/10.64 inference(miniscoping,[status(thm)],[f78])).
% 0.15/10.64 fof(f514,plain,(
% 0.15/10.64 ![X0]: (function(identity_relation(X0)))),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f512])).
% 0.15/10.64 fof(f765,plain,(
% 0.15/10.64 (?[A,B]: (in(B,A)&~apply(identity_relation(A),B)=B))),
% 0.15/10.64 inference(pre_NNF_transformation,[status(thm)],[f166])).
% 0.15/10.64 fof(f766,plain,(
% 0.15/10.64 (in(sK67_skl,sK66_skl)&~apply(identity_relation(sK66_skl),sK67_skl)=sK67_skl)),
% 0.15/10.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK66_skl,sK67_skl]),skolemize(A,sK66_skl),skolemize(B,sK67_skl)],[f765])).
% 0.15/10.64 fof(f767,plain,(
% 0.15/10.64 in(sK67_skl,sK66_skl)),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f766])).
% 0.15/10.64 fof(f768,plain,(
% 0.15/10.64 ~apply(identity_relation(sK66_skl),sK67_skl)=sK67_skl),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f766])).
% 0.15/10.64 fof(f872,plain,(
% 0.15/10.64 (![A]: relation_dom(identity_relation(A))=A)&(![A]: relation_rng(identity_relation(A))=A)),
% 0.15/10.64 inference(miniscoping,[status(thm)],[f206])).
% 0.15/10.64 fof(f873,plain,(
% 0.15/10.64 ![X0]: (relation_dom(identity_relation(X0))=X0)),
% 0.15/10.64 inference(cnf_transformation,[status(thm)],[f872])).
% 0.15/10.64 fof(f943,plain,(
% 0.15/10.64 ![X0,X1]: (~relation(identity_relation(X0))|in(ordered_pair(X1,X1),identity_relation(X0))|~in(X1,X0))),
% 0.15/10.64 inference(destructive_equality_resolution,[status(thm)],[f241])).
% 0.15/10.64 fof(f1013,plain,(
% 0.15/10.64 ![X0,X1]: (in(ordered_pair(X0,X0),identity_relation(X1))|~in(X0,X1))),
% 0.15/10.64 inference(forward_subsumption_resolution,[status(thm)],[f943,f483])).
% 0.15/10.64 fof(f1014,plain,(
% 0.15/10.64 in(ordered_pair(sK67_skl,sK67_skl),identity_relation(sK66_skl))),
% 0.15/10.64 inference(resolution,[status(thm)],[f1013,f767])).
% 0.15/10.64 fof(f1024,plain,(
% 0.15/10.64 ~relation(identity_relation(sK66_skl))|~function(identity_relation(sK66_skl))|~in(sK67_skl,relation_dom(identity_relation(sK66_skl)))|sK67_skl=apply(identity_relation(sK66_skl),sK67_skl)),
% 0.15/10.64 inference(resolution,[status(thm)],[f396,f1014])).
% 0.15/10.64 fof(f1025,definition,(
% 0.15/10.64 sQ0_spl <=> (relation(identity_relation(sK66_skl)))),
% 0.15/10.64 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/10.64 fof(f1027,plain,(
% 0.15/10.64 ~relation(identity_relation(sK66_skl))|sQ0_spl),
% 0.15/10.64 inference(component_clause,[status(thm)],[f1025])).
% 0.15/10.64 fof(f1028,definition,(
% 0.15/10.64 sQ1_spl <=> (function(identity_relation(sK66_skl)))),
% 0.15/10.64 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/10.64 fof(f1030,plain,(
% 0.15/10.64 ~function(identity_relation(sK66_skl))|sQ1_spl),
% 0.15/10.64 inference(component_clause,[status(thm)],[f1028])).
% 0.15/10.64 fof(f1031,definition,(
% 0.15/10.64 sQ2_spl <=> (in(sK67_skl,relation_dom(identity_relation(sK66_skl))))),
% 0.15/10.64 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/10.64 fof(f1033,plain,(
% 0.15/10.64 ~in(sK67_skl,relation_dom(identity_relation(sK66_skl)))|sQ2_spl),
% 0.15/10.64 inference(component_clause,[status(thm)],[f1031])).
% 0.15/10.64 fof(f1034,definition,(
% 0.15/10.64 sQ3_spl <=> (sK67_skl=apply(identity_relation(sK66_skl),sK67_skl))),
% 0.15/10.64 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/10.64 fof(f1035,plain,(
% 0.15/10.64 sK67_skl=apply(identity_relation(sK66_skl),sK67_skl)|~sQ3_spl),
% 0.15/10.64 inference(component_clause,[status(thm)],[f1034])).
% 0.15/10.64 fof(f1037,plain,(
% 0.15/10.64 ~sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl),
% 0.15/10.64 inference(split_clause,[status(thm)],[f1024,f1025,f1028,f1031,f1034])).
% 0.15/10.64 fof(f1038,plain,(
% 0.15/10.64 $false|~sQ3_spl),
% 0.15/10.64 inference(forward_subsumption_resolution,[status(thm)],[f1035,f768])).
% 0.15/10.64 fof(f1039,plain,(
% 0.15/10.64 ~sQ3_spl),
% 0.15/10.64 inference(contradiction_clause,[status(thm)],[f1038])).
% 0.15/10.64 fof(f1040,plain,(
% 0.15/10.64 ~in(sK67_skl,sK66_skl)|sQ2_spl),
% 0.15/10.64 inference(forward_demodulation,[status(thm)],[f873,f1033])).
% 0.15/10.64 fof(f1041,plain,(
% 0.15/10.64 $false|sQ2_spl),
% 0.15/10.64 inference(forward_subsumption_resolution,[status(thm)],[f1040,f767])).
% 0.15/10.64 fof(f1042,plain,(
% 0.15/10.64 sQ2_spl),
% 0.15/10.64 inference(contradiction_clause,[status(thm)],[f1041])).
% 0.15/10.64 fof(f1043,plain,(
% 0.15/10.64 $false|sQ0_spl),
% 0.15/10.64 inference(forward_subsumption_resolution,[status(thm)],[f1027,f483])).
% 0.15/10.64 fof(f1044,plain,(
% 0.15/10.64 sQ0_spl),
% 0.15/10.64 inference(contradiction_clause,[status(thm)],[f1043])).
% 0.15/10.64 fof(f1046,plain,(
% 0.15/10.64 $false|sQ1_spl),
% 0.15/10.64 inference(forward_subsumption_resolution,[status(thm)],[f1030,f514])).
% 0.15/10.64 fof(f1047,plain,(
% 0.15/10.64 sQ1_spl),
% 0.15/10.64 inference(contradiction_clause,[status(thm)],[f1046])).
% 0.15/10.64 fof(f1048,plain,(
% 0.15/10.64 $false),
% 0.15/10.64 inference(sat_refutation,[status(thm)],[f1037,f1039,f1042,f1044,f1047])).
% 0.15/10.64 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/10.67 % Elapsed time: 0.062930 seconds
% 0.15/10.67 % CPU time: 0.172151 seconds
% 0.15/10.67 % Total memory used: 75.011 MB
% 0.15/10.67 % Net memory used: 74.812 MB
%------------------------------------------------------------------------------