%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU215+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:01 PM UTC 2026
% Result : Theorem 3.00s 0.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU215+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n004.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 05:58:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 3.00/0.80 % Refutation found
% 3.00/0.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.00/0.80 % SZS output start CNFRefutation for theBenchmark
% 3.00/0.80 fof(f5,axiom,(
% 3.00/0.80 (! [A] :( ( relation(A)& function(A) )=> (! [B,C] :( ( in(B,relation_dom(A))=> ( C = apply(A,B)<=> in(ordered_pair(B,C),A) ) )& ( ~ in(B,relation_dom(A))=> ( C = apply(A,B)<=> C = empty_set ) ) ) )) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f7,axiom,(
% 3.00/0.80 (! [A,B] :( ( relation(A)& relation(B) )=> relation(relation_composition(A,B)) ) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f10,axiom,(
% 3.00/0.80 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f11,axiom,(
% 3.00/0.80 (! [A,B] :( ( relation(A)& function(A)& relation(B)& function(B) )=> ( relation(relation_composition(A,B))& function(relation_composition(A,B)) ) ) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f19,axiom,(
% 3.00/0.80 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f24,axiom,(
% 3.00/0.80 (? [A] : empty(A) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f31,axiom,(
% 3.00/0.80 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( in(A,relation_dom(relation_composition(C,B)))<=> ( in(A,relation_dom(C))& in(apply(C,A),relation_dom(B)) ) ) ) )) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f32,axiom,(
% 3.00/0.80 (! [A,B] :( ( relation(B)& function(B) )=> (! [C] :( ( relation(C)& function(C) )=> ( in(A,relation_dom(relation_composition(C,B)))=> apply(relation_composition(C,B),A) = apply(B,apply(C,A)) ) ) )) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f33,conjecture,(
% 3.00/0.80 (! [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)) ) ) )) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f34,negated_conjecture,(
% 3.00/0.80 ~((! [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)) ) ) )) ))),
% 3.00/0.80 inference(negated_conjecture,[status(cth)],[f33])).
% 3.00/0.80 fof(f39,axiom,(
% 3.00/0.80 (! [A] :( empty(A)=> A = empty_set ) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f40,axiom,(
% 3.00/0.80 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 3.00/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.00/0.80 fof(f49,plain,(
% 3.00/0.80 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|(C=apply(A,B)<=>in(ordered_pair(B,C),A)))&(in(B,relation_dom(A))|(C=apply(A,B)<=>C=empty_set)))))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 3.00/0.80 fof(f50,plain,(
% 3.00/0.80 ![A]: ((~relation(A)|~function(A))|(![B,C]: ((~in(B,relation_dom(A))|((~C=apply(A,B)|in(ordered_pair(B,C),A))&(C=apply(A,B)|~in(ordered_pair(B,C),A))))&(in(B,relation_dom(A))|((~C=apply(A,B)|C=empty_set)&(C=apply(A,B)|~C=empty_set))))))),
% 3.00/0.80 inference(NNF_transformation,[status(thm)],[f49])).
% 3.00/0.80 fof(f51,plain,(
% 3.00/0.80 ![A]: ((~relation(A)|~function(A))|((![B]: (~in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|in(ordered_pair(B,C),A)))&(![C]: (C=apply(A,B)|~in(ordered_pair(B,C),A))))))&(![B]: (in(B,relation_dom(A))|((![C]: (~C=apply(A,B)|C=empty_set))&(![C]: (C=apply(A,B)|~C=empty_set)))))))),
% 3.00/0.80 inference(miniscoping,[status(thm)],[f50])).
% 3.00/0.80 fof(f54,plain,(
% 3.00/0.80 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|~X2=apply(X0,X1)|X2=empty_set)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f51])).
% 3.00/0.80 fof(f57,plain,(
% 3.00/0.80 ![A,B]: ((~relation(A)|~relation(B))|relation(relation_composition(A,B)))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 3.00/0.80 fof(f58,plain,(
% 3.00/0.80 ![X0,X1]: (~relation(X0)|~relation(X1)|relation(relation_composition(X0,X1)))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f57])).
% 3.00/0.80 fof(f64,plain,(
% 3.00/0.80 empty(empty_set)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f10])).
% 3.00/0.80 fof(f67,plain,(
% 3.00/0.80 ![A,B]: ((((~relation(A)|~function(A))|~relation(B))|~function(B))|(relation(relation_composition(A,B))&function(relation_composition(A,B))))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 3.00/0.80 fof(f69,plain,(
% 3.00/0.80 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|function(relation_composition(X0,X1)))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f67])).
% 3.00/0.80 fof(f79,plain,(
% 3.00/0.80 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 3.00/0.80 fof(f80,plain,(
% 3.00/0.80 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f79])).
% 3.00/0.80 fof(f95,plain,(
% 3.00/0.80 empty(sK4_skl)),
% 3.00/0.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f24])).
% 3.00/0.80 fof(f96,plain,(
% 3.00/0.80 empty(sK4_skl)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f95])).
% 3.00/0.80 fof(f112,plain,(
% 3.00/0.80 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(in(A,relation_dom(relation_composition(C,B)))<=>(in(A,relation_dom(C))&in(apply(C,A),relation_dom(B)))))))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 3.00/0.80 fof(f113,plain,(
% 3.00/0.80 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((~in(A,relation_dom(relation_composition(C,B)))|(in(A,relation_dom(C))&in(apply(C,A),relation_dom(B))))&(in(A,relation_dom(relation_composition(C,B)))|(~in(A,relation_dom(C))|~in(apply(C,A),relation_dom(B))))))))),
% 3.00/0.80 inference(NNF_transformation,[status(thm)],[f112])).
% 3.00/0.80 fof(f114,plain,(
% 3.00/0.80 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|((![A]: (~in(A,relation_dom(relation_composition(C,B)))|(in(A,relation_dom(C))&in(apply(C,A),relation_dom(B)))))&(![A]: (in(A,relation_dom(relation_composition(C,B)))|(~in(A,relation_dom(C))|~in(apply(C,A),relation_dom(B)))))))))),
% 3.00/0.80 inference(miniscoping,[status(thm)],[f113])).
% 3.00/0.80 fof(f117,plain,(
% 3.00/0.80 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|in(X2,relation_dom(relation_composition(X1,X0)))|~in(X2,relation_dom(X1))|~in(apply(X1,X2),relation_dom(X0)))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f114])).
% 3.00/0.80 fof(f118,plain,(
% 3.00/0.80 ![A,B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(~in(A,relation_dom(relation_composition(C,B)))|apply(relation_composition(C,B),A)=apply(B,apply(C,A))))))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 3.00/0.80 fof(f119,plain,(
% 3.00/0.80 ![B]: ((~relation(B)|~function(B))|(![C]: ((~relation(C)|~function(C))|(![A]: (~in(A,relation_dom(relation_composition(C,B)))|apply(relation_composition(C,B),A)=apply(B,apply(C,A)))))))),
% 3.00/0.80 inference(miniscoping,[status(thm)],[f118])).
% 3.00/0.80 fof(f120,plain,(
% 3.00/0.80 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~in(X2,relation_dom(relation_composition(X1,X0)))|apply(relation_composition(X1,X0),X2)=apply(X0,apply(X1,X2)))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f119])).
% 3.00/0.80 fof(f121,plain,(
% 3.00/0.80 (?[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)))))))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 3.00/0.80 fof(f122,plain,(
% 3.00/0.80 ?[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)))))))),
% 3.00/0.80 inference(miniscoping,[status(thm)],[f121])).
% 3.00/0.80 fof(f123,plain,(
% 3.00/0.80 ((relation(sK9_skl)&function(sK9_skl))&((relation(sK10_skl)&function(sK10_skl))&(in(sK11_skl,relation_dom(sK9_skl))&~apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=apply(sK10_skl,apply(sK9_skl,sK11_skl)))))),
% 3.00/0.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(B,sK9_skl),skolemize(C,sK10_skl),skolemize(A,sK11_skl)],[f122])).
% 3.00/0.80 fof(f124,plain,(
% 3.00/0.80 relation(sK9_skl)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f123])).
% 3.00/0.80 fof(f125,plain,(
% 3.00/0.80 function(sK9_skl)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f123])).
% 3.00/0.80 fof(f126,plain,(
% 3.00/0.80 relation(sK10_skl)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f123])).
% 3.00/0.80 fof(f127,plain,(
% 3.00/0.80 function(sK10_skl)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f123])).
% 3.00/0.80 fof(f128,plain,(
% 3.00/0.80 in(sK11_skl,relation_dom(sK9_skl))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f123])).
% 3.00/0.80 fof(f129,plain,(
% 3.00/0.80 ~apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=apply(sK10_skl,apply(sK9_skl,sK11_skl))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f123])).
% 3.00/0.80 fof(f142,plain,(
% 3.00/0.80 ![A]: (~empty(A)|A=empty_set)),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 3.00/0.80 fof(f143,plain,(
% 3.00/0.80 ![X0]: (~empty(X0)|X0=empty_set)),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f142])).
% 3.00/0.80 fof(f144,plain,(
% 3.00/0.80 ![A,B]: (~in(A,B)|~empty(B))),
% 3.00/0.80 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 3.00/0.80 fof(f145,plain,(
% 3.00/0.80 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 3.00/0.80 inference(miniscoping,[status(thm)],[f144])).
% 3.00/0.80 fof(f146,plain,(
% 3.00/0.80 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 3.00/0.80 inference(cnf_transformation,[status(thm)],[f145])).
% 3.00/0.80 fof(f151,plain,(
% 3.00/0.80 ![X0,X1]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|apply(X0,X1)=empty_set)),
% 3.00/0.80 inference(destructive_equality_resolution,[status(thm)],[f54])).
% 3.00/0.80 fof(f156,plain,(
% 3.00/0.80 ![X0]: (~in(X0,empty_set))),
% 3.00/0.80 inference(resolution,[status(thm)],[f64,f146])).
% 3.00/0.80 fof(f199,plain,(
% 3.00/0.80 empty(relation_dom(sK4_skl))),
% 3.00/0.80 inference(resolution,[status(thm)],[f96,f80])).
% 3.00/0.80 fof(f276,plain,(
% 3.00/0.80 sK4_skl=empty_set),
% 3.00/0.80 inference(resolution,[status(thm)],[f143,f96])).
% 3.00/0.80 fof(f277,plain,(
% 3.00/0.80 relation_dom(sK4_skl)=empty_set),
% 3.00/0.80 inference(resolution,[status(thm)],[f143,f199])).
% 3.00/0.80 fof(f300,plain,(
% 3.00/0.80 relation_dom(empty_set)=empty_set),
% 3.00/0.80 inference(forward_demodulation,[status(thm)],[f276,f277])).
% 3.00/0.80 fof(f337,plain,(
% 3.00/0.80 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|in(X2,relation_dom(relation_composition(X1,X0)))|~in(X2,relation_dom(X1))|~relation(X0)|~function(X0)|apply(X0,apply(X1,X2))=empty_set)),
% 3.00/0.80 inference(resolution,[status(thm)],[f117,f151])).
% 3.00/0.80 fof(f340,plain,(
% 3.00/0.80 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|in(X2,relation_dom(relation_composition(X1,X0)))|~in(X2,relation_dom(X1))|apply(X0,apply(X1,X2))=empty_set)),
% 3.00/0.80 inference(duplicate_literals_removal,[status(thm)],[f337])).
% 3.00/0.80 fof(f408,definition,(
% 3.00/0.80 sQ25_spl <=> (relation(sK9_skl))),
% 3.00/0.80 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 3.00/0.80 fof(f410,plain,(
% 3.00/0.80 ~relation(sK9_skl)|sQ25_spl),
% 3.00/0.80 inference(component_clause,[status(thm)],[f408])).
% 3.00/0.80 fof(f412,plain,(
% 3.00/0.80 $false|sQ25_spl),
% 3.00/0.80 inference(forward_subsumption_resolution,[status(thm)],[f410,f124])).
% 3.00/0.80 fof(f413,plain,(
% 3.00/0.80 sQ25_spl),
% 3.00/0.80 inference(contradiction_clause,[status(thm)],[f412])).
% 3.00/0.80 fof(f498,definition,(
% 3.00/0.80 sQ27_spl <=> (function(sK9_skl))),
% 3.00/0.80 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 3.00/0.80 fof(f500,plain,(
% 3.00/0.80 ~function(sK9_skl)|sQ27_spl),
% 3.00/0.80 inference(component_clause,[status(thm)],[f498])).
% 3.00/0.80 fof(f518,plain,(
% 3.00/0.80 $false|sQ27_spl),
% 3.00/0.80 inference(forward_subsumption_resolution,[status(thm)],[f500,f125])).
% 3.00/0.80 fof(f519,plain,(
% 3.00/0.80 sQ27_spl),
% 3.00/0.80 inference(contradiction_clause,[status(thm)],[f518])).
% 3.00/0.80 fof(f711,definition,(
% 3.00/0.80 sQ53_spl <=> (relation(sK10_skl))),
% 3.00/0.80 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 3.00/0.80 fof(f713,plain,(
% 3.00/0.80 ~relation(sK10_skl)|sQ53_spl),
% 3.00/0.80 inference(component_clause,[status(thm)],[f711])).
% 3.00/0.80 fof(f715,definition,(
% 3.00/0.80 sQ54_spl <=> (function(sK10_skl))),
% 3.00/0.80 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 3.00/0.80 fof(f717,plain,(
% 3.00/0.80 ~function(sK10_skl)|sQ54_spl),
% 3.00/0.80 inference(component_clause,[status(thm)],[f715])).
% 3.00/0.80 fof(f738,plain,(
% 3.00/0.80 $false|sQ53_spl),
% 3.00/0.80 inference(forward_subsumption_resolution,[status(thm)],[f713,f126])).
% 3.00/0.80 fof(f739,plain,(
% 3.00/0.80 sQ53_spl),
% 3.00/0.80 inference(contradiction_clause,[status(thm)],[f738])).
% 3.00/0.80 fof(f740,plain,(
% 3.00/0.80 $false|sQ54_spl),
% 3.00/0.80 inference(forward_subsumption_resolution,[status(thm)],[f717,f127])).
% 3.00/0.80 fof(f741,plain,(
% 3.00/0.80 sQ54_spl),
% 3.00/0.80 inference(contradiction_clause,[status(thm)],[f740])).
% 3.00/0.80 fof(f1477,plain,(
% 3.00/0.80 ![X0]: (~relation(X0)|~function(X0)|~relation(sK9_skl)|~function(sK9_skl)|in(sK11_skl,relation_dom(relation_composition(sK9_skl,X0)))|apply(X0,apply(sK9_skl,sK11_skl))=empty_set)),
% 3.00/0.80 inference(resolution,[status(thm)],[f340,f128])).
% 3.00/0.80 fof(f1482,definition,(
% 3.00/0.80 ![X0]: (sQ111_spl <=> (~relation(X0)|~function(X0)|in(sK11_skl,relation_dom(relation_composition(sK9_skl,X0)))|apply(X0,apply(sK9_skl,sK11_skl))=empty_set))),
% 3.00/0.81 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 3.00/0.81 fof(f1483,plain,(
% 3.00/0.81 ![X0]: (~relation(X0)|~function(X0)|in(sK11_skl,relation_dom(relation_composition(sK9_skl,X0)))|apply(X0,apply(sK9_skl,sK11_skl))=empty_set|~sQ111_spl)),
% 3.00/0.81 inference(component_clause,[status(thm)],[f1482])).
% 3.00/0.81 fof(f1485,plain,(
% 3.00/0.81 sQ111_spl|~sQ25_spl|~sQ27_spl),
% 3.00/0.81 inference(split_clause,[status(thm)],[f1477,f1482,f408,f498])).
% 3.00/0.81 fof(f2558,plain,(
% 3.00/0.81 ~relation(sK10_skl)|in(sK11_skl,relation_dom(relation_composition(sK9_skl,sK10_skl)))|apply(sK10_skl,apply(sK9_skl,sK11_skl))=empty_set|~sQ111_spl),
% 3.00/0.81 inference(resolution,[status(thm)],[f1483,f127])).
% 3.00/0.81 fof(f2581,definition,(
% 3.00/0.81 sQ211_spl <=> (in(sK11_skl,relation_dom(relation_composition(sK9_skl,sK10_skl))))),
% 3.00/0.81 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 3.00/0.81 fof(f2582,plain,(
% 3.00/0.81 in(sK11_skl,relation_dom(relation_composition(sK9_skl,sK10_skl)))|~sQ211_spl),
% 3.00/0.81 inference(component_clause,[status(thm)],[f2581])).
% 3.00/0.81 fof(f2583,plain,(
% 3.00/0.81 ~in(sK11_skl,relation_dom(relation_composition(sK9_skl,sK10_skl)))|sQ211_spl),
% 3.00/0.81 inference(component_clause,[status(thm)],[f2581])).
% 3.00/0.81 fof(f2584,definition,(
% 3.00/0.81 sQ212_spl <=> (apply(sK10_skl,apply(sK9_skl,sK11_skl))=empty_set)),
% 3.00/0.81 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 3.00/0.81 fof(f2585,plain,(
% 3.00/0.81 apply(sK10_skl,apply(sK9_skl,sK11_skl))=empty_set|~sQ212_spl),
% 3.00/0.81 inference(component_clause,[status(thm)],[f2584])).
% 3.00/0.81 fof(f2587,plain,(
% 3.00/0.81 ~sQ53_spl|sQ211_spl|sQ212_spl|~sQ111_spl),
% 3.00/0.81 inference(split_clause,[status(thm)],[f2558,f711,f2581,f2584,f1482])).
% 3.00/0.81 fof(f3189,plain,(
% 3.00/0.81 ~relation(sK10_skl)|~function(sK10_skl)|~relation(sK9_skl)|~function(sK9_skl)|apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=apply(sK10_skl,apply(sK9_skl,sK11_skl))|~sQ211_spl),
% 3.00/0.81 inference(resolution,[status(thm)],[f2582,f120])).
% 3.00/0.81 fof(f3196,definition,(
% 3.00/0.81 sQ288_spl <=> (apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=apply(sK10_skl,apply(sK9_skl,sK11_skl)))),
% 3.00/0.81 introduced(definition,[new_symbols(definition,[sQ288_spl])],[split_symbol_definition])).
% 3.00/0.81 fof(f3197,plain,(
% 3.00/0.81 apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=apply(sK10_skl,apply(sK9_skl,sK11_skl))|~sQ288_spl),
% 3.00/0.81 inference(component_clause,[status(thm)],[f3196])).
% 3.00/0.81 fof(f3199,plain,(
% 3.00/0.81 ~sQ53_spl|~sQ54_spl|~sQ25_spl|~sQ27_spl|sQ288_spl|~sQ211_spl),
% 3.00/0.81 inference(split_clause,[status(thm)],[f3189,f711,f715,f408,f498,f3196,f2581])).
% 3.00/0.81 fof(f3208,definition,(
% 3.00/0.81 sQ291_spl <=> (relation(relation_composition(sK9_skl,sK10_skl)))),
% 3.00/0.81 introduced(definition,[new_symbols(definition,[sQ291_spl])],[split_symbol_definition])).
% 3.00/0.81 fof(f3210,plain,(
% 3.00/0.81 ~relation(relation_composition(sK9_skl,sK10_skl))|sQ291_spl),
% 3.00/0.81 inference(component_clause,[status(thm)],[f3208])).
% 3.00/0.81 fof(f3211,definition,(
% 3.00/0.81 sQ292_spl <=> (function(relation_composition(sK9_skl,sK10_skl)))),
% 3.00/0.81 introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition])).
% 3.00/0.81 fof(f3213,plain,(
% 3.00/0.81 ~function(relation_composition(sK9_skl,sK10_skl))|sQ292_spl),
% 3.00/0.81 inference(component_clause,[status(thm)],[f3211])).
% 3.00/0.81 fof(f3215,plain,(
% 3.00/0.81 $false|~sQ288_spl),
% 3.00/0.81 inference(forward_subsumption_resolution,[status(thm)],[f3197,f129])).
% 3.00/0.81 fof(f3216,plain,(
% 3.00/0.81 ~sQ288_spl),
% 3.00/0.81 inference(contradiction_clause,[status(thm)],[f3215])).
% 3.00/0.81 fof(f3217,plain,(
% 3.00/0.81 ~relation(sK9_skl)|~function(sK9_skl)|~relation(sK10_skl)|~function(sK10_skl)|sQ292_spl),
% 3.00/0.81 inference(resolution,[status(thm)],[f3213,f69])).
% 3.00/0.81 fof(f3218,plain,(
% 3.00/0.81 ~sQ25_spl|~sQ27_spl|~sQ53_spl|~sQ54_spl|sQ292_spl),
% 3.00/0.81 inference(split_clause,[status(thm)],[f3217,f408,f498,f711,f715,f3211])).
% 3.00/0.81 fof(f3221,plain,(
% 3.00/0.81 ~relation(sK9_skl)|~relation(sK10_skl)|sQ291_spl),
% 3.00/0.81 inference(resolution,[status(thm)],[f3210,f58])).
% 3.00/0.81 fof(f3225,plain,(
% 3.00/0.81 ~sQ25_spl|~sQ53_spl|sQ291_spl),
% 3.00/0.81 inference(split_clause,[status(thm)],[f3221,f408,f711,f3208])).
% 3.00/0.81 fof(f3405,plain,(
% 3.00/0.81 ~apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=empty_set|~sQ212_spl),
% 1.92/0.81 inference(backward_demodulation,[status(thm)],[f2585,f129])).
% 1.92/0.81 fof(f3945,definition,(
% 1.92/0.81 sQ387_spl <=> (in(empty_set,relation_dom(empty_set)))),
% 1.92/0.81 introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition])).
% 1.92/0.81 fof(f3946,plain,(
% 1.92/0.81 in(empty_set,relation_dom(empty_set))|~sQ387_spl),
% 1.92/0.81 inference(component_clause,[status(thm)],[f3945])).
% 1.92/0.81 fof(f3952,plain,(
% 1.92/0.81 in(empty_set,empty_set)|~sQ387_spl),
% 1.92/0.81 inference(forward_demodulation,[status(thm)],[f300,f3946])).
% 1.92/0.81 fof(f3953,plain,(
% 1.92/0.81 $false|~sQ387_spl),
% 1.92/0.81 inference(forward_subsumption_resolution,[status(thm)],[f3952,f156])).
% 1.92/0.81 fof(f3954,plain,(
% 1.92/0.81 ~sQ387_spl),
% 1.92/0.81 inference(contradiction_clause,[status(thm)],[f3953])).
% 1.92/0.81 fof(f4082,plain,(
% 1.92/0.81 ~relation(relation_composition(sK9_skl,sK10_skl))|~function(relation_composition(sK9_skl,sK10_skl))|apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=empty_set|sQ211_spl),
% 1.92/0.81 inference(resolution,[status(thm)],[f2583,f151])).
% 1.92/0.81 fof(f4083,definition,(
% 1.92/0.81 sQ399_spl <=> (apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=empty_set)),
% 1.92/0.81 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 1.92/0.81 fof(f4084,plain,(
% 1.92/0.81 apply(relation_composition(sK9_skl,sK10_skl),sK11_skl)=empty_set|~sQ399_spl),
% 1.92/0.81 inference(component_clause,[status(thm)],[f4083])).
% 1.92/0.81 fof(f4086,plain,(
% 1.92/0.81 ~sQ291_spl|~sQ292_spl|sQ399_spl|sQ211_spl),
% 1.92/0.81 inference(split_clause,[status(thm)],[f4082,f3208,f3211,f4083,f2581])).
% 1.92/0.81 fof(f4087,plain,(
% 1.92/0.81 $false|~sQ212_spl|~sQ399_spl),
% 1.92/0.81 inference(forward_subsumption_resolution,[status(thm)],[f4084,f3405])).
% 1.92/0.81 fof(f4088,plain,(
% 1.92/0.81 ~sQ212_spl|~sQ399_spl),
% 1.92/0.81 inference(contradiction_clause,[status(thm)],[f4087])).
% 1.92/0.81 fof(f4089,plain,(
% 1.92/0.81 $false),
% 1.92/0.81 inference(sat_refutation,[status(thm)],[f413,f519,f739,f741,f1485,f2587,f3199,f3216,f3218,f3225,f3954,f4086,f4088])).
% 1.92/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 1.92/0.83 % Elapsed time: 0.455031 seconds
% 1.92/0.83 % CPU time: 3.256178 seconds
% 1.92/0.83 % Total memory used: 164.871 MB
% 1.92/0.83 % Net memory used: 161.317 MB
%------------------------------------------------------------------------------