%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU240+1 : 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 : n016.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:06 PM UTC 2026
% Result : Theorem 0.12s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU240+1 : 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.08/0.34 % Computer : n016.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % 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 06:07:23 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.12/0.41 % Refutation found
% 0.12/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.41 fof(f6,axiom,(
% 0.12/0.41 (! [A] :( relation(A)=> ( transitive(A)<=> is_transitive_in(A,relation_field(A)) ) ) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f9,axiom,(
% 0.12/0.41 (! [A] :( relation(A)=> (! [B] :( is_transitive_in(A,B)<=> (! [C,D,E] :( ( in(C,B)& in(D,B)& in(E,B)& in(ordered_pair(C,D),A)& in(ordered_pair(D,E),A) )=> in(ordered_pair(C,E),A) ) )) )) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f25,conjecture,(
% 0.12/0.41 (! [A] :( relation(A)=> ( transitive(A)<=> (! [B,C,D] :( ( in(ordered_pair(B,C),A)& in(ordered_pair(C,D),A) )=> in(ordered_pair(B,D),A) ) )) ) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f26,negated_conjecture,(
% 0.12/0.41 ~((! [A] :( relation(A)=> ( transitive(A)<=> (! [B,C,D] :( ( in(ordered_pair(B,C),A)& in(ordered_pair(C,D),A) )=> in(ordered_pair(B,D),A) ) )) ) ))),
% 0.12/0.41 inference(negated_conjecture,[status(cth)],[f25])).
% 0.12/0.41 fof(f35,axiom,(
% 0.12/0.41 (! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_field(C))& in(B,relation_field(C)) ) ) ) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f49,plain,(
% 0.12/0.41 ![A]: (~relation(A)|(transitive(A)<=>is_transitive_in(A,relation_field(A))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.12/0.41 fof(f50,plain,(
% 0.12/0.41 ![A]: (~relation(A)|((~transitive(A)|is_transitive_in(A,relation_field(A)))&(transitive(A)|~is_transitive_in(A,relation_field(A)))))),
% 0.12/0.41 inference(NNF_transformation,[status(thm)],[f49])).
% 0.12/0.41 fof(f51,plain,(
% 0.12/0.41 ![X0]: (~relation(X0)|~transitive(X0)|is_transitive_in(X0,relation_field(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f50])).
% 0.12/0.41 fof(f52,plain,(
% 0.12/0.41 ![X0]: (~relation(X0)|transitive(X0)|~is_transitive_in(X0,relation_field(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f50])).
% 0.12/0.41 fof(f56,plain,(
% 0.12/0.41 ![A]: (~relation(A)|(![B]: (is_transitive_in(A,B)<=>(![C,D,E]: (((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A))|in(ordered_pair(C,E),A))))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.12/0.41 fof(f57,plain,(
% 0.12/0.41 ![A]: (~relation(A)|(![B]: ((~is_transitive_in(A,B)|(![C,D,E]: (((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A))|in(ordered_pair(C,E),A))))&(is_transitive_in(A,B)|(?[C,D,E]: (((((in(C,B)&in(D,B))&in(E,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,E),A))&~in(ordered_pair(C,E),A)))))))),
% 0.12/0.41 inference(NNF_transformation,[status(thm)],[f56])).
% 0.12/0.41 fof(f58,plain,(
% 0.12/0.41 ![A]: (~relation(A)|((![B]: (~is_transitive_in(A,B)|(![C,E]: ((![D]: ((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A)))|in(ordered_pair(C,E),A)))))&(![B]: (is_transitive_in(A,B)|(?[C,E]: ((?[D]: ((((in(C,B)&in(D,B))&in(E,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,E),A)))&~in(ordered_pair(C,E),A)))))))),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f57])).
% 0.12/0.41 fof(f59,plain,(
% 0.12/0.41 ![A]: (~relation(A)|((![B]: (~is_transitive_in(A,B)|(![C,E]: ((![D]: ((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A)))|in(ordered_pair(C,E),A)))))&(![B]: (is_transitive_in(A,B)|(((((in(sK0_skl(B,A),B)&in(sK2_skl(B,A),B))&in(sK1_skl(B,A),B))&in(ordered_pair(sK0_skl(B,A),sK2_skl(B,A)),A))&in(ordered_pair(sK2_skl(B,A),sK1_skl(B,A)),A))&~in(ordered_pair(sK0_skl(B,A),sK1_skl(B,A)),A))))))),
% 0.12/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(C,sK0_skl(B,A)),skolemize(E,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f58])).
% 0.12/0.41 fof(f60,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4]: (~relation(X0)|~is_transitive_in(X0,X1)|~in(X2,X1)|~in(X3,X1)|~in(X4,X1)|~in(ordered_pair(X2,X3),X0)|~in(ordered_pair(X3,X4),X0)|in(ordered_pair(X2,X4),X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.41 fof(f64,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(ordered_pair(sK0_skl(X1,X0),sK2_skl(X1,X0)),X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.41 fof(f65,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(ordered_pair(sK2_skl(X1,X0),sK1_skl(X1,X0)),X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.41 fof(f66,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|~in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.41 fof(f79,plain,(
% 0.12/0.41 (?[A]: (relation(A)&(transitive(A)<~>(![B,C,D]: ((~in(ordered_pair(B,C),A)|~in(ordered_pair(C,D),A))|in(ordered_pair(B,D),A))))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.12/0.41 fof(f80,plain,(
% 0.12/0.41 ?[A]: (relation(A)&((transitive(A)|(![B,C,D]: ((~in(ordered_pair(B,C),A)|~in(ordered_pair(C,D),A))|in(ordered_pair(B,D),A))))&(~transitive(A)|(?[B,C,D]: ((in(ordered_pair(B,C),A)&in(ordered_pair(C,D),A))&~in(ordered_pair(B,D),A))))))),
% 0.12/0.41 inference(NNF_transformation,[status(thm)],[f79])).
% 0.12/0.41 fof(f81,plain,(
% 0.12/0.41 ?[A]: (relation(A)&((transitive(A)|(![B,D]: ((![C]: (~in(ordered_pair(B,C),A)|~in(ordered_pair(C,D),A)))|in(ordered_pair(B,D),A))))&(~transitive(A)|(?[B,D]: ((?[C]: (in(ordered_pair(B,C),A)&in(ordered_pair(C,D),A)))&~in(ordered_pair(B,D),A))))))),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f80])).
% 0.12/0.41 fof(f82,plain,(
% 0.12/0.41 (relation(sK4_skl)&((transitive(sK4_skl)|(![B,D]: ((![C]: (~in(ordered_pair(B,C),sK4_skl)|~in(ordered_pair(C,D),sK4_skl)))|in(ordered_pair(B,D),sK4_skl))))&(~transitive(sK4_skl)|((in(ordered_pair(sK5_skl,sK7_skl),sK4_skl)&in(ordered_pair(sK7_skl,sK6_skl),sK4_skl))&~in(ordered_pair(sK5_skl,sK6_skl),sK4_skl)))))),
% 0.12/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(A,sK4_skl),skolemize(B,sK5_skl),skolemize(D,sK6_skl),skolemize(C,sK7_skl)],[f81])).
% 0.12/0.41 fof(f83,plain,(
% 0.12/0.41 relation(sK4_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f82])).
% 0.12/0.41 fof(f84,plain,(
% 0.12/0.41 ![X0,X1,X2]: (transitive(sK4_skl)|~in(ordered_pair(X0,X1),sK4_skl)|~in(ordered_pair(X1,X2),sK4_skl)|in(ordered_pair(X0,X2),sK4_skl))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f82])).
% 0.12/0.41 fof(f85,plain,(
% 0.12/0.41 ~transitive(sK4_skl)|in(ordered_pair(sK5_skl,sK7_skl),sK4_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f82])).
% 0.12/0.41 fof(f86,plain,(
% 0.12/0.41 ~transitive(sK4_skl)|in(ordered_pair(sK7_skl,sK6_skl),sK4_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f82])).
% 0.12/0.41 fof(f87,plain,(
% 0.12/0.41 ~transitive(sK4_skl)|~in(ordered_pair(sK5_skl,sK6_skl),sK4_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f82])).
% 0.12/0.41 fof(f108,plain,(
% 0.12/0.41 ![A,B,C]: (~relation(C)|(~in(ordered_pair(A,B),C)|(in(A,relation_field(C))&in(B,relation_field(C)))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.12/0.41 fof(f109,plain,(
% 0.12/0.41 ![C]: (~relation(C)|(![A,B]: (~in(ordered_pair(A,B),C)|(in(A,relation_field(C))&in(B,relation_field(C))))))),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f108])).
% 0.12/0.41 fof(f110,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~relation(X0)|~in(ordered_pair(X1,X2),X0)|in(X1,relation_field(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/0.41 fof(f111,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~relation(X0)|~in(ordered_pair(X1,X2),X0)|in(X2,relation_field(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/0.41 fof(f144,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(sK4_skl)|is_transitive_in(sK4_skl,X0)|transitive(sK4_skl)|~in(ordered_pair(X1,sK2_skl(X0,sK4_skl)),sK4_skl)|in(ordered_pair(X1,sK1_skl(X0,sK4_skl)),sK4_skl))),
% 0.12/0.41 inference(resolution,[status(thm)],[f65,f84])).
% 0.12/0.41 fof(f146,plain,(
% 0.12/0.41 ![X0,X1]: (is_transitive_in(sK4_skl,X0)|transitive(sK4_skl)|~in(ordered_pair(X1,sK2_skl(X0,sK4_skl)),sK4_skl)|in(ordered_pair(X1,sK1_skl(X0,sK4_skl)),sK4_skl))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f144,f83])).
% 0.12/0.41 fof(f147,plain,(
% 0.12/0.41 ![X0]: (is_transitive_in(sK4_skl,X0)|transitive(sK4_skl)|in(ordered_pair(sK0_skl(X0,sK4_skl),sK1_skl(X0,sK4_skl)),sK4_skl)|~relation(sK4_skl)|is_transitive_in(sK4_skl,X0))),
% 0.12/0.41 inference(resolution,[status(thm)],[f146,f64])).
% 0.12/0.41 fof(f148,plain,(
% 0.12/0.41 ![X0]: (is_transitive_in(sK4_skl,X0)|transitive(sK4_skl)|in(ordered_pair(sK0_skl(X0,sK4_skl),sK1_skl(X0,sK4_skl)),sK4_skl)|~relation(sK4_skl))),
% 0.12/0.41 inference(duplicate_literals_removal,[status(thm)],[f147])).
% 0.12/0.41 fof(f149,plain,(
% 0.12/0.41 ![X0]: (is_transitive_in(sK4_skl,X0)|transitive(sK4_skl)|in(ordered_pair(sK0_skl(X0,sK4_skl),sK1_skl(X0,sK4_skl)),sK4_skl))),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f148,f83])).
% 0.12/0.42 fof(f174,plain,(
% 0.12/0.42 ![X0,X1,X2,X3]: (~relation(X0)|~in(X1,relation_field(X0))|~in(X2,relation_field(X0))|~in(X3,relation_field(X0))|~in(ordered_pair(X1,X2),X0)|~in(ordered_pair(X2,X3),X0)|in(ordered_pair(X1,X3),X0)|~relation(X0)|~transitive(X0))),
% 0.12/0.42 inference(resolution,[status(thm)],[f60,f51])).
% 0.12/0.42 fof(f175,plain,(
% 0.12/0.42 ![X0,X1,X2,X3]: (~relation(X0)|~in(X1,relation_field(X0))|~in(X2,relation_field(X0))|~in(X3,relation_field(X0))|~in(ordered_pair(X1,X2),X0)|~in(ordered_pair(X2,X3),X0)|in(ordered_pair(X1,X3),X0)|~transitive(X0))),
% 0.12/0.42 inference(duplicate_literals_removal,[status(thm)],[f174])).
% 0.12/0.42 fof(f176,plain,(
% 0.12/0.42 ![X0]: (~relation(sK4_skl)|is_transitive_in(sK4_skl,X0)|is_transitive_in(sK4_skl,X0)|transitive(sK4_skl))),
% 0.12/0.42 inference(resolution,[status(thm)],[f66,f149])).
% 0.12/0.42 fof(f177,plain,(
% 0.12/0.42 ![X0]: (~relation(sK4_skl)|is_transitive_in(sK4_skl,X0)|transitive(sK4_skl))),
% 0.12/0.42 inference(duplicate_literals_removal,[status(thm)],[f176])).
% 0.12/0.42 fof(f178,plain,(
% 0.12/0.42 ![X0]: (is_transitive_in(sK4_skl,X0)|transitive(sK4_skl))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f177,f83])).
% 0.12/0.42 fof(f179,plain,(
% 0.12/0.42 transitive(sK4_skl)|~relation(sK4_skl)|transitive(sK4_skl)),
% 0.12/0.42 inference(resolution,[status(thm)],[f178,f52])).
% 0.12/0.42 fof(f181,plain,(
% 0.12/0.42 transitive(sK4_skl)|~relation(sK4_skl)),
% 0.12/0.42 inference(duplicate_literals_removal,[status(thm)],[f179])).
% 0.12/0.42 fof(f182,plain,(
% 0.12/0.42 transitive(sK4_skl)),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f181,f83])).
% 0.12/0.42 fof(f184,plain,(
% 0.12/0.42 in(ordered_pair(sK5_skl,sK7_skl),sK4_skl)),
% 0.12/0.42 inference(backward_subsumption_resolution,[status(thm)],[f85,f182])).
% 0.12/0.42 fof(f185,plain,(
% 0.12/0.42 ~in(ordered_pair(sK5_skl,sK6_skl),sK4_skl)),
% 0.12/0.42 inference(backward_subsumption_resolution,[status(thm)],[f87,f182])).
% 0.12/0.42 fof(f186,plain,(
% 0.12/0.42 in(ordered_pair(sK7_skl,sK6_skl),sK4_skl)),
% 0.12/0.42 inference(backward_subsumption_resolution,[status(thm)],[f86,f182])).
% 0.12/0.42 fof(f222,plain,(
% 0.12/0.42 ![X0,X1]: (~in(ordered_pair(X0,X1),sK4_skl)|in(X0,relation_field(sK4_skl)))),
% 0.12/0.42 inference(resolution,[status(thm)],[f110,f83])).
% 0.12/0.42 fof(f244,plain,(
% 0.12/0.42 ![X0,X1]: (~in(ordered_pair(X0,X1),sK4_skl)|in(X1,relation_field(sK4_skl)))),
% 0.12/0.42 inference(resolution,[status(thm)],[f111,f83])).
% 0.12/0.42 fof(f317,plain,(
% 0.12/0.42 ![X0,X1,X2,X3]: (~relation(X0)|~in(X1,relation_field(X0))|~in(X2,relation_field(X0))|~in(ordered_pair(X1,X3),X0)|~in(ordered_pair(X3,X2),X0)|in(ordered_pair(X1,X2),X0)|~transitive(X0))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f175,f111])).
% 0.12/0.42 fof(f319,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~relation(sK4_skl)|~in(X0,relation_field(sK4_skl))|~in(X1,relation_field(sK4_skl))|~in(ordered_pair(X0,X2),sK4_skl)|~in(ordered_pair(X2,X1),sK4_skl)|in(ordered_pair(X0,X1),sK4_skl))),
% 0.12/0.42 inference(resolution,[status(thm)],[f317,f182])).
% 0.12/0.42 fof(f320,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~in(X0,relation_field(sK4_skl))|~in(X1,relation_field(sK4_skl))|~in(ordered_pair(X0,X2),sK4_skl)|~in(ordered_pair(X2,X1),sK4_skl)|in(ordered_pair(X0,X1),sK4_skl))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f319,f83])).
% 0.12/0.42 fof(f321,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~in(X0,relation_field(sK4_skl))|~in(ordered_pair(X0,X1),sK4_skl)|~in(ordered_pair(X1,X2),sK4_skl)|in(ordered_pair(X0,X2),sK4_skl))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f320,f244])).
% 0.12/0.42 fof(f322,plain,(
% 0.12/0.42 ![X0]: (~in(X0,relation_field(sK4_skl))|~in(ordered_pair(X0,sK7_skl),sK4_skl)|in(ordered_pair(X0,sK6_skl),sK4_skl))),
% 0.12/0.42 inference(resolution,[status(thm)],[f321,f186])).
% 0.12/0.42 fof(f326,plain,(
% 0.12/0.42 ![X0]: (~in(ordered_pair(X0,sK7_skl),sK4_skl)|in(ordered_pair(X0,sK6_skl),sK4_skl))),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f322,f222])).
% 0.12/0.42 fof(f335,plain,(
% 0.12/0.42 in(ordered_pair(sK5_skl,sK6_skl),sK4_skl)),
% 0.12/0.42 inference(resolution,[status(thm)],[f326,f184])).
% 0.12/0.42 fof(f336,plain,(
% 0.12/0.42 $false),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f335,f185])).
% 0.12/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.44 % Elapsed time: 0.081373 seconds
% 0.12/0.44 % CPU time: 0.344241 seconds
% 0.12/0.44 % Total memory used: 63.159 MB
% 0.12/0.44 % Net memory used: 63.052 MB
%------------------------------------------------------------------------------