%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU271+1 : 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 : n014.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:11 PM UTC 2026
% Result : Theorem 0.17s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU271+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n014.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 06:05:04 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.17/0.52 % Refutation found
% 0.17/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.52 fof(f9,axiom,(
% 0.17/0.52 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 0.17/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f10,axiom,(
% 0.17/0.52 (! [A] :( relation(A)=> ( antisymmetric(A)<=> is_antisymmetric_in(A,relation_field(A)) ) ) )),
% 0.17/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f11,axiom,(
% 0.17/0.52 (! [A,B] :( relation(B)=> ( B = inclusion_relation(A)<=> ( relation_field(B) = A& (! [C,D] :( ( in(C,A)& in(D,A) )=> ( in(ordered_pair(C,D),B)<=> subset(C,D) ) ) )) ) ) )),
% 0.17/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f12,axiom,(
% 0.17/0.52 (! [A] :( relation(A)=> (! [B] :( is_antisymmetric_in(A,B)<=> (! [C,D] :( ( in(C,B)& in(D,B)& in(ordered_pair(C,D),A)& in(ordered_pair(D,C),A) )=> C = D ) )) )) )),
% 0.17/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f17,axiom,(
% 0.17/0.52 (! [A] : relation(inclusion_relation(A)) )),
% 0.17/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f49,conjecture,(
% 0.17/0.52 (! [A] : antisymmetric(inclusion_relation(A)) )),
% 0.17/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.52 fof(f50,negated_conjecture,(
% 0.17/0.52 ~((! [A] : antisymmetric(inclusion_relation(A)) ))),
% 0.17/0.52 inference(negated_conjecture,[status(cth)],[f49])).
% 0.17/0.52 fof(f73,plain,(
% 0.17/0.52 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 0.17/0.52 inference(NNF_transformation,[status(thm)],[f9])).
% 0.17/0.52 fof(f74,plain,(
% 0.17/0.52 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f73])).
% 0.17/0.52 fof(f77,plain,(
% 0.17/0.52 ![X0,X1]: (X0=X1|~subset(X0,X1)|~subset(X1,X0))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f74])).
% 0.17/0.52 fof(f78,plain,(
% 0.17/0.52 ![A]: (~relation(A)|(antisymmetric(A)<=>is_antisymmetric_in(A,relation_field(A))))),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.17/0.52 fof(f79,plain,(
% 0.17/0.52 ![A]: (~relation(A)|((~antisymmetric(A)|is_antisymmetric_in(A,relation_field(A)))&(antisymmetric(A)|~is_antisymmetric_in(A,relation_field(A)))))),
% 0.17/0.52 inference(NNF_transformation,[status(thm)],[f78])).
% 0.17/0.52 fof(f81,plain,(
% 0.17/0.52 ![X0]: (~relation(X0)|antisymmetric(X0)|~is_antisymmetric_in(X0,relation_field(X0)))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.17/0.52 fof(f82,plain,(
% 0.17/0.52 ![A,B]: (~relation(B)|(B=inclusion_relation(A)<=>(relation_field(B)=A&(![C,D]: ((~in(C,A)|~in(D,A))|(in(ordered_pair(C,D),B)<=>subset(C,D)))))))),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.17/0.52 fof(f83,plain,(
% 0.17/0.52 ![A,B]: (~relation(B)|((~B=inclusion_relation(A)|(relation_field(B)=A&(![C,D]: ((~in(C,A)|~in(D,A))|((~in(ordered_pair(C,D),B)|subset(C,D))&(in(ordered_pair(C,D),B)|~subset(C,D)))))))&(B=inclusion_relation(A)|(~relation_field(B)=A|(?[C,D]: ((in(C,A)&in(D,A))&((~in(ordered_pair(C,D),B)|~subset(C,D))&(in(ordered_pair(C,D),B)|subset(C,D)))))))))),
% 0.17/0.52 inference(NNF_transformation,[status(thm)],[f82])).
% 0.17/0.52 fof(f84,plain,(
% 0.17/0.52 ![B]: (~relation(B)|((![A]: (~B=inclusion_relation(A)|(relation_field(B)=A&(![C,D]: ((~in(C,A)|~in(D,A))|((~in(ordered_pair(C,D),B)|subset(C,D))&(in(ordered_pair(C,D),B)|~subset(C,D))))))))&(![A]: (B=inclusion_relation(A)|(~relation_field(B)=A|(?[C,D]: ((in(C,A)&in(D,A))&((~in(ordered_pair(C,D),B)|~subset(C,D))&(in(ordered_pair(C,D),B)|subset(C,D))))))))))),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f83])).
% 0.17/0.52 fof(f85,plain,(
% 0.17/0.52 ![B]: (~relation(B)|((![A]: (~B=inclusion_relation(A)|(relation_field(B)=A&(![C,D]: ((~in(C,A)|~in(D,A))|((~in(ordered_pair(C,D),B)|subset(C,D))&(in(ordered_pair(C,D),B)|~subset(C,D))))))))&(![A]: (B=inclusion_relation(A)|(~relation_field(B)=A|((in(sK0_skl(A,B),A)&in(sK1_skl(A,B),A))&((~in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B)|~subset(sK0_skl(A,B),sK1_skl(A,B)))&(in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B)|subset(sK0_skl(A,B),sK1_skl(A,B))))))))))),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f84])).
% 0.17/0.52 fof(f86,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(X0)|~X0=inclusion_relation(X1)|relation_field(X0)=X1)),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f85])).
% 0.17/0.52 fof(f87,plain,(
% 0.17/0.52 ![X0,X1,X2,X3]: (~relation(X0)|~X0=inclusion_relation(X1)|~in(X2,X1)|~in(X3,X1)|~in(ordered_pair(X2,X3),X0)|subset(X2,X3))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f85])).
% 0.17/0.52 fof(f93,plain,(
% 0.17/0.52 ![A]: (~relation(A)|(![B]: (is_antisymmetric_in(A,B)<=>(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D)))))),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.17/0.52 fof(f94,plain,(
% 0.17/0.52 ![A]: (~relation(A)|(![B]: ((~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D)))&(is_antisymmetric_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,C),A))&~C=D))))))),
% 0.17/0.52 inference(NNF_transformation,[status(thm)],[f93])).
% 0.17/0.52 fof(f95,plain,(
% 0.17/0.52 ![A]: (~relation(A)|((![B]: (~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D))))&(![B]: (is_antisymmetric_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,C),A))&~C=D))))))),
% 0.17/0.52 inference(miniscoping,[status(thm)],[f94])).
% 0.17/0.52 fof(f96,plain,(
% 0.17/0.52 ![A]: (~relation(A)|((![B]: (~is_antisymmetric_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,C),A))|C=D))))&(![B]: (is_antisymmetric_in(A,B)|((((in(sK2_skl(B,A),B)&in(sK3_skl(B,A),B))&in(ordered_pair(sK2_skl(B,A),sK3_skl(B,A)),A))&in(ordered_pair(sK3_skl(B,A),sK2_skl(B,A)),A))&~sK2_skl(B,A)=sK3_skl(B,A))))))),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f95])).
% 0.17/0.52 fof(f98,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(X0)|is_antisymmetric_in(X0,X1)|in(sK2_skl(X1,X0),X1))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f96])).
% 0.17/0.52 fof(f99,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(X0)|is_antisymmetric_in(X0,X1)|in(sK3_skl(X1,X0),X1))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f96])).
% 0.17/0.52 fof(f100,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(X0)|is_antisymmetric_in(X0,X1)|in(ordered_pair(sK2_skl(X1,X0),sK3_skl(X1,X0)),X0))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f96])).
% 0.17/0.52 fof(f101,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(X0)|is_antisymmetric_in(X0,X1)|in(ordered_pair(sK3_skl(X1,X0),sK2_skl(X1,X0)),X0))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f96])).
% 0.17/0.52 fof(f102,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(X0)|is_antisymmetric_in(X0,X1)|~sK2_skl(X1,X0)=sK3_skl(X1,X0))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f96])).
% 0.17/0.52 fof(f106,plain,(
% 0.17/0.52 ![X0]: (relation(inclusion_relation(X0)))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f17])).
% 0.17/0.52 fof(f180,plain,(
% 0.17/0.52 (?[A]: ~antisymmetric(inclusion_relation(A)))),
% 0.17/0.52 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.17/0.52 fof(f181,plain,(
% 0.17/0.52 ~antisymmetric(inclusion_relation(sK14_skl))),
% 0.17/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f180])).
% 0.17/0.52 fof(f182,plain,(
% 0.17/0.52 ~antisymmetric(inclusion_relation(sK14_skl))),
% 0.17/0.52 inference(cnf_transformation,[status(thm)],[f181])).
% 0.17/0.52 fof(f194,plain,(
% 0.17/0.52 ![X0]: (~relation(inclusion_relation(X0))|relation_field(inclusion_relation(X0))=X0)),
% 0.17/0.52 inference(destructive_equality_resolution,[status(thm)],[f86])).
% 0.17/0.52 fof(f195,plain,(
% 0.17/0.52 ![X0,X1,X2]: (~relation(inclusion_relation(X0))|~in(X1,X0)|~in(X2,X0)|~in(ordered_pair(X1,X2),inclusion_relation(X0))|subset(X1,X2))),
% 0.17/0.52 inference(destructive_equality_resolution,[status(thm)],[f87])).
% 0.17/0.52 fof(f202,plain,(
% 0.17/0.52 ![X0,X1,X2]: (~in(X0,X1)|~in(X2,X1)|~in(ordered_pair(X0,X2),inclusion_relation(X1))|subset(X0,X2))),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f195,f106])).
% 0.17/0.52 fof(f203,plain,(
% 0.17/0.52 ![X0]: (relation_field(inclusion_relation(X0))=X0)),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f194,f106])).
% 0.17/0.52 fof(f206,plain,(
% 0.17/0.52 ![X0]: (antisymmetric(inclusion_relation(X0))|~is_antisymmetric_in(inclusion_relation(X0),relation_field(inclusion_relation(X0))))),
% 0.17/0.52 inference(resolution,[status(thm)],[f81,f106])).
% 0.17/0.52 fof(f207,plain,(
% 0.17/0.52 ![X0]: (antisymmetric(inclusion_relation(X0))|~is_antisymmetric_in(inclusion_relation(X0),X0))),
% 0.17/0.52 inference(forward_demodulation,[status(thm)],[f203,f206])).
% 0.17/0.52 fof(f252,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(inclusion_relation(X0))|is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|subset(sK2_skl(X1,inclusion_relation(X0)),sK3_skl(X1,inclusion_relation(X0))))),
% 0.17/0.52 inference(resolution,[status(thm)],[f100,f202])).
% 0.17/0.52 fof(f254,plain,(
% 0.17/0.52 ![X0,X1]: (is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|subset(sK2_skl(X1,inclusion_relation(X0)),sK3_skl(X1,inclusion_relation(X0))))),
% 0.17/0.52 inference(forward_subsumption_resolution,[status(thm)],[f252,f106])).
% 0.17/0.52 fof(f256,plain,(
% 0.17/0.52 ![X0,X1]: (is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|sK3_skl(X1,inclusion_relation(X0))=sK2_skl(X1,inclusion_relation(X0))|~subset(sK3_skl(X1,inclusion_relation(X0)),sK2_skl(X1,inclusion_relation(X0))))),
% 0.17/0.52 inference(resolution,[status(thm)],[f254,f77])).
% 0.17/0.52 fof(f263,plain,(
% 0.17/0.52 ![X0,X1]: (~relation(inclusion_relation(X0))|is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|subset(sK3_skl(X1,inclusion_relation(X0)),sK2_skl(X1,inclusion_relation(X0))))),
% 0.17/0.52 inference(resolution,[status(thm)],[f101,f202])).
% 0.17/0.52 fof(f265,plain,(
% 0.17/0.52 ![X0,X1]: (is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|sK3_skl(X1,inclusion_relation(X0))=sK2_skl(X1,inclusion_relation(X0)))),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f256,f266])).
% 0.17/0.52 fof(f266,plain,(
% 0.17/0.52 ![X0,X1]: (is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|subset(sK3_skl(X1,inclusion_relation(X0)),sK2_skl(X1,inclusion_relation(X0))))),
% 0.17/0.52 inference(forward_subsumption_resolution,[status(thm)],[f263,f106])).
% 0.17/0.52 fof(f302,plain,(
% 0.17/0.52 ![X0,X1]: (is_antisymmetric_in(inclusion_relation(X0),X1)|~sK2_skl(X1,inclusion_relation(X0))=sK3_skl(X1,inclusion_relation(X0)))),
% 0.17/0.52 inference(resolution,[status(thm)],[f102,f106])).
% 0.17/0.52 fof(f303,plain,(
% 0.17/0.52 ![X0,X1]: (is_antisymmetric_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0))),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f265,f302])).
% 0.17/0.52 fof(f320,plain,(
% 0.17/0.52 ![X0]: (is_antisymmetric_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0))|is_antisymmetric_in(inclusion_relation(X0),X0))),
% 0.17/0.52 inference(resolution,[status(thm)],[f303,f99])).
% 0.17/0.52 fof(f321,plain,(
% 0.17/0.52 ![X0]: (is_antisymmetric_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0)))),
% 0.17/0.52 inference(duplicate_literals_removal,[status(thm)],[f320])).
% 0.17/0.52 fof(f322,plain,(
% 0.17/0.52 ![X0]: (is_antisymmetric_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0)))),
% 0.17/0.52 inference(forward_subsumption_resolution,[status(thm)],[f321,f98])).
% 0.17/0.52 fof(f323,plain,(
% 0.17/0.52 ![X0]: (is_antisymmetric_in(inclusion_relation(X0),X0))),
% 0.17/0.52 inference(resolution,[status(thm)],[f322,f106])).
% 0.17/0.52 fof(f324,plain,(
% 0.17/0.52 ![X0]: (antisymmetric(inclusion_relation(X0)))),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f207,f323])).
% 0.17/0.52 fof(f326,plain,(
% 0.17/0.52 $false),
% 0.17/0.52 inference(backward_subsumption_resolution,[status(thm)],[f182,f324])).
% 0.17/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.54 % Elapsed time: 0.078956 seconds
% 0.17/0.54 % CPU time: 0.144582 seconds
% 0.17/0.54 % Total memory used: 36.569 MB
% 0.17/0.54 % Net memory used: 36.504 MB
%------------------------------------------------------------------------------