%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU140+1 : 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:21:46 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU140+1 : 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:52:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f3,axiom,(
% 0.14/0.40 (! [A,B] :( disjoint(A,B)<=> set_intersection2(A,B) = empty_set ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f12,axiom,(
% 0.14/0.40 (! [A,B,C] :( subset(A,B)=> subset(set_intersection2(A,C),set_intersection2(B,C)) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f14,axiom,(
% 0.14/0.40 (! [A] :( subset(A,empty_set)=> A = empty_set ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f15,conjecture,(
% 0.14/0.40 (! [A,B,C] :( ( subset(A,B)& disjoint(B,C) )=> disjoint(A,C) ) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f16,negated_conjecture,(
% 0.14/0.40 ~((! [A,B,C] :( ( subset(A,B)& disjoint(B,C) )=> disjoint(A,C) ) ))),
% 0.14/0.40 inference(negated_conjecture,[status(cth)],[f15])).
% 0.14/0.40 fof(f23,plain,(
% 0.14/0.40 ![A,B]: ((~disjoint(A,B)|set_intersection2(A,B)=empty_set)&(disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 0.14/0.40 inference(NNF_transformation,[status(thm)],[f3])).
% 0.14/0.40 fof(f24,plain,(
% 0.14/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.14/0.40 inference(miniscoping,[status(thm)],[f23])).
% 0.14/0.40 fof(f25,plain,(
% 0.14/0.40 ![X0,X1]: (~disjoint(X0,X1)|set_intersection2(X0,X1)=empty_set)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.40 fof(f26,plain,(
% 0.14/0.40 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X0,X1)=empty_set)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/0.40 fof(f38,plain,(
% 0.14/0.40 ![A,B,C]: (~subset(A,B)|subset(set_intersection2(A,C),set_intersection2(B,C)))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f39,plain,(
% 0.14/0.40 ![A,B]: (~subset(A,B)|(![C]: subset(set_intersection2(A,C),set_intersection2(B,C))))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f38])).
% 0.14/0.40 fof(f40,plain,(
% 0.14/0.40 ![X0,X1,X2]: (~subset(X0,X1)|subset(set_intersection2(X0,X2),set_intersection2(X1,X2)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.40 fof(f42,plain,(
% 0.14/0.40 ![A]: (~subset(A,empty_set)|A=empty_set)),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.14/0.40 fof(f43,plain,(
% 0.14/0.40 ![X0]: (~subset(X0,empty_set)|X0=empty_set)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.40 fof(f44,plain,(
% 0.14/0.40 (?[A,B,C]: ((subset(A,B)&disjoint(B,C))&~disjoint(A,C)))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.14/0.40 fof(f45,plain,(
% 0.14/0.40 ?[A,C]: ((?[B]: (subset(A,B)&disjoint(B,C)))&~disjoint(A,C))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f44])).
% 0.14/0.40 fof(f46,plain,(
% 0.14/0.40 ((subset(sK2_skl,sK4_skl)&disjoint(sK4_skl,sK3_skl))&~disjoint(sK2_skl,sK3_skl))),
% 0.14/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl]),skolemize(A,sK2_skl),skolemize(C,sK3_skl),skolemize(B,sK4_skl)],[f45])).
% 0.14/0.40 fof(f47,plain,(
% 0.14/0.40 subset(sK2_skl,sK4_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/0.40 fof(f48,plain,(
% 0.14/0.40 disjoint(sK4_skl,sK3_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/0.40 fof(f49,plain,(
% 0.14/0.40 ~disjoint(sK2_skl,sK3_skl)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/0.40 fof(f61,plain,(
% 0.14/0.40 set_intersection2(sK4_skl,sK3_skl)=empty_set),
% 0.14/0.40 inference(resolution,[status(thm)],[f25,f48])).
% 0.14/0.40 fof(f69,plain,(
% 0.14/0.40 ![X0]: (subset(set_intersection2(sK2_skl,X0),set_intersection2(sK4_skl,X0)))),
% 0.14/0.40 inference(resolution,[status(thm)],[f40,f47])).
% 0.14/0.40 fof(f72,plain,(
% 0.14/0.40 subset(set_intersection2(sK2_skl,sK3_skl),empty_set)),
% 0.14/0.40 inference(paramodulation,[status(thm)],[f61,f69])).
% 0.14/0.40 fof(f73,plain,(
% 0.14/0.40 set_intersection2(sK2_skl,sK3_skl)=empty_set),
% 0.14/0.40 inference(resolution,[status(thm)],[f72,f43])).
% 0.14/0.40 fof(f76,plain,(
% 0.14/0.40 disjoint(sK2_skl,sK3_skl)),
% 0.14/0.40 inference(resolution,[status(thm)],[f73,f26])).
% 0.14/0.40 fof(f79,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f76,f49])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.41 % Elapsed time: 0.048696 seconds
% 0.14/0.41 % CPU time: 0.138972 seconds
% 0.14/0.41 % Total memory used: 66.624 MB
% 0.14/0.41 % Net memory used: 66.242 MB
%------------------------------------------------------------------------------