%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU292+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 : 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:14 PM UTC 2026
% Result : Theorem 0.14s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU292+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 06:08:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.49 % Refutation found
% 0.14/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.49 fof(f4,axiom,(
% 0.14/0.49 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f6,axiom,(
% 0.14/0.49 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> ( ( ( B = empty_set=> A = empty_set )=> ( quasi_total(C,A,B)<=> A = relation_dom_as_subset(A,B,C) ) )& ( B = empty_set=> ( A = empty_set| ( quasi_total(C,A,B)<=> C = empty_set ) ) ) ) ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f16,axiom,(
% 0.14/0.49 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f35,axiom,(
% 0.14/0.49 (? [A] : empty(A) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f36,axiom,(
% 0.14/0.49 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f44,axiom,(
% 0.14/0.49 (! [A,B,C] :( relation_of2(C,A,B)=> relation_dom_as_subset(A,B,C) = relation_dom(C) ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f45,axiom,(
% 0.14/0.49 (! [A,B,C] :( relation_of2_as_subset(C,A,B)<=> relation_of2(C,A,B) ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f48,conjecture,(
% 0.14/0.49 (! [A,B,C,D] :( ( function(D)& quasi_total(D,A,B)& relation_of2_as_subset(D,A,B) )=> (! [E] :( ( relation(E)& function(E) )=> ( in(C,A)=> ( B = empty_set| apply(relation_composition(D,E),C) = apply(E,apply(D,C)) ) ) ) )) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f49,negated_conjecture,(
% 0.14/0.49 ~((! [A,B,C,D] :( ( function(D)& quasi_total(D,A,B)& relation_of2_as_subset(D,A,B) )=> (! [E] :( ( relation(E)& function(E) )=> ( in(C,A)=> ( B = empty_set| apply(relation_composition(D,E),C) = apply(E,apply(D,C)) ) ) ) )) ))),
% 0.14/0.49 inference(negated_conjecture,[status(cth)],[f48])).
% 0.14/0.49 fof(f50,axiom,(
% 0.14/0.49 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( in(A,relation_dom(B))=> apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) )) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f55,axiom,(
% 0.14/0.49 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.14/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.49 fof(f64,plain,(
% 0.14/0.49 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.14/0.49 fof(f65,plain,(
% 0.14/0.49 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f64])).
% 0.14/0.49 fof(f66,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f65])).
% 0.14/0.49 fof(f71,plain,(
% 0.14/0.49 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|(((B=empty_set&~A=empty_set)|(quasi_total(C,A,B)<=>A=relation_dom_as_subset(A,B,C)))&(~B=empty_set|(A=empty_set|(quasi_total(C,A,B)<=>C=empty_set)))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.14/0.49 fof(f72,definition,(
% 0.14/0.49 ![A,B]: (sP0_prd(B,A)<=>(B=empty_set&~A=empty_set))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.14/0.49 fof(f73,plain,(
% 0.14/0.49 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|((sP0_prd(B,A)|(quasi_total(C,A,B)<=>A=relation_dom_as_subset(A,B,C)))&(~B=empty_set|(A=empty_set|(quasi_total(C,A,B)<=>C=empty_set)))))),
% 0.14/0.49 inference(formula_renaming,[status(thm)],[f71,f72])).
% 0.14/0.49 fof(f74,plain,(
% 0.14/0.49 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|((sP0_prd(B,A)|((~quasi_total(C,A,B)|A=relation_dom_as_subset(A,B,C))&(quasi_total(C,A,B)|~A=relation_dom_as_subset(A,B,C))))&(~B=empty_set|(A=empty_set|((~quasi_total(C,A,B)|C=empty_set)&(quasi_total(C,A,B)|~C=empty_set))))))),
% 0.14/0.49 inference(NNF_transformation,[status(thm)],[f73])).
% 0.14/0.49 fof(f75,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|sP0_prd(X2,X1)|~quasi_total(X0,X1,X2)|X1=relation_dom_as_subset(X1,X2,X0))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f74])).
% 0.14/0.49 fof(f83,plain,(
% 0.14/0.49 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.14/0.49 fof(f84,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f83])).
% 0.14/0.49 fof(f134,plain,(
% 0.14/0.49 empty(sK8_skl)),
% 0.14/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f35])).
% 0.14/0.49 fof(f135,plain,(
% 0.14/0.49 empty(sK8_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f134])).
% 0.14/0.49 fof(f136,plain,(
% 0.14/0.49 ((relation(sK9_skl)&empty(sK9_skl))&function(sK9_skl))),
% 0.14/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f36])).
% 0.14/0.49 fof(f138,plain,(
% 0.14/0.49 empty(sK9_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.14/0.49 fof(f163,plain,(
% 0.14/0.49 ![A,B,C]: (~relation_of2(C,A,B)|relation_dom_as_subset(A,B,C)=relation_dom(C))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.14/0.49 fof(f164,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~relation_of2(X0,X1,X2)|relation_dom_as_subset(X1,X2,X0)=relation_dom(X0))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f163])).
% 0.14/0.49 fof(f165,plain,(
% 0.14/0.49 ![A,B,C]: ((~relation_of2_as_subset(C,A,B)|relation_of2(C,A,B))&(relation_of2_as_subset(C,A,B)|~relation_of2(C,A,B)))),
% 0.14/0.49 inference(NNF_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f166,plain,(
% 0.14/0.49 (![A,B,C]: (~relation_of2_as_subset(C,A,B)|relation_of2(C,A,B)))&(![A,B,C]: (relation_of2_as_subset(C,A,B)|~relation_of2(C,A,B)))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f165])).
% 0.14/0.49 fof(f167,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|relation_of2(X0,X1,X2))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f166])).
% 0.14/0.49 fof(f173,plain,(
% 0.14/0.49 (?[A,B,C,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(?[E]: ((relation(E)&function(E))&(in(C,A)&(~B=empty_set&~apply(relation_composition(D,E),C)=apply(E,apply(D,C))))))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.14/0.49 fof(f174,plain,(
% 0.14/0.49 ?[A,B,D]: (((function(D)&quasi_total(D,A,B))&relation_of2_as_subset(D,A,B))&(?[E]: ((relation(E)&function(E))&(?[C]: (in(C,A)&(~B=empty_set&~apply(relation_composition(D,E),C)=apply(E,apply(D,C))))))))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f173])).
% 0.14/0.49 fof(f175,plain,(
% 0.14/0.49 (((function(sK19_skl)&quasi_total(sK19_skl,sK17_skl,sK18_skl))&relation_of2_as_subset(sK19_skl,sK17_skl,sK18_skl))&((relation(sK20_skl)&function(sK20_skl))&(in(sK21_skl,sK17_skl)&(~sK18_skl=empty_set&~apply(relation_composition(sK19_skl,sK20_skl),sK21_skl)=apply(sK20_skl,apply(sK19_skl,sK21_skl))))))),
% 0.14/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(A,sK17_skl),skolemize(B,sK18_skl),skolemize(D,sK19_skl),skolemize(E,sK20_skl),skolemize(C,sK21_skl)],[f174])).
% 0.14/0.49 fof(f176,plain,(
% 0.14/0.49 function(sK19_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f177,plain,(
% 0.14/0.49 quasi_total(sK19_skl,sK17_skl,sK18_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f178,plain,(
% 0.14/0.49 relation_of2_as_subset(sK19_skl,sK17_skl,sK18_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f179,plain,(
% 0.14/0.49 relation(sK20_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f180,plain,(
% 0.14/0.49 function(sK20_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f181,plain,(
% 0.14/0.49 in(sK21_skl,sK17_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f182,plain,(
% 0.14/0.49 ~sK18_skl=empty_set),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f183,plain,(
% 0.14/0.49 ~apply(relation_composition(sK19_skl,sK20_skl),sK21_skl)=apply(sK20_skl,apply(sK19_skl,sK21_skl))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f175])).
% 0.14/0.49 fof(f184,plain,(
% 0.14/0.49 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(~in(A,relation_dom(B))|apply(relation_composition(B,C),A)=apply(C,apply(B,A))))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.14/0.49 fof(f185,plain,(
% 0.14/0.49 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(![A]: (~in(A,relation_dom(B))|apply(relation_composition(B,C),A)=apply(C,apply(B,A)))))))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f184])).
% 0.14/0.49 fof(f186,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~in(X2,relation_dom(X0))|apply(relation_composition(X0,X1),X2)=apply(X1,apply(X0,X2)))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f185])).
% 0.14/0.49 fof(f199,plain,(
% 0.14/0.49 ![A]: (~empty(A)|A=empty_set)),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.14/0.49 fof(f200,plain,(
% 0.14/0.49 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f199])).
% 0.14/0.49 fof(f207,plain,(
% 0.14/0.49 ![A,B]: ((~sP0_prd(B,A)|(B=empty_set&~A=empty_set))&(sP0_prd(B,A)|(~B=empty_set|A=empty_set)))),
% 0.14/0.49 inference(NNF_transformation,[status(thm)],[f72])).
% 0.14/0.49 fof(f208,plain,(
% 0.14/0.49 (![A,B]: (~sP0_prd(B,A)|(B=empty_set&~A=empty_set)))&(![A,B]: (sP0_prd(B,A)|(~B=empty_set|A=empty_set)))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f207])).
% 0.14/0.49 fof(f209,plain,(
% 0.14/0.49 ![X0,X1]: (~sP0_prd(X0,X1)|X0=empty_set)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f208])).
% 0.14/0.49 fof(f274,plain,(
% 0.14/0.49 sP0_prd(sK18_skl,sK17_skl)|~quasi_total(sK19_skl,sK17_skl,sK18_skl)|sK17_skl=relation_dom_as_subset(sK17_skl,sK18_skl,sK19_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f178,f75])).
% 0.14/0.49 fof(f275,definition,(
% 0.14/0.49 sQ10_spl <=> (sP0_prd(sK18_skl,sK17_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f276,plain,(
% 0.14/0.49 sP0_prd(sK18_skl,sK17_skl)|~sQ10_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f275])).
% 0.14/0.49 fof(f278,definition,(
% 0.14/0.49 sQ11_spl <=> (quasi_total(sK19_skl,sK17_skl,sK18_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f280,plain,(
% 0.14/0.49 ~quasi_total(sK19_skl,sK17_skl,sK18_skl)|sQ11_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f278])).
% 0.14/0.49 fof(f281,definition,(
% 0.14/0.49 sQ12_spl <=> (sK17_skl=relation_dom_as_subset(sK17_skl,sK18_skl,sK19_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f282,plain,(
% 0.14/0.49 sK17_skl=relation_dom_as_subset(sK17_skl,sK18_skl,sK19_skl)|~sQ12_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f281])).
% 0.14/0.49 fof(f284,plain,(
% 0.14/0.49 sQ10_spl|~sQ11_spl|sQ12_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f274,f275,f278,f281])).
% 0.14/0.49 fof(f291,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|relation(X0))),
% 0.14/0.49 inference(resolution,[status(thm)],[f84,f66])).
% 0.14/0.49 fof(f297,plain,(
% 0.14/0.49 sK9_skl=empty_set),
% 0.14/0.49 inference(resolution,[status(thm)],[f200,f138])).
% 0.14/0.49 fof(f298,plain,(
% 0.14/0.49 sK8_skl=empty_set),
% 0.14/0.49 inference(resolution,[status(thm)],[f200,f135])).
% 0.14/0.49 fof(f305,plain,(
% 0.14/0.49 ~sK18_skl=sK9_skl),
% 0.14/0.49 inference(backward_demodulation,[status(thm)],[f297,f182])).
% 0.14/0.49 fof(f317,plain,(
% 0.14/0.49 sK9_skl=sK8_skl),
% 0.14/0.49 inference(backward_demodulation,[status(thm)],[f298,f297])).
% 0.14/0.49 fof(f339,plain,(
% 0.14/0.49 ![X0,X1]: (~sP0_prd(X0,X1)|X0=sK8_skl)),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f298,f209])).
% 0.14/0.49 fof(f340,plain,(
% 0.14/0.49 sK18_skl=sK8_skl|~sQ10_spl),
% 0.14/0.49 inference(resolution,[status(thm)],[f339,f276])).
% 0.14/0.49 fof(f366,plain,(
% 0.14/0.49 ~sK8_skl=sK9_skl|~sQ10_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f340,f305])).
% 0.14/0.49 fof(f367,plain,(
% 0.14/0.49 ~sK8_skl=sK8_skl|~sQ10_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f317,f366])).
% 0.14/0.49 fof(f368,plain,(
% 0.14/0.49 $false|~sQ10_spl),
% 0.14/0.49 inference(trivial_equality_resolution,[status(thm)],[f367])).
% 0.14/0.49 fof(f369,plain,(
% 0.14/0.49 ~sQ10_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f368])).
% 0.14/0.49 fof(f375,plain,(
% 0.14/0.49 $false|sQ11_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f280,f177])).
% 0.14/0.49 fof(f376,plain,(
% 0.14/0.49 sQ11_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f375])).
% 0.14/0.49 fof(f407,plain,(
% 0.14/0.49 relation(sK19_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f291,f178])).
% 0.14/0.49 fof(f451,definition,(
% 0.14/0.49 sQ20_spl <=> (relation(sK19_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f453,plain,(
% 0.14/0.49 ~relation(sK19_skl)|sQ20_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f451])).
% 0.14/0.49 fof(f467,definition,(
% 0.14/0.49 sQ24_spl <=> (function(sK19_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f469,plain,(
% 0.14/0.49 ~function(sK19_skl)|sQ24_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f467])).
% 0.14/0.49 fof(f472,plain,(
% 0.14/0.49 $false|sQ20_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f453,f407])).
% 0.14/0.50 fof(f473,plain,(
% 0.14/0.50 sQ20_spl),
% 0.14/0.50 inference(contradiction_clause,[status(thm)],[f472])).
% 0.14/0.50 fof(f529,definition,(
% 0.14/0.50 sQ28_spl <=> (relation(sK20_skl))),
% 0.14/0.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.50 fof(f531,plain,(
% 0.14/0.50 ~relation(sK20_skl)|sQ28_spl),
% 0.14/0.50 inference(component_clause,[status(thm)],[f529])).
% 0.14/0.50 fof(f544,plain,(
% 0.14/0.50 $false|sQ28_spl),
% 0.14/0.50 inference(forward_subsumption_resolution,[status(thm)],[f531,f179])).
% 0.14/0.50 fof(f545,plain,(
% 0.14/0.50 sQ28_spl),
% 0.14/0.50 inference(contradiction_clause,[status(thm)],[f544])).
% 0.14/0.50 fof(f583,plain,(
% 0.14/0.50 $false|sQ24_spl),
% 0.14/0.50 inference(forward_subsumption_resolution,[status(thm)],[f469,f176])).
% 0.14/0.50 fof(f584,plain,(
% 0.14/0.50 sQ24_spl),
% 0.14/0.50 inference(contradiction_clause,[status(thm)],[f583])).
% 0.14/0.50 fof(f702,plain,(
% 0.14/0.50 relation_of2(sK19_skl,sK17_skl,sK18_skl)),
% 0.14/0.50 inference(resolution,[status(thm)],[f167,f178])).
% 0.14/0.50 fof(f709,plain,(
% 0.14/0.50 relation_dom_as_subset(sK17_skl,sK18_skl,sK19_skl)=relation_dom(sK19_skl)),
% 0.14/0.50 inference(resolution,[status(thm)],[f702,f164])).
% 0.14/0.50 fof(f712,plain,(
% 0.14/0.50 sK17_skl=relation_dom(sK19_skl)|~sQ12_spl),
% 0.14/0.50 inference(forward_demodulation,[status(thm)],[f282,f709])).
% 0.14/0.50 fof(f714,plain,(
% 0.14/0.50 ![X0,X1]: (~relation(sK19_skl)|~function(sK19_skl)|~relation(X0)|~function(X0)|~in(X1,sK17_skl)|apply(relation_composition(sK19_skl,X0),X1)=apply(X0,apply(sK19_skl,X1))|~sQ12_spl)),
% 0.14/0.50 inference(paramodulation,[status(thm)],[f712,f186])).
% 0.14/0.50 fof(f715,definition,(
% 0.14/0.50 ![X0,X1]: (sQ43_spl <=> (~relation(X0)|~function(X0)|~in(X1,sK17_skl)|apply(relation_composition(sK19_skl,X0),X1)=apply(X0,apply(sK19_skl,X1))))),
% 0.14/0.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.50 fof(f716,plain,(
% 0.14/0.50 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,sK17_skl)|apply(relation_composition(sK19_skl,X0),X1)=apply(X0,apply(sK19_skl,X1))|~sQ43_spl)),
% 0.14/0.50 inference(component_clause,[status(thm)],[f715])).
% 0.14/0.50 fof(f718,plain,(
% 0.14/0.50 ~sQ20_spl|~sQ24_spl|sQ43_spl|~sQ12_spl),
% 0.14/0.50 inference(split_clause,[status(thm)],[f714,f451,f467,f715,f281])).
% 0.14/0.50 fof(f1162,plain,(
% 0.14/0.50 ![X0]: (~relation(X0)|~function(X0)|apply(relation_composition(sK19_skl,X0),sK21_skl)=apply(X0,apply(sK19_skl,sK21_skl))|~sQ43_spl)),
% 0.14/0.50 inference(resolution,[status(thm)],[f716,f181])).
% 0.14/0.50 fof(f1177,plain,(
% 0.14/0.50 ~relation(sK20_skl)|apply(relation_composition(sK19_skl,sK20_skl),sK21_skl)=apply(sK20_skl,apply(sK19_skl,sK21_skl))|~sQ43_spl),
% 0.14/0.50 inference(resolution,[status(thm)],[f1162,f180])).
% 0.14/0.50 fof(f1203,definition,(
% 0.14/0.50 sQ70_spl <=> (apply(relation_composition(sK19_skl,sK20_skl),sK21_skl)=apply(sK20_skl,apply(sK19_skl,sK21_skl)))),
% 0.14/0.50 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/0.50 fof(f1204,plain,(
% 0.14/0.50 apply(relation_composition(sK19_skl,sK20_skl),sK21_skl)=apply(sK20_skl,apply(sK19_skl,sK21_skl))|~sQ70_spl),
% 0.14/0.50 inference(component_clause,[status(thm)],[f1203])).
% 0.14/0.50 fof(f1206,plain,(
% 0.14/0.50 ~sQ28_spl|sQ70_spl|~sQ43_spl),
% 0.14/0.50 inference(split_clause,[status(thm)],[f1177,f529,f1203,f715])).
% 0.14/0.50 fof(f1211,plain,(
% 0.14/0.50 $false|~sQ70_spl),
% 0.14/0.50 inference(forward_subsumption_resolution,[status(thm)],[f1204,f183])).
% 0.14/0.50 fof(f1212,plain,(
% 0.14/0.50 ~sQ70_spl),
% 0.14/0.50 inference(contradiction_clause,[status(thm)],[f1211])).
% 0.14/0.50 fof(f1213,plain,(
% 0.14/0.50 $false),
% 0.14/0.50 inference(sat_refutation,[status(thm)],[f284,f369,f376,f473,f545,f584,f718,f1206,f1212])).
% 0.14/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.92/0.53 % Elapsed time: 0.140327 seconds
% 0.92/0.53 % CPU time: 0.719773 seconds
% 0.92/0.53 % Total memory used: 90.699 MB
% 0.92/0.53 % Net memory used: 90.187 MB
%------------------------------------------------------------------------------