%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU219+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : 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:02 PM UTC 2026
% Result : Theorem 1.33s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU219+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 05:59:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.41 % Drodi V4.1.1
% 1.33/0.77 % Refutation found
% 1.33/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.33/0.77 % SZS output start CNFRefutation for theBenchmark
% 1.33/0.77 fof(f42,axiom,(
% 1.33/0.77 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> function_inverse(A) = relation_inverse(A) ) ) )),
% 1.33/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.33/0.77 fof(f50,axiom,(
% 1.33/0.77 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 1.33/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.33/0.77 fof(f174,lemma,(
% 1.33/0.77 (! [A] :( relation(A)=> ( relation_rng(A) = relation_dom(relation_inverse(A))& relation_dom(A) = relation_rng(relation_inverse(A)) ) ) )),
% 1.33/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.33/0.77 fof(f200,lemma,(
% 1.33/0.77 (! [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.33/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.33/0.77 fof(f202,conjecture,(
% 1.33/0.77 (! [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.33/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.33/0.77 fof(f203,negated_conjecture,(
% 1.33/0.77 ~((! [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.33/0.77 inference(negated_conjecture,[status(cth)],[f202])).
% 1.33/0.77 fof(f487,plain,(
% 1.33/0.77 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|function_inverse(A)=relation_inverse(A)))),
% 1.33/0.77 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 1.33/0.77 fof(f488,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|function_inverse(X0)=relation_inverse(X0))),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f487])).
% 1.33/0.77 fof(f489,plain,(
% 1.33/0.77 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 1.33/0.77 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 1.33/0.77 fof(f490,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f489])).
% 1.33/0.77 fof(f491,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f489])).
% 1.33/0.77 fof(f800,plain,(
% 1.33/0.77 ![A]: (~relation(A)|(relation_rng(A)=relation_dom(relation_inverse(A))&relation_dom(A)=relation_rng(relation_inverse(A))))),
% 1.33/0.77 inference(pre_NNF_transformation,[status(thm)],[f174])).
% 1.33/0.77 fof(f802,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|relation_dom(X0)=relation_rng(relation_inverse(X0)))),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f800])).
% 1.33/0.77 fof(f870,plain,(
% 1.33/0.77 ![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.33/0.77 inference(pre_NNF_transformation,[status(thm)],[f200])).
% 1.33/0.77 fof(f871,definition,(
% 1.33/0.77 ![A,B,C,D]: (sP1_prd(D,C,B,A)<=>((~in(C,relation_rng(A))|~D=apply(B,C))|(in(D,relation_dom(A))&C=apply(A,D))))),
% 1.33/0.77 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 1.33/0.77 fof(f872,plain,(
% 1.33/0.77 ![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]: (sP1_prd(D,C,B,A)&((~in(D,relation_dom(A))|~C=apply(A,D))|(in(C,relation_rng(A))&D=apply(B,C)))))))))))),
% 1.33/0.77 inference(formula_renaming,[status(thm)],[f870,f871])).
% 1.33/0.77 fof(f873,plain,(
% 1.33/0.77 ![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]: (sP1_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]: (~sP1_prd(D,C,B,A)|((in(D,relation_dom(A))&C=apply(A,D))&(~in(C,relation_rng(A))|~D=apply(B,C))))))))))))),
% 1.33/0.77 inference(NNF_transformation,[status(thm)],[f872])).
% 1.33/0.77 fof(f874,plain,(
% 1.33/0.77 ![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]: sP1_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]: ~sP1_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.33/0.77 inference(miniscoping,[status(thm)],[f873])).
% 1.33/0.77 fof(f875,plain,(
% 1.33/0.77 ![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]: sP1_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)|(~sP1_prd(sK71_skl(B,A),sK70_skl(B,A),B,A)|((in(sK73_skl(B,A),relation_dom(A))&sK72_skl(B,A)=apply(A,sK73_skl(B,A)))&(~in(sK72_skl(B,A),relation_rng(A))|~sK73_skl(B,A)=apply(B,sK72_skl(B,A))))))))))))),
% 1.33/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK70_skl,sK71_skl,sK72_skl,sK73_skl]),skolemize(C,sK70_skl(B,A)),skolemize(D,sK71_skl(B,A)),skolemize(C,sK72_skl(B,A)),skolemize(D,sK73_skl(B,A))],[f874])).
% 1.33/0.77 fof(f876,plain,(
% 1.33/0.77 ![X0,X1]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(X1)|~function(X1)|~X1=function_inverse(X0)|relation_dom(X1)=relation_rng(X0))),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f875])).
% 1.33/0.77 fof(f886,plain,(
% 1.33/0.77 (?[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.33/0.77 inference(pre_NNF_transformation,[status(thm)],[f203])).
% 1.33/0.77 fof(f887,plain,(
% 1.33/0.77 ((relation(sK74_skl)&function(sK74_skl))&(one_to_one(sK74_skl)&(~relation_rng(sK74_skl)=relation_dom(function_inverse(sK74_skl))|~relation_dom(sK74_skl)=relation_rng(function_inverse(sK74_skl)))))),
% 1.33/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK74_skl]),skolemize(A,sK74_skl)],[f886])).
% 1.33/0.77 fof(f888,plain,(
% 1.33/0.77 relation(sK74_skl)),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f887])).
% 1.33/0.77 fof(f889,plain,(
% 1.33/0.77 function(sK74_skl)),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f887])).
% 1.33/0.77 fof(f890,plain,(
% 1.33/0.77 one_to_one(sK74_skl)),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f887])).
% 1.33/0.77 fof(f891,plain,(
% 1.33/0.77 ~relation_rng(sK74_skl)=relation_dom(function_inverse(sK74_skl))|~relation_dom(sK74_skl)=relation_rng(function_inverse(sK74_skl))),
% 1.33/0.77 inference(cnf_transformation,[status(thm)],[f887])).
% 1.33/0.77 fof(f1088,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~relation(function_inverse(X0))|~function(function_inverse(X0))|relation_dom(function_inverse(X0))=relation_rng(X0))),
% 1.33/0.77 inference(destructive_equality_resolution,[status(thm)],[f876])).
% 1.33/0.77 fof(f1089,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|~function(function_inverse(X0))|relation_dom(function_inverse(X0))=relation_rng(X0))),
% 1.33/0.77 inference(forward_subsumption_resolution,[status(thm)],[f1088,f490])).
% 1.33/0.77 fof(f1102,plain,(
% 1.33/0.77 ~function(sK74_skl)|~one_to_one(sK74_skl)|function_inverse(sK74_skl)=relation_inverse(sK74_skl)),
% 1.33/0.77 inference(resolution,[status(thm)],[f488,f888])).
% 1.33/0.77 fof(f1103,plain,(
% 1.33/0.77 ~one_to_one(sK74_skl)|function_inverse(sK74_skl)=relation_inverse(sK74_skl)),
% 1.33/0.77 inference(forward_subsumption_resolution,[status(thm)],[f1102,f889])).
% 1.33/0.77 fof(f1104,plain,(
% 1.33/0.77 function_inverse(sK74_skl)=relation_inverse(sK74_skl)),
% 1.33/0.77 inference(resolution,[status(thm)],[f1103,f890])).
% 1.33/0.77 fof(f1126,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(function_inverse(X0))=relation_rng(X0)|~relation(X0)|~function(X0))),
% 1.33/0.77 inference(resolution,[status(thm)],[f1089,f491])).
% 1.33/0.77 fof(f1127,plain,(
% 1.33/0.77 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_dom(function_inverse(X0))=relation_rng(X0))),
% 1.33/0.77 inference(duplicate_literals_removal,[status(thm)],[f1126])).
% 1.33/0.78 fof(f1161,plain,(
% 1.33/0.78 ~relation(sK74_skl)|~function(sK74_skl)|relation_dom(function_inverse(sK74_skl))=relation_rng(sK74_skl)),
% 1.33/0.78 inference(resolution,[status(thm)],[f1127,f890])).
% 1.33/0.78 fof(f1163,plain,(
% 1.33/0.78 ~function(sK74_skl)|relation_dom(function_inverse(sK74_skl))=relation_rng(sK74_skl)),
% 1.33/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1161,f888])).
% 1.33/0.78 fof(f1164,plain,(
% 1.33/0.78 relation_dom(function_inverse(sK74_skl))=relation_rng(sK74_skl)),
% 1.33/0.78 inference(resolution,[status(thm)],[f1163,f889])).
% 1.33/0.78 fof(f1166,plain,(
% 1.33/0.78 ~relation_rng(sK74_skl)=relation_rng(sK74_skl)|~relation_dom(sK74_skl)=relation_rng(function_inverse(sK74_skl))),
% 1.33/0.78 inference(backward_demodulation,[status(thm)],[f1164,f891])).
% 1.33/0.78 fof(f1167,plain,(
% 1.33/0.78 ~relation_dom(sK74_skl)=relation_rng(function_inverse(sK74_skl))),
% 1.33/0.78 inference(trivial_equality_resolution,[status(thm)],[f1166])).
% 1.33/0.78 fof(f1304,plain,(
% 1.33/0.78 relation_dom(sK74_skl)=relation_rng(relation_inverse(sK74_skl))),
% 1.33/0.78 inference(resolution,[status(thm)],[f802,f888])).
% 1.33/0.78 fof(f1306,plain,(
% 1.33/0.78 relation_dom(sK74_skl)=relation_rng(function_inverse(sK74_skl))),
% 1.33/0.78 inference(forward_demodulation,[status(thm)],[f1104,f1304])).
% 1.33/0.78 fof(f1307,plain,(
% 1.33/0.78 $false),
% 1.33/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1306,f1167])).
% 1.33/0.78 % SZS output end CNFRefutation for theBenchmark.p
% 1.33/0.82 % Elapsed time: 0.436426 seconds
% 1.33/0.82 % CPU time: 2.763391 seconds
% 1.33/0.82 % Total memory used: 144.031 MB
% 1.33/0.82 % Net memory used: 140.339 MB
%------------------------------------------------------------------------------