%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU034+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 : n012.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:36 PM UTC 2026
% Result : Theorem 0.11s 5.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU034+1 : 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/5.56 % Computer : n012.cluster.edu
% 0.08/5.56 % Model : x86_64 x86_64
% 0.08/5.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.56 % Memory : 8046.5625MB
% 0.08/5.56 % OS : Linux 6.8.0-71-generic
% 0.08/5.56 % CPULimit : 300
% 0.08/5.56 % WCLimit : 300
% 0.08/5.56 % DateTime : Mon Sep 21 05:47:12 UTC 2026
% 0.08/5.56 % CPUTime :
% 0.08/5.57 % Drodi V4.1.1
% 0.11/5.63 % Refutation found
% 0.11/5.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/5.63 % SZS output start CNFRefutation for theBenchmark
% 0.11/5.63 fof(f5,axiom,(
% 0.11/5.63 (! [A] :( ( relation(A)& function(A) )=> ( relation(function_inverse(A))& function(function_inverse(A)) ) ) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f7,axiom,(
% 0.11/5.63 (! [A] : relation(identity_relation(A)) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f14,axiom,(
% 0.11/5.63 (! [A] :( relation(identity_relation(A))& function(identity_relation(A)) ) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f35,axiom,(
% 0.11/5.63 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( relation_rng(A) = relation_dom(B)& relation_composition(A,B) = A )=> B = identity_relation(relation_dom(B)) ) ) )) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f37,axiom,(
% 0.11/5.63 (! [A] : one_to_one(identity_relation(A)) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f38,axiom,(
% 0.11/5.63 (! [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)) ) ) ) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f40,axiom,(
% 0.11/5.63 (! [A] :( ( relation(A)& function(A) )=> ( one_to_one(A)=> ( relation_composition(A,function_inverse(A)) = identity_relation(relation_dom(A))& relation_composition(function_inverse(A),A) = identity_relation(relation_rng(A)) ) ) ) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f41,conjecture,(
% 0.11/5.63 (! [A] : function_inverse(identity_relation(A)) = identity_relation(A) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f42,negated_conjecture,(
% 0.11/5.63 ~((! [A] : function_inverse(identity_relation(A)) = identity_relation(A) ))),
% 0.11/5.63 inference(negated_conjecture,[status(cth)],[f41])).
% 0.11/5.63 fof(f44,axiom,(
% 0.11/5.63 (! [A] :( relation_dom(identity_relation(A)) = A& relation_rng(identity_relation(A)) = A ) )),
% 0.11/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/5.63 fof(f57,plain,(
% 0.11/5.63 ![A]: ((~relation(A)|~function(A))|(relation(function_inverse(A))&function(function_inverse(A))))),
% 0.11/5.63 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.11/5.63 fof(f58,plain,(
% 0.11/5.63 ![X0]: (~relation(X0)|~function(X0)|relation(function_inverse(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f57])).
% 0.11/5.63 fof(f59,plain,(
% 0.11/5.63 ![X0]: (~relation(X0)|~function(X0)|function(function_inverse(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f57])).
% 0.11/5.63 fof(f62,plain,(
% 0.11/5.63 ![X0]: (relation(identity_relation(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f7])).
% 0.11/5.63 fof(f76,plain,(
% 0.11/5.63 (![A]: relation(identity_relation(A)))&(![A]: function(identity_relation(A)))),
% 0.11/5.63 inference(miniscoping,[status(thm)],[f14])).
% 0.11/5.63 fof(f78,plain,(
% 0.11/5.63 ![X0]: (function(identity_relation(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f76])).
% 0.11/5.63 fof(f135,plain,(
% 0.11/5.63 ![A]: ((~relation(A)|~function(A))|(![B]: ((~relation(B)|~function(B))|((~relation_rng(A)=relation_dom(B)|~relation_composition(A,B)=A)|B=identity_relation(relation_dom(B))))))),
% 0.11/5.63 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.11/5.63 fof(f136,plain,(
% 0.11/5.63 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation_rng(X0)=relation_dom(X1)|~relation_composition(X0,X1)=X0|X1=identity_relation(relation_dom(X1)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f135])).
% 0.11/5.63 fof(f140,plain,(
% 0.11/5.63 ![X0]: (one_to_one(identity_relation(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f37])).
% 0.11/5.63 fof(f141,plain,(
% 0.11/5.63 ![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)))))),
% 0.11/5.63 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.11/5.63 fof(f142,plain,(
% 0.11/5.63 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_rng(X0)=relation_dom(function_inverse(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f141])).
% 0.11/5.63 fof(f147,plain,(
% 0.11/5.63 ![A]: ((~relation(A)|~function(A))|(~one_to_one(A)|(relation_composition(A,function_inverse(A))=identity_relation(relation_dom(A))&relation_composition(function_inverse(A),A)=identity_relation(relation_rng(A)))))),
% 0.11/5.63 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.11/5.63 fof(f148,plain,(
% 0.11/5.63 ![X0]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_composition(X0,function_inverse(X0))=identity_relation(relation_dom(X0)))),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f147])).
% 0.11/5.63 fof(f150,plain,(
% 0.11/5.63 (?[A]: ~function_inverse(identity_relation(A))=identity_relation(A))),
% 0.11/5.63 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.11/5.63 fof(f151,plain,(
% 0.11/5.63 ~function_inverse(identity_relation(sK11_skl))=identity_relation(sK11_skl)),
% 0.11/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f150])).
% 0.11/5.63 fof(f152,plain,(
% 0.11/5.63 ~function_inverse(identity_relation(sK11_skl))=identity_relation(sK11_skl)),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f151])).
% 0.11/5.63 fof(f155,plain,(
% 0.11/5.63 (![A]: relation_dom(identity_relation(A))=A)&(![A]: relation_rng(identity_relation(A))=A)),
% 0.11/5.63 inference(miniscoping,[status(thm)],[f44])).
% 0.11/5.63 fof(f156,plain,(
% 0.11/5.63 ![X0]: (relation_dom(identity_relation(X0))=X0)),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f155])).
% 0.11/5.63 fof(f157,plain,(
% 0.11/5.63 ![X0]: (relation_rng(identity_relation(X0))=X0)),
% 0.11/5.63 inference(cnf_transformation,[status(thm)],[f155])).
% 0.11/5.63 fof(f210,plain,(
% 0.11/5.63 ![X0]: (~relation(identity_relation(X0))|~function(identity_relation(X0))|relation_composition(identity_relation(X0),function_inverse(identity_relation(X0)))=identity_relation(relation_dom(identity_relation(X0))))),
% 0.11/5.63 inference(resolution,[status(thm)],[f140,f148])).
% 0.11/5.63 fof(f212,plain,(
% 0.11/5.63 ![X0]: (~relation(identity_relation(X0))|~function(identity_relation(X0))|relation_rng(identity_relation(X0))=relation_dom(function_inverse(identity_relation(X0))))),
% 0.11/5.63 inference(resolution,[status(thm)],[f140,f142])).
% 0.11/5.63 fof(f214,plain,(
% 0.11/5.63 ![X0]: (~function(identity_relation(X0))|relation_composition(identity_relation(X0),function_inverse(identity_relation(X0)))=identity_relation(relation_dom(identity_relation(X0))))),
% 0.11/5.63 inference(forward_subsumption_resolution,[status(thm)],[f210,f62])).
% 0.11/5.63 fof(f216,plain,(
% 0.11/5.63 ![X0]: (~function(identity_relation(X0))|relation_rng(identity_relation(X0))=relation_dom(function_inverse(identity_relation(X0))))),
% 0.11/5.63 inference(forward_subsumption_resolution,[status(thm)],[f212,f62])).
% 0.11/5.63 fof(f233,plain,(
% 0.11/5.63 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(function_inverse(X1))|~relation_rng(X0)=relation_dom(function_inverse(X1))|~relation_composition(X0,function_inverse(X1))=X0|function_inverse(X1)=identity_relation(relation_dom(function_inverse(X1)))|~relation(X1)|~function(X1))),
% 0.11/5.63 inference(resolution,[status(thm)],[f136,f59])).
% 0.11/5.63 fof(f240,plain,(
% 0.11/5.63 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=relation_dom(function_inverse(X1))|~relation_composition(X0,function_inverse(X1))=X0|function_inverse(X1)=identity_relation(relation_dom(function_inverse(X1)))|~relation(X1)|~function(X1))),
% 0.11/5.63 inference(forward_subsumption_resolution,[status(thm)],[f233,f58])).
% 0.11/5.63 fof(f250,plain,(
% 0.11/5.63 ![X0]: (relation_composition(identity_relation(X0),function_inverse(identity_relation(X0)))=identity_relation(relation_dom(identity_relation(X0))))),
% 0.11/5.63 inference(forward_subsumption_resolution,[status(thm)],[f214,f78])).
% 0.11/5.63 fof(f262,plain,(
% 0.11/5.63 ![X0]: (relation_rng(identity_relation(X0))=relation_dom(function_inverse(identity_relation(X0))))),
% 0.11/5.63 inference(forward_subsumption_resolution,[status(thm)],[f216,f78])).
% 0.11/5.63 fof(f284,plain,(
% 0.11/5.63 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=relation_dom(function_inverse(identity_relation(X1)))|~relation_composition(X0,function_inverse(identity_relation(X1)))=X0|function_inverse(identity_relation(X1))=identity_relation(relation_dom(function_inverse(identity_relation(X1))))|~relation(identity_relation(X1)))),
% 0.11/5.63 inference(resolution,[status(thm)],[f240,f78])).
% 0.11/5.63 fof(f293,plain,(
% 0.11/5.63 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=relation_rng(identity_relation(X1))|~relation_composition(X0,function_inverse(identity_relation(X1)))=X0|function_inverse(identity_relation(X1))=identity_relation(relation_dom(function_inverse(identity_relation(X1))))|~relation(identity_relation(X1)))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f262,f284])).
% 0.11/5.64 fof(f294,plain,(
% 0.11/5.64 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=relation_rng(identity_relation(X1))|~relation_composition(X0,function_inverse(identity_relation(X1)))=X0|function_inverse(identity_relation(X1))=identity_relation(relation_rng(identity_relation(X1)))|~relation(identity_relation(X1)))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f262,f293])).
% 0.11/5.64 fof(f295,plain,(
% 0.11/5.64 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=relation_rng(identity_relation(X1))|~relation_composition(X0,function_inverse(identity_relation(X1)))=X0|function_inverse(identity_relation(X1))=identity_relation(relation_rng(identity_relation(X1))))),
% 0.11/5.64 inference(forward_subsumption_resolution,[status(thm)],[f294,f62])).
% 0.11/5.64 fof(f314,plain,(
% 0.11/5.64 ![X0]: (relation_composition(identity_relation(X0),function_inverse(identity_relation(X0)))=identity_relation(X0))),
% 0.11/5.64 inference(backward_demodulation,[status(thm)],[f156,f250])).
% 0.11/5.64 fof(f716,plain,(
% 0.11/5.64 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=X1|~relation_composition(X0,function_inverse(identity_relation(X1)))=X0|function_inverse(identity_relation(X1))=identity_relation(relation_rng(identity_relation(X1))))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f157,f295])).
% 0.11/5.64 fof(f717,plain,(
% 0.11/5.64 ![X0,X1]: (~relation(X0)|~function(X0)|~relation_rng(X0)=X1|~relation_composition(X0,function_inverse(identity_relation(X1)))=X0|function_inverse(identity_relation(X1))=identity_relation(X1))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f157,f716])).
% 0.11/5.64 fof(f718,plain,(
% 0.11/5.64 ![X0]: (~relation(X0)|~function(X0)|~relation_composition(X0,function_inverse(identity_relation(relation_rng(X0))))=X0|function_inverse(identity_relation(relation_rng(X0)))=identity_relation(relation_rng(X0)))),
% 0.11/5.64 inference(destructive_equality_resolution,[status(thm)],[f717])).
% 0.11/5.64 fof(f723,plain,(
% 0.11/5.64 ![X0]: (~relation(identity_relation(X0))|~relation_composition(identity_relation(X0),function_inverse(identity_relation(relation_rng(identity_relation(X0)))))=identity_relation(X0)|function_inverse(identity_relation(relation_rng(identity_relation(X0))))=identity_relation(relation_rng(identity_relation(X0))))),
% 0.11/5.64 inference(resolution,[status(thm)],[f718,f78])).
% 0.11/5.64 fof(f736,plain,(
% 0.11/5.64 ![X0]: (~relation(identity_relation(X0))|~relation_composition(identity_relation(X0),function_inverse(identity_relation(X0)))=identity_relation(X0)|function_inverse(identity_relation(relation_rng(identity_relation(X0))))=identity_relation(relation_rng(identity_relation(X0))))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f157,f723])).
% 0.11/5.64 fof(f737,plain,(
% 0.11/5.64 ![X0]: (~relation(identity_relation(X0))|~identity_relation(X0)=identity_relation(X0)|function_inverse(identity_relation(relation_rng(identity_relation(X0))))=identity_relation(relation_rng(identity_relation(X0))))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f314,f736])).
% 0.11/5.64 fof(f738,plain,(
% 0.11/5.64 ![X0]: (~relation(identity_relation(X0))|~identity_relation(X0)=identity_relation(X0)|function_inverse(identity_relation(X0))=identity_relation(relation_rng(identity_relation(X0))))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f157,f737])).
% 0.11/5.64 fof(f739,plain,(
% 0.11/5.64 ![X0]: (~relation(identity_relation(X0))|~identity_relation(X0)=identity_relation(X0)|function_inverse(identity_relation(X0))=identity_relation(X0))),
% 0.11/5.64 inference(forward_demodulation,[status(thm)],[f157,f738])).
% 0.11/5.64 fof(f740,plain,(
% 0.11/5.64 ![X0]: (~relation(identity_relation(X0))|function_inverse(identity_relation(X0))=identity_relation(X0))),
% 0.11/5.64 inference(trivial_equality_resolution,[status(thm)],[f739])).
% 0.11/5.64 fof(f741,plain,(
% 0.11/5.64 ![X0]: (function_inverse(identity_relation(X0))=identity_relation(X0))),
% 0.11/5.64 inference(forward_subsumption_resolution,[status(thm)],[f740,f62])).
% 0.11/5.64 fof(f1016,plain,(
% 0.11/5.64 ~identity_relation(sK11_skl)=identity_relation(sK11_skl)),
% 0.11/5.64 inference(backward_demodulation,[status(thm)],[f741,f152])).
% 0.11/5.64 fof(f1028,plain,(
% 0.11/5.64 $false),
% 0.11/5.64 inference(trivial_equality_resolution,[status(thm)],[f1016])).
% 0.11/5.64 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/5.66 % Elapsed time: 0.083313 seconds
% 0.11/5.66 % CPU time: 0.426055 seconds
% 0.11/5.66 % Total memory used: 113.495 MB
% 0.11/5.66 % Net memory used: 112.758 MB
%------------------------------------------------------------------------------