%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU023+1 : 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 : 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:21:35 PM UTC 2026
% Result : Theorem 0.18s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU023+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n014.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 05:47:34 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 0.18/0.51 % Refutation found
% 0.18/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.51 fof(f5,axiom,(
% 0.18/0.51 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.18/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f31,axiom,(
% 0.18/0.51 (! [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.18/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f35,axiom,(
% 0.18/0.51 (! [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) ) ) ) )) ) ) )) ) )),
% 0.18/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f36,conjecture,(
% 0.18/0.51 (! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_dom(B)) )=> ( A = apply(function_inverse(B),apply(B,A))& A = apply(relation_composition(B,function_inverse(B)),A) ) ) ) )),
% 0.18/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.51 fof(f37,negated_conjecture,(
% 0.18/0.51 ~((! [A,B] :( ( relation(B)& function(B) )=> ( ( one_to_one(B)& in(A,relation_dom(B)) )=> ( A = apply(function_inverse(B),apply(B,A))& A = apply(relation_composition(B,function_inverse(B)),A) ) ) ) ))),
% 0.18/0.51 inference(negated_conjecture,[status(cth)],[f36])).
% 0.18/0.51 fof(f52,plain,(
% 0.18/0.51 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.18/0.51 fof(f53,plain,(
% 0.18/0.51 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f52])).
% 0.18/0.51 fof(f54,plain,(
% 0.18/0.51 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f52])).
% 0.18/0.51 fof(f120,plain,(
% 0.18/0.51 ![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.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.18/0.51 fof(f121,plain,(
% 0.18/0.51 ![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.18/0.51 inference(miniscoping,[status(thm)],[f120])).
% 0.18/0.51 fof(f122,plain,(
% 0.18/0.51 ![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.18/0.51 inference(cnf_transformation,[status(thm)],[f121])).
% 0.18/0.51 fof(f132,plain,(
% 0.18/0.51 ![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)))))))))))),
% 0.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.18/0.51 fof(f133,definition,(
% 0.18/0.51 ![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))))),
% 0.18/0.51 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.18/0.51 fof(f134,plain,(
% 0.18/0.51 ![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)))))))))))),
% 0.18/0.51 inference(formula_renaming,[status(thm)],[f132,f133])).
% 0.18/0.51 fof(f135,plain,(
% 0.18/0.51 ![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))))))))))))),
% 0.18/0.51 inference(NNF_transformation,[status(thm)],[f134])).
% 0.18/0.51 fof(f136,plain,(
% 0.18/0.51 ![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))))))))))))),
% 0.18/0.51 inference(miniscoping,[status(thm)],[f135])).
% 0.18/0.51 fof(f137,plain,(
% 0.18/0.51 ![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(sK12_skl(B,A),sK11_skl(B,A),B,A)|((in(sK14_skl(B,A),relation_dom(A))&sK13_skl(B,A)=apply(A,sK14_skl(B,A)))&(~in(sK13_skl(B,A),relation_rng(A))|~sK14_skl(B,A)=apply(B,sK13_skl(B,A))))))))))))),
% 0.18/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(C,sK11_skl(B,A)),skolemize(D,sK12_skl(B,A)),skolemize(C,sK13_skl(B,A)),skolemize(D,sK14_skl(B,A))],[f136])).
% 0.18/0.51 fof(f141,plain,(
% 0.18/0.51 ![X0,X1,X2,X3]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(X1)|~function(X1)|~X1=function_inverse(X0)|~in(X2,relation_dom(X0))|~X3=apply(X0,X2)|X2=apply(X1,X3))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f137])).
% 0.18/0.51 fof(f145,plain,(
% 0.18/0.51 (?[A,B]: ((relation(B)&function(B))&((one_to_one(B)&in(A,relation_dom(B)))&(~A=apply(function_inverse(B),apply(B,A))|~A=apply(relation_composition(B,function_inverse(B)),A)))))),
% 0.18/0.51 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.18/0.51 fof(f146,plain,(
% 0.18/0.51 ?[B]: ((relation(B)&function(B))&(?[A]: ((one_to_one(B)&in(A,relation_dom(B)))&(~A=apply(function_inverse(B),apply(B,A))|~A=apply(relation_composition(B,function_inverse(B)),A)))))),
% 0.18/0.51 inference(miniscoping,[status(thm)],[f145])).
% 0.18/0.51 fof(f147,plain,(
% 0.18/0.51 ((relation(sK15_skl)&function(sK15_skl))&((one_to_one(sK15_skl)&in(sK16_skl,relation_dom(sK15_skl)))&(~sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))|~sK16_skl=apply(relation_composition(sK15_skl,function_inverse(sK15_skl)),sK16_skl))))),
% 0.18/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(B,sK15_skl),skolemize(A,sK16_skl)],[f146])).
% 0.18/0.51 fof(f148,plain,(
% 0.18/0.51 relation(sK15_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f147])).
% 0.18/0.51 fof(f149,plain,(
% 0.18/0.51 function(sK15_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f147])).
% 0.18/0.51 fof(f150,plain,(
% 0.18/0.51 one_to_one(sK15_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f147])).
% 0.18/0.51 fof(f151,plain,(
% 0.18/0.51 in(sK16_skl,relation_dom(sK15_skl))),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f147])).
% 0.18/0.51 fof(f152,plain,(
% 0.18/0.51 ~sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))|~sK16_skl=apply(relation_composition(sK15_skl,function_inverse(sK15_skl)),sK16_skl)),
% 0.18/0.51 inference(cnf_transformation,[status(thm)],[f147])).
% 0.18/0.51 fof(f174,plain,(
% 0.18/0.51 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(function_inverse(X0))|~function(function_inverse(X0))|~in(X1,relation_dom(X0))|X1=apply(function_inverse(X0),apply(X0,X1)))),
% 0.18/0.51 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 0.18/0.51 fof(f180,plain,(
% 0.18/0.51 ~function(sK15_skl)|relation(function_inverse(sK15_skl))),
% 0.18/0.51 inference(resolution,[status(thm)],[f53,f148])).
% 0.18/0.51 fof(f181,plain,(
% 0.18/0.51 relation(function_inverse(sK15_skl))),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f180,f149])).
% 0.18/0.51 fof(f182,plain,(
% 0.18/0.51 ~function(sK15_skl)|function(function_inverse(sK15_skl))),
% 0.18/0.51 inference(resolution,[status(thm)],[f54,f148])).
% 0.18/0.51 fof(f183,plain,(
% 0.18/0.51 function(function_inverse(sK15_skl))),
% 0.18/0.51 inference(forward_subsumption_resolution,[status(thm)],[f182,f149])).
% 0.18/0.51 fof(f215,plain,(
% 0.18/0.51 ![X0]: (~relation(sK15_skl)|~function(sK15_skl)|~relation(X0)|~function(X0)|apply(relation_composition(sK15_skl,X0),sK16_skl)=apply(X0,apply(sK15_skl,sK16_skl)))),
% 0.18/0.52 inference(resolution,[status(thm)],[f122,f151])).
% 0.18/0.52 fof(f216,plain,(
% 0.18/0.52 ![X0]: (~function(sK15_skl)|~relation(X0)|~function(X0)|apply(relation_composition(sK15_skl,X0),sK16_skl)=apply(X0,apply(sK15_skl,sK16_skl)))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f215,f148])).
% 0.18/0.52 fof(f223,plain,(
% 0.18/0.52 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~function(function_inverse(X0))|~in(X1,relation_dom(X0))|X1=apply(function_inverse(X0),apply(X0,X1)))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f174,f53])).
% 0.18/0.52 fof(f224,plain,(
% 0.18/0.52 ~relation(sK15_skl)|~function(sK15_skl)|~one_to_one(sK15_skl)|~function(function_inverse(sK15_skl))|sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f223,f151])).
% 0.18/0.52 fof(f225,plain,(
% 0.18/0.52 ~function(sK15_skl)|~one_to_one(sK15_skl)|~function(function_inverse(sK15_skl))|sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f224,f148])).
% 0.18/0.52 fof(f290,plain,(
% 0.18/0.52 ![X0]: (~relation(X0)|~function(X0)|apply(relation_composition(sK15_skl,X0),sK16_skl)=apply(X0,apply(sK15_skl,sK16_skl)))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f216,f149])).
% 0.18/0.52 fof(f295,plain,(
% 0.18/0.52 ~function(function_inverse(sK15_skl))|apply(relation_composition(sK15_skl,function_inverse(sK15_skl)),sK16_skl)=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(resolution,[status(thm)],[f290,f181])).
% 0.18/0.52 fof(f299,plain,(
% 0.18/0.52 apply(relation_composition(sK15_skl,function_inverse(sK15_skl)),sK16_skl)=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f295,f183])).
% 0.18/0.52 fof(f375,plain,(
% 0.18/0.52 ~one_to_one(sK15_skl)|~function(function_inverse(sK15_skl))|sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f225,f149])).
% 0.18/0.52 fof(f1292,plain,(
% 0.18/0.52 ~sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))|~sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(backward_demodulation,[status(thm)],[f299,f152])).
% 0.18/0.52 fof(f1295,plain,(
% 0.18/0.52 ~sK16_skl=apply(function_inverse(sK15_skl),apply(sK15_skl,sK16_skl))),
% 0.18/0.52 inference(duplicate_literals_removal,[status(thm)],[f1292])).
% 0.18/0.52 fof(f1298,plain,(
% 0.18/0.52 ~one_to_one(sK15_skl)|~function(function_inverse(sK15_skl))),
% 0.18/0.52 inference(backward_subsumption_resolution,[status(thm)],[f375,f1295])).
% 0.18/0.52 fof(f1299,plain,(
% 0.18/0.52 ~function(function_inverse(sK15_skl))),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f1298,f150])).
% 0.18/0.52 fof(f1328,plain,(
% 0.18/0.52 $false),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f1299,f183])).
% 0.18/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/0.59 % Elapsed time: 0.134904 seconds
% 0.25/0.59 % CPU time: 0.212880 seconds
% 0.25/0.59 % Total memory used: 22.237 MB
% 0.25/0.59 % Net memory used: 22.097 MB
%------------------------------------------------------------------------------