%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU186+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 : n005.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:56 PM UTC 2026
% Result : Theorem 0.12s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU186+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:56:03 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.50 % Refutation found
% 0.12/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.50 fof(f1,axiom,(
% 0.12/0.50 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f8,axiom,(
% 0.12/0.50 (! [A] :( relation(A)<=> (! [B] :~ ( in(B,A)& (! [C,D] : B != ordered_pair(C,D) )) )) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f9,axiom,(
% 0.12/0.50 (! [A,B] :( ( A != empty_set=> ( B = set_meet(A)<=> (! [C] :( in(C,B)<=> (! [D] :( in(D,A)=> in(C,D) ) )) )) )& ( A = empty_set=> ( B = set_meet(A)<=> B = empty_set ) ) ) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f147,conjecture,(
% 0.12/0.50 (! [A] :( relation(A)=> ( (! [B,C] : ~ in(ordered_pair(B,C),A))=> A = empty_set ) ) )),
% 0.12/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.50 fof(f148,negated_conjecture,(
% 0.12/0.50 ~((! [A] :( relation(A)=> ( (! [B,C] : ~ in(ordered_pair(B,C),A))=> A = empty_set ) ) ))),
% 0.12/0.50 inference(negated_conjecture,[status(cth)],[f147])).
% 0.12/0.50 fof(f166,plain,(
% 0.12/0.50 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.12/0.50 fof(f167,plain,(
% 0.12/0.50 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f166])).
% 0.12/0.50 fof(f180,plain,(
% 0.12/0.50 ![A]: (relation(A)<=>(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.12/0.50 fof(f181,plain,(
% 0.12/0.50 ![A]: ((~relation(A)|(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))&(relation(A)|(?[B]: (in(B,A)&(![C,D]: ~B=ordered_pair(C,D))))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f180])).
% 0.12/0.50 fof(f182,plain,(
% 0.12/0.50 (![A]: (~relation(A)|(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D))))))&(![A]: (relation(A)|(?[B]: (in(B,A)&(![C,D]: ~B=ordered_pair(C,D))))))),
% 0.12/0.50 inference(miniscoping,[status(thm)],[f181])).
% 0.12/0.50 fof(f183,plain,(
% 0.12/0.50 (![A]: (~relation(A)|(![B]: (~in(B,A)|B=ordered_pair(sK0_skl(B,A),sK1_skl(B,A))))))&(![A]: (relation(A)|(in(sK2_skl(A),A)&(![C,D]: ~sK2_skl(A)=ordered_pair(C,D)))))),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A)),skolemize(B,sK2_skl(A))],[f182])).
% 0.12/0.50 fof(f184,plain,(
% 0.12/0.50 ![X0,X1]: (~relation(X0)|~in(X1,X0)|X1=ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f183])).
% 0.12/0.50 fof(f187,plain,(
% 0.12/0.50 ![A,B]: ((A=empty_set|(B=set_meet(A)<=>(![C]: (in(C,B)<=>(![D]: (~in(D,A)|in(C,D)))))))&(~A=empty_set|(B=set_meet(A)<=>B=empty_set)))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.12/0.50 fof(f188,plain,(
% 0.12/0.50 ![A,B]: ((A=empty_set|((~B=set_meet(A)|(![C]: ((~in(C,B)|(![D]: (~in(D,A)|in(C,D))))&(in(C,B)|(?[D]: (in(D,A)&~in(C,D)))))))&(B=set_meet(A)|(?[C]: ((~in(C,B)|(?[D]: (in(D,A)&~in(C,D))))&(in(C,B)|(![D]: (~in(D,A)|in(C,D)))))))))&(~A=empty_set|((~B=set_meet(A)|B=empty_set)&(B=set_meet(A)|~B=empty_set))))),
% 0.12/0.50 inference(NNF_transformation,[status(thm)],[f187])).
% 0.12/0.50 fof(f189,plain,(
% 0.12/0.50 (![A]: (A=empty_set|((![B]: (~B=set_meet(A)|((![C]: (~in(C,B)|(![D]: (~in(D,A)|in(C,D)))))&(![C]: (in(C,B)|(?[D]: (in(D,A)&~in(C,D))))))))&(![B]: (B=set_meet(A)|(?[C]: ((~in(C,B)|(?[D]: (in(D,A)&~in(C,D))))&(in(C,B)|(![D]: (~in(D,A)|in(C,D)))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 0.12/0.50 inference(miniscoping,[status(thm)],[f188])).
% 0.12/0.50 fof(f190,plain,(
% 0.12/0.50 (![A]: (A=empty_set|((![B]: (~B=set_meet(A)|((![C]: (~in(C,B)|(![D]: (~in(D,A)|in(C,D)))))&(![C]: (in(C,B)|(in(sK3_skl(C,B,A),A)&~in(C,sK3_skl(C,B,A))))))))&(![B]: (B=set_meet(A)|((~in(sK4_skl(B,A),B)|(in(sK5_skl(B,A),A)&~in(sK4_skl(B,A),sK5_skl(B,A))))&(in(sK4_skl(B,A),B)|(![D]: (~in(D,A)|in(sK4_skl(B,A),D))))))))))&(![A]: (~A=empty_set|((![B]: (~B=set_meet(A)|B=empty_set))&(![B]: (B=set_meet(A)|~B=empty_set)))))),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(D,sK3_skl(C,B,A)),skolemize(C,sK4_skl(B,A)),skolemize(D,sK5_skl(B,A))],[f189])).
% 0.12/0.50 fof(f192,plain,(
% 0.12/0.50 ![X0,X1,X2]: (X0=empty_set|~X1=set_meet(X0)|in(X2,X1)|in(sK3_skl(X2,X1,X0),X0))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f190])).
% 0.12/0.50 fof(f592,plain,(
% 0.12/0.50 (?[A]: (relation(A)&((![B,C]: ~in(ordered_pair(B,C),A))&~A=empty_set)))),
% 0.12/0.50 inference(pre_NNF_transformation,[status(thm)],[f148])).
% 0.12/0.50 fof(f593,plain,(
% 0.12/0.50 (relation(sK47_skl)&((![B,C]: ~in(ordered_pair(B,C),sK47_skl))&~sK47_skl=empty_set))),
% 0.12/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl]),skolemize(A,sK47_skl)],[f592])).
% 0.12/0.50 fof(f594,plain,(
% 0.12/0.50 relation(sK47_skl)),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f593])).
% 0.12/0.50 fof(f595,plain,(
% 0.12/0.50 ![X0,X1]: (~in(ordered_pair(X0,X1),sK47_skl))),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f593])).
% 0.12/0.50 fof(f596,plain,(
% 0.12/0.50 ~sK47_skl=empty_set),
% 0.12/0.50 inference(cnf_transformation,[status(thm)],[f593])).
% 0.12/0.50 fof(f653,plain,(
% 0.12/0.50 ![X0,X1]: (X0=empty_set|in(X1,set_meet(X0))|in(sK3_skl(X1,set_meet(X0),X0),X0))),
% 0.12/0.50 inference(destructive_equality_resolution,[status(thm)],[f192])).
% 0.12/0.50 fof(f743,plain,(
% 0.12/0.50 ![X0]: (~in(X0,sK47_skl)|X0=ordered_pair(sK0_skl(X0,sK47_skl),sK1_skl(X0,sK47_skl)))),
% 0.12/0.50 inference(resolution,[status(thm)],[f184,f594])).
% 0.12/0.50 fof(f760,plain,(
% 0.12/0.50 ![X0]: (sK47_skl=empty_set|in(X0,set_meet(sK47_skl))|sK3_skl(X0,set_meet(sK47_skl),sK47_skl)=ordered_pair(sK0_skl(sK3_skl(X0,set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(X0,set_meet(sK47_skl),sK47_skl),sK47_skl)))),
% 0.12/0.50 inference(resolution,[status(thm)],[f653,f743])).
% 0.12/0.50 fof(f763,plain,(
% 0.12/0.50 ![X0]: (in(X0,set_meet(sK47_skl))|sK3_skl(X0,set_meet(sK47_skl),sK47_skl)=ordered_pair(sK0_skl(sK3_skl(X0,set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(X0,set_meet(sK47_skl),sK47_skl),sK47_skl)))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f760,f596])).
% 0.12/0.50 fof(f787,plain,(
% 0.12/0.50 ![X0]: (sK3_skl(X0,set_meet(sK47_skl),sK47_skl)=ordered_pair(sK0_skl(sK3_skl(X0,set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(X0,set_meet(sK47_skl),sK47_skl),sK47_skl))|~in(set_meet(sK47_skl),X0))),
% 0.12/0.50 inference(resolution,[status(thm)],[f763,f167])).
% 0.12/0.50 fof(f789,plain,(
% 0.12/0.50 sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl)=ordered_pair(sK0_skl(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl))|sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl)=ordered_pair(sK0_skl(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl))),
% 0.12/0.50 inference(resolution,[status(thm)],[f787,f763])).
% 0.12/0.50 fof(f795,plain,(
% 0.12/0.50 sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl)=ordered_pair(sK0_skl(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl),sK1_skl(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl))),
% 0.12/0.50 inference(duplicate_literals_removal,[status(thm)],[f789])).
% 0.12/0.50 fof(f810,plain,(
% 0.12/0.50 ~in(sK3_skl(set_meet(sK47_skl),set_meet(sK47_skl),sK47_skl),sK47_skl)),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f795,f595])).
% 0.12/0.50 fof(f811,plain,(
% 0.12/0.50 sK47_skl=empty_set|in(set_meet(sK47_skl),set_meet(sK47_skl))),
% 0.12/0.50 inference(resolution,[status(thm)],[f810,f653])).
% 0.12/0.50 fof(f812,plain,(
% 0.12/0.50 in(set_meet(sK47_skl),set_meet(sK47_skl))),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f811,f596])).
% 0.12/0.50 fof(f864,plain,(
% 0.12/0.50 ~in(set_meet(sK47_skl),set_meet(sK47_skl))),
% 0.12/0.50 inference(resolution,[status(thm)],[f812,f167])).
% 0.12/0.50 fof(f866,plain,(
% 0.12/0.50 $false),
% 0.12/0.50 inference(forward_subsumption_resolution,[status(thm)],[f864,f812])).
% 0.12/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.52 % Elapsed time: 0.158501 seconds
% 0.12/0.52 % CPU time: 0.883647 seconds
% 0.12/0.52 % Total memory used: 123.442 MB
% 0.12/0.52 % Net memory used: 121.778 MB
%------------------------------------------------------------------------------