%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU020+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 : n020.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.12s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU020+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.09/0.37 % Computer : n020.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 05:48:03 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.41 % Refutation found
% 0.12/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.41 fof(f29,axiom,(
% 0.12/0.41 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( relation_dom(relation_composition(B,A)) = relation_dom(B)=> subset(relation_rng(B),relation_dom(A)) ) ) )) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f32,axiom,(
% 0.12/0.41 (! [A] :( ( relation(A)& function(A) )=> (! [B] :( ( relation(B)& function(B) )=> ( ( one_to_one(relation_composition(B,A))& subset(relation_rng(B),relation_dom(A)) )=> one_to_one(B) ) ) )) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f34,axiom,(
% 0.12/0.41 (! [A] : one_to_one(identity_relation(A)) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f35,conjecture,(
% 0.12/0.41 (! [A] :( ( relation(A)& function(A) )=> ( (? [B] :( relation(B)& function(B)& relation_composition(A,B) = identity_relation(relation_dom(A)) ))=> one_to_one(A) ) ) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f36,negated_conjecture,(
% 0.12/0.41 ~((! [A] :( ( relation(A)& function(A) )=> ( (? [B] :( relation(B)& function(B)& relation_composition(A,B) = identity_relation(relation_dom(A)) ))=> one_to_one(A) ) ) ))),
% 0.12/0.41 inference(negated_conjecture,[status(cth)],[f35])).
% 0.12/0.41 fof(f39,axiom,(
% 0.12/0.41 (! [A] :( relation_dom(identity_relation(A)) = A& relation_rng(identity_relation(A)) = A ) )),
% 0.12/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f109,plain,(
% 0.12/0.41 ![A]: ((~relation(A)|~function(A))|(![B]: ((~relation(B)|~function(B))|(~relation_dom(relation_composition(B,A))=relation_dom(B)|subset(relation_rng(B),relation_dom(A))))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.12/0.41 fof(f110,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation_dom(relation_composition(X1,X0))=relation_dom(X1)|subset(relation_rng(X1),relation_dom(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/0.41 fof(f117,plain,(
% 0.12/0.41 ![A]: ((~relation(A)|~function(A))|(![B]: ((~relation(B)|~function(B))|((~one_to_one(relation_composition(B,A))|~subset(relation_rng(B),relation_dom(A)))|one_to_one(B)))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.12/0.41 fof(f118,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~one_to_one(relation_composition(X1,X0))|~subset(relation_rng(X1),relation_dom(X0))|one_to_one(X1))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f117])).
% 0.12/0.41 fof(f122,plain,(
% 0.12/0.41 ![X0]: (one_to_one(identity_relation(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f34])).
% 0.12/0.41 fof(f123,plain,(
% 0.12/0.41 (?[A]: ((relation(A)&function(A))&((?[B]: ((relation(B)&function(B))&relation_composition(A,B)=identity_relation(relation_dom(A))))&~one_to_one(A))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.12/0.41 fof(f124,plain,(
% 0.12/0.41 ((relation(sK9_skl)&function(sK9_skl))&(((relation(sK10_skl)&function(sK10_skl))&relation_composition(sK9_skl,sK10_skl)=identity_relation(relation_dom(sK9_skl)))&~one_to_one(sK9_skl)))),
% 0.12/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(A,sK9_skl),skolemize(B,sK10_skl)],[f123])).
% 0.12/0.41 fof(f125,plain,(
% 0.12/0.41 relation(sK9_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.41 fof(f126,plain,(
% 0.12/0.41 function(sK9_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.41 fof(f127,plain,(
% 0.12/0.41 relation(sK10_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.41 fof(f128,plain,(
% 0.12/0.41 function(sK10_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.41 fof(f129,plain,(
% 0.12/0.41 relation_composition(sK9_skl,sK10_skl)=identity_relation(relation_dom(sK9_skl))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.41 fof(f130,plain,(
% 0.12/0.41 ~one_to_one(sK9_skl)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.12/0.41 fof(f136,plain,(
% 0.12/0.41 (![A]: relation_dom(identity_relation(A))=A)&(![A]: relation_rng(identity_relation(A))=A)),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f39])).
% 0.12/0.41 fof(f137,plain,(
% 0.12/0.41 ![X0]: (relation_dom(identity_relation(X0))=X0)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f136])).
% 0.12/0.41 fof(f147,plain,(
% 0.12/0.41 one_to_one(relation_composition(sK9_skl,sK10_skl))),
% 0.12/0.41 inference(paramodulation,[status(thm)],[f129,f122])).
% 0.12/0.41 fof(f150,plain,(
% 0.12/0.41 relation_dom(relation_composition(sK9_skl,sK10_skl))=relation_dom(sK9_skl)),
% 0.12/0.41 inference(paramodulation,[status(thm)],[f129,f137])).
% 0.12/0.41 fof(f178,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation_dom(relation_composition(X1,X0))=relation_dom(X1)|~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~one_to_one(relation_composition(X1,X0))|one_to_one(X1))),
% 0.12/0.41 inference(resolution,[status(thm)],[f110,f118])).
% 0.12/0.41 fof(f182,plain,(
% 0.12/0.41 ![X0,X1]: (~relation(X0)|~function(X0)|~relation(X1)|~function(X1)|~relation_dom(relation_composition(X1,X0))=relation_dom(X1)|~one_to_one(relation_composition(X1,X0))|one_to_one(X1))),
% 0.12/0.41 inference(duplicate_literals_removal,[status(thm)],[f178])).
% 0.12/0.41 fof(f209,plain,(
% 0.12/0.41 ~relation(sK10_skl)|~function(sK10_skl)|~relation(sK9_skl)|~function(sK9_skl)|~relation_dom(relation_composition(sK9_skl,sK10_skl))=relation_dom(sK9_skl)|one_to_one(sK9_skl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f182,f147])).
% 0.12/0.41 fof(f210,plain,(
% 0.12/0.41 ~relation(sK10_skl)|~function(sK10_skl)|~relation(sK9_skl)|~function(sK9_skl)|~relation_dom(sK9_skl)=relation_dom(sK9_skl)|one_to_one(sK9_skl)),
% 0.12/0.41 inference(forward_demodulation,[status(thm)],[f150,f209])).
% 0.12/0.41 fof(f211,plain,(
% 0.12/0.41 ~relation(sK10_skl)|~function(sK10_skl)|~relation(sK9_skl)|~function(sK9_skl)|one_to_one(sK9_skl)),
% 0.12/0.41 inference(trivial_equality_resolution,[status(thm)],[f210])).
% 0.12/0.41 fof(f212,plain,(
% 0.12/0.41 ~function(sK10_skl)|~relation(sK9_skl)|~function(sK9_skl)|one_to_one(sK9_skl)),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f211,f127])).
% 0.12/0.41 fof(f278,plain,(
% 0.12/0.41 ~relation(sK9_skl)|~function(sK9_skl)|one_to_one(sK9_skl)),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f212,f128])).
% 0.12/0.41 fof(f279,plain,(
% 0.12/0.41 ~relation(sK9_skl)|~function(sK9_skl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f278,f130])).
% 0.12/0.41 fof(f280,plain,(
% 0.12/0.41 ~function(sK9_skl)),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f279,f125])).
% 0.12/0.41 fof(f282,plain,(
% 0.12/0.41 $false),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f280,f126])).
% 0.12/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45 % Elapsed time: 0.068912 seconds
% 0.12/0.45 % CPU time: 0.216464 seconds
% 0.12/0.45 % Total memory used: 97.219 MB
% 0.12/0.45 % Net memory used: 97.134 MB
%------------------------------------------------------------------------------