%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU180+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:21:55 PM UTC 2026
% Result : Theorem 5.92s 1.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU180+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 05:54:51 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 5.92/1.24 % Refutation found
% 5.92/1.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.92/1.24 % SZS output start CNFRefutation for theBenchmark
% 5.92/1.24 fof(f4,axiom,(
% 5.92/1.24 (! [A,B] : set_union2(A,B) = set_union2(B,A) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f14,axiom,(
% 5.92/1.24 (! [A,B,C] :( C = set_union2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)| in(D,B) ) ) )) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f16,axiom,(
% 5.92/1.24 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f18,axiom,(
% 5.92/1.24 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f22,axiom,(
% 5.92/1.24 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f25,axiom,(
% 5.92/1.24 (! [A] :( relation(A)=> relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f91,lemma,(
% 5.92/1.24 (! [A,B] :( subset(A,B)=> set_union2(A,B) = B ) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f108,conjecture,(
% 5.92/1.24 (! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_field(C))& in(B,relation_field(C)) ) ) ) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f109,negated_conjecture,(
% 5.92/1.24 ~((! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_field(C))& in(B,relation_field(C)) ) ) ) ))),
% 5.92/1.24 inference(negated_conjecture,[status(cth)],[f108])).
% 5.92/1.24 fof(f143,lemma,(
% 5.92/1.24 (! [A,B] : subset(A,set_union2(A,B)) )),
% 5.92/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.92/1.24 fof(f157,plain,(
% 5.92/1.24 ![X0,X1]: (set_union2(X0,X1)=set_union2(X1,X0))),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f4])).
% 5.92/1.24 fof(f218,plain,(
% 5.92/1.24 ![A,B,C]: ((~C=set_union2(A,B)|(![D]: ((~in(D,C)|(in(D,A)|in(D,B)))&(in(D,C)|(~in(D,A)&~in(D,B))))))&(C=set_union2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))))),
% 5.92/1.24 inference(NNF_transformation,[status(thm)],[f14])).
% 5.92/1.24 fof(f219,plain,(
% 5.92/1.24 (![A,B,C]: (~C=set_union2(A,B)|((![D]: (~in(D,C)|(in(D,A)|in(D,B))))&(![D]: (in(D,C)|(~in(D,A)&~in(D,B)))))))&(![A,B,C]: (C=set_union2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))))),
% 5.92/1.24 inference(miniscoping,[status(thm)],[f218])).
% 5.92/1.24 fof(f220,plain,(
% 5.92/1.24 (![A,B,C]: (~C=set_union2(A,B)|((![D]: (~in(D,C)|(in(D,A)|in(D,B))))&(![D]: (in(D,C)|(~in(D,A)&~in(D,B)))))))&(![A,B,C]: (C=set_union2(A,B)|((~in(sK10_skl(C,B,A),C)|(~in(sK10_skl(C,B,A),A)&~in(sK10_skl(C,B,A),B)))&(in(sK10_skl(C,B,A),C)|(in(sK10_skl(C,B,A),A)|in(sK10_skl(C,B,A),B))))))),
% 5.92/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(D,sK10_skl(C,B,A))],[f219])).
% 5.92/1.24 fof(f223,plain,(
% 5.92/1.24 ![X0,X1,X2,X3]: (~X0=set_union2(X1,X2)|in(X3,X0)|~in(X3,X2))),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f220])).
% 5.92/1.24 fof(f236,plain,(
% 5.92/1.24 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 5.92/1.24 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 5.92/1.24 fof(f237,plain,(
% 5.92/1.24 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 5.92/1.24 inference(NNF_transformation,[status(thm)],[f236])).
% 5.92/1.24 fof(f238,plain,(
% 5.92/1.24 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 5.92/1.24 inference(miniscoping,[status(thm)],[f237])).
% 5.92/1.24 fof(f239,plain,(
% 5.92/1.24 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK16_skl(B,A),A)&~in(sK16_skl(B,A),B))))),
% 5.92/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(C,sK16_skl(B,A))],[f238])).
% 5.92/1.24 fof(f240,plain,(
% 5.92/1.24 ![X0,X1,X2]: (~subset(X0,X1)|~in(X2,X0)|in(X2,X1))),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f239])).
% 5.92/1.24 fof(f252,plain,(
% 5.92/1.24 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 5.92/1.24 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 5.92/1.24 fof(f253,plain,(
% 5.92/1.24 ![A]: (~relation(A)|(![B]: ((~B=relation_dom(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(C,D),A)))&(in(C,B)|(![D]: ~in(ordered_pair(C,D),A))))))&(B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 5.92/1.24 inference(NNF_transformation,[status(thm)],[f252])).
% 5.92/1.24 fof(f254,plain,(
% 5.92/1.24 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(C,D),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 5.92/1.24 inference(miniscoping,[status(thm)],[f253])).
% 5.92/1.24 fof(f255,plain,(
% 5.92/1.24 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|in(ordered_pair(C,sK18_skl(C,B,A)),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|((~in(sK19_skl(B,A),B)|(![D]: ~in(ordered_pair(sK19_skl(B,A),D),A)))&(in(sK19_skl(B,A),B)|in(ordered_pair(sK19_skl(B,A),sK20_skl(B,A)),A)))))))),
% 5.92/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(D,sK18_skl(C,B,A)),skolemize(C,sK19_skl(B,A)),skolemize(D,sK20_skl(B,A))],[f254])).
% 5.92/1.24 fof(f257,plain,(
% 5.92/1.24 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f255])).
% 5.92/1.24 fof(f279,plain,(
% 5.92/1.24 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 5.92/1.24 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 5.92/1.24 fof(f280,plain,(
% 5.92/1.24 ![A]: (~relation(A)|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(D,C),A)))&(in(C,B)|(![D]: ~in(ordered_pair(D,C),A))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 5.92/1.24 inference(NNF_transformation,[status(thm)],[f279])).
% 5.92/1.24 fof(f281,plain,(
% 5.92/1.24 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(D,C),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 5.92/1.24 inference(miniscoping,[status(thm)],[f280])).
% 5.92/1.24 fof(f282,plain,(
% 5.92/1.24 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|in(ordered_pair(sK25_skl(C,B,A),C),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|((~in(sK26_skl(B,A),B)|(![D]: ~in(ordered_pair(D,sK26_skl(B,A)),A)))&(in(sK26_skl(B,A),B)|in(ordered_pair(sK27_skl(B,A),sK26_skl(B,A)),A)))))))),
% 5.92/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl,sK27_skl]),skolemize(D,sK25_skl(C,B,A)),skolemize(C,sK26_skl(B,A)),skolemize(D,sK27_skl(B,A))],[f281])).
% 5.92/1.24 fof(f284,plain,(
% 5.92/1.24 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f282])).
% 5.92/1.24 fof(f290,plain,(
% 5.92/1.24 ![A]: (~relation(A)|relation_field(A)=set_union2(relation_dom(A),relation_rng(A)))),
% 5.92/1.24 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 5.92/1.24 fof(f291,plain,(
% 5.92/1.24 ![X0]: (~relation(X0)|relation_field(X0)=set_union2(relation_dom(X0),relation_rng(X0)))),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f290])).
% 5.92/1.24 fof(f421,plain,(
% 5.92/1.24 ![A,B]: (~subset(A,B)|set_union2(A,B)=B)),
% 5.92/1.24 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 5.92/1.24 fof(f422,plain,(
% 5.92/1.24 ![X0,X1]: (~subset(X0,X1)|set_union2(X0,X1)=X1)),
% 5.92/1.24 inference(cnf_transformation,[status(thm)],[f421])).
% 5.92/1.24 fof(f463,plain,(
% 5.92/1.24 (?[A,B,C]: (relation(C)&(in(ordered_pair(A,B),C)&(~in(A,relation_field(C))|~in(B,relation_field(C))))))),
% 5.92/1.24 inference(pre_NNF_transformation,[status(thm)],[f109])).
% 5.92/1.24 fof(f464,plain,(
% 5.92/1.24 ?[C]: (relation(C)&(?[A,B]: (in(ordered_pair(A,B),C)&(~in(A,relation_field(C))|~in(B,relation_field(C))))))),
% 5.92/1.24 inference(miniscoping,[status(thm)],[f463])).
% 5.92/1.24 fof(f465,plain,(
% 5.92/1.24 (relation(sK38_skl)&(in(ordered_pair(sK39_skl,sK40_skl),sK38_skl)&(~in(sK39_skl,relation_field(sK38_skl))|~in(sK40_skl,relation_field(sK38_skl)))))),
% 5.92/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl,sK40_skl]),skolemize(C,sK38_skl),skolemize(A,sK39_skl),skolemize(B,sK40_skl)],[f464])).
% 5.92/1.25 fof(f466,plain,(
% 5.92/1.25 relation(sK38_skl)),
% 5.92/1.25 inference(cnf_transformation,[status(thm)],[f465])).
% 5.92/1.25 fof(f467,plain,(
% 5.92/1.25 in(ordered_pair(sK39_skl,sK40_skl),sK38_skl)),
% 5.92/1.25 inference(cnf_transformation,[status(thm)],[f465])).
% 5.92/1.25 fof(f468,plain,(
% 5.92/1.25 ~in(sK39_skl,relation_field(sK38_skl))|~in(sK40_skl,relation_field(sK38_skl))),
% 5.92/1.25 inference(cnf_transformation,[status(thm)],[f465])).
% 5.92/1.25 fof(f558,plain,(
% 5.92/1.25 ![X0,X1]: (subset(X0,set_union2(X0,X1)))),
% 5.92/1.25 inference(cnf_transformation,[status(thm)],[f143])).
% 5.92/1.25 fof(f608,plain,(
% 5.92/1.25 ![X0,X1,X2]: (in(X0,set_union2(X1,X2))|~in(X0,X2))),
% 5.92/1.25 inference(destructive_equality_resolution,[status(thm)],[f223])).
% 5.92/1.25 fof(f615,plain,(
% 5.92/1.25 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 5.92/1.25 inference(destructive_equality_resolution,[status(thm)],[f257])).
% 5.92/1.25 fof(f623,plain,(
% 5.92/1.25 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 5.92/1.25 inference(destructive_equality_resolution,[status(thm)],[f284])).
% 5.92/1.25 fof(f635,plain,(
% 5.92/1.25 relation_field(sK38_skl)=set_union2(relation_dom(sK38_skl),relation_rng(sK38_skl))),
% 5.92/1.25 inference(resolution,[status(thm)],[f291,f466])).
% 5.92/1.25 fof(f641,plain,(
% 5.92/1.25 relation_field(sK38_skl)=set_union2(relation_rng(sK38_skl),relation_dom(sK38_skl))),
% 5.92/1.25 inference(paramodulation,[status(thm)],[f635,f157])).
% 5.92/1.25 fof(f784,plain,(
% 5.92/1.25 subset(relation_rng(sK38_skl),relation_field(sK38_skl))),
% 5.92/1.25 inference(paramodulation,[status(thm)],[f641,f558])).
% 5.92/1.25 fof(f786,plain,(
% 5.92/1.25 subset(relation_dom(sK38_skl),relation_field(sK38_skl))),
% 5.92/1.25 inference(paramodulation,[status(thm)],[f635,f558])).
% 5.92/1.25 fof(f1149,plain,(
% 5.92/1.25 set_union2(relation_dom(sK38_skl),relation_field(sK38_skl))=relation_field(sK38_skl)),
% 5.92/1.25 inference(resolution,[status(thm)],[f422,f786])).
% 5.92/1.25 fof(f1237,plain,(
% 5.92/1.25 set_union2(relation_field(sK38_skl),relation_dom(sK38_skl))=relation_field(sK38_skl)),
% 5.92/1.25 inference(paramodulation,[status(thm)],[f157,f1149])).
% 5.92/1.25 fof(f3983,plain,(
% 5.92/1.25 ~relation(sK38_skl)|in(sK39_skl,relation_dom(sK38_skl))),
% 5.92/1.25 inference(resolution,[status(thm)],[f615,f467])).
% 5.92/1.25 fof(f4001,plain,(
% 5.92/1.25 in(sK39_skl,relation_dom(sK38_skl))),
% 5.92/1.25 inference(forward_subsumption_resolution,[status(thm)],[f3983,f466])).
% 5.92/1.25 fof(f4012,plain,(
% 5.92/1.25 ![X0]: (in(sK39_skl,set_union2(X0,relation_dom(sK38_skl))))),
% 5.92/1.25 inference(resolution,[status(thm)],[f4001,f608])).
% 5.92/1.25 fof(f4650,plain,(
% 5.92/1.25 in(sK39_skl,relation_field(sK38_skl))),
% 5.92/1.25 inference(paramodulation,[status(thm)],[f1237,f4012])).
% 5.92/1.25 fof(f4659,plain,(
% 5.92/1.25 ~in(sK40_skl,relation_field(sK38_skl))),
% 5.92/1.25 inference(backward_subsumption_resolution,[status(thm)],[f468,f4650])).
% 5.92/1.25 fof(f4676,plain,(
% 5.92/1.25 ![X0]: (~subset(X0,relation_field(sK38_skl))|~in(sK40_skl,X0))),
% 5.92/1.25 inference(resolution,[status(thm)],[f4659,f240])).
% 5.92/1.25 fof(f4681,plain,(
% 5.92/1.25 ~in(sK40_skl,relation_rng(sK38_skl))),
% 5.92/1.25 inference(resolution,[status(thm)],[f4676,f784])).
% 5.92/1.25 fof(f5479,plain,(
% 5.92/1.25 ~relation(sK38_skl)|in(sK40_skl,relation_rng(sK38_skl))),
% 5.92/1.25 inference(resolution,[status(thm)],[f623,f467])).
% 5.92/1.25 fof(f5498,plain,(
% 5.92/1.25 in(sK40_skl,relation_rng(sK38_skl))),
% 5.92/1.25 inference(forward_subsumption_resolution,[status(thm)],[f5479,f466])).
% 5.92/1.25 fof(f5500,plain,(
% 5.92/1.25 $false),
% 5.92/1.25 inference(forward_subsumption_resolution,[status(thm)],[f5498,f4681])).
% 5.92/1.25 % SZS output end CNFRefutation for theBenchmark.p
% 5.92/1.27 % Elapsed time: 0.958436 seconds
% 5.92/1.27 % CPU time: 7.285788 seconds
% 5.92/1.27 % Total memory used: 194.544 MB
% 5.92/1.27 % Net memory used: 182.920 MB
%------------------------------------------------------------------------------