%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU268+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 : n013.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 6.16s 1.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU268+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.10/0.36 % Computer : n013.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:05:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 6.16/1.30 % Refutation found
% 6.16/1.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.16/1.30 % SZS output start CNFRefutation for theBenchmark
% 6.16/1.30 fof(f15,axiom,(
% 6.16/1.30 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 6.16/1.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.16/1.30 fof(f29,axiom,(
% 6.16/1.30 (! [A] :( relation(A)=> (! [B] :( is_reflexive_in(A,B)<=> (! [C] :( in(C,B)=> in(ordered_pair(C,C),A) ) )) )) )),
% 6.16/1.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.16/1.30 fof(f34,axiom,(
% 6.16/1.30 (! [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) ) ) )) ) ) )),
% 6.16/1.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.16/1.30 fof(f76,axiom,(
% 6.16/1.30 (! [A] :( relation(A)=> ( reflexive(A)<=> is_reflexive_in(A,relation_field(A)) ) ) )),
% 6.16/1.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.16/1.30 fof(f86,axiom,(
% 6.16/1.30 (! [A] : relation(inclusion_relation(A)) )),
% 6.16/1.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.16/1.30 fof(f259,conjecture,(
% 6.16/1.30 (! [A] : reflexive(inclusion_relation(A)) )),
% 6.16/1.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.16/1.30 fof(f260,negated_conjecture,(
% 6.16/1.30 ~((! [A] : reflexive(inclusion_relation(A)) ))),
% 6.16/1.30 inference(negated_conjecture,[status(cth)],[f259])).
% 6.16/1.30 fof(f386,plain,(
% 6.16/1.30 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 6.16/1.30 inference(NNF_transformation,[status(thm)],[f15])).
% 6.16/1.30 fof(f387,plain,(
% 6.16/1.30 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 6.16/1.30 inference(miniscoping,[status(thm)],[f386])).
% 6.16/1.30 fof(f388,plain,(
% 6.16/1.30 ![X0,X1]: (~X0=X1|subset(X0,X1))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f387])).
% 6.16/1.30 fof(f488,plain,(
% 6.16/1.30 ![A]: (~relation(A)|(![B]: (is_reflexive_in(A,B)<=>(![C]: (~in(C,B)|in(ordered_pair(C,C),A))))))),
% 6.16/1.30 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 6.16/1.30 fof(f489,plain,(
% 6.16/1.30 ![A]: (~relation(A)|(![B]: ((~is_reflexive_in(A,B)|(![C]: (~in(C,B)|in(ordered_pair(C,C),A))))&(is_reflexive_in(A,B)|(?[C]: (in(C,B)&~in(ordered_pair(C,C),A)))))))),
% 6.16/1.30 inference(NNF_transformation,[status(thm)],[f488])).
% 6.16/1.30 fof(f490,plain,(
% 6.16/1.30 ![A]: (~relation(A)|((![B]: (~is_reflexive_in(A,B)|(![C]: (~in(C,B)|in(ordered_pair(C,C),A)))))&(![B]: (is_reflexive_in(A,B)|(?[C]: (in(C,B)&~in(ordered_pair(C,C),A)))))))),
% 6.16/1.30 inference(miniscoping,[status(thm)],[f489])).
% 6.16/1.30 fof(f491,plain,(
% 6.16/1.30 ![A]: (~relation(A)|((![B]: (~is_reflexive_in(A,B)|(![C]: (~in(C,B)|in(ordered_pair(C,C),A)))))&(![B]: (is_reflexive_in(A,B)|(in(sK22_skl(B,A),B)&~in(ordered_pair(sK22_skl(B,A),sK22_skl(B,A)),A))))))),
% 6.16/1.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(C,sK22_skl(B,A))],[f490])).
% 6.16/1.30 fof(f493,plain,(
% 6.16/1.30 ![X0,X1]: (~relation(X0)|is_reflexive_in(X0,X1)|in(sK22_skl(X1,X0),X1))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f491])).
% 6.16/1.30 fof(f494,plain,(
% 6.16/1.30 ![X0,X1]: (~relation(X0)|is_reflexive_in(X0,X1)|~in(ordered_pair(sK22_skl(X1,X0),sK22_skl(X1,X0)),X0))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f491])).
% 6.16/1.30 fof(f528,plain,(
% 6.16/1.30 ![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)))))))),
% 6.16/1.30 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 6.16/1.30 fof(f529,plain,(
% 6.16/1.30 ![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)))))))))),
% 6.16/1.30 inference(NNF_transformation,[status(thm)],[f528])).
% 6.16/1.30 fof(f530,plain,(
% 6.16/1.30 ![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))))))))))),
% 6.16/1.30 inference(miniscoping,[status(thm)],[f529])).
% 6.16/1.30 fof(f531,plain,(
% 6.16/1.30 ![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(sK28_skl(A,B),A)&in(sK29_skl(A,B),A))&((~in(ordered_pair(sK28_skl(A,B),sK29_skl(A,B)),B)|~subset(sK28_skl(A,B),sK29_skl(A,B)))&(in(ordered_pair(sK28_skl(A,B),sK29_skl(A,B)),B)|subset(sK28_skl(A,B),sK29_skl(A,B))))))))))),
% 6.16/1.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(C,sK28_skl(A,B)),skolemize(D,sK29_skl(A,B))],[f530])).
% 6.16/1.30 fof(f532,plain,(
% 6.16/1.30 ![X0,X1]: (~relation(X0)|~X0=inclusion_relation(X1)|relation_field(X0)=X1)),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f531])).
% 6.16/1.30 fof(f534,plain,(
% 6.16/1.30 ![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))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f531])).
% 6.16/1.30 fof(f830,plain,(
% 6.16/1.30 ![A]: (~relation(A)|(reflexive(A)<=>is_reflexive_in(A,relation_field(A))))),
% 6.16/1.30 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 6.16/1.30 fof(f831,plain,(
% 6.16/1.30 ![A]: (~relation(A)|((~reflexive(A)|is_reflexive_in(A,relation_field(A)))&(reflexive(A)|~is_reflexive_in(A,relation_field(A)))))),
% 6.16/1.30 inference(NNF_transformation,[status(thm)],[f830])).
% 6.16/1.30 fof(f833,plain,(
% 6.16/1.30 ![X0]: (~relation(X0)|reflexive(X0)|~is_reflexive_in(X0,relation_field(X0)))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f831])).
% 6.16/1.30 fof(f834,plain,(
% 6.16/1.30 ![X0]: (relation(inclusion_relation(X0)))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f86])).
% 6.16/1.30 fof(f1317,plain,(
% 6.16/1.30 (?[A]: ~reflexive(inclusion_relation(A)))),
% 6.16/1.30 inference(pre_NNF_transformation,[status(thm)],[f260])).
% 6.16/1.30 fof(f1318,plain,(
% 6.16/1.30 ~reflexive(inclusion_relation(sK119_skl))),
% 6.16/1.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK119_skl]),skolemize(A,sK119_skl)],[f1317])).
% 6.16/1.30 fof(f1319,plain,(
% 6.16/1.30 ~reflexive(inclusion_relation(sK119_skl))),
% 6.16/1.30 inference(cnf_transformation,[status(thm)],[f1318])).
% 6.16/1.30 fof(f1648,plain,(
% 6.16/1.30 ![X0]: (subset(X0,X0))),
% 6.16/1.30 inference(destructive_equality_resolution,[status(thm)],[f388])).
% 6.16/1.30 fof(f1682,plain,(
% 6.16/1.30 ![X0]: (~relation(inclusion_relation(X0))|relation_field(inclusion_relation(X0))=X0)),
% 6.16/1.30 inference(destructive_equality_resolution,[status(thm)],[f532])).
% 6.16/1.30 fof(f1684,plain,(
% 6.16/1.30 ![X0,X1,X2]: (~relation(inclusion_relation(X0))|~in(X1,X0)|~in(X2,X0)|in(ordered_pair(X1,X2),inclusion_relation(X0))|~subset(X1,X2))),
% 6.16/1.30 inference(destructive_equality_resolution,[status(thm)],[f534])).
% 6.16/1.30 fof(f1754,plain,(
% 6.16/1.30 ![X0]: (relation_field(inclusion_relation(X0))=X0)),
% 6.16/1.30 inference(backward_subsumption_resolution,[status(thm)],[f1682,f834])).
% 6.16/1.30 fof(f1760,plain,(
% 6.16/1.30 ![X0,X1,X2]: (~in(X0,X1)|~in(X2,X1)|in(ordered_pair(X0,X2),inclusion_relation(X1))|~subset(X0,X2))),
% 6.16/1.30 inference(forward_subsumption_resolution,[status(thm)],[f1684,f834])).
% 6.16/1.30 fof(f1861,plain,(
% 6.16/1.30 ![X0,X1]: (~in(X0,X1)|~in(X0,X1)|in(ordered_pair(X0,X0),inclusion_relation(X1)))),
% 6.16/1.30 inference(resolution,[status(thm)],[f1648,f1760])).
% 6.16/1.30 fof(f1862,plain,(
% 6.16/1.30 ![X0,X1]: (~in(X0,X1)|in(ordered_pair(X0,X0),inclusion_relation(X1)))),
% 6.16/1.30 inference(duplicate_literals_removal,[status(thm)],[f1861])).
% 6.16/1.30 fof(f1908,plain,(
% 6.16/1.30 ![X0]: (~relation(inclusion_relation(X0))|reflexive(inclusion_relation(X0))|~is_reflexive_in(inclusion_relation(X0),X0))),
% 6.16/1.30 inference(paramodulation,[status(thm)],[f1754,f833])).
% 6.16/1.30 fof(f1909,plain,(
% 6.16/1.30 ![X0]: (reflexive(inclusion_relation(X0))|~is_reflexive_in(inclusion_relation(X0),X0))),
% 6.16/1.30 inference(forward_subsumption_resolution,[status(thm)],[f1908,f834])).
% 6.16/1.30 fof(f3535,plain,(
% 6.16/1.30 ![X0,X1]: (~relation(inclusion_relation(X0))|is_reflexive_in(inclusion_relation(X0),X1)|~in(sK22_skl(X1,inclusion_relation(X0)),X0))),
% 6.16/1.30 inference(resolution,[status(thm)],[f494,f1862])).
% 6.16/1.30 fof(f3541,plain,(
% 6.16/1.30 ![X0,X1]: (is_reflexive_in(inclusion_relation(X0),X1)|~in(sK22_skl(X1,inclusion_relation(X0)),X0))),
% 6.16/1.30 inference(forward_subsumption_resolution,[status(thm)],[f3535,f834])).
% 6.16/1.30 fof(f3543,plain,(
% 6.16/1.30 ![X0]: (is_reflexive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0))|is_reflexive_in(inclusion_relation(X0),X0))),
% 6.16/1.30 inference(resolution,[status(thm)],[f3541,f493])).
% 6.16/1.30 fof(f3548,plain,(
% 6.16/1.30 ![X0]: (is_reflexive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0)))),
% 6.16/1.30 inference(duplicate_literals_removal,[status(thm)],[f3543])).
% 6.16/1.30 fof(f3549,plain,(
% 6.16/1.30 ![X0]: (is_reflexive_in(inclusion_relation(X0),X0))),
% 6.16/1.30 inference(forward_subsumption_resolution,[status(thm)],[f3548,f834])).
% 6.16/1.30 fof(f3550,plain,(
% 6.16/1.30 ![X0]: (reflexive(inclusion_relation(X0)))),
% 6.16/1.30 inference(backward_subsumption_resolution,[status(thm)],[f1909,f3549])).
% 6.16/1.30 fof(f3554,plain,(
% 6.16/1.30 $false),
% 6.16/1.30 inference(backward_subsumption_resolution,[status(thm)],[f1319,f3550])).
% 6.16/1.30 % SZS output end CNFRefutation for theBenchmark.p
% 6.16/1.32 % Elapsed time: 0.949363 seconds
% 6.16/1.32 % CPU time: 7.057519 seconds
% 6.16/1.32 % Total memory used: 212.743 MB
% 6.16/1.32 % Net memory used: 204.358 MB
%------------------------------------------------------------------------------