%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU178+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:21:54 PM UTC 2026
% Result : Theorem 76.86s 10.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU178+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.15/0.43 % Computer : n019.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 05:55:19 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 76.86/10.31 % Refutation found
% 76.86/10.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.86/10.31 % SZS output start CNFRefutation for theBenchmark
% 76.86/10.31 fof(f3,axiom,(
% 76.86/10.31 (! [A] :( relation(A)<=> (! [B] :~ ( in(B,A)& (! [C,D] : B != ordered_pair(C,D) )) )) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f4,axiom,(
% 76.86/10.31 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f5,axiom,(
% 76.86/10.31 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f6,axiom,(
% 76.86/10.31 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f24,axiom,(
% 76.86/10.31 (? [A] :( empty(A)& relation(A) ) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f30,axiom,(
% 76.86/10.31 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f32,conjecture,(
% 76.86/10.31 (! [A] :( relation(A)=> subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ) )),
% 76.86/10.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.86/10.31 fof(f33,negated_conjecture,(
% 76.86/10.31 ~((! [A] :( relation(A)=> subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ) ))),
% 76.86/10.31 inference(negated_conjecture,[status(cth)],[f32])).
% 76.86/10.31 fof(f44,plain,(
% 76.86/10.31 ![A]: (relation(A)<=>(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))),
% 76.86/10.31 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 76.86/10.31 fof(f45,plain,(
% 76.86/10.31 ![A]: ((~relation(A)|(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D)))))&(relation(A)|(?[B]: (in(B,A)&(![C,D]: ~B=ordered_pair(C,D))))))),
% 76.86/10.31 inference(NNF_transformation,[status(thm)],[f44])).
% 76.86/10.31 fof(f46,plain,(
% 76.86/10.31 (![A]: (~relation(A)|(![B]: (~in(B,A)|(?[C,D]: B=ordered_pair(C,D))))))&(![A]: (relation(A)|(?[B]: (in(B,A)&(![C,D]: ~B=ordered_pair(C,D))))))),
% 76.86/10.31 inference(miniscoping,[status(thm)],[f45])).
% 76.86/10.31 fof(f47,plain,(
% 76.86/10.31 (![A]: (~relation(A)|(![B]: (~in(B,A)|B=ordered_pair(sK0_skl(B,A),sK1_skl(B,A))))))&(![A]: (relation(A)|(in(sK2_skl(A),A)&(![C,D]: ~sK2_skl(A)=ordered_pair(C,D)))))),
% 76.86/10.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A)),skolemize(B,sK2_skl(A))],[f46])).
% 76.86/10.31 fof(f48,plain,(
% 76.86/10.31 ![X0,X1]: (~relation(X0)|~in(X1,X0)|X1=ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f47])).
% 76.86/10.31 fof(f51,plain,(
% 76.86/10.31 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 76.86/10.31 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 76.86/10.31 fof(f52,plain,(
% 76.86/10.31 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 76.86/10.31 inference(NNF_transformation,[status(thm)],[f51])).
% 76.86/10.31 fof(f53,plain,(
% 76.86/10.31 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 76.86/10.31 inference(miniscoping,[status(thm)],[f52])).
% 76.86/10.31 fof(f54,plain,(
% 76.86/10.31 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK3_skl(B,A),A)&~in(sK3_skl(B,A),B))))),
% 76.86/10.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f53])).
% 76.86/10.31 fof(f56,plain,(
% 76.86/10.31 ![X0,X1]: (subset(X0,X1)|in(sK3_skl(X1,X0),X0))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f54])).
% 76.86/10.31 fof(f57,plain,(
% 76.86/10.31 ![X0,X1]: (subset(X0,X1)|~in(sK3_skl(X1,X0),X1))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f54])).
% 76.86/10.31 fof(f58,plain,(
% 76.86/10.31 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 76.86/10.31 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 76.86/10.31 fof(f59,plain,(
% 76.86/10.31 ![A]: (~relation(A)|(![B]: ((~B=relation_dom(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(C,D),A)))&(in(C,B)|(![D]: ~in(ordered_pair(C,D),A))))))&(B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 76.86/10.31 inference(NNF_transformation,[status(thm)],[f58])).
% 76.86/10.31 fof(f60,plain,(
% 76.86/10.31 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(C,D),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 76.86/10.31 inference(miniscoping,[status(thm)],[f59])).
% 76.86/10.31 fof(f61,plain,(
% 76.86/10.31 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|in(ordered_pair(C,sK4_skl(C,B,A)),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|((~in(sK5_skl(B,A),B)|(![D]: ~in(ordered_pair(sK5_skl(B,A),D),A)))&(in(sK5_skl(B,A),B)|in(ordered_pair(sK5_skl(B,A),sK6_skl(B,A)),A)))))))),
% 76.86/10.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f60])).
% 76.86/10.31 fof(f63,plain,(
% 76.86/10.31 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f61])).
% 76.86/10.31 fof(f66,plain,(
% 76.86/10.31 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 76.86/10.31 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 76.86/10.31 fof(f67,plain,(
% 76.86/10.31 ![A]: (~relation(A)|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(D,C),A)))&(in(C,B)|(![D]: ~in(ordered_pair(D,C),A))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 76.86/10.31 inference(NNF_transformation,[status(thm)],[f66])).
% 76.86/10.31 fof(f68,plain,(
% 76.86/10.31 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(D,C),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 76.86/10.31 inference(miniscoping,[status(thm)],[f67])).
% 76.86/10.31 fof(f69,plain,(
% 76.86/10.31 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|in(ordered_pair(sK7_skl(C,B,A),C),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|((~in(sK8_skl(B,A),B)|(![D]: ~in(ordered_pair(D,sK8_skl(B,A)),A)))&(in(sK8_skl(B,A),B)|in(ordered_pair(sK9_skl(B,A),sK8_skl(B,A)),A)))))))),
% 76.86/10.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(D,sK7_skl(C,B,A)),skolemize(C,sK8_skl(B,A)),skolemize(D,sK9_skl(B,A))],[f68])).
% 76.86/10.31 fof(f71,plain,(
% 76.86/10.31 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f69])).
% 76.86/10.31 fof(f84,plain,(
% 76.86/10.31 (empty(sK11_skl)&relation(sK11_skl))),
% 76.86/10.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f24])).
% 76.86/10.31 fof(f85,plain,(
% 76.86/10.31 empty(sK11_skl)),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f84])).
% 76.86/10.31 fof(f100,plain,(
% 76.86/10.31 ![A,B,C,D]: ((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 76.86/10.31 inference(NNF_transformation,[status(thm)],[f30])).
% 76.86/10.31 fof(f101,plain,(
% 76.86/10.31 (![A,B,C,D]: (~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D))))&(![A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 76.86/10.31 inference(miniscoping,[status(thm)],[f100])).
% 76.86/10.31 fof(f102,plain,(
% 76.86/10.31 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X0,X2))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f101])).
% 76.86/10.31 fof(f104,plain,(
% 76.86/10.31 ![X0,X1,X2,X3]: (in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|~in(X0,X2)|~in(X1,X3))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f101])).
% 76.86/10.31 fof(f107,plain,(
% 76.86/10.31 (?[A]: (relation(A)&~subset(A,cartesian_product2(relation_dom(A),relation_rng(A)))))),
% 76.86/10.31 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 76.86/10.31 fof(f108,plain,(
% 76.86/10.31 (relation(sK16_skl)&~subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl))))),
% 76.86/10.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f107])).
% 76.86/10.31 fof(f109,plain,(
% 76.86/10.31 relation(sK16_skl)),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f108])).
% 76.86/10.31 fof(f110,plain,(
% 76.86/10.31 ~subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)))),
% 76.86/10.31 inference(cnf_transformation,[status(thm)],[f108])).
% 76.86/10.31 fof(f132,plain,(
% 76.86/10.31 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 76.86/10.31 inference(destructive_equality_resolution,[status(thm)],[f63])).
% 76.86/10.31 fof(f134,plain,(
% 76.86/10.31 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 76.86/10.31 inference(destructive_equality_resolution,[status(thm)],[f71])).
% 76.86/10.31 fof(f506,plain,(
% 76.86/10.31 ![X0,X1]: (subset(X0,X1)|~relation(X0)|sK3_skl(X1,X0)=ordered_pair(sK0_skl(sK3_skl(X1,X0),X0),sK1_skl(sK3_skl(X1,X0),X0)))),
% 76.86/10.31 inference(resolution,[status(thm)],[f56,f48])).
% 76.86/10.31 fof(f702,plain,(
% 76.86/10.31 ~relation(sK16_skl)|sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl)=ordered_pair(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl))),
% 76.86/10.31 inference(resolution,[status(thm)],[f506,f110])).
% 76.86/10.31 fof(f773,definition,(
% 76.86/10.31 sQ12_spl <=> (relation(sK16_skl))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f775,plain,(
% 76.86/10.31 ~relation(sK16_skl)|sQ12_spl),
% 76.86/10.31 inference(component_clause,[status(thm)],[f773])).
% 76.86/10.31 fof(f776,definition,(
% 76.86/10.31 sQ13_spl <=> (sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl)=ordered_pair(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f777,plain,(
% 76.86/10.31 sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl)=ordered_pair(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl))|~sQ13_spl),
% 76.86/10.31 inference(component_clause,[status(thm)],[f776])).
% 76.86/10.31 fof(f779,plain,(
% 76.86/10.31 ~sQ12_spl|sQ13_spl),
% 76.86/10.31 inference(split_clause,[status(thm)],[f702,f773,f776])).
% 76.86/10.31 fof(f781,plain,(
% 76.86/10.31 $false|sQ12_spl),
% 76.86/10.31 inference(forward_subsumption_resolution,[status(thm)],[f775,f109])).
% 76.86/10.31 fof(f782,plain,(
% 76.86/10.31 sQ12_spl),
% 76.86/10.31 inference(contradiction_clause,[status(thm)],[f781])).
% 76.86/10.31 fof(f1096,plain,(
% 76.86/10.31 ![X0]: (~relation(X0)|in(sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_rng(X0))|~in(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),X0)|~sQ13_spl)),
% 76.86/10.31 inference(paramodulation,[status(thm)],[f777,f134])).
% 76.86/10.31 fof(f1097,plain,(
% 76.86/10.31 ![X0]: (~relation(X0)|in(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_dom(X0))|~in(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),X0)|~sQ13_spl)),
% 76.86/10.31 inference(paramodulation,[status(thm)],[f777,f132])).
% 76.86/10.31 fof(f1259,plain,(
% 76.86/10.31 ![X0,X1]: (in(ordered_pair(sK3_skl(X0,X1),sK3_skl(X0,X1)),cartesian_product2(X1,X1))|subset(X1,X0))),
% 76.86/10.31 inference(resolution,[status(thm)],[f104,f56])).
% 76.86/10.31 fof(f1260,plain,(
% 76.86/10.31 ![X0,X1,X2,X3]: (in(ordered_pair(sK3_skl(X0,X1),X2),cartesian_product2(X1,X3))|~in(X2,X3)|subset(X1,X0))),
% 76.86/10.31 inference(resolution,[status(thm)],[f104,f56])).
% 76.86/10.31 fof(f1415,plain,(
% 76.86/10.31 ![X0,X1]: (in(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),cartesian_product2(X0,X1))|~in(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),X0)|~in(sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),X1)|~sQ13_spl)),
% 76.86/10.31 inference(paramodulation,[status(thm)],[f777,f104])).
% 76.86/10.31 fof(f1417,definition,(
% 76.86/10.31 ![X0,X1]: (sQ43_spl <=> (~in(X0,X1)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f1418,plain,(
% 76.86/10.31 ![X0,X1]: (~in(X0,X1)|~sQ43_spl)),
% 76.86/10.31 inference(component_clause,[status(thm)],[f1417])).
% 76.86/10.31 fof(f2402,plain,(
% 76.86/10.31 ![X0,X1,X2,X3]: (~in(X0,X1)|subset(X2,X3)|in(sK3_skl(X3,X2),X2))),
% 76.86/10.31 inference(resolution,[status(thm)],[f1260,f102])).
% 76.86/10.31 fof(f2504,definition,(
% 76.86/10.31 ![X2,X3]: (sQ100_spl <=> (subset(X2,X3)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f2505,plain,(
% 76.86/10.31 ![X0,X1]: (subset(X0,X1)|~sQ100_spl)),
% 76.86/10.31 inference(component_clause,[status(thm)],[f2504])).
% 76.86/10.31 fof(f2508,definition,(
% 76.86/10.31 ![X2,X3]: (sQ101_spl <=> (subset(X2,X3)|in(sK3_skl(X3,X2),X2)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f2509,plain,(
% 76.86/10.31 ![X0,X1]: (subset(X0,X1)|in(sK3_skl(X1,X0),X0)|~sQ101_spl)),
% 76.86/10.31 inference(component_clause,[status(thm)],[f2508])).
% 76.86/10.31 fof(f2511,plain,(
% 76.86/10.31 sQ43_spl|sQ101_spl),
% 76.86/10.31 inference(split_clause,[status(thm)],[f2402,f1417,f2508])).
% 76.86/10.31 fof(f5027,definition,(
% 76.86/10.31 sQ170_spl <=> (subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl))))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f5028,plain,(
% 76.86/10.31 subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)))|~sQ170_spl),
% 76.86/10.31 inference(component_clause,[status(thm)],[f5027])).
% 76.86/10.31 fof(f5067,plain,(
% 76.86/10.31 $false|~sQ170_spl),
% 76.86/10.31 inference(forward_subsumption_resolution,[status(thm)],[f5028,f110])).
% 76.86/10.31 fof(f5068,plain,(
% 76.86/10.31 ~sQ170_spl),
% 76.86/10.31 inference(contradiction_clause,[status(thm)],[f5067])).
% 76.86/10.31 fof(f5141,plain,(
% 76.86/10.31 ![X0,X1]: (subset(X0,X1)|~sQ43_spl)),
% 76.86/10.31 inference(backward_subsumption_resolution,[status(thm)],[f1259,f1418])).
% 76.86/10.31 fof(f10631,definition,(
% 76.86/10.31 ![X0]: (sQ271_spl <=> (~empty(X0)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f10632,plain,(
% 76.86/10.31 ![X0]: (~empty(X0)|~sQ271_spl)),
% 76.86/10.31 inference(component_clause,[status(thm)],[f10631])).
% 76.86/10.31 fof(f13846,plain,(
% 76.86/10.31 $false|~sQ100_spl),
% 76.86/10.31 inference(backward_subsumption_resolution,[status(thm)],[f110,f2505])).
% 76.86/10.31 fof(f13861,plain,(
% 76.86/10.31 ~sQ100_spl),
% 76.86/10.31 inference(contradiction_clause,[status(thm)],[f13846])).
% 76.86/10.31 fof(f15694,plain,(
% 76.86/10.31 $false|~sQ271_spl),
% 76.86/10.31 inference(forward_subsumption_resolution,[status(thm)],[f85,f10632])).
% 76.86/10.31 fof(f15695,plain,(
% 76.86/10.31 ~sQ271_spl),
% 76.86/10.31 inference(contradiction_clause,[status(thm)],[f15694])).
% 76.86/10.31 fof(f17462,plain,(
% 76.86/10.31 ~relation(sK16_skl)|in(sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_rng(sK16_skl))|subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)))|~sQ13_spl|~sQ101_spl),
% 76.86/10.31 inference(resolution,[status(thm)],[f1096,f2509])).
% 76.86/10.31 fof(f17467,definition,(
% 76.86/10.31 sQ335_spl <=> (in(sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_rng(sK16_skl)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f17470,plain,(
% 76.86/10.31 ~sQ12_spl|sQ335_spl|sQ170_spl|~sQ13_spl|~sQ101_spl),
% 76.86/10.31 inference(split_clause,[status(thm)],[f17462,f773,f17467,f5027,f776,f2508])).
% 76.86/10.31 fof(f20274,plain,(
% 76.86/10.31 ~relation(sK16_skl)|in(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_dom(sK16_skl))|subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)))|~sQ13_spl|~sQ101_spl),
% 76.86/10.31 inference(resolution,[status(thm)],[f1097,f2509])).
% 76.86/10.31 fof(f20280,definition,(
% 76.86/10.31 sQ384_spl <=> (in(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_dom(sK16_skl)))),
% 76.86/10.31 introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition])).
% 76.86/10.31 fof(f20283,plain,(
% 76.86/10.31 ~sQ12_spl|sQ384_spl|sQ170_spl|~sQ13_spl|~sQ101_spl),
% 76.86/10.31 inference(split_clause,[status(thm)],[f20274,f773,f20280,f5027,f776,f2508])).
% 76.86/10.31 fof(f20295,plain,(
% 76.86/10.31 ~in(sK0_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_dom(sK16_skl))|~in(sK1_skl(sK3_skl(cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)),sK16_skl),sK16_skl),relation_rng(sK16_skl))|subset(sK16_skl,cartesian_product2(relation_dom(sK16_skl),relation_rng(sK16_skl)))|~sQ13_spl),
% 76.86/10.31 inference(resolution,[status(thm)],[f1415,f57])).
% 76.86/10.33 fof(f20330,plain,(
% 76.86/10.33 ~sQ384_spl|~sQ335_spl|sQ170_spl|~sQ13_spl),
% 76.86/10.33 inference(split_clause,[status(thm)],[f20295,f20280,f17467,f5027,f776])).
% 76.86/10.33 fof(f20332,plain,(
% 76.86/10.33 sQ100_spl|~sQ43_spl),
% 76.86/10.33 inference(split_clause,[status(thm)],[f5141,f2504,f1417])).
% 76.86/10.33 fof(f20341,plain,(
% 76.86/10.33 $false),
% 76.86/10.33 inference(sat_refutation,[status(thm)],[f779,f782,f2511,f5068,f13861,f15695,f17470,f20283,f20330,f20332])).
% 76.86/10.33 % SZS output end CNFRefutation for theBenchmark.p
% 1.67/10.37 % Elapsed time: 9.921589 seconds
% 1.67/10.37 % CPU time: 77.928807 seconds
% 1.67/10.37 % Total memory used: 430.302 MB
% 1.67/10.37 % Net memory used: 387.638 MB
%------------------------------------------------------------------------------