%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU269+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 : n019.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.10s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU269+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.10/0.36 % Computer : n019.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:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.45 % Refutation found
% 0.10/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.45 fof(f9,axiom,(
% 0.10/0.45 (! [A] :( relation(A)=> ( transitive(A)<=> is_transitive_in(A,relation_field(A)) ) ) )),
% 0.10/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.45 fof(f10,axiom,(
% 0.10/0.45 (! [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.10/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.45 fof(f13,axiom,(
% 0.10/0.45 (! [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.10/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.45 fof(f16,axiom,(
% 0.10/0.45 (! [A] : relation(inclusion_relation(A)) )),
% 0.10/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.45 fof(f44,axiom,(
% 0.10/0.45 (! [A,B,C] :( ( subset(A,B)& subset(B,C) )=> subset(A,C) ) )),
% 0.10/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.45 fof(f47,conjecture,(
% 0.10/0.45 (! [A] : transitive(inclusion_relation(A)) )),
% 0.10/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.45 fof(f48,negated_conjecture,(
% 0.10/0.45 ~((! [A] : transitive(inclusion_relation(A)) ))),
% 0.10/0.45 inference(negated_conjecture,[status(cth)],[f47])).
% 0.10/0.45 fof(f73,plain,(
% 0.10/0.45 ![A]: (~relation(A)|(transitive(A)<=>is_transitive_in(A,relation_field(A))))),
% 0.10/0.45 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.10/0.45 fof(f74,plain,(
% 0.10/0.45 ![A]: (~relation(A)|((~transitive(A)|is_transitive_in(A,relation_field(A)))&(transitive(A)|~is_transitive_in(A,relation_field(A)))))),
% 0.10/0.45 inference(NNF_transformation,[status(thm)],[f73])).
% 0.10/0.45 fof(f76,plain,(
% 0.10/0.45 ![X0]: (~relation(X0)|transitive(X0)|~is_transitive_in(X0,relation_field(X0)))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f74])).
% 0.10/0.45 fof(f77,plain,(
% 0.10/0.45 ![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.10/0.45 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.10/0.45 fof(f78,plain,(
% 0.10/0.45 ![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.10/0.45 inference(NNF_transformation,[status(thm)],[f77])).
% 0.10/0.45 fof(f79,plain,(
% 0.10/0.45 ![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.10/0.45 inference(miniscoping,[status(thm)],[f78])).
% 0.10/0.45 fof(f80,plain,(
% 0.10/0.45 ![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.10/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f79])).
% 0.10/0.45 fof(f81,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|~X0=inclusion_relation(X1)|relation_field(X0)=X1)),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f80])).
% 0.10/0.45 fof(f82,plain,(
% 0.10/0.45 ![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.10/0.45 inference(cnf_transformation,[status(thm)],[f80])).
% 0.10/0.45 fof(f83,plain,(
% 0.10/0.45 ![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.10/0.45 inference(cnf_transformation,[status(thm)],[f80])).
% 0.10/0.45 fof(f91,plain,(
% 0.10/0.45 ![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.10/0.45 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.10/0.45 fof(f92,plain,(
% 0.10/0.45 ![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.10/0.45 inference(NNF_transformation,[status(thm)],[f91])).
% 0.10/0.45 fof(f93,plain,(
% 0.10/0.45 ![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.10/0.45 inference(miniscoping,[status(thm)],[f92])).
% 0.10/0.45 fof(f94,plain,(
% 0.10/0.45 ![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(sK2_skl(B,A),B)&in(sK4_skl(B,A),B))&in(sK3_skl(B,A),B))&in(ordered_pair(sK2_skl(B,A),sK4_skl(B,A)),A))&in(ordered_pair(sK4_skl(B,A),sK3_skl(B,A)),A))&~in(ordered_pair(sK2_skl(B,A),sK3_skl(B,A)),A))))))),
% 0.10/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl]),skolemize(C,sK2_skl(B,A)),skolemize(E,sK3_skl(B,A)),skolemize(D,sK4_skl(B,A))],[f93])).
% 0.10/0.45 fof(f96,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(sK2_skl(X1,X0),X1))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.10/0.45 fof(f97,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(sK4_skl(X1,X0),X1))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.10/0.45 fof(f98,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(sK3_skl(X1,X0),X1))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.10/0.45 fof(f99,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(ordered_pair(sK2_skl(X1,X0),sK4_skl(X1,X0)),X0))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.10/0.45 fof(f100,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(ordered_pair(sK4_skl(X1,X0),sK3_skl(X1,X0)),X0))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.10/0.45 fof(f101,plain,(
% 0.10/0.45 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|~in(ordered_pair(sK2_skl(X1,X0),sK3_skl(X1,X0)),X0))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.10/0.45 fof(f102,plain,(
% 0.10/0.45 ![X0]: (relation(inclusion_relation(X0)))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.45 fof(f164,plain,(
% 0.10/0.45 ![A,B,C]: ((~subset(A,B)|~subset(B,C))|subset(A,C))),
% 0.10/0.45 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.10/0.45 fof(f165,plain,(
% 0.10/0.45 ![A,C]: ((![B]: (~subset(A,B)|~subset(B,C)))|subset(A,C))),
% 0.10/0.45 inference(miniscoping,[status(thm)],[f164])).
% 0.10/0.45 fof(f166,plain,(
% 0.10/0.45 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X1,X2)|subset(X0,X2))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f165])).
% 0.10/0.45 fof(f173,plain,(
% 0.10/0.45 (?[A]: ~transitive(inclusion_relation(A)))),
% 0.10/0.45 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.10/0.45 fof(f174,plain,(
% 0.10/0.45 ~transitive(inclusion_relation(sK15_skl))),
% 0.10/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f173])).
% 0.10/0.45 fof(f175,plain,(
% 0.10/0.45 ~transitive(inclusion_relation(sK15_skl))),
% 0.10/0.45 inference(cnf_transformation,[status(thm)],[f174])).
% 0.10/0.45 fof(f191,plain,(
% 0.10/0.45 ![X0]: (~relation(inclusion_relation(X0))|relation_field(inclusion_relation(X0))=X0)),
% 0.10/0.45 inference(destructive_equality_resolution,[status(thm)],[f81])).
% 0.10/0.45 fof(f192,plain,(
% 0.10/0.45 ![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.10/0.45 inference(destructive_equality_resolution,[status(thm)],[f82])).
% 0.10/0.45 fof(f193,plain,(
% 0.10/0.45 ![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.10/0.45 inference(destructive_equality_resolution,[status(thm)],[f83])).
% 0.10/0.47 fof(f198,plain,(
% 0.10/0.47 ![X0,X1,X2]: (~in(X0,X1)|~in(X2,X1)|in(ordered_pair(X0,X2),inclusion_relation(X1))|~subset(X0,X2))),
% 0.10/0.47 inference(backward_subsumption_resolution,[status(thm)],[f193,f102])).
% 0.10/0.47 fof(f199,plain,(
% 0.10/0.47 ![X0,X1,X2]: (~in(X0,X1)|~in(X2,X1)|~in(ordered_pair(X0,X2),inclusion_relation(X1))|subset(X0,X2))),
% 0.10/0.47 inference(backward_subsumption_resolution,[status(thm)],[f192,f102])).
% 0.10/0.47 fof(f200,plain,(
% 0.10/0.47 ![X0]: (relation_field(inclusion_relation(X0))=X0)),
% 0.10/0.47 inference(backward_subsumption_resolution,[status(thm)],[f191,f102])).
% 0.10/0.47 fof(f203,plain,(
% 0.10/0.47 ![X0]: (transitive(inclusion_relation(X0))|~is_transitive_in(inclusion_relation(X0),relation_field(inclusion_relation(X0))))),
% 0.10/0.47 inference(resolution,[status(thm)],[f76,f102])).
% 0.10/0.47 fof(f204,plain,(
% 0.10/0.47 ![X0]: (transitive(inclusion_relation(X0))|~is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.47 inference(forward_demodulation,[status(thm)],[f200,f203])).
% 0.10/0.47 fof(f271,plain,(
% 0.10/0.47 ![X0,X1]: (~relation(inclusion_relation(X0))|is_transitive_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK4_skl(X1,inclusion_relation(X0)),X0)|subset(sK2_skl(X1,inclusion_relation(X0)),sK4_skl(X1,inclusion_relation(X0))))),
% 0.10/0.47 inference(resolution,[status(thm)],[f99,f199])).
% 0.10/0.47 fof(f273,plain,(
% 0.10/0.47 ![X0,X1]: (is_transitive_in(inclusion_relation(X0),X1)|~in(sK2_skl(X1,inclusion_relation(X0)),X0)|~in(sK4_skl(X1,inclusion_relation(X0)),X0)|subset(sK2_skl(X1,inclusion_relation(X0)),sK4_skl(X1,inclusion_relation(X0))))),
% 0.10/0.47 inference(forward_subsumption_resolution,[status(thm)],[f271,f102])).
% 0.10/0.47 fof(f310,plain,(
% 0.10/0.47 ![X0,X1]: (~relation(inclusion_relation(X0))|is_transitive_in(inclusion_relation(X0),X1)|~in(sK4_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|subset(sK4_skl(X1,inclusion_relation(X0)),sK3_skl(X1,inclusion_relation(X0))))),
% 0.10/0.47 inference(resolution,[status(thm)],[f100,f199])).
% 0.10/0.47 fof(f312,plain,(
% 0.10/0.47 ![X0,X1]: (is_transitive_in(inclusion_relation(X0),X1)|~in(sK4_skl(X1,inclusion_relation(X0)),X0)|~in(sK3_skl(X1,inclusion_relation(X0)),X0)|subset(sK4_skl(X1,inclusion_relation(X0)),sK3_skl(X1,inclusion_relation(X0))))),
% 0.10/0.47 inference(forward_subsumption_resolution,[status(thm)],[f310,f102])).
% 0.10/0.47 fof(f313,plain,(
% 0.10/0.47 ![X0,X1]: (~relation(inclusion_relation(X0))|is_transitive_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.10/0.47 inference(resolution,[status(thm)],[f101,f198])).
% 0.10/0.47 fof(f314,plain,(
% 0.10/0.47 ![X0,X1]: (is_transitive_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.10/0.47 inference(forward_subsumption_resolution,[status(thm)],[f313,f102])).
% 0.10/0.47 fof(f362,plain,(
% 0.10/0.47 ![X0,X1,X2]: (~subset(sK2_skl(X0,inclusion_relation(X1)),X2)|~subset(X2,sK3_skl(X0,inclusion_relation(X1)))|is_transitive_in(inclusion_relation(X1),X0)|~in(sK2_skl(X0,inclusion_relation(X1)),X1)|~in(sK3_skl(X0,inclusion_relation(X1)),X1))),
% 0.10/0.47 inference(resolution,[status(thm)],[f166,f314])).
% 0.10/0.47 fof(f370,plain,(
% 0.10/0.47 ![X0,X1]: (~subset(sK2_skl(X0,inclusion_relation(X0)),X1)|~subset(X1,sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0))|is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.47 inference(resolution,[status(thm)],[f362,f98])).
% 0.10/0.47 fof(f371,plain,(
% 0.10/0.47 ![X0,X1]: (~subset(sK2_skl(X0,inclusion_relation(X0)),X1)|~subset(X1,sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0)))),
% 0.10/0.47 inference(duplicate_literals_removal,[status(thm)],[f370])).
% 0.10/0.47 fof(f372,plain,(
% 0.10/0.47 ![X0,X1]: (~subset(sK2_skl(X0,inclusion_relation(X0)),X1)|~subset(X1,sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0)))),
% 0.10/0.47 inference(forward_subsumption_resolution,[status(thm)],[f371,f96])).
% 0.10/0.48 fof(f373,plain,(
% 0.10/0.48 ![X0,X1]: (~subset(sK2_skl(X0,inclusion_relation(X0)),X1)|~subset(X1,sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f372,f102])).
% 0.10/0.48 fof(f374,plain,(
% 0.10/0.48 ![X0]: (~subset(sK4_skl(X0,inclusion_relation(X0)),sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|is_transitive_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~in(sK4_skl(X0,inclusion_relation(X0)),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f373,f273])).
% 0.10/0.48 fof(f377,plain,(
% 0.10/0.48 ![X0]: (~subset(sK4_skl(X0,inclusion_relation(X0)),sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~in(sK4_skl(X0,inclusion_relation(X0)),X0))),
% 0.10/0.48 inference(duplicate_literals_removal,[status(thm)],[f374])).
% 0.10/0.48 fof(f387,plain,(
% 0.10/0.48 ![X0]: (~subset(sK4_skl(X0,inclusion_relation(X0)),sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0))|is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f377,f97])).
% 0.10/0.48 fof(f388,plain,(
% 0.10/0.48 ![X0]: (~subset(sK4_skl(X0,inclusion_relation(X0)),sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~in(sK2_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0)))),
% 0.10/0.48 inference(duplicate_literals_removal,[status(thm)],[f387])).
% 0.10/0.48 fof(f389,plain,(
% 0.10/0.48 ![X0]: (~subset(sK4_skl(X0,inclusion_relation(X0)),sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0)))),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f388,f96])).
% 0.10/0.48 fof(f412,plain,(
% 0.10/0.48 ![X0]: (~subset(sK4_skl(X0,inclusion_relation(X0)),sK3_skl(X0,inclusion_relation(X0)))|is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f389,f102])).
% 0.10/0.48 fof(f413,plain,(
% 0.10/0.48 ![X0]: (is_transitive_in(inclusion_relation(X0),X0)|is_transitive_in(inclusion_relation(X0),X0)|~in(sK4_skl(X0,inclusion_relation(X0)),X0)|~in(sK3_skl(X0,inclusion_relation(X0)),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f412,f312])).
% 0.10/0.48 fof(f415,plain,(
% 0.10/0.48 ![X0]: (is_transitive_in(inclusion_relation(X0),X0)|~in(sK4_skl(X0,inclusion_relation(X0)),X0)|~in(sK3_skl(X0,inclusion_relation(X0)),X0))),
% 0.10/0.48 inference(duplicate_literals_removal,[status(thm)],[f413])).
% 0.10/0.48 fof(f419,plain,(
% 0.10/0.48 ![X0]: (is_transitive_in(inclusion_relation(X0),X0)|~in(sK3_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0))|is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f415,f97])).
% 0.10/0.48 fof(f420,plain,(
% 0.10/0.48 ![X0]: (is_transitive_in(inclusion_relation(X0),X0)|~in(sK3_skl(X0,inclusion_relation(X0)),X0)|~relation(inclusion_relation(X0)))),
% 0.10/0.48 inference(duplicate_literals_removal,[status(thm)],[f419])).
% 0.10/0.48 fof(f421,plain,(
% 0.10/0.48 ![X0]: (is_transitive_in(inclusion_relation(X0),X0)|~relation(inclusion_relation(X0)))),
% 0.10/0.48 inference(forward_subsumption_resolution,[status(thm)],[f420,f98])).
% 0.10/0.48 fof(f422,plain,(
% 0.10/0.48 ![X0]: (is_transitive_in(inclusion_relation(X0),X0))),
% 0.10/0.48 inference(resolution,[status(thm)],[f421,f102])).
% 0.10/0.48 fof(f423,plain,(
% 0.10/0.48 ![X0]: (transitive(inclusion_relation(X0)))),
% 0.10/0.48 inference(backward_subsumption_resolution,[status(thm)],[f204,f422])).
% 0.10/0.48 fof(f425,plain,(
% 0.10/0.48 $false),
% 0.10/0.48 inference(backward_subsumption_resolution,[status(thm)],[f175,f423])).
% 0.10/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.49 % Elapsed time: 0.118555 seconds
% 0.10/0.49 % CPU time: 0.625957 seconds
% 0.10/0.49 % Total memory used: 111.564 MB
% 0.10/0.49 % Net memory used: 110.967 MB
%------------------------------------------------------------------------------