%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU242+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 : 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:22:07 PM UTC 2026
% Result : Theorem 0.18s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU242+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n005.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 06:02:17 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 0.18/0.52 % Refutation found
% 0.18/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.52 fof(f6,axiom,(
% 0.18/0.52 (! [A] :( relation(A)=> ( connected(A)<=> is_connected_in(A,relation_field(A)) ) ) )),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f9,axiom,(
% 0.18/0.52 (! [A] :( relation(A)=> (! [B] :( is_connected_in(A,B)<=> (! [C,D] :~ ( in(C,B)& in(D,B)& C != D& ~ in(ordered_pair(C,D),A)& ~ in(ordered_pair(D,C),A) ) )) )) )),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f25,conjecture,(
% 0.18/0.52 (! [A] :( relation(A)=> ( connected(A)<=> (! [B,C] :~ ( in(B,relation_field(A))& in(C,relation_field(A))& B != C& ~ in(ordered_pair(B,C),A)& ~ in(ordered_pair(C,B),A) ) )) ) )),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f26,negated_conjecture,(
% 0.18/0.52 ~((! [A] :( relation(A)=> ( connected(A)<=> (! [B,C] :~ ( in(B,relation_field(A))& in(C,relation_field(A))& B != C& ~ in(ordered_pair(B,C),A)& ~ in(ordered_pair(C,B),A) ) )) ) ))),
% 0.18/0.52 inference(negated_conjecture,[status(cth)],[f25])).
% 0.18/0.52 fof(f48,plain,(
% 0.18/0.52 ![A]: (~relation(A)|(connected(A)<=>is_connected_in(A,relation_field(A))))),
% 0.18/0.52 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.18/0.52 fof(f49,plain,(
% 0.18/0.52 ![A]: (~relation(A)|((~connected(A)|is_connected_in(A,relation_field(A)))&(connected(A)|~is_connected_in(A,relation_field(A)))))),
% 0.18/0.52 inference(NNF_transformation,[status(thm)],[f48])).
% 0.18/0.52 fof(f50,plain,(
% 0.18/0.52 ![X0]: (~relation(X0)|~connected(X0)|is_connected_in(X0,relation_field(X0)))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f49])).
% 0.18/0.52 fof(f51,plain,(
% 0.18/0.52 ![X0]: (~relation(X0)|connected(X0)|~is_connected_in(X0,relation_field(X0)))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f49])).
% 0.18/0.52 fof(f55,plain,(
% 0.18/0.52 ![A]: (~relation(A)|(![B]: (is_connected_in(A,B)<=>(![C,D]: ((((~in(C,B)|~in(D,B))|C=D)|in(ordered_pair(C,D),A))|in(ordered_pair(D,C),A))))))),
% 0.18/0.52 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.18/0.52 fof(f56,plain,(
% 0.18/0.52 ![A]: (~relation(A)|(![B]: ((~is_connected_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|C=D)|in(ordered_pair(C,D),A))|in(ordered_pair(D,C),A))))&(is_connected_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&~C=D)&~in(ordered_pair(C,D),A))&~in(ordered_pair(D,C),A)))))))),
% 0.18/0.52 inference(NNF_transformation,[status(thm)],[f55])).
% 0.18/0.52 fof(f57,plain,(
% 0.18/0.52 ![A]: (~relation(A)|((![B]: (~is_connected_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|C=D)|in(ordered_pair(C,D),A))|in(ordered_pair(D,C),A)))))&(![B]: (is_connected_in(A,B)|(?[C,D]: ((((in(C,B)&in(D,B))&~C=D)&~in(ordered_pair(C,D),A))&~in(ordered_pair(D,C),A)))))))),
% 0.18/0.52 inference(miniscoping,[status(thm)],[f56])).
% 0.18/0.52 fof(f58,plain,(
% 0.18/0.52 ![A]: (~relation(A)|((![B]: (~is_connected_in(A,B)|(![C,D]: ((((~in(C,B)|~in(D,B))|C=D)|in(ordered_pair(C,D),A))|in(ordered_pair(D,C),A)))))&(![B]: (is_connected_in(A,B)|((((in(sK0_skl(B,A),B)&in(sK1_skl(B,A),B))&~sK0_skl(B,A)=sK1_skl(B,A))&~in(ordered_pair(sK0_skl(B,A),sK1_skl(B,A)),A))&~in(ordered_pair(sK1_skl(B,A),sK0_skl(B,A)),A))))))),
% 0.18/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A))],[f57])).
% 0.18/0.52 fof(f59,plain,(
% 0.18/0.52 ![X0,X1,X2,X3]: (~relation(X0)|~is_connected_in(X0,X1)|~in(X2,X1)|~in(X3,X1)|X2=X3|in(ordered_pair(X2,X3),X0)|in(ordered_pair(X3,X2),X0))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/0.52 fof(f60,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|is_connected_in(X0,X1)|in(sK0_skl(X1,X0),X1))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/0.52 fof(f61,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|is_connected_in(X0,X1)|in(sK1_skl(X1,X0),X1))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/0.52 fof(f62,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|is_connected_in(X0,X1)|~sK0_skl(X1,X0)=sK1_skl(X1,X0))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/0.52 fof(f63,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|is_connected_in(X0,X1)|~in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/0.52 fof(f64,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|is_connected_in(X0,X1)|~in(ordered_pair(sK1_skl(X1,X0),sK0_skl(X1,X0)),X0))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f58])).
% 0.18/0.52 fof(f77,plain,(
% 0.18/0.52 (?[A]: (relation(A)&(connected(A)<~>(![B,C]: ((((~in(B,relation_field(A))|~in(C,relation_field(A)))|B=C)|in(ordered_pair(B,C),A))|in(ordered_pair(C,B),A))))))),
% 0.18/0.52 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.18/0.52 fof(f78,plain,(
% 0.18/0.52 ?[A]: (relation(A)&((connected(A)|(![B,C]: ((((~in(B,relation_field(A))|~in(C,relation_field(A)))|B=C)|in(ordered_pair(B,C),A))|in(ordered_pair(C,B),A))))&(~connected(A)|(?[B,C]: ((((in(B,relation_field(A))&in(C,relation_field(A)))&~B=C)&~in(ordered_pair(B,C),A))&~in(ordered_pair(C,B),A))))))),
% 0.18/0.52 inference(NNF_transformation,[status(thm)],[f77])).
% 0.18/0.52 fof(f79,plain,(
% 0.18/0.52 (relation(sK3_skl)&((connected(sK3_skl)|(![B,C]: ((((~in(B,relation_field(sK3_skl))|~in(C,relation_field(sK3_skl)))|B=C)|in(ordered_pair(B,C),sK3_skl))|in(ordered_pair(C,B),sK3_skl))))&(~connected(sK3_skl)|((((in(sK4_skl,relation_field(sK3_skl))&in(sK5_skl,relation_field(sK3_skl)))&~sK4_skl=sK5_skl)&~in(ordered_pair(sK4_skl,sK5_skl),sK3_skl))&~in(ordered_pair(sK5_skl,sK4_skl),sK3_skl)))))),
% 0.18/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK3_skl),skolemize(B,sK4_skl),skolemize(C,sK5_skl)],[f78])).
% 0.18/0.52 fof(f80,plain,(
% 0.18/0.52 relation(sK3_skl)),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f81,plain,(
% 0.18/0.52 ![X0,X1]: (connected(sK3_skl)|~in(X0,relation_field(sK3_skl))|~in(X1,relation_field(sK3_skl))|X0=X1|in(ordered_pair(X0,X1),sK3_skl)|in(ordered_pair(X1,X0),sK3_skl))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f82,plain,(
% 0.18/0.52 ~connected(sK3_skl)|in(sK4_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f83,plain,(
% 0.18/0.52 ~connected(sK3_skl)|in(sK5_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f84,plain,(
% 0.18/0.52 ~connected(sK3_skl)|~sK4_skl=sK5_skl),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f85,plain,(
% 0.18/0.52 ~connected(sK3_skl)|~in(ordered_pair(sK4_skl,sK5_skl),sK3_skl)),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f86,plain,(
% 0.18/0.52 ~connected(sK3_skl)|~in(ordered_pair(sK5_skl,sK4_skl),sK3_skl)),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/0.52 fof(f134,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|is_connected_in(X0,relation_field(sK3_skl))|connected(sK3_skl)|~in(X1,relation_field(sK3_skl))|X1=sK0_skl(relation_field(sK3_skl),X0)|in(ordered_pair(X1,sK0_skl(relation_field(sK3_skl),X0)),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),X0),X1),sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f60,f81])).
% 0.18/0.52 fof(f139,plain,(
% 0.18/0.52 ![X0]: (is_connected_in(sK3_skl,X0)|in(sK1_skl(X0,sK3_skl),X0))),
% 0.18/0.52 inference(resolution,[status(thm)],[f61,f80])).
% 0.18/0.52 fof(f143,plain,(
% 0.18/0.52 ![X0]: (is_connected_in(sK3_skl,relation_field(sK3_skl))|~relation(X0)|is_connected_in(X0,relation_field(sK3_skl))|connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),X0)|in(ordered_pair(sK1_skl(relation_field(sK3_skl),sK3_skl),sK0_skl(relation_field(sK3_skl),X0)),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),X0),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f139,f134])).
% 0.18/0.52 fof(f153,plain,(
% 0.18/0.52 is_connected_in(sK3_skl,relation_field(sK3_skl))|is_connected_in(sK3_skl,relation_field(sK3_skl))|connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|in(ordered_pair(sK1_skl(relation_field(sK3_skl),sK3_skl),sK0_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),sK3_skl),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)),
% 0.18/0.52 inference(resolution,[status(thm)],[f143,f80])).
% 0.18/0.52 fof(f154,plain,(
% 0.18/0.52 is_connected_in(sK3_skl,relation_field(sK3_skl))|connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|in(ordered_pair(sK1_skl(relation_field(sK3_skl),sK3_skl),sK0_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),sK3_skl),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)),
% 0.18/0.52 inference(duplicate_literals_removal,[status(thm)],[f153])).
% 0.18/0.52 fof(f191,plain,(
% 0.18/0.52 is_connected_in(sK3_skl,relation_field(sK3_skl))|connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),sK3_skl),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)|~relation(sK3_skl)|is_connected_in(sK3_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f154,f64])).
% 0.18/0.52 fof(f193,plain,(
% 0.18/0.52 is_connected_in(sK3_skl,relation_field(sK3_skl))|connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),sK3_skl),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)|~relation(sK3_skl)),
% 0.18/0.52 inference(duplicate_literals_removal,[status(thm)],[f191])).
% 0.18/0.52 fof(f194,plain,(
% 0.18/0.52 connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),sK3_skl),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)|~relation(sK3_skl)),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f193,f51])).
% 0.18/0.52 fof(f308,plain,(
% 0.18/0.52 connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|in(ordered_pair(sK0_skl(relation_field(sK3_skl),sK3_skl),sK1_skl(relation_field(sK3_skl),sK3_skl)),sK3_skl)),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f194,f80])).
% 0.18/0.52 fof(f309,plain,(
% 0.18/0.52 connected(sK3_skl)|sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|~relation(sK3_skl)|is_connected_in(sK3_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f308,f63])).
% 0.18/0.52 fof(f311,plain,(
% 0.18/0.52 sK1_skl(relation_field(sK3_skl),sK3_skl)=sK0_skl(relation_field(sK3_skl),sK3_skl)|~relation(sK3_skl)|is_connected_in(sK3_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f309,f50])).
% 0.18/0.52 fof(f312,plain,(
% 0.18/0.52 ~relation(sK3_skl)|is_connected_in(sK3_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f311,f62])).
% 0.18/0.52 fof(f313,plain,(
% 0.18/0.52 is_connected_in(sK3_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f312,f80])).
% 0.18/0.52 fof(f341,plain,(
% 0.18/0.52 ~relation(sK3_skl)|connected(sK3_skl)),
% 0.18/0.52 inference(resolution,[status(thm)],[f313,f51])).
% 0.18/0.52 fof(f342,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(sK3_skl)|~in(X0,relation_field(sK3_skl))|~in(X1,relation_field(sK3_skl))|X0=X1|in(ordered_pair(X0,X1),sK3_skl)|in(ordered_pair(X1,X0),sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f313,f59])).
% 0.18/0.52 fof(f343,plain,(
% 0.18/0.52 connected(sK3_skl)),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f341,f80])).
% 0.18/0.52 fof(f344,plain,(
% 0.18/0.52 ![X0,X1]: (~in(X0,relation_field(sK3_skl))|~in(X1,relation_field(sK3_skl))|X0=X1|in(ordered_pair(X0,X1),sK3_skl)|in(ordered_pair(X1,X0),sK3_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f342,f80])).
% 0.18/0.52 fof(f354,plain,(
% 0.18/0.52 ~in(ordered_pair(sK5_skl,sK4_skl),sK3_skl)),
% 0.18/0.52 inference(backward_subsumption_resolution,[status(thm)],[f86,f343])).
% 0.18/0.52 fof(f355,plain,(
% 0.18/0.52 ~in(ordered_pair(sK4_skl,sK5_skl),sK3_skl)),
% 0.18/0.52 inference(backward_subsumption_resolution,[status(thm)],[f85,f343])).
% 0.18/0.52 fof(f356,plain,(
% 0.18/0.52 ~sK4_skl=sK5_skl),
% 0.18/0.52 inference(backward_subsumption_resolution,[status(thm)],[f84,f343])).
% 0.18/0.52 fof(f357,plain,(
% 0.18/0.52 in(sK5_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(backward_subsumption_resolution,[status(thm)],[f83,f343])).
% 0.18/0.52 fof(f358,plain,(
% 0.18/0.52 in(sK4_skl,relation_field(sK3_skl))),
% 0.18/0.52 inference(backward_subsumption_resolution,[status(thm)],[f82,f343])).
% 0.18/0.52 fof(f427,plain,(
% 0.18/0.52 ![X0]: (~in(X0,relation_field(sK3_skl))|X0=sK4_skl|in(ordered_pair(X0,sK4_skl),sK3_skl)|in(ordered_pair(sK4_skl,X0),sK3_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f344,f358])).
% 0.18/0.52 fof(f437,plain,(
% 0.18/0.52 sK5_skl=sK4_skl|in(ordered_pair(sK5_skl,sK4_skl),sK3_skl)|in(ordered_pair(sK4_skl,sK5_skl),sK3_skl)),
% 0.18/0.52 inference(resolution,[status(thm)],[f427,f357])).
% 0.18/0.52 fof(f443,plain,(
% 0.18/0.52 in(ordered_pair(sK5_skl,sK4_skl),sK3_skl)|in(ordered_pair(sK4_skl,sK5_skl),sK3_skl)),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f437,f356])).
% 0.18/0.52 fof(f445,plain,(
% 0.18/0.52 in(ordered_pair(sK4_skl,sK5_skl),sK3_skl)),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f443,f354])).
% 0.18/0.53 fof(f446,plain,(
% 0.18/0.53 $false),
% 0.18/0.53 inference(backward_subsumption_resolution,[status(thm)],[f355,f445])).
% 0.18/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.57 % Elapsed time: 0.110653 seconds
% 0.18/0.57 % CPU time: 0.257756 seconds
% 0.18/0.57 % Total memory used: 41.338 MB
% 0.18/0.57 % Net memory used: 41.205 MB
%------------------------------------------------------------------------------