%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU430+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:22:39 PM UTC 2026
% Result : Theorem 26.15s 11.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU430+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.56 % Computer : n001.cluster.edu
% 0.11/5.56 % Model : x86_64 x86_64
% 0.11/5.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.56 % Memory : 8046.5625MB
% 0.11/5.56 % OS : Linux 6.8.0-71-generic
% 0.11/5.56 % CPULimit : 300
% 0.11/5.56 % WCLimit : 300
% 0.11/5.56 % DateTime : Mon Sep 21 06:34:29 UTC 2026
% 0.11/5.56 % CPUTime :
% 3.06/8.55 % Drodi V4.1.1
% 26.15/11.55 % Refutation found
% 26.15/11.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 26.15/11.55 % SZS output start CNFRefutation for theBenchmark
% 26.15/11.55 fof(f9,axiom,(
% 26.15/11.55 (! [A,B] :( B = k3_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> (? [D] :( r2_hidden(C,D)& r2_hidden(D,A) ) )) )) )),
% 26.15/11.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.15/11.55 fof(f29,axiom,(
% 26.15/11.55 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 26.15/11.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.15/11.55 fof(f669,axiom,(
% 26.15/11.55 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> k5_setfam_1(A,B) = k3_tarski(B) ) )),
% 26.15/11.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.15/11.55 fof(f19101,conjecture,(
% 26.15/11.55 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> ( k5_setfam_1(A,B) = k1_xboole_0<=> (! [C] :( r2_hidden(C,B)=> C = k1_xboole_0 ) )) ) )),
% 26.15/11.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 26.15/11.55 fof(f19102,negated_conjecture,(
% 26.15/11.55 ~((! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> ( k5_setfam_1(A,B) = k1_xboole_0<=> (! [C] :( r2_hidden(C,B)=> C = k1_xboole_0 ) )) ) ))),
% 26.15/11.55 inference(negated_conjecture,[status(cth)],[f19101])).
% 26.15/11.55 fof(f19133,plain,(
% 26.15/11.55 ![A,B]: ((~B=k3_tarski(A)|(![C]: ((~r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A))))&(r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A)))))))&(B=k3_tarski(A)|(?[C]: ((~r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))&(r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A))))))))),
% 26.15/11.55 inference(NNF_transformation,[status(thm)],[f9])).
% 26.15/11.55 fof(f19134,plain,(
% 26.15/11.55 (![A,B]: (~B=k3_tarski(A)|((![C]: (~r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A)))))&(![C]: (r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))))))&(![A,B]: (B=k3_tarski(A)|(?[C]: ((~r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))&(r2_hidden(C,B)|(?[D]: (r2_hidden(C,D)&r2_hidden(D,A))))))))),
% 26.15/11.55 inference(miniscoping,[status(thm)],[f19133])).
% 26.15/11.55 fof(f19135,plain,(
% 26.15/11.55 (![A,B]: (~B=k3_tarski(A)|((![C]: (~r2_hidden(C,B)|(r2_hidden(C,sK4_skl(C,B,A))&r2_hidden(sK4_skl(C,B,A),A))))&(![C]: (r2_hidden(C,B)|(![D]: (~r2_hidden(C,D)|~r2_hidden(D,A))))))))&(![A,B]: (B=k3_tarski(A)|((~r2_hidden(sK5_skl(B,A),B)|(![D]: (~r2_hidden(sK5_skl(B,A),D)|~r2_hidden(D,A))))&(r2_hidden(sK5_skl(B,A),B)|(r2_hidden(sK5_skl(B,A),sK6_skl(B,A))&r2_hidden(sK6_skl(B,A),A))))))),
% 26.15/11.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f19134])).
% 26.15/11.55 fof(f19138,plain,(
% 26.15/11.55 ![X0,X1,X2,X3]: (~X0=k3_tarski(X1)|r2_hidden(X2,X0)|~r2_hidden(X2,X3)|~r2_hidden(X3,X1))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f19135])).
% 26.15/11.55 fof(f19140,plain,(
% 26.15/11.55 ![X0,X1]: (X0=k3_tarski(X1)|r2_hidden(sK5_skl(X0,X1),X0)|r2_hidden(sK5_skl(X0,X1),sK6_skl(X0,X1)))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f19135])).
% 26.15/11.55 fof(f19141,plain,(
% 26.15/11.55 ![X0,X1]: (X0=k3_tarski(X1)|r2_hidden(sK5_skl(X0,X1),X0)|r2_hidden(sK6_skl(X0,X1),X1))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f19135])).
% 26.15/11.55 fof(f19192,plain,(
% 26.15/11.55 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 26.15/11.55 inference(NNF_transformation,[status(thm)],[f29])).
% 26.15/11.55 fof(f19193,plain,(
% 26.15/11.55 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 26.15/11.55 inference(miniscoping,[status(thm)],[f19192])).
% 26.15/11.55 fof(f19194,plain,(
% 26.15/11.55 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 26.15/11.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f19193])).
% 26.15/11.55 fof(f19195,plain,(
% 26.15/11.55 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f19194])).
% 26.15/11.55 fof(f19196,plain,(
% 26.15/11.55 ![X0]: (X0=k1_xboole_0|r2_hidden(sK22_skl(X0),X0))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f19194])).
% 26.15/11.55 fof(f20553,plain,(
% 26.15/11.55 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|k5_setfam_1(A,B)=k3_tarski(B))),
% 26.15/11.55 inference(pre_NNF_transformation,[status(thm)],[f669])).
% 26.15/11.55 fof(f20554,plain,(
% 26.15/11.55 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|k5_setfam_1(X1,X0)=k3_tarski(X0))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f20553])).
% 26.15/11.55 fof(f89326,plain,(
% 26.15/11.55 (?[A,B]: (m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))&(k5_setfam_1(A,B)=k1_xboole_0<~>(![C]: (~r2_hidden(C,B)|C=k1_xboole_0)))))),
% 26.15/11.55 inference(pre_NNF_transformation,[status(thm)],[f19102])).
% 26.15/11.55 fof(f89327,plain,(
% 26.15/11.55 ?[A,B]: (m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))&((k5_setfam_1(A,B)=k1_xboole_0|(![C]: (~r2_hidden(C,B)|C=k1_xboole_0)))&(~k5_setfam_1(A,B)=k1_xboole_0|(?[C]: (r2_hidden(C,B)&~C=k1_xboole_0)))))),
% 26.15/11.55 inference(NNF_transformation,[status(thm)],[f89326])).
% 26.15/11.55 fof(f89328,plain,(
% 26.15/11.55 (m1_subset_1(sK6524_skl,k1_zfmisc_1(k1_zfmisc_1(sK6523_skl)))&((k5_setfam_1(sK6523_skl,sK6524_skl)=k1_xboole_0|(![C]: (~r2_hidden(C,sK6524_skl)|C=k1_xboole_0)))&(~k5_setfam_1(sK6523_skl,sK6524_skl)=k1_xboole_0|(r2_hidden(sK6525_skl,sK6524_skl)&~sK6525_skl=k1_xboole_0))))),
% 26.15/11.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK6523_skl,sK6524_skl,sK6525_skl]),skolemize(A,sK6523_skl),skolemize(B,sK6524_skl),skolemize(C,sK6525_skl)],[f89327])).
% 26.15/11.55 fof(f89329,plain,(
% 26.15/11.55 m1_subset_1(sK6524_skl,k1_zfmisc_1(k1_zfmisc_1(sK6523_skl)))),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f89328])).
% 26.15/11.55 fof(f89330,plain,(
% 26.15/11.55 ![X0]: (k5_setfam_1(sK6523_skl,sK6524_skl)=k1_xboole_0|~r2_hidden(X0,sK6524_skl)|X0=k1_xboole_0)),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f89328])).
% 26.15/11.55 fof(f89331,plain,(
% 26.15/11.55 ~k5_setfam_1(sK6523_skl,sK6524_skl)=k1_xboole_0|r2_hidden(sK6525_skl,sK6524_skl)),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f89328])).
% 26.15/11.55 fof(f89332,plain,(
% 26.15/11.55 ~k5_setfam_1(sK6523_skl,sK6524_skl)=k1_xboole_0|~sK6525_skl=k1_xboole_0),
% 26.15/11.55 inference(cnf_transformation,[status(thm)],[f89328])).
% 26.15/11.55 fof(f95912,plain,(
% 26.15/11.55 ![X0,X1,X2]: (r2_hidden(X0,k3_tarski(X1))|~r2_hidden(X0,X2)|~r2_hidden(X2,X1))),
% 26.15/11.55 inference(destructive_equality_resolution,[status(thm)],[f19138])).
% 26.15/11.55 fof(f95915,plain,(
% 26.15/11.55 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 26.15/11.55 inference(destructive_equality_resolution,[status(thm)],[f19195])).
% 26.15/11.55 fof(f100914,plain,(
% 26.15/11.55 k5_setfam_1(sK6523_skl,sK6524_skl)=k3_tarski(sK6524_skl)),
% 26.15/11.55 inference(resolution,[status(thm)],[f20554,f89329])).
% 26.15/11.55 fof(f100930,plain,(
% 26.15/11.55 ![X0]: (X0=k3_tarski(sK6524_skl)|r2_hidden(sK5_skl(X0,sK6524_skl),X0)|k5_setfam_1(sK6523_skl,sK6524_skl)=k1_xboole_0|sK6_skl(X0,sK6524_skl)=k1_xboole_0)),
% 26.15/11.55 inference(resolution,[status(thm)],[f19141,f89330])).
% 26.15/11.55 fof(f100964,plain,(
% 26.15/11.55 ~k3_tarski(sK6524_skl)=k1_xboole_0|~sK6525_skl=k1_xboole_0),
% 26.15/11.55 inference(backward_demodulation,[status(thm)],[f100914,f89332])).
% 26.15/11.55 fof(f100965,plain,(
% 26.15/11.55 ~k3_tarski(sK6524_skl)=k1_xboole_0|r2_hidden(sK6525_skl,sK6524_skl)),
% 26.15/11.55 inference(backward_demodulation,[status(thm)],[f100914,f89331])).
% 26.15/11.55 fof(f101442,plain,(
% 26.15/11.55 ![X0]: (X0=k3_tarski(sK6524_skl)|r2_hidden(sK5_skl(X0,sK6524_skl),X0)|k3_tarski(sK6524_skl)=k1_xboole_0|sK6_skl(X0,sK6524_skl)=k1_xboole_0)),
% 26.15/11.55 inference(forward_demodulation,[status(thm)],[f100914,f100930])).
% 26.15/11.55 fof(f101449,plain,(
% 26.15/11.55 k1_xboole_0=k3_tarski(sK6524_skl)|k3_tarski(sK6524_skl)=k1_xboole_0|sK6_skl(k1_xboole_0,sK6524_skl)=k1_xboole_0),
% 26.15/11.55 inference(resolution,[status(thm)],[f101442,f95915])).
% 26.15/11.55 fof(f101478,plain,(
% 26.15/11.55 k1_xboole_0=k3_tarski(sK6524_skl)|sK6_skl(k1_xboole_0,sK6524_skl)=k1_xboole_0),
% 26.15/11.55 inference(duplicate_literals_removal,[status(thm)],[f101449])).
% 26.15/11.55 fof(f102065,plain,(
% 26.15/11.55 k1_xboole_0=k3_tarski(sK6524_skl)|r2_hidden(sK5_skl(k1_xboole_0,sK6524_skl),k1_xboole_0)|r2_hidden(sK5_skl(k1_xboole_0,sK6524_skl),k1_xboole_0)|k1_xboole_0=k3_tarski(sK6524_skl)),
% 26.15/11.55 inference(paramodulation,[status(thm)],[f101478,f19140])).
% 26.15/11.55 fof(f102068,plain,(
% 26.15/11.55 k1_xboole_0=k3_tarski(sK6524_skl)|r2_hidden(sK5_skl(k1_xboole_0,sK6524_skl),k1_xboole_0)),
% 26.15/11.55 inference(duplicate_literals_removal,[status(thm)],[f102065])).
% 26.15/11.55 fof(f102069,plain,(
% 26.15/11.55 k1_xboole_0=k3_tarski(sK6524_skl)),
% 26.15/11.55 inference(forward_subsumption_resolution,[status(thm)],[f102068,f95915])).
% 26.15/11.55 fof(f102545,plain,(
% 26.15/11.55 ~k1_xboole_0=k1_xboole_0|r2_hidden(sK6525_skl,sK6524_skl)),
% 26.15/11.55 inference(backward_demodulation,[status(thm)],[f102069,f100965])).
% 26.15/11.55 fof(f102546,plain,(
% 26.15/11.55 ~k1_xboole_0=k1_xboole_0|~sK6525_skl=k1_xboole_0),
% 26.15/11.55 inference(backward_demodulation,[status(thm)],[f102069,f100964])).
% 26.15/11.55 fof(f102549,plain,(
% 26.15/11.55 ![X0,X1]: (r2_hidden(X0,k1_xboole_0)|~r2_hidden(X0,X1)|~r2_hidden(X1,sK6524_skl))),
% 26.05/11.89 inference(paramodulation,[status(thm)],[f102069,f95912])).
% 26.05/11.89 fof(f102554,plain,(
% 26.05/11.89 r2_hidden(sK6525_skl,sK6524_skl)),
% 26.05/11.89 inference(trivial_equality_resolution,[status(thm)],[f102545])).
% 26.05/11.89 fof(f102555,plain,(
% 26.05/11.89 ~sK6525_skl=k1_xboole_0),
% 26.05/11.89 inference(trivial_equality_resolution,[status(thm)],[f102546])).
% 26.05/11.89 fof(f102558,plain,(
% 26.05/11.89 ![X0,X1]: (~r2_hidden(X0,X1)|~r2_hidden(X1,sK6524_skl))),
% 26.05/11.89 inference(forward_subsumption_resolution,[status(thm)],[f102549,f95915])).
% 26.05/11.89 fof(f104525,plain,(
% 26.05/11.89 ![X0]: (~r2_hidden(X0,sK6525_skl))),
% 26.05/11.89 inference(resolution,[status(thm)],[f102558,f102554])).
% 26.05/11.89 fof(f104589,plain,(
% 26.05/11.89 sK6525_skl=k1_xboole_0),
% 26.05/11.89 inference(resolution,[status(thm)],[f104525,f19196])).
% 26.05/11.89 fof(f104604,plain,(
% 26.05/11.89 $false),
% 26.05/11.89 inference(forward_subsumption_resolution,[status(thm)],[f104589,f102555])).
% 26.05/11.89 % SZS output end CNFRefutation for theBenchmark.p
% 3.94/12.01 % Elapsed time: 6.354539 seconds
% 3.94/12.01 % CPU time: 27.237087 seconds
% 3.94/12.01 % Total memory used: 5.358 GB
% 3.94/12.01 % Net memory used: 5.310 GB
%------------------------------------------------------------------------------