%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU220+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 : n014.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:02 PM UTC 2026
% Result : Theorem 1.49s 0.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU220+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.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:59:19 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 1.49/0.64 % Refutation found
% 1.49/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.49/0.64 % SZS output start CNFRefutation for theBenchmark
% 1.49/0.64 fof(f2,axiom,(
% 1.49/0.64 (! [A] :( empty(A)=> function(A) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f8,axiom,(
% 1.49/0.64 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f14,axiom,(
% 1.49/0.64 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f20,axiom,(
% 1.49/0.64 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f23,axiom,(
% 1.49/0.64 (? [A] :( relation(A)& function(A) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f24,axiom,(
% 1.49/0.64 (? [A] :( empty(A)& relation(A) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f25,axiom,(
% 1.49/0.64 (? [A] : empty(A) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f26,axiom,(
% 1.49/0.64 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f32,axiom,(
% 1.49/0.64 (! [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)) ) ) )) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f34,axiom,(
% 1.49/0.64 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> (! [B] :( ( relation(B)& function(B) )=> ( B = function_inverse(A)<=> ( relation_dom(B) = relation_rng(A)& (! [C,D] :( ( ( in(C,relation_rng(A))& D = apply(B,C) )=> ( in(D,relation_dom(A))& C = apply(A,D) ) )& ( ( in(D,relation_dom(A))& C = apply(A,D) )=> ( in(C,relation_rng(A))& D = apply(B,C) ) ) ) )) ) ) )) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f35,axiom,(
% 1.49/0.64 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_rng(A) = relation_dom(function_inverse(A))& relation_dom(A) = relation_rng(function_inverse(A)) ) ) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f36,conjecture,(
% 1.49/0.64 (! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_rng(B)) )=> ( A = apply(B,apply(function_inverse(B),A))& A = apply(relation_composition(function_inverse(B),B),A) ) ) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f37,negated_conjecture,(
% 1.49/0.64 ~((! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_rng(B)) )=> ( A = apply(B,apply(function_inverse(B),A))& A = apply(relation_composition(function_inverse(B),B),A) ) ) ) ))),
% 1.49/0.64 inference(negated_conjecture,[status(cth)],[f36])).
% 1.49/0.64 fof(f38,axiom,(
% 1.49/0.64 (! [A] :( empty(A)=> A = empty_set ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f39,axiom,(
% 1.49/0.64 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 1.49/0.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.49/0.64 fof(f43,plain,(
% 1.49/0.64 ![A]: (~empty(A)|function(A))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 1.49/0.64 fof(f44,plain,(
% 1.49/0.64 ![X0]: (~empty(X0)|function(X0))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f43])).
% 1.49/0.64 fof(f51,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 1.49/0.64 fof(f52,plain,(
% 1.49/0.64 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f51])).
% 1.49/0.64 fof(f53,plain,(
% 1.49/0.64 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f51])).
% 1.49/0.64 fof(f61,plain,(
% 1.49/0.64 empty(empty_set)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f14])).
% 1.49/0.64 fof(f62,plain,(
% 1.49/0.64 relation(empty_set)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f14])).
% 1.49/0.64 fof(f74,plain,(
% 1.49/0.64 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 1.49/0.64 fof(f75,plain,(
% 1.49/0.64 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f74])).
% 1.49/0.64 fof(f83,plain,(
% 1.49/0.64 (relation(sK1_skl)&function(sK1_skl))),
% 1.49/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f23])).
% 1.49/0.64 fof(f84,plain,(
% 1.49/0.64 relation(sK1_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f83])).
% 1.49/0.64 fof(f86,plain,(
% 1.49/0.64 (empty(sK2_skl)&relation(sK2_skl))),
% 1.49/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f24])).
% 1.49/0.64 fof(f87,plain,(
% 1.49/0.64 empty(sK2_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f86])).
% 1.49/0.64 fof(f89,plain,(
% 1.49/0.64 empty(sK3_skl)),
% 1.49/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f25])).
% 1.49/0.64 fof(f90,plain,(
% 1.49/0.64 empty(sK3_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f89])).
% 1.49/0.64 fof(f91,plain,(
% 1.49/0.64 ((relation(sK4_skl)&empty(sK4_skl))&function(sK4_skl))),
% 1.49/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f26])).
% 1.49/0.64 fof(f94,plain,(
% 1.49/0.64 function(sK4_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f91])).
% 1.49/0.64 fof(f109,plain,(
% 1.49/0.64 ![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))))))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 1.49/0.64 fof(f110,plain,(
% 1.49/0.64 ![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)))))))),
% 1.49/0.64 inference(miniscoping,[status(thm)],[f109])).
% 1.49/0.64 fof(f111,plain,(
% 1.49/0.64 ![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)))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f110])).
% 1.49/0.64 fof(f114,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|(B=function_inverse(A)<=>(relation_dom(B)=relation_rng(A)&(![C,D]: (((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D)))&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))))))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 1.49/0.64 fof(f115,definition,(
% 1.49/0.64 ![A,B,C,D]: (sP0_prd(D,C,B,A)<=>((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D))))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 1.49/0.64 fof(f116,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|(B=function_inverse(A)<=>(relation_dom(B)=relation_rng(A)&(![C,D]: (sP0_prd(D,C,B,A)&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))))))),
% 1.49/0.64 inference(formula_renaming,[status(thm)],[f114,f115])).
% 1.49/0.64 fof(f117,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|((~B=function_inverse(A)|(relation_dom(B)=relation_rng(A)&(![C,D]: (sP0_prd(D,C,B,A)&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))&(B=function_inverse(A)|(~relation_dom(B)=relation_rng(A)|(?[C,D]: (~sP0_prd(D,C,B,A)|((in(D,relation_dom(A))&C=apply(A,D))&(~in(C,relation_rng(A))|~D=apply(B,C))))))))))))),
% 1.49/0.64 inference(NNF_transformation,[status(thm)],[f116])).
% 1.49/0.64 fof(f118,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|((~B=function_inverse(A)|(relation_dom(B)=relation_rng(A)&((![C,D]: sP0_prd(D,C,B,A))&(![C,D]: ((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))&(B=function_inverse(A)|(~relation_dom(B)=relation_rng(A)|((?[C,D]: ~sP0_prd(D,C,B,A))|(?[C,D]: ((in(D,relation_dom(A))&C=apply(A,D))&(~in(C,relation_rng(A))|~D=apply(B,C))))))))))))),
% 1.49/0.64 inference(miniscoping,[status(thm)],[f117])).
% 1.49/0.64 fof(f119,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(![B]: ((~relation(B)|~function(B))|((~B=function_inverse(A)|(relation_dom(B)=relation_rng(A)&((![C,D]: sP0_prd(D,C,B,A))&(![C,D]: ((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))&(B=function_inverse(A)|(~relation_dom(B)=relation_rng(A)|(~sP0_prd(sK10_skl(B,A),sK9_skl(B,A),B,A)|((in(sK12_skl(B,A),relation_dom(A))&sK11_skl(B,A)=apply(A,sK12_skl(B,A)))&(~in(sK11_skl(B,A),relation_rng(A))|~sK12_skl(B,A)=apply(B,sK11_skl(B,A))))))))))))),
% 1.49/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(C,sK9_skl(B,A)),skolemize(D,sK10_skl(B,A)),skolemize(C,sK11_skl(B,A)),skolemize(D,sK12_skl(B,A))],[f118])).
% 1.49/0.64 fof(f121,plain,(
% 1.49/0.64 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(X1)|~function(X1)|~X1=function_inverse(X0)|sP0_prd(X2,X3,X1,X0))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f119])).
% 1.49/0.64 fof(f127,plain,(
% 1.49/0.64 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_rng(A)=relation_dom(function_inverse(A))&relation_dom(A)=relation_rng(function_inverse(A)))))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 1.49/0.64 fof(f128,plain,(
% 1.49/0.64 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(X0)=relation_dom(function_inverse(X0)))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f127])).
% 1.49/0.64 fof(f130,plain,(
% 1.49/0.64 (?[A,B]: ((relation(B)&function(B))&((one_to_one(B)&in(A,relation_rng(B)))&(~A=apply(B,apply(function_inverse(B),A))|~A=apply(relation_composition(function_inverse(B),B),A)))))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 1.49/0.64 fof(f131,plain,(
% 1.49/0.64 ?[B]: ((relation(B)&function(B))&(?[A]: ((one_to_one(B)&in(A,relation_rng(B)))&(~A=apply(B,apply(function_inverse(B),A))|~A=apply(relation_composition(function_inverse(B),B),A)))))),
% 1.49/0.64 inference(miniscoping,[status(thm)],[f130])).
% 1.49/0.64 fof(f132,plain,(
% 1.49/0.64 ((relation(sK13_skl)&function(sK13_skl))&((one_to_one(sK13_skl)&in(sK14_skl,relation_rng(sK13_skl)))&(~sK14_skl=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|~sK14_skl=apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl))))),
% 1.49/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(B,sK13_skl),skolemize(A,sK14_skl)],[f131])).
% 1.49/0.64 fof(f133,plain,(
% 1.49/0.64 relation(sK13_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f132])).
% 1.49/0.64 fof(f134,plain,(
% 1.49/0.64 function(sK13_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f132])).
% 1.49/0.64 fof(f135,plain,(
% 1.49/0.64 one_to_one(sK13_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f132])).
% 1.49/0.64 fof(f136,plain,(
% 1.49/0.64 in(sK14_skl,relation_rng(sK13_skl))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f132])).
% 1.49/0.64 fof(f137,plain,(
% 1.49/0.64 ~sK14_skl=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|~sK14_skl=apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f132])).
% 1.49/0.64 fof(f138,plain,(
% 1.49/0.64 ![A]: (~empty(A)|A=empty_set)),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 1.49/0.64 fof(f139,plain,(
% 1.49/0.64 ![X0]: (~empty(X0)|X0=empty_set)),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f138])).
% 1.49/0.64 fof(f140,plain,(
% 1.49/0.64 ![A,B]: (~in(A,B)|~empty(B))),
% 1.49/0.64 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 1.49/0.64 fof(f141,plain,(
% 1.49/0.64 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 1.49/0.64 inference(miniscoping,[status(thm)],[f140])).
% 1.49/0.64 fof(f142,plain,(
% 1.49/0.64 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f141])).
% 1.49/0.64 fof(f146,plain,(
% 1.49/0.64 ![A,B,C,D]: ((~sP0_prd(D,C,B,A)|((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D))))&(sP0_prd(D,C,B,A)|((in(C,relation_rng(A))&D=apply(B,C))&(~in(D,relation_dom(A))|~C=apply(A,D)))))),
% 1.49/0.64 inference(NNF_transformation,[status(thm)],[f115])).
% 1.49/0.64 fof(f147,plain,(
% 1.49/0.64 (![A,B,C,D]: (~sP0_prd(D,C,B,A)|((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D)))))&(![A,B,C,D]: (sP0_prd(D,C,B,A)|((in(C,relation_rng(A))&D=apply(B,C))&(~in(D,relation_dom(A))|~C=apply(A,D)))))),
% 1.49/0.64 inference(miniscoping,[status(thm)],[f146])).
% 1.49/0.64 fof(f149,plain,(
% 1.49/0.64 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|~in(X1,relation_rng(X3))|~X0=apply(X2,X1)|X1=apply(X3,X0))),
% 1.49/0.64 inference(cnf_transformation,[status(thm)],[f147])).
% 1.49/0.64 fof(f153,definition,(
% 1.49/0.64 sQ0_spl <=> (sK14_skl=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f155,plain,(
% 1.49/0.64 ~sK14_skl=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|sQ0_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f153])).
% 1.49/0.64 fof(f156,definition,(
% 1.49/0.64 sQ1_spl <=> (sK14_skl=apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f158,plain,(
% 1.49/0.64 ~sK14_skl=apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl)|sQ1_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f156])).
% 1.49/0.64 fof(f159,plain,(
% 1.49/0.64 ~sQ0_spl|~sQ1_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f137,f153,f156])).
% 1.49/0.64 fof(f163,plain,(
% 1.49/0.64 ![X0,X2,X3]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(function_inverse(X0))|~function(function_inverse(X0))|sP0_prd(X2,X3,function_inverse(X0),X0))),
% 1.49/0.64 inference(destructive_equality_resolution,[status(thm)],[f121])).
% 1.49/0.64 fof(f164,plain,(
% 1.49/0.64 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~function(function_inverse(X0))|sP0_prd(X1,X2,function_inverse(X0),X0))),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f163,f52])).
% 1.49/0.64 fof(f170,plain,(
% 1.49/0.64 ![X0,X1,X2]: (~sP0_prd(apply(X0,X1),X1,X0,X2)|~in(X1,relation_rng(X2))|X1=apply(X2,apply(X0,X1)))),
% 1.49/0.64 inference(destructive_equality_resolution,[status(thm)],[f149])).
% 1.49/0.64 fof(f181,plain,(
% 1.49/0.64 function(empty_set)),
% 1.49/0.64 inference(resolution,[status(thm)],[f61,f44])).
% 1.49/0.64 fof(f182,plain,(
% 1.49/0.64 empty(relation_dom(empty_set))),
% 1.49/0.64 inference(resolution,[status(thm)],[f75,f61])).
% 1.49/0.64 fof(f184,plain,(
% 1.49/0.64 ~empty(relation_rng(sK13_skl))),
% 1.49/0.64 inference(resolution,[status(thm)],[f142,f136])).
% 1.49/0.64 fof(f196,plain,(
% 1.49/0.64 ~relation(sK13_skl)|~function(sK13_skl)|relation_rng(sK13_skl)=relation_dom(function_inverse(sK13_skl))),
% 1.49/0.64 inference(resolution,[status(thm)],[f128,f135])).
% 1.49/0.64 fof(f198,definition,(
% 1.49/0.64 sQ2_spl <=> (relation(sK13_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f200,plain,(
% 1.49/0.64 ~relation(sK13_skl)|sQ2_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f198])).
% 1.49/0.64 fof(f201,definition,(
% 1.49/0.64 sQ3_spl <=> (function(sK13_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f203,plain,(
% 1.49/0.64 ~function(sK13_skl)|sQ3_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f201])).
% 1.49/0.64 fof(f204,definition,(
% 1.49/0.64 sQ4_spl <=> (relation_rng(sK13_skl)=relation_dom(function_inverse(sK13_skl)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f205,plain,(
% 1.49/0.64 relation_rng(sK13_skl)=relation_dom(function_inverse(sK13_skl))|~sQ4_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f204])).
% 1.49/0.64 fof(f207,plain,(
% 1.49/0.64 ~sQ2_spl|~sQ3_spl|sQ4_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f196,f198,f201,f204])).
% 1.49/0.64 fof(f229,plain,(
% 1.49/0.64 function(sK2_skl)),
% 1.49/0.64 inference(resolution,[status(thm)],[f87,f44])).
% 1.49/0.64 fof(f234,plain,(
% 1.49/0.64 function(sK3_skl)),
% 1.49/0.64 inference(resolution,[status(thm)],[f90,f44])).
% 1.49/0.64 fof(f244,plain,(
% 1.49/0.64 ![X0,X1]: (~relation(function_inverse(sK13_skl))|~function(function_inverse(sK13_skl))|~relation(X0)|~function(X0)|~in(X1,relation_rng(sK13_skl))|apply(relation_composition(function_inverse(sK13_skl),X0),X1)=apply(X0,apply(function_inverse(sK13_skl),X1))|~sQ4_spl)),
% 1.49/0.64 inference(paramodulation,[status(thm)],[f205,f111])).
% 1.49/0.64 fof(f245,definition,(
% 1.49/0.64 sQ8_spl <=> (relation(function_inverse(sK13_skl)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f247,plain,(
% 1.49/0.64 ~relation(function_inverse(sK13_skl))|sQ8_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f245])).
% 1.49/0.64 fof(f248,definition,(
% 1.49/0.64 sQ9_spl <=> (function(function_inverse(sK13_skl)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f250,plain,(
% 1.49/0.64 ~function(function_inverse(sK13_skl))|sQ9_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f248])).
% 1.49/0.64 fof(f272,definition,(
% 1.49/0.64 sQ16_spl <=> (empty(relation_rng(sK13_skl)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f273,plain,(
% 1.49/0.64 empty(relation_rng(sK13_skl))|~sQ16_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f272])).
% 1.49/0.64 fof(f276,definition,(
% 1.49/0.64 ![X0,X1]: (sQ17_spl <=> (~relation(X0)|~function(X0)|~in(X1,relation_rng(sK13_skl))|apply(relation_composition(function_inverse(sK13_skl),X0),X1)=apply(X0,apply(function_inverse(sK13_skl),X1))))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f277,plain,(
% 1.49/0.64 ![X0,X1]: (~relation(X0)|~function(X0)|~in(X1,relation_rng(sK13_skl))|apply(relation_composition(function_inverse(sK13_skl),X0),X1)=apply(X0,apply(function_inverse(sK13_skl),X1))|~sQ17_spl)),
% 1.49/0.64 inference(component_clause,[status(thm)],[f276])).
% 1.49/0.64 fof(f279,plain,(
% 1.49/0.64 ~sQ8_spl|~sQ9_spl|sQ17_spl|~sQ4_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f244,f245,f248,f276,f204])).
% 1.49/0.64 fof(f280,plain,(
% 1.49/0.64 $false|sQ3_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f203,f134])).
% 1.49/0.64 fof(f281,plain,(
% 1.49/0.64 sQ3_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f280])).
% 1.49/0.64 fof(f292,plain,(
% 1.49/0.64 ~relation(sK13_skl)|~function(sK13_skl)|sQ8_spl),
% 1.49/0.64 inference(resolution,[status(thm)],[f247,f52])).
% 1.49/0.64 fof(f293,plain,(
% 1.49/0.64 ~sQ2_spl|~sQ3_spl|sQ8_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f292,f198,f201,f245])).
% 1.49/0.64 fof(f307,plain,(
% 1.49/0.64 $false|sQ2_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f200,f133])).
% 1.49/0.64 fof(f308,plain,(
% 1.49/0.64 sQ2_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f307])).
% 1.49/0.64 fof(f366,plain,(
% 1.49/0.64 ~relation(sK13_skl)|~function(sK13_skl)|sQ9_spl),
% 1.49/0.64 inference(resolution,[status(thm)],[f250,f53])).
% 1.49/0.64 fof(f367,plain,(
% 1.49/0.64 ~sQ2_spl|~sQ3_spl|sQ9_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f366,f198,f201,f248])).
% 1.49/0.64 fof(f379,definition,(
% 1.49/0.64 sQ27_spl <=> (function(sK4_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f381,plain,(
% 1.49/0.64 ~function(sK4_skl)|sQ27_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f379])).
% 1.49/0.64 fof(f386,definition,(
% 1.49/0.64 sQ29_spl <=> (function(sK3_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f388,plain,(
% 1.49/0.64 ~function(sK3_skl)|sQ29_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f386])).
% 1.49/0.64 fof(f393,definition,(
% 1.49/0.64 sQ31_spl <=> (function(sK2_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f395,plain,(
% 1.49/0.64 ~function(sK2_skl)|sQ31_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f393])).
% 1.49/0.64 fof(f404,definition,(
% 1.49/0.64 sQ33_spl <=> (function(empty_set))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f406,plain,(
% 1.49/0.64 ~function(empty_set)|sQ33_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f404])).
% 1.49/0.64 fof(f412,plain,(
% 1.49/0.64 $false|sQ33_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f406,f181])).
% 1.49/0.64 fof(f413,plain,(
% 1.49/0.64 sQ33_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f412])).
% 1.49/0.64 fof(f414,plain,(
% 1.49/0.64 $false|sQ31_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f395,f229])).
% 1.49/0.64 fof(f415,plain,(
% 1.49/0.64 sQ31_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f414])).
% 1.49/0.64 fof(f416,plain,(
% 1.49/0.64 $false|sQ29_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f388,f234])).
% 1.49/0.64 fof(f417,plain,(
% 1.49/0.64 sQ29_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f416])).
% 1.49/0.64 fof(f418,plain,(
% 1.49/0.64 $false|sQ27_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f381,f94])).
% 1.49/0.64 fof(f419,plain,(
% 1.49/0.64 sQ27_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f418])).
% 1.49/0.64 fof(f552,plain,(
% 1.49/0.64 ![X0,X1]: (~in(X0,relation_rng(X1))|X0=apply(X1,apply(function_inverse(X1),X0))|~relation(X1)|~function(X1)|~one_to_one(X1)|~function(function_inverse(X1)))),
% 1.49/0.64 inference(resolution,[status(thm)],[f170,f164])).
% 1.49/0.64 fof(f553,plain,(
% 1.49/0.64 ![X0,X1]: (~in(X0,relation_rng(X1))|X0=apply(X1,apply(function_inverse(X1),X0))|~relation(X1)|~function(X1)|~one_to_one(X1))),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f552,f53])).
% 1.49/0.64 fof(f565,plain,(
% 1.49/0.64 ![X0]: (~relation(X0)|~function(X0)|apply(relation_composition(function_inverse(sK13_skl),X0),sK14_skl)=apply(X0,apply(function_inverse(sK13_skl),sK14_skl))|~sQ17_spl)),
% 1.49/0.64 inference(resolution,[status(thm)],[f277,f136])).
% 1.49/0.64 fof(f678,plain,(
% 1.49/0.64 relation_dom(empty_set)=empty_set),
% 1.49/0.64 inference(resolution,[status(thm)],[f182,f139])).
% 1.49/0.64 fof(f689,definition,(
% 1.49/0.64 sQ55_spl <=> (relation(empty_set))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f691,plain,(
% 1.49/0.64 ~relation(empty_set)|sQ55_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f689])).
% 1.49/0.64 fof(f696,definition,(
% 1.49/0.64 sQ56_spl <=> (function(relation_dom(empty_set)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f698,plain,(
% 1.49/0.64 ~function(relation_dom(empty_set))|sQ56_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f696])).
% 1.49/0.64 fof(f719,plain,(
% 1.49/0.64 ~function(empty_set)|sQ56_spl),
% 1.49/0.64 inference(forward_demodulation,[status(thm)],[f678,f698])).
% 1.49/0.64 fof(f720,plain,(
% 1.49/0.64 $false|sQ56_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f719,f181])).
% 1.49/0.64 fof(f721,plain,(
% 1.49/0.64 sQ56_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f720])).
% 1.49/0.64 fof(f749,plain,(
% 1.49/0.64 ~relation(sK13_skl)|apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl)=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|~sQ17_spl),
% 1.49/0.64 inference(resolution,[status(thm)],[f565,f134])).
% 1.49/0.64 fof(f760,definition,(
% 1.49/0.64 sQ63_spl <=> (relation(sK1_skl))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f762,plain,(
% 1.49/0.64 ~relation(sK1_skl)|sQ63_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f760])).
% 1.49/0.64 fof(f772,definition,(
% 1.49/0.64 sQ66_spl <=> (apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl)=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl)))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f773,plain,(
% 1.49/0.64 apply(relation_composition(function_inverse(sK13_skl),sK13_skl),sK14_skl)=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|~sQ66_spl),
% 1.49/0.64 inference(component_clause,[status(thm)],[f772])).
% 1.49/0.64 fof(f775,plain,(
% 1.49/0.64 ~sQ2_spl|sQ66_spl|~sQ17_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f749,f198,f772,f276])).
% 1.49/0.64 fof(f776,plain,(
% 1.49/0.64 $false|sQ55_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f691,f62])).
% 1.49/0.64 fof(f777,plain,(
% 1.49/0.64 sQ55_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f776])).
% 1.49/0.64 fof(f778,plain,(
% 1.49/0.64 $false|sQ63_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f762,f84])).
% 1.49/0.64 fof(f779,plain,(
% 1.49/0.64 sQ63_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f778])).
% 1.49/0.64 fof(f862,plain,(
% 1.49/0.64 ![X0]: (~in(X0,relation_rng(sK13_skl))|X0=apply(sK13_skl,apply(function_inverse(sK13_skl),X0))|~relation(sK13_skl)|~function(sK13_skl))),
% 1.49/0.64 inference(resolution,[status(thm)],[f553,f135])).
% 1.49/0.64 fof(f868,definition,(
% 1.49/0.64 ![X0]: (sQ74_spl <=> (~in(X0,relation_rng(sK13_skl))|X0=apply(sK13_skl,apply(function_inverse(sK13_skl),X0))))),
% 1.49/0.64 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 1.49/0.64 fof(f869,plain,(
% 1.49/0.64 ![X0]: (~in(X0,relation_rng(sK13_skl))|X0=apply(sK13_skl,apply(function_inverse(sK13_skl),X0))|~sQ74_spl)),
% 1.49/0.64 inference(component_clause,[status(thm)],[f868])).
% 1.49/0.64 fof(f871,plain,(
% 1.49/0.64 sQ74_spl|~sQ2_spl|~sQ3_spl),
% 1.49/0.64 inference(split_clause,[status(thm)],[f862,f868,f198,f201])).
% 1.49/0.64 fof(f1080,plain,(
% 1.49/0.64 sK14_skl=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|~sQ74_spl),
% 1.49/0.64 inference(resolution,[status(thm)],[f869,f136])).
% 1.49/0.64 fof(f1085,plain,(
% 1.49/0.64 $false|sQ0_spl|~sQ74_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1080,f155])).
% 1.49/0.64 fof(f1086,plain,(
% 1.49/0.64 sQ0_spl|~sQ74_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f1085])).
% 1.49/0.64 fof(f1087,plain,(
% 1.49/0.64 ~sK14_skl=apply(sK13_skl,apply(function_inverse(sK13_skl),sK14_skl))|~sQ66_spl|sQ1_spl),
% 1.49/0.64 inference(forward_demodulation,[status(thm)],[f773,f158])).
% 1.49/0.64 fof(f1089,plain,(
% 1.49/0.64 $false|~sQ16_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f273,f184])).
% 1.49/0.64 fof(f1090,plain,(
% 1.49/0.64 ~sQ16_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f1089])).
% 1.49/0.64 fof(f1091,plain,(
% 1.49/0.64 $false|~sQ66_spl|sQ1_spl|~sQ74_spl),
% 1.49/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1080,f1087])).
% 1.49/0.64 fof(f1092,plain,(
% 1.49/0.64 ~sQ66_spl|sQ1_spl|~sQ74_spl),
% 1.49/0.64 inference(contradiction_clause,[status(thm)],[f1091])).
% 1.49/0.64 fof(f1093,plain,(
% 1.49/0.64 $false),
% 1.49/0.64 inference(sat_refutation,[status(thm)],[f159,f207,f279,f281,f293,f308,f367,f413,f415,f417,f419,f721,f775,f777,f779,f871,f1086,f1090,f1092])).
% 1.49/0.64 % SZS output end CNFRefutation for theBenchmark.p
% 1.49/0.66 % Elapsed time: 0.287518 seconds
% 1.49/0.66 % CPU time: 2.064889 seconds
% 1.49/0.66 % Total memory used: 122.982 MB
% 1.49/0.66 % Net memory used: 120.155 MB
%------------------------------------------------------------------------------