%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU268+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.14s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU268+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n014.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 06:05:19 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.44 % Drodi V4.1.1
% 0.14/0.46 % Refutation found
% 0.14/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.46 fof(f9,axiom,(
% 0.14/0.46 (! [A] :( relation(A)=> (! [B] :( is_reflexive_in(A,B)<=> (! [C] :( in(C,B)=> in(ordered_pair(C,C),A) ) )) )) )),
% 0.14/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.46 fof(f10,axiom,(
% 0.14/0.46 (! [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.14/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.46 fof(f13,axiom,(
% 0.14/0.46 (! [A] :( relation(A)=> ( reflexive(A)<=> is_reflexive_in(A,relation_field(A)) ) ) )),
% 0.14/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.46 fof(f16,axiom,(
% 0.14/0.46 (! [A] : relation(inclusion_relation(A)) )),
% 0.14/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.46 fof(f41,axiom,(
% 0.14/0.46 (! [A,B] : subset(A,A) )),
% 0.14/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.46 fof(f45,conjecture,(
% 0.14/0.46 (! [A] : reflexive(inclusion_relation(A)) )),
% 0.14/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.47 fof(f46,negated_conjecture,(
% 0.14/0.47 ~((! [A] : reflexive(inclusion_relation(A)) ))),
% 0.14/0.47 inference(negated_conjecture,[status(cth)],[f45])).
% 0.14/0.47 fof(f72,plain,(
% 0.14/0.47 ![A]: (~relation(A)|(![B]: (is_reflexive_in(A,B)<=>(![C]: (~in(C,B)|in(ordered_pair(C,C),A))))))),
% 0.14/0.47 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.47 fof(f73,plain,(
% 0.14/0.47 ![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)))))))),
% 0.14/0.47 inference(NNF_transformation,[status(thm)],[f72])).
% 0.14/0.47 fof(f74,plain,(
% 0.14/0.47 ![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)))))))),
% 0.14/0.47 inference(miniscoping,[status(thm)],[f73])).
% 0.14/0.47 fof(f75,plain,(
% 0.14/0.47 ![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(sK0_skl(B,A),B)&~in(ordered_pair(sK0_skl(B,A),sK0_skl(B,A)),A))))))),
% 0.14/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f74])).
% 0.14/0.47 fof(f77,plain,(
% 0.14/0.47 ![X0,X1]: (~relation(X0)|is_reflexive_in(X0,X1)|in(sK0_skl(X1,X0),X1))),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/0.47 fof(f78,plain,(
% 0.14/0.47 ![X0,X1]: (~relation(X0)|is_reflexive_in(X0,X1)|~in(ordered_pair(sK0_skl(X1,X0),sK0_skl(X1,X0)),X0))),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/0.47 fof(f79,plain,(
% 0.14/0.47 ![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.14/0.47 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.14/0.47 fof(f80,plain,(
% 0.14/0.47 ![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.14/0.47 inference(NNF_transformation,[status(thm)],[f79])).
% 0.14/0.47 fof(f81,plain,(
% 0.14/0.47 ![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.14/0.47 inference(miniscoping,[status(thm)],[f80])).
% 0.14/0.47 fof(f82,plain,(
% 0.14/0.47 ![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(sK1_skl(A,B),A)&in(sK2_skl(A,B),A))&((~in(ordered_pair(sK1_skl(A,B),sK2_skl(A,B)),B)|~subset(sK1_skl(A,B),sK2_skl(A,B)))&(in(ordered_pair(sK1_skl(A,B),sK2_skl(A,B)),B)|subset(sK1_skl(A,B),sK2_skl(A,B))))))))))),
% 0.14/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(C,sK1_skl(A,B)),skolemize(D,sK2_skl(A,B))],[f81])).
% 0.14/0.47 fof(f83,plain,(
% 0.14/0.47 ![X0,X1]: (~relation(X0)|~X0=inclusion_relation(X1)|relation_field(X0)=X1)),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f82])).
% 0.14/0.47 fof(f85,plain,(
% 0.14/0.47 ![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.14/0.47 inference(cnf_transformation,[status(thm)],[f82])).
% 0.14/0.47 fof(f93,plain,(
% 0.14/0.47 ![A]: (~relation(A)|(reflexive(A)<=>is_reflexive_in(A,relation_field(A))))),
% 0.14/0.47 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.14/0.47 fof(f94,plain,(
% 0.14/0.47 ![A]: (~relation(A)|((~reflexive(A)|is_reflexive_in(A,relation_field(A)))&(reflexive(A)|~is_reflexive_in(A,relation_field(A)))))),
% 0.14/0.47 inference(NNF_transformation,[status(thm)],[f93])).
% 0.14/0.47 fof(f96,plain,(
% 0.14/0.47 ![X0]: (~relation(X0)|reflexive(X0)|~is_reflexive_in(X0,relation_field(X0)))),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f94])).
% 0.14/0.47 fof(f97,plain,(
% 0.14/0.47 ![X0]: (relation(inclusion_relation(X0)))),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/0.47 fof(f154,plain,(
% 0.14/0.47 ![A]: subset(A,A)),
% 0.14/0.47 inference(miniscoping,[status(thm)],[f41])).
% 0.14/0.47 fof(f155,plain,(
% 0.14/0.47 ![X0]: (subset(X0,X0))),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f154])).
% 0.14/0.47 fof(f161,plain,(
% 0.14/0.47 (?[A]: ~reflexive(inclusion_relation(A)))),
% 0.14/0.47 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.14/0.47 fof(f162,plain,(
% 0.14/0.47 ~reflexive(inclusion_relation(sK13_skl))),
% 0.14/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f161])).
% 0.14/0.47 fof(f163,plain,(
% 0.14/0.47 ~reflexive(inclusion_relation(sK13_skl))),
% 0.14/0.47 inference(cnf_transformation,[status(thm)],[f162])).
% 0.14/0.47 fof(f183,plain,(
% 0.14/0.47 ![X0]: (~relation(inclusion_relation(X0))|relation_field(inclusion_relation(X0))=X0)),
% 0.14/0.47 inference(destructive_equality_resolution,[status(thm)],[f83])).
% 0.14/0.47 fof(f185,plain,(
% 0.14/0.47 ![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.14/0.47 inference(destructive_equality_resolution,[status(thm)],[f85])).
% 0.14/0.47 fof(f190,plain,(
% 0.14/0.47 ![X0,X1,X2]: (~in(X0,X1)|~in(X2,X1)|in(ordered_pair(X0,X2),inclusion_relation(X1))|~subset(X0,X2))),
% 0.14/0.47 inference(backward_subsumption_resolution,[status(thm)],[f185,f97])).
% 0.14/0.47 fof(f192,plain,(
% 0.14/0.47 ![X0]: (relation_field(inclusion_relation(X0))=X0)),
% 0.14/0.47 inference(backward_subsumption_resolution,[status(thm)],[f183,f97])).
% 0.14/0.47 fof(f193,plain,(
% 0.14/0.47 ![X0]: (~relation(inclusion_relation(X0))|reflexive(inclusion_relation(X0))|~is_reflexive_in(inclusion_relation(X0),X0))),
% 0.14/0.47 inference(paramodulation,[status(thm)],[f192,f96])).
% 0.14/0.47 fof(f194,plain,(
% 0.14/0.47 ![X0]: (reflexive(inclusion_relation(X0))|~is_reflexive_in(inclusion_relation(X0),X0))),
% 0.14/0.47 inference(forward_subsumption_resolution,[status(thm)],[f193,f97])).
% 0.14/0.47 fof(f211,plain,(
% 0.14/0.47 ![X0,X1]: (~relation(inclusion_relation(X0))|is_reflexive_in(inclusion_relation(X0),X1)|~in(sK0_skl(X1,inclusion_relation(X0)),X0)|~in(sK0_skl(X1,inclusion_relation(X0)),X0)|~subset(sK0_skl(X1,inclusion_relation(X0)),sK0_skl(X1,inclusion_relation(X0))))),
% 0.14/0.47 inference(resolution,[status(thm)],[f78,f190])).
% 0.14/0.47 fof(f212,plain,(
% 0.14/0.47 ![X0,X1]: (~relation(inclusion_relation(X0))|is_reflexive_in(inclusion_relation(X0),X1)|~in(sK0_skl(X1,inclusion_relation(X0)),X0)|~subset(sK0_skl(X1,inclusion_relation(X0)),sK0_skl(X1,inclusion_relation(X0))))),
% 0.14/0.47 inference(duplicate_literals_removal,[status(thm)],[f211])).
% 0.14/0.47 fof(f213,plain,(
% 0.14/0.47 ![X0,X1]: (is_reflexive_in(inclusion_relation(X0),X1)|~in(sK0_skl(X1,inclusion_relation(X0)),X0)|~subset(sK0_skl(X1,inclusion_relation(X0)),sK0_skl(X1,inclusion_relation(X0))))),
% 0.14/0.47 inference(forward_subsumption_resolution,[status(thm)],[f212,f97])).
% 0.14/0.47 fof(f234,plain,(
% 0.14/0.47 ![X0,X1]: (is_reflexive_in(inclusion_relation(X0),X1)|~in(sK0_skl(X1,inclusion_relation(X0)),X0))),
% 0.14/0.47 inference(resolution,[status(thm)],[f155,f213])).
% 0.14/0.47 fof(f259,plain,(
% 0.14/0.47 ![X0]: (is_reflexive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0))|is_reflexive_in(inclusion_relation(X0),X0))),
% 0.14/0.47 inference(resolution,[status(thm)],[f234,f77])).
% 0.14/0.47 fof(f260,plain,(
% 0.14/0.47 ![X0]: (is_reflexive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0)))),
% 0.14/0.47 inference(duplicate_literals_removal,[status(thm)],[f259])).
% 0.14/0.47 fof(f261,plain,(
% 0.14/0.47 ![X0]: (reflexive(inclusion_relation(X0)))),
% 0.14/0.47 inference(backward_subsumption_resolution,[status(thm)],[f194,f262])).
% 0.14/0.47 fof(f262,plain,(
% 0.14/0.47 ![X0]: (is_reflexive_in(inclusion_relation(X0),X0))),
% 0.14/0.47 inference(forward_subsumption_resolution,[status(thm)],[f260,f97])).
% 0.14/0.47 fof(f264,plain,(
% 0.14/0.47 $false),
% 0.14/0.47 inference(backward_subsumption_resolution,[status(thm)],[f163,f261])).
% 0.14/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.52 % Elapsed time: 0.081725 seconds
% 0.14/0.52 % CPU time: 0.164214 seconds
% 0.14/0.52 % Total memory used: 36.455 MB
% 0.14/0.52 % Net memory used: 36.408 MB
%------------------------------------------------------------------------------