%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU094+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 : n008.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:40 PM UTC 2026
% Result : Theorem 0.23s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU094+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.65 % Computer : n008.cluster.edu
% 0.17/0.65 % Model : x86_64 x86_64
% 0.17/0.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.65 % Memory : 8046.5625MB
% 0.17/0.65 % OS : Linux 6.8.0-71-generic
% 0.17/0.65 % CPULimit : 300
% 0.22/0.65 % WCLimit : 300
% 0.22/0.65 % DateTime : Mon Sep 21 05:50:54 UTC 2026
% 0.22/0.65 % CPUTime :
% 0.22/0.67 % Drodi V4.1.1
% 0.23/0.77 % Refutation found
% 0.23/0.77 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.77 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.77 fof(f21,axiom,(
% 0.23/0.77 (! [A] :( ( finite(A)& (! [B] :( in(B,A)=> finite(B) ) ))=> finite(union(A)) ) )),
% 0.23/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.77 fof(f48,axiom,(
% 0.23/0.77 (! [A] : subset(A,powerset(union(A))) )),
% 0.23/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.77 fof(f49,axiom,(
% 0.23/0.77 (! [A,B] :( ( subset(A,B)& finite(B) )=> finite(A) ) )),
% 0.23/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.77 fof(f51,axiom,(
% 0.23/0.77 (! [A] :( finite(A)<=> finite(powerset(A)) ) )),
% 0.23/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.77 fof(f52,conjecture,(
% 0.23/0.77 (! [A] :( ( finite(A)& (! [B] :( in(B,A)=> finite(B) ) ))<=> finite(union(A)) ) )),
% 0.23/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.77 fof(f53,negated_conjecture,(
% 0.23/0.77 ~((! [A] :( ( finite(A)& (! [B] :( in(B,A)=> finite(B) ) ))<=> finite(union(A)) ) ))),
% 0.23/0.77 inference(negated_conjecture,[status(cth)],[f52])).
% 0.23/0.77 fof(f61,axiom,(
% 0.23/0.77 (! [A,B] :( in(A,B)=> subset(A,union(B)) ) )),
% 0.23/0.77 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.77 fof(f121,plain,(
% 0.23/0.77 ![A]: ((~finite(A)|(?[B]: (in(B,A)&~finite(B))))|finite(union(A)))),
% 0.23/0.77 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.23/0.77 fof(f122,plain,(
% 0.23/0.77 ![A]: ((~finite(A)|(in(sK1_skl(A),A)&~finite(sK1_skl(A))))|finite(union(A)))),
% 0.23/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f121])).
% 0.23/0.77 fof(f123,plain,(
% 0.23/0.77 ![X0]: (~finite(X0)|in(sK1_skl(X0),X0)|finite(union(X0)))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f122])).
% 0.23/0.77 fof(f124,plain,(
% 0.23/0.77 ![X0]: (~finite(X0)|~finite(sK1_skl(X0))|finite(union(X0)))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f122])).
% 0.23/0.77 fof(f239,plain,(
% 0.23/0.77 ![X0]: (subset(X0,powerset(union(X0))))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f48])).
% 0.23/0.77 fof(f240,plain,(
% 0.23/0.77 ![A,B]: ((~subset(A,B)|~finite(B))|finite(A))),
% 0.23/0.77 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.23/0.77 fof(f241,plain,(
% 0.23/0.77 ![A]: ((![B]: (~subset(A,B)|~finite(B)))|finite(A))),
% 0.23/0.77 inference(miniscoping,[status(thm)],[f240])).
% 0.23/0.77 fof(f242,plain,(
% 0.23/0.77 ![X0,X1]: (~subset(X0,X1)|~finite(X1)|finite(X0))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f241])).
% 0.23/0.77 fof(f245,plain,(
% 0.23/0.77 ![A]: ((~finite(A)|finite(powerset(A)))&(finite(A)|~finite(powerset(A))))),
% 0.23/0.77 inference(NNF_transformation,[status(thm)],[f51])).
% 0.23/0.77 fof(f246,plain,(
% 0.23/0.77 (![A]: (~finite(A)|finite(powerset(A))))&(![A]: (finite(A)|~finite(powerset(A))))),
% 0.23/0.77 inference(miniscoping,[status(thm)],[f245])).
% 0.23/0.77 fof(f247,plain,(
% 0.23/0.77 ![X0]: (~finite(X0)|finite(powerset(X0)))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f246])).
% 0.23/0.77 fof(f249,plain,(
% 0.23/0.77 (?[A]: ((finite(A)&(![B]: (~in(B,A)|finite(B))))<~>finite(union(A))))),
% 0.23/0.77 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.23/0.77 fof(f250,plain,(
% 0.23/0.77 ?[A]: (((finite(A)&(![B]: (~in(B,A)|finite(B))))|finite(union(A)))&((~finite(A)|(?[B]: (in(B,A)&~finite(B))))|~finite(union(A))))),
% 0.23/0.77 inference(NNF_transformation,[status(thm)],[f249])).
% 0.23/0.77 fof(f251,plain,(
% 0.23/0.77 (((finite(sK27_skl)&(![B]: (~in(B,sK27_skl)|finite(B))))|finite(union(sK27_skl)))&((~finite(sK27_skl)|(in(sK28_skl,sK27_skl)&~finite(sK28_skl)))|~finite(union(sK27_skl))))),
% 0.23/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(A,sK27_skl),skolemize(B,sK28_skl)],[f250])).
% 0.23/0.77 fof(f252,plain,(
% 0.23/0.77 finite(sK27_skl)|finite(union(sK27_skl))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f251])).
% 0.23/0.77 fof(f253,plain,(
% 0.23/0.77 ![X0]: (~in(X0,sK27_skl)|finite(X0)|finite(union(sK27_skl)))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f251])).
% 0.23/0.77 fof(f254,plain,(
% 0.23/0.77 ~finite(sK27_skl)|in(sK28_skl,sK27_skl)|~finite(union(sK27_skl))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f251])).
% 0.23/0.77 fof(f255,plain,(
% 0.23/0.77 ~finite(sK27_skl)|~finite(sK28_skl)|~finite(union(sK27_skl))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f251])).
% 0.23/0.77 fof(f276,plain,(
% 0.23/0.77 ![A,B]: (~in(A,B)|subset(A,union(B)))),
% 0.23/0.77 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.23/0.77 fof(f277,plain,(
% 0.23/0.77 ![X0,X1]: (~in(X0,X1)|subset(X0,union(X1)))),
% 0.23/0.77 inference(cnf_transformation,[status(thm)],[f276])).
% 0.23/0.79 fof(f891,plain,(
% 0.23/0.79 ![X0]: (~finite(powerset(union(X0)))|finite(X0))),
% 0.23/0.79 inference(resolution,[status(thm)],[f242,f239])).
% 0.23/0.79 fof(f912,plain,(
% 0.23/0.79 ![X0,X1]: (~in(X0,X1)|~finite(union(X1))|finite(X0))),
% 0.23/0.79 inference(resolution,[status(thm)],[f277,f242])).
% 0.23/0.79 fof(f913,plain,(
% 0.23/0.79 ![X0]: (~in(X0,sK27_skl)|finite(X0))),
% 0.23/0.79 inference(backward_subsumption_resolution,[status(thm)],[f253,f912])).
% 0.23/0.79 fof(f1009,plain,(
% 0.23/0.79 ![X0]: (finite(X0)|~finite(union(X0)))),
% 0.23/0.79 inference(resolution,[status(thm)],[f891,f247])).
% 0.23/0.79 fof(f1010,plain,(
% 0.23/0.79 in(sK28_skl,sK27_skl)|~finite(union(sK27_skl))),
% 0.23/0.79 inference(backward_subsumption_resolution,[status(thm)],[f254,f1009])).
% 0.23/0.79 fof(f1011,plain,(
% 0.23/0.79 ~finite(sK28_skl)|~finite(union(sK27_skl))),
% 0.23/0.79 inference(backward_subsumption_resolution,[status(thm)],[f255,f1009])).
% 0.23/0.79 fof(f1012,plain,(
% 0.23/0.79 finite(sK27_skl)),
% 0.23/0.79 inference(backward_subsumption_resolution,[status(thm)],[f252,f1009])).
% 0.23/0.79 fof(f1013,plain,(
% 0.23/0.79 in(sK1_skl(sK27_skl),sK27_skl)|finite(union(sK27_skl))),
% 0.23/0.79 inference(resolution,[status(thm)],[f1012,f123])).
% 0.23/0.79 fof(f1028,plain,(
% 0.23/0.79 finite(union(sK27_skl))|finite(sK1_skl(sK27_skl))),
% 0.23/0.79 inference(resolution,[status(thm)],[f1013,f913])).
% 0.23/0.79 fof(f1031,plain,(
% 0.23/0.79 finite(sK1_skl(sK27_skl))|~finite(sK28_skl)),
% 0.23/0.79 inference(resolution,[status(thm)],[f1028,f1011])).
% 0.23/0.79 fof(f1032,plain,(
% 0.23/0.79 finite(sK1_skl(sK27_skl))|in(sK28_skl,sK27_skl)),
% 0.23/0.79 inference(resolution,[status(thm)],[f1028,f1010])).
% 0.23/0.79 fof(f1090,plain,(
% 0.23/0.79 finite(sK1_skl(sK27_skl))|finite(sK28_skl)),
% 0.23/0.79 inference(resolution,[status(thm)],[f1032,f913])).
% 0.23/0.79 fof(f1093,plain,(
% 0.23/0.79 finite(sK1_skl(sK27_skl))),
% 0.23/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1090,f1031])).
% 0.23/0.79 fof(f1094,plain,(
% 0.23/0.79 ~finite(sK27_skl)|finite(union(sK27_skl))),
% 0.23/0.79 inference(resolution,[status(thm)],[f1093,f124])).
% 0.23/0.79 fof(f1096,plain,(
% 0.23/0.79 ~finite(sK28_skl)),
% 0.23/0.79 inference(backward_subsumption_resolution,[status(thm)],[f1011,f1098])).
% 0.23/0.79 fof(f1097,plain,(
% 0.23/0.79 in(sK28_skl,sK27_skl)),
% 0.23/0.79 inference(backward_subsumption_resolution,[status(thm)],[f1010,f1098])).
% 0.23/0.79 fof(f1098,plain,(
% 0.23/0.79 finite(union(sK27_skl))),
% 0.23/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1094,f1012])).
% 0.23/0.79 fof(f1102,plain,(
% 0.23/0.79 finite(sK28_skl)),
% 0.23/0.79 inference(resolution,[status(thm)],[f1097,f913])).
% 0.23/0.79 fof(f1105,plain,(
% 0.23/0.79 $false),
% 0.23/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1102,f1096])).
% 0.23/0.79 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.80 % Elapsed time: 0.126479 seconds
% 0.23/0.80 % CPU time: 0.744873 seconds
% 0.23/0.80 % Total memory used: 93.092 MB
% 0.23/0.80 % Net memory used: 92.235 MB
%------------------------------------------------------------------------------