%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU215+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 : n026.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 13.38s 12.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU215+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/10.39 % Computer : n026.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Mon Sep 21 06:01:47 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.14/10.40 % Drodi V4.1.1
% 13.38/12.21 % Refutation found
% 13.38/12.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.38/12.21 % SZS output start CNFRefutation for theBenchmark
% 13.38/12.21 fof(f5,axiom,(
% 13.38/12.21 (! [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 ) ) ) )) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f13,axiom,(
% 13.38/12.21 (! [A,B] :( ( relation(A)& relation(B) )=> relation(relation_composition(A,B)) ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f16,axiom,(
% 13.38/12.21 (! [A,B] :( ( empty(A)& relation(B) )=> ( empty(relation_composition(B,A))& relation(relation_composition(B,A)) ) ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f17,axiom,(
% 13.38/12.21 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f18,axiom,(
% 13.38/12.21 (! [A,B] :( ( relation(A)& function(A)& relation(B)& function(B) )=> ( relation(relation_composition(A,B))& function(relation_composition(A,B)) ) ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f25,axiom,(
% 13.38/12.21 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f28,axiom,(
% 13.38/12.21 (? [A] :( empty(A)& relation(A) ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f29,axiom,(
% 13.38/12.21 (? [A] : empty(A) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f34,axiom,(
% 13.38/12.21 (! [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)) ) ) ) )) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f35,axiom,(
% 13.38/12.21 (! [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)) ) ) )) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f36,conjecture,(
% 13.38/12.21 (! [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)) ) ) )) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f37,negated_conjecture,(
% 13.38/12.21 ~((! [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)) ) ) )) ))),
% 13.38/12.21 inference(negated_conjecture,[status(cth)],[f36])).
% 13.38/12.21 fof(f39,axiom,(
% 13.38/12.21 (! [A] :( empty(A)=> A = empty_set ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f40,axiom,(
% 13.38/12.21 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 13.38/12.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.38/12.21 fof(f49,plain,(
% 13.38/12.21 ![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)))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 13.38/12.21 fof(f50,plain,(
% 13.38/12.21 ![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))))))),
% 13.38/12.21 inference(NNF_transformation,[status(thm)],[f49])).
% 13.38/12.21 fof(f51,plain,(
% 13.38/12.21 ![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)))))))),
% 13.38/12.21 inference(miniscoping,[status(thm)],[f50])).
% 13.38/12.21 fof(f54,plain,(
% 13.38/12.21 ![X0,X1,X2]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|~X2=apply(X0,X1)|X2=empty_set)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f51])).
% 13.38/12.21 fof(f57,plain,(
% 13.38/12.21 ![A,B]: ((~relation(A)|~relation(B))|relation(relation_composition(A,B)))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 13.38/12.21 fof(f58,plain,(
% 13.38/12.21 ![X0,X1]: (~relation(X0)|~relation(X1)|relation(relation_composition(X0,X1)))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f57])).
% 13.38/12.21 fof(f61,plain,(
% 13.38/12.21 ![A,B]: ((~empty(A)|~relation(B))|(empty(relation_composition(B,A))&relation(relation_composition(B,A))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 13.38/12.21 fof(f62,plain,(
% 13.38/12.21 ![X0,X1]: (~empty(X0)|~relation(X1)|empty(relation_composition(X1,X0)))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f61])).
% 13.38/12.21 fof(f64,plain,(
% 13.38/12.21 empty(empty_set)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f17])).
% 13.38/12.21 fof(f67,plain,(
% 13.38/12.21 ![A,B]: ((((~relation(A)|~function(A))|~relation(B))|~function(B))|(relation(relation_composition(A,B))&function(relation_composition(A,B))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 13.38/12.21 fof(f69,plain,(
% 13.38/12.21 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|function(relation_composition(X0,X1)))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f67])).
% 13.38/12.21 fof(f78,plain,(
% 13.38/12.21 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 13.38/12.21 fof(f79,plain,(
% 13.38/12.21 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f78])).
% 13.38/12.21 fof(f87,plain,(
% 13.38/12.21 (empty(sK2_skl)&relation(sK2_skl))),
% 13.38/12.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f28])).
% 13.38/12.21 fof(f88,plain,(
% 13.38/12.21 empty(sK2_skl)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f87])).
% 13.38/12.21 fof(f90,plain,(
% 13.38/12.21 empty(sK3_skl)),
% 13.38/12.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f29])).
% 13.38/12.21 fof(f91,plain,(
% 13.38/12.21 empty(sK3_skl)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f90])).
% 13.38/12.21 fof(f102,plain,(
% 13.38/12.21 ![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)))))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 13.38/12.21 fof(f103,plain,(
% 13.38/12.21 ![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))))))))),
% 13.38/12.21 inference(NNF_transformation,[status(thm)],[f102])).
% 13.38/12.21 fof(f104,plain,(
% 13.38/12.21 ![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)))))))))),
% 13.38/12.21 inference(miniscoping,[status(thm)],[f103])).
% 13.38/12.21 fof(f107,plain,(
% 13.38/12.21 ![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)))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f104])).
% 13.38/12.21 fof(f108,plain,(
% 13.38/12.21 ![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))))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 13.38/12.21 fof(f109,plain,(
% 13.38/12.21 ![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)))))))),
% 13.38/12.21 inference(miniscoping,[status(thm)],[f108])).
% 13.38/12.21 fof(f110,plain,(
% 13.38/12.21 ![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)))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f109])).
% 13.38/12.21 fof(f111,plain,(
% 13.38/12.21 (?[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)))))))),
% 13.38/12.21 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 13.38/12.21 fof(f112,plain,(
% 13.38/12.21 ?[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)))))))),
% 13.38/12.21 inference(miniscoping,[status(thm)],[f111])).
% 13.38/12.21 fof(f113,plain,(
% 13.38/12.21 ((relation(sK7_skl)&function(sK7_skl))&((relation(sK8_skl)&function(sK8_skl))&(in(sK9_skl,relation_dom(sK7_skl))&~apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=apply(sK8_skl,apply(sK7_skl,sK9_skl)))))),
% 13.38/12.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(B,sK7_skl),skolemize(C,sK8_skl),skolemize(A,sK9_skl)],[f112])).
% 13.38/12.21 fof(f114,plain,(
% 13.38/12.21 relation(sK7_skl)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f113])).
% 13.38/12.21 fof(f115,plain,(
% 13.38/12.21 function(sK7_skl)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f113])).
% 13.38/12.21 fof(f116,plain,(
% 13.38/12.21 relation(sK8_skl)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f113])).
% 13.38/12.21 fof(f117,plain,(
% 13.38/12.21 function(sK8_skl)),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f113])).
% 13.38/12.21 fof(f118,plain,(
% 13.38/12.21 in(sK9_skl,relation_dom(sK7_skl))),
% 13.38/12.21 inference(cnf_transformation,[status(thm)],[f113])).
% 13.38/12.21 fof(f119,plain,(
% 13.38/12.21 ~apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=apply(sK8_skl,apply(sK7_skl,sK9_skl))),
% 13.38/12.22 inference(cnf_transformation,[status(thm)],[f113])).
% 13.38/12.22 fof(f122,plain,(
% 13.38/12.22 ![A]: (~empty(A)|A=empty_set)),
% 13.38/12.22 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 13.38/12.22 fof(f123,plain,(
% 13.38/12.22 ![X0]: (~empty(X0)|X0=empty_set)),
% 13.38/12.22 inference(cnf_transformation,[status(thm)],[f122])).
% 13.38/12.22 fof(f124,plain,(
% 13.38/12.22 ![A,B]: (~in(A,B)|~empty(B))),
% 13.38/12.22 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 13.38/12.22 fof(f125,plain,(
% 13.38/12.22 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 13.38/12.22 inference(miniscoping,[status(thm)],[f124])).
% 13.38/12.22 fof(f126,plain,(
% 13.38/12.22 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 13.38/12.22 inference(cnf_transformation,[status(thm)],[f125])).
% 13.38/12.22 fof(f131,plain,(
% 13.38/12.22 ![X0,X1]: (~relation(X0)|~function(X0)|in(X1,relation_dom(X0))|apply(X0,X1)=empty_set)),
% 13.38/12.22 inference(destructive_equality_resolution,[status(thm)],[f54])).
% 13.38/12.22 fof(f135,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|empty(relation_composition(X0,sK2_skl)))),
% 13.38/12.22 inference(resolution,[status(thm)],[f88,f62])).
% 13.38/12.22 fof(f140,plain,(
% 13.38/12.22 empty(relation_dom(sK3_skl))),
% 13.38/12.22 inference(resolution,[status(thm)],[f91,f79])).
% 13.38/12.22 fof(f193,definition,(
% 13.38/12.22 sQ8_spl <=> (relation(sK7_skl))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f195,plain,(
% 13.38/12.22 ~relation(sK7_skl)|sQ8_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f193])).
% 13.38/12.22 fof(f196,definition,(
% 13.38/12.22 sQ9_spl <=> (function(sK7_skl))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f198,plain,(
% 13.38/12.22 ~function(sK7_skl)|sQ9_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f196])).
% 13.38/12.22 fof(f214,plain,(
% 13.38/12.22 $false|sQ9_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f198,f115])).
% 13.38/12.22 fof(f215,plain,(
% 13.38/12.22 sQ9_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f214])).
% 13.38/12.22 fof(f216,plain,(
% 13.38/12.22 $false|sQ8_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f195,f114])).
% 13.38/12.22 fof(f217,plain,(
% 13.38/12.22 sQ8_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f216])).
% 13.38/12.22 fof(f274,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|~function(X0)|~relation(sK7_skl)|~function(sK7_skl)|in(sK9_skl,relation_dom(relation_composition(sK7_skl,X0)))|~in(apply(sK7_skl,sK9_skl),relation_dom(X0)))),
% 13.38/12.22 inference(resolution,[status(thm)],[f107,f118])).
% 13.38/12.22 fof(f276,definition,(
% 13.38/12.22 ![X0]: (sQ19_spl <=> (~relation(X0)|~function(X0)|in(sK9_skl,relation_dom(relation_composition(sK7_skl,X0)))|~in(apply(sK7_skl,sK9_skl),relation_dom(X0))))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f277,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|~function(X0)|in(sK9_skl,relation_dom(relation_composition(sK7_skl,X0)))|~in(apply(sK7_skl,sK9_skl),relation_dom(X0))|~sQ19_spl)),
% 13.38/12.22 inference(component_clause,[status(thm)],[f276])).
% 13.38/12.22 fof(f279,plain,(
% 13.38/12.22 sQ19_spl|~sQ8_spl|~sQ9_spl),
% 13.38/12.22 inference(split_clause,[status(thm)],[f274,f276,f193,f196])).
% 13.38/12.22 fof(f286,plain,(
% 13.38/12.22 ![X0]: (~in(X0,empty_set))),
% 13.38/12.22 inference(resolution,[status(thm)],[f64,f126])).
% 13.38/12.22 fof(f310,definition,(
% 13.38/12.22 sQ24_spl <=> (relation(sK8_skl))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f312,plain,(
% 13.38/12.22 ~relation(sK8_skl)|sQ24_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f310])).
% 13.38/12.22 fof(f324,plain,(
% 13.38/12.22 $false|sQ24_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f312,f116])).
% 13.38/12.22 fof(f325,plain,(
% 13.38/12.22 sQ24_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f324])).
% 13.38/12.22 fof(f333,plain,(
% 13.38/12.22 relation_dom(sK3_skl)=empty_set),
% 13.38/12.22 inference(resolution,[status(thm)],[f123,f140])).
% 13.38/12.22 fof(f335,plain,(
% 13.38/12.22 sK3_skl=empty_set),
% 13.38/12.22 inference(resolution,[status(thm)],[f123,f91])).
% 13.38/12.22 fof(f336,plain,(
% 13.38/12.22 sK2_skl=empty_set),
% 13.38/12.22 inference(resolution,[status(thm)],[f123,f88])).
% 13.38/12.22 fof(f366,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|~function(X0)|in(sK9_skl,relation_dom(relation_composition(sK7_skl,X0)))|~relation(X0)|~function(X0)|apply(X0,apply(sK7_skl,sK9_skl))=empty_set|~sQ19_spl)),
% 13.38/12.22 inference(resolution,[status(thm)],[f277,f131])).
% 13.38/12.22 fof(f367,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|~function(X0)|in(sK9_skl,relation_dom(relation_composition(sK7_skl,X0)))|apply(X0,apply(sK7_skl,sK9_skl))=empty_set|~sQ19_spl)),
% 13.38/12.22 inference(duplicate_literals_removal,[status(thm)],[f366])).
% 13.38/12.22 fof(f379,definition,(
% 13.38/12.22 sQ29_spl <=> (function(sK8_skl))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f381,plain,(
% 13.38/12.22 ~function(sK8_skl)|sQ29_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f379])).
% 13.38/12.22 fof(f385,plain,(
% 13.38/12.22 ~relation(sK8_skl)|in(sK9_skl,relation_dom(relation_composition(sK7_skl,sK8_skl)))|apply(sK8_skl,apply(sK7_skl,sK9_skl))=empty_set|~sQ19_spl),
% 13.38/12.22 inference(resolution,[status(thm)],[f367,f117])).
% 13.38/12.22 fof(f396,definition,(
% 13.38/12.22 sQ32_spl <=> (in(sK9_skl,relation_dom(relation_composition(sK7_skl,sK8_skl))))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f397,plain,(
% 13.38/12.22 in(sK9_skl,relation_dom(relation_composition(sK7_skl,sK8_skl)))|~sQ32_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f396])).
% 13.38/12.22 fof(f398,plain,(
% 13.38/12.22 ~in(sK9_skl,relation_dom(relation_composition(sK7_skl,sK8_skl)))|sQ32_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f396])).
% 13.38/12.22 fof(f399,definition,(
% 13.38/12.22 sQ33_spl <=> (apply(sK8_skl,apply(sK7_skl,sK9_skl))=empty_set)),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f400,plain,(
% 13.38/12.22 apply(sK8_skl,apply(sK7_skl,sK9_skl))=empty_set|~sQ33_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f399])).
% 13.38/12.22 fof(f402,plain,(
% 13.38/12.22 ~sQ24_spl|sQ32_spl|sQ33_spl|~sQ19_spl),
% 13.38/12.22 inference(split_clause,[status(thm)],[f385,f310,f396,f399,f276])).
% 13.38/12.22 fof(f440,definition,(
% 13.38/12.22 sQ41_spl <=> (in(sK9_skl,relation_dom(relation_composition(sK7_skl,empty_set))))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f441,plain,(
% 13.38/12.22 in(sK9_skl,relation_dom(relation_composition(sK7_skl,empty_set)))|~sQ41_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f440])).
% 13.38/12.22 fof(f465,definition,(
% 13.38/12.22 sQ46_spl <=> (in(sK9_skl,relation_dom(relation_composition(sK7_skl,relation_dom(empty_set)))))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f466,plain,(
% 13.38/12.22 in(sK9_skl,relation_dom(relation_composition(sK7_skl,relation_dom(empty_set))))|~sQ46_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f465])).
% 13.38/12.22 fof(f489,plain,(
% 13.38/12.22 relation_dom(empty_set)=empty_set),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f335,f333])).
% 13.38/12.22 fof(f539,plain,(
% 13.38/12.22 in(sK9_skl,relation_dom(relation_composition(sK7_skl,empty_set)))|~sQ46_spl),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f489,f466])).
% 13.38/12.22 fof(f549,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|empty(relation_composition(X0,empty_set)))),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f336,f135])).
% 13.38/12.22 fof(f551,plain,(
% 13.38/12.22 ![X0]: (~relation(X0)|relation_composition(X0,empty_set)=empty_set)),
% 13.38/12.22 inference(resolution,[status(thm)],[f549,f123])).
% 13.38/12.22 fof(f576,plain,(
% 13.38/12.22 relation_composition(sK7_skl,empty_set)=empty_set),
% 13.38/12.22 inference(resolution,[status(thm)],[f551,f114])).
% 13.38/12.22 fof(f808,plain,(
% 13.38/12.22 $false|sQ29_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f381,f117])).
% 13.38/12.22 fof(f809,plain,(
% 13.38/12.22 sQ29_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f808])).
% 13.38/12.22 fof(f1941,plain,(
% 13.38/12.22 ~relation(sK8_skl)|~function(sK8_skl)|~relation(sK7_skl)|~function(sK7_skl)|apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=apply(sK8_skl,apply(sK7_skl,sK9_skl))|~sQ32_spl),
% 13.38/12.22 inference(resolution,[status(thm)],[f397,f110])).
% 13.38/12.22 fof(f1947,definition,(
% 13.38/12.22 sQ195_spl <=> (apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=apply(sK8_skl,apply(sK7_skl,sK9_skl)))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f1948,plain,(
% 13.38/12.22 apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=apply(sK8_skl,apply(sK7_skl,sK9_skl))|~sQ195_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f1947])).
% 13.38/12.22 fof(f1950,plain,(
% 13.38/12.22 ~sQ24_spl|~sQ29_spl|~sQ8_spl|~sQ9_spl|sQ195_spl|~sQ32_spl),
% 13.38/12.22 inference(split_clause,[status(thm)],[f1941,f310,f379,f193,f196,f1947,f396])).
% 13.38/12.22 fof(f1959,definition,(
% 13.38/12.22 sQ198_spl <=> (relation(relation_composition(sK7_skl,sK8_skl)))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f1961,plain,(
% 13.38/12.22 ~relation(relation_composition(sK7_skl,sK8_skl))|sQ198_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f1959])).
% 13.38/12.22 fof(f1962,definition,(
% 13.38/12.22 sQ199_spl <=> (function(relation_composition(sK7_skl,sK8_skl)))),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f1964,plain,(
% 13.38/12.22 ~function(relation_composition(sK7_skl,sK8_skl))|sQ199_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f1962])).
% 13.38/12.22 fof(f1970,plain,(
% 13.38/12.22 $false|~sQ195_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f1948,f119])).
% 13.38/12.22 fof(f1971,plain,(
% 13.38/12.22 ~sQ195_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f1970])).
% 13.38/12.22 fof(f1972,plain,(
% 13.38/12.22 ~relation(relation_composition(sK7_skl,sK8_skl))|~function(relation_composition(sK7_skl,sK8_skl))|apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=empty_set|sQ32_spl),
% 13.38/12.22 inference(resolution,[status(thm)],[f398,f131])).
% 13.38/12.22 fof(f1973,definition,(
% 13.38/12.22 sQ201_spl <=> (apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=empty_set)),
% 13.38/12.22 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 13.38/12.22 fof(f1974,plain,(
% 13.38/12.22 apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=empty_set|~sQ201_spl),
% 13.38/12.22 inference(component_clause,[status(thm)],[f1973])).
% 13.38/12.22 fof(f1976,plain,(
% 13.38/12.22 ~sQ198_spl|~sQ199_spl|sQ201_spl|sQ32_spl),
% 13.38/12.22 inference(split_clause,[status(thm)],[f1972,f1959,f1962,f1973,f396])).
% 13.38/12.22 fof(f1977,plain,(
% 13.38/12.22 ~relation(sK7_skl)|~function(sK7_skl)|~relation(sK8_skl)|~function(sK8_skl)|sQ199_spl),
% 13.38/12.22 inference(resolution,[status(thm)],[f1964,f69])).
% 13.38/12.22 fof(f1979,plain,(
% 13.38/12.22 ~sQ8_spl|~sQ9_spl|~sQ24_spl|~sQ29_spl|sQ199_spl),
% 13.38/12.22 inference(split_clause,[status(thm)],[f1977,f193,f196,f310,f379,f1962])).
% 13.38/12.22 fof(f1982,plain,(
% 13.38/12.22 ~relation(sK7_skl)|~relation(sK8_skl)|sQ198_spl),
% 13.38/12.22 inference(resolution,[status(thm)],[f1961,f58])).
% 13.38/12.22 fof(f1986,plain,(
% 13.38/12.22 ~sQ8_spl|~sQ24_spl|sQ198_spl),
% 13.38/12.22 inference(split_clause,[status(thm)],[f1982,f193,f310,f1959])).
% 13.38/12.22 fof(f3720,plain,(
% 13.38/12.22 in(sK9_skl,relation_dom(empty_set))|~sQ41_spl),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f576,f441])).
% 13.38/12.22 fof(f3721,plain,(
% 13.38/12.22 in(sK9_skl,empty_set)|~sQ41_spl),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f489,f3720])).
% 13.38/12.22 fof(f3722,plain,(
% 13.38/12.22 $false|~sQ41_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f3721,f286])).
% 13.38/12.22 fof(f3723,plain,(
% 13.38/12.22 ~sQ41_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f3722])).
% 13.38/12.22 fof(f3726,plain,(
% 13.38/12.22 in(sK9_skl,relation_dom(empty_set))|~sQ46_spl),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f576,f539])).
% 13.38/12.22 fof(f3727,plain,(
% 13.38/12.22 in(sK9_skl,empty_set)|~sQ46_spl),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f489,f3726])).
% 13.38/12.22 fof(f3728,plain,(
% 13.38/12.22 $false|~sQ46_spl),
% 13.38/12.22 inference(forward_subsumption_resolution,[status(thm)],[f3727,f286])).
% 13.38/12.22 fof(f3729,plain,(
% 13.38/12.22 ~sQ46_spl),
% 13.38/12.22 inference(contradiction_clause,[status(thm)],[f3728])).
% 13.38/12.22 fof(f3965,plain,(
% 13.38/12.22 ~apply(relation_composition(sK7_skl,sK8_skl),sK9_skl)=empty_set|~sQ33_spl),
% 13.38/12.22 inference(backward_demodulation,[status(thm)],[f400,f119])).
% 13.38/12.22 fof(f4067,plain,(
% 13.38/12.22 ~empty_set=empty_set|~sQ201_spl|~sQ33_spl),
% 13.38/12.22 inference(forward_demodulation,[status(thm)],[f1974,f3965])).
% 13.38/12.22 fof(f4068,plain,(
% 13.38/12.22 $false|~sQ201_spl|~sQ33_spl),
% 12.76/12.26 inference(trivial_equality_resolution,[status(thm)],[f4067])).
% 12.76/12.26 fof(f4069,plain,(
% 12.76/12.26 ~sQ201_spl|~sQ33_spl),
% 12.76/12.26 inference(contradiction_clause,[status(thm)],[f4068])).
% 12.76/12.26 fof(f4070,plain,(
% 12.76/12.26 $false),
% 12.76/12.26 inference(sat_refutation,[status(thm)],[f215,f217,f279,f325,f402,f809,f1950,f1971,f1976,f1979,f1986,f3723,f3729,f4069])).
% 12.76/12.26 % SZS output end CNFRefutation for theBenchmark.p
% 12.76/12.28 % Elapsed time: 1.871726 seconds
% 12.76/12.28 % CPU time: 14.544400 seconds
% 12.76/12.28 % Total memory used: 265.994 MB
% 12.76/12.28 % Net memory used: 258.898 MB
%------------------------------------------------------------------------------