%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU056+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:38 PM UTC 2026
% Result : Theorem 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU056+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.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:48:22 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f5,axiom,(
% 0.13/0.40 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f6,axiom,(
% 0.13/0.40 (! [A,B] :( disjoint(A,B)<=> set_intersection2(A,B) = empty_set ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f25,axiom,(
% 0.13/0.40 (! [A,B] :( disjoint(A,B)=> disjoint(B,A) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f26,axiom,(
% 0.13/0.40 (! [A,B,C] :( ( relation(C)& function(C) )=> ( one_to_one(C)=> relation_image(C,set_intersection2(A,B)) = set_intersection2(relation_image(C,A),relation_image(C,B)) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f27,conjecture,(
% 0.13/0.40 (! [A,B,C] :( ( relation(C)& function(C) )=> ( ( disjoint(A,B)& one_to_one(C) )=> disjoint(relation_image(C,A),relation_image(C,B)) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f28,negated_conjecture,(
% 0.13/0.40 ~((! [A,B,C] :( ( relation(C)& function(C) )=> ( ( disjoint(A,B)& one_to_one(C) )=> disjoint(relation_image(C,A),relation_image(C,B)) ) ) ))),
% 0.13/0.40 inference(negated_conjecture,[status(cth)],[f27])).
% 0.13/0.40 fof(f29,axiom,(
% 0.13/0.40 (! [A] :( relation(A)=> relation_image(A,empty_set) = empty_set ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f49,plain,(
% 0.13/0.40 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.40 fof(f50,plain,(
% 0.13/0.40 ![A,B]: ((~disjoint(A,B)|set_intersection2(A,B)=empty_set)&(disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f6])).
% 0.13/0.40 fof(f51,plain,(
% 0.13/0.40 (![A,B]: (~disjoint(A,B)|set_intersection2(A,B)=empty_set))&(![A,B]: (disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f50])).
% 0.13/0.40 fof(f52,plain,(
% 0.13/0.40 ![X0,X1]: (~disjoint(X0,X1)|set_intersection2(X0,X1)=empty_set)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f51])).
% 0.13/0.40 fof(f53,plain,(
% 0.13/0.40 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X0,X1)=empty_set)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f51])).
% 0.13/0.40 fof(f100,plain,(
% 0.13/0.40 ![A,B]: (~disjoint(A,B)|disjoint(B,A))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.13/0.40 fof(f101,plain,(
% 0.13/0.40 ![X0,X1]: (~disjoint(X0,X1)|disjoint(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f100])).
% 0.13/0.40 fof(f102,plain,(
% 0.13/0.40 ![A,B,C]: ((~relation(C)|~function(C))|(~one_to_one(C)|relation_image(C,set_intersection2(A,B))=set_intersection2(relation_image(C,A),relation_image(C,B))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.13/0.40 fof(f103,plain,(
% 0.13/0.40 ![C]: ((~relation(C)|~function(C))|(~one_to_one(C)|(![A,B]: relation_image(C,set_intersection2(A,B))=set_intersection2(relation_image(C,A),relation_image(C,B)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f102])).
% 0.13/0.40 fof(f104,plain,(
% 0.13/0.40 ![X0,X1,X2]: (~relation(X0)|~function(X0)|~one_to_one(X0)|relation_image(X0,set_intersection2(X1,X2))=set_intersection2(relation_image(X0,X1),relation_image(X0,X2)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f103])).
% 0.13/0.40 fof(f105,plain,(
% 0.13/0.40 (?[A,B,C]: ((relation(C)&function(C))&((disjoint(A,B)&one_to_one(C))&~disjoint(relation_image(C,A),relation_image(C,B)))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.13/0.40 fof(f106,plain,(
% 0.13/0.40 ?[C]: ((relation(C)&function(C))&(?[A,B]: ((disjoint(A,B)&one_to_one(C))&~disjoint(relation_image(C,A),relation_image(C,B)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f105])).
% 0.13/0.40 fof(f107,plain,(
% 0.13/0.40 ((relation(sK11_skl)&function(sK11_skl))&((disjoint(sK12_skl,sK13_skl)&one_to_one(sK11_skl))&~disjoint(relation_image(sK11_skl,sK12_skl),relation_image(sK11_skl,sK13_skl))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl]),skolemize(C,sK11_skl),skolemize(A,sK12_skl),skolemize(B,sK13_skl)],[f106])).
% 0.13/0.40 fof(f108,plain,(
% 0.13/0.40 relation(sK11_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.40 fof(f109,plain,(
% 0.13/0.40 function(sK11_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.40 fof(f110,plain,(
% 0.13/0.41 disjoint(sK12_skl,sK13_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.41 fof(f111,plain,(
% 0.13/0.41 one_to_one(sK11_skl)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.41 fof(f112,plain,(
% 0.13/0.41 ~disjoint(relation_image(sK11_skl,sK12_skl),relation_image(sK11_skl,sK13_skl))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.41 fof(f113,plain,(
% 0.13/0.41 ![A]: (~relation(A)|relation_image(A,empty_set)=empty_set)),
% 0.13/0.41 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.13/0.41 fof(f114,plain,(
% 0.13/0.41 ![X0]: (~relation(X0)|relation_image(X0,empty_set)=empty_set)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f113])).
% 0.13/0.41 fof(f144,plain,(
% 0.13/0.41 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X1,X0)=empty_set)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f49,f53])).
% 0.13/0.41 fof(f152,plain,(
% 0.13/0.41 disjoint(sK13_skl,sK12_skl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f101,f110])).
% 0.13/0.41 fof(f154,plain,(
% 0.13/0.41 set_intersection2(sK13_skl,sK12_skl)=empty_set),
% 0.13/0.41 inference(resolution,[status(thm)],[f152,f52])).
% 0.13/0.41 fof(f163,plain,(
% 0.13/0.41 ![X0,X1]: (~relation(sK11_skl)|~function(sK11_skl)|relation_image(sK11_skl,set_intersection2(X0,X1))=set_intersection2(relation_image(sK11_skl,X0),relation_image(sK11_skl,X1)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f104,f111])).
% 0.13/0.41 fof(f165,plain,(
% 0.13/0.41 ![X0,X1]: (~function(sK11_skl)|relation_image(sK11_skl,set_intersection2(X0,X1))=set_intersection2(relation_image(sK11_skl,X0),relation_image(sK11_skl,X1)))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f163,f108])).
% 0.13/0.41 fof(f170,plain,(
% 0.13/0.41 relation_image(sK11_skl,empty_set)=empty_set),
% 0.13/0.41 inference(resolution,[status(thm)],[f114,f108])).
% 0.13/0.41 fof(f172,plain,(
% 0.13/0.41 ~set_intersection2(relation_image(sK11_skl,sK13_skl),relation_image(sK11_skl,sK12_skl))=empty_set),
% 0.13/0.41 inference(resolution,[status(thm)],[f144,f112])).
% 0.13/0.41 fof(f181,plain,(
% 0.13/0.41 ![X0,X1]: (relation_image(sK11_skl,set_intersection2(X0,X1))=set_intersection2(relation_image(sK11_skl,X0),relation_image(sK11_skl,X1)))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f165,f109])).
% 0.13/0.41 fof(f192,plain,(
% 0.13/0.41 ~relation_image(sK11_skl,set_intersection2(sK13_skl,sK12_skl))=empty_set),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f181,f172])).
% 0.13/0.41 fof(f193,plain,(
% 0.13/0.41 ~relation_image(sK11_skl,empty_set)=empty_set),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f154,f192])).
% 0.13/0.41 fof(f194,plain,(
% 0.13/0.41 ~empty_set=empty_set),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f170,f193])).
% 0.13/0.41 fof(f195,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(trivial_equality_resolution,[status(thm)],[f194])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.44 % Elapsed time: 0.056224 seconds
% 0.13/0.44 % CPU time: 0.157921 seconds
% 0.13/0.44 % Total memory used: 102.820 MB
% 0.13/0.44 % Net memory used: 102.790 MB
%------------------------------------------------------------------------------