%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU430+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 92.57s 35.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU430+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.37 % Computer : n010.cluster.edu
% 0.10/10.37 % Model : x86_64 x86_64
% 0.10/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.37 % Memory : 8046.5625MB
% 0.10/10.37 % OS : Linux 6.8.0-71-generic
% 0.10/10.37 % CPULimit : 300
% 0.10/10.37 % WCLimit : 300
% 0.10/10.37 % DateTime : Mon Sep 21 06:30:23 UTC 2026
% 0.10/10.37 % CPUTime :
% 15.25/25.56 % Drodi V4.1.1
% 92.57/35.45 % Refutation found
% 92.57/35.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 92.57/35.45 % SZS output start CNFRefutation for theBenchmark
% 92.57/35.45 fof(f9,axiom,(
% 92.57/35.45 (! [A,B] :( B = k3_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> (? [D] :( r2_hidden(C,D)& r2_hidden(D,A) ) )) )) )),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f29,axiom,(
% 92.57/35.45 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f67,axiom,(
% 92.57/35.45 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f669,axiom,(
% 92.57/35.45 (! [A,B] :( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))=> k5_setfam_1(A,B) = k3_tarski(B) ) )),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f3028,axiom,(
% 92.57/35.45 ( v1_xboole_0(k12_arytm_3)& m1_subset_1(k12_arytm_3,k6_arytm_3) ) ),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f3029,axiom,(
% 92.57/35.45 k12_arytm_3 = k1_xboole_0 ),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f5328,axiom,(
% 92.57/35.45 np__0 = k1_xboole_0 ),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f71112,conjecture,(
% 92.57/35.45 (! [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 ) )) ) )),
% 92.57/35.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 92.57/35.45 fof(f71113,negated_conjecture,(
% 92.57/35.45 ~((! [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 ) )) ) ))),
% 92.57/35.45 inference(negated_conjecture,[status(cth)],[f71112])).
% 92.57/35.45 fof(f71144,plain,(
% 92.57/35.45 ![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))))))))),
% 92.57/35.45 inference(NNF_transformation,[status(thm)],[f9])).
% 92.57/35.45 fof(f71145,plain,(
% 92.57/35.45 (![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))))))))),
% 92.57/35.45 inference(miniscoping,[status(thm)],[f71144])).
% 92.57/35.45 fof(f71146,plain,(
% 92.57/35.45 (![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))))))),
% 92.57/35.45 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))],[f71145])).
% 92.57/35.45 fof(f71149,plain,(
% 92.57/35.45 ![X0,X1,X2,X3]: (~X0=k3_tarski(X1)|r2_hidden(X2,X0)|~r2_hidden(X2,X3)|~r2_hidden(X3,X1))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f71146])).
% 92.57/35.45 fof(f71151,plain,(
% 92.57/35.45 ![X0,X1]: (X0=k3_tarski(X1)|r2_hidden(sK5_skl(X0,X1),X0)|r2_hidden(sK5_skl(X0,X1),sK6_skl(X0,X1)))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f71146])).
% 92.57/35.45 fof(f71152,plain,(
% 92.57/35.45 ![X0,X1]: (X0=k3_tarski(X1)|r2_hidden(sK5_skl(X0,X1),X0)|r2_hidden(sK6_skl(X0,X1),X1))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f71146])).
% 92.57/35.45 fof(f71203,plain,(
% 92.57/35.45 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 92.57/35.45 inference(NNF_transformation,[status(thm)],[f29])).
% 92.57/35.45 fof(f71204,plain,(
% 92.57/35.45 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 92.57/35.45 inference(miniscoping,[status(thm)],[f71203])).
% 92.57/35.45 fof(f71205,plain,(
% 92.57/35.45 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 92.57/35.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f71204])).
% 92.57/35.45 fof(f71206,plain,(
% 92.57/35.45 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f71205])).
% 92.57/35.45 fof(f71207,plain,(
% 92.57/35.45 ![X0]: (X0=k1_xboole_0|r2_hidden(sK22_skl(X0),X0))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f71205])).
% 92.57/35.45 fof(f71331,plain,(
% 92.57/35.45 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 92.57/35.45 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 92.57/35.45 fof(f71332,plain,(
% 92.57/35.45 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f71331])).
% 92.57/35.45 fof(f72564,plain,(
% 92.57/35.45 ![A,B]: (~m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))|k5_setfam_1(A,B)=k3_tarski(B))),
% 92.57/35.45 inference(pre_NNF_transformation,[status(thm)],[f669])).
% 92.57/35.45 fof(f72565,plain,(
% 92.57/35.45 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1)))|k5_setfam_1(X1,X0)=k3_tarski(X0))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f72564])).
% 92.57/35.45 fof(f79724,plain,(
% 92.57/35.45 v1_xboole_0(k12_arytm_3)),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f3028])).
% 92.57/35.45 fof(f79726,plain,(
% 92.57/35.45 k12_arytm_3=k1_xboole_0),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f3029])).
% 92.57/35.45 fof(f85461,plain,(
% 92.57/35.45 np__0=k1_xboole_0),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f5328])).
% 92.57/35.45 fof(f336029,plain,(
% 92.57/35.45 (?[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)))))),
% 92.57/35.45 inference(pre_NNF_transformation,[status(thm)],[f71113])).
% 92.57/35.45 fof(f336030,plain,(
% 92.57/35.45 ?[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)))))),
% 92.57/35.45 inference(NNF_transformation,[status(thm)],[f336029])).
% 92.57/35.45 fof(f336031,plain,(
% 92.57/35.45 (m1_subset_1(sK23837_skl,k1_zfmisc_1(k1_zfmisc_1(sK23836_skl)))&((k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|(![C]: (~r2_hidden(C,sK23837_skl)|C=k1_xboole_0)))&(~k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|(r2_hidden(sK23838_skl,sK23837_skl)&~sK23838_skl=k1_xboole_0))))),
% 92.57/35.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK23836_skl,sK23837_skl,sK23838_skl]),skolemize(A,sK23836_skl),skolemize(B,sK23837_skl),skolemize(C,sK23838_skl)],[f336030])).
% 92.57/35.45 fof(f336032,plain,(
% 92.57/35.45 m1_subset_1(sK23837_skl,k1_zfmisc_1(k1_zfmisc_1(sK23836_skl)))),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f336031])).
% 92.57/35.45 fof(f336033,plain,(
% 92.57/35.45 ![X0]: (k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|~r2_hidden(X0,sK23837_skl)|X0=k1_xboole_0)),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f336031])).
% 92.57/35.45 fof(f336034,plain,(
% 92.57/35.45 ~k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|r2_hidden(sK23838_skl,sK23837_skl)),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f336031])).
% 92.57/35.45 fof(f336035,plain,(
% 92.57/35.45 ~k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|~sK23838_skl=k1_xboole_0),
% 92.57/35.45 inference(cnf_transformation,[status(thm)],[f336031])).
% 92.57/35.45 fof(f366805,plain,(
% 92.57/35.45 ![X0,X1,X2]: (r2_hidden(X0,k3_tarski(X1))|~r2_hidden(X0,X2)|~r2_hidden(X2,X1))),
% 92.57/35.45 inference(destructive_equality_resolution,[status(thm)],[f71149])).
% 92.57/35.45 fof(f366808,plain,(
% 92.57/35.45 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 92.57/35.45 inference(destructive_equality_resolution,[status(thm)],[f71206])).
% 92.57/35.45 fof(f387214,plain,(
% 92.57/35.45 ![X0]: (~r2_hidden(X0,np__0))),
% 92.57/35.45 inference(backward_demodulation,[status(thm)],[f85461,f366808])).
% 92.57/35.45 fof(f387218,plain,(
% 92.57/35.45 ![X0]: (k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|~r2_hidden(X0,sK23837_skl)|X0=np__0)),
% 92.57/35.45 inference(backward_demodulation,[status(thm)],[f85461,f336033])).
% 92.57/35.45 fof(f387219,plain,(
% 92.57/35.45 ~k5_setfam_1(sK23836_skl,sK23837_skl)=np__0|r2_hidden(sK23838_skl,sK23837_skl)),
% 92.57/35.45 inference(backward_demodulation,[status(thm)],[f85461,f336034])).
% 92.57/35.45 fof(f387220,plain,(
% 92.57/35.45 ~k5_setfam_1(sK23836_skl,sK23837_skl)=k1_xboole_0|~sK23838_skl=np__0),
% 92.57/35.45 inference(backward_demodulation,[status(thm)],[f85461,f336035])).
% 92.57/35.45 fof(f387230,plain,(
% 92.57/35.45 ![X0]: (k5_setfam_1(sK23836_skl,sK23837_skl)=np__0|~r2_hidden(X0,sK23837_skl)|X0=np__0)),
% 92.57/35.45 inference(forward_demodulation,[status(thm)],[f85461,f387218])).
% 92.57/35.45 fof(f387231,plain,(
% 92.57/35.45 ~k5_setfam_1(sK23836_skl,sK23837_skl)=np__0|~sK23838_skl=np__0),
% 92.57/35.45 inference(forward_demodulation,[status(thm)],[f85461,f387220])).
% 92.57/35.45 fof(f387236,plain,(
% 92.57/35.45 ![X0]: (~v1_xboole_0(X0)|X0=np__0)),
% 92.57/35.45 inference(forward_demodulation,[status(thm)],[f85461,f71332])).
% 53.50/36.94 fof(f387563,plain,(
% 53.50/36.94 ![X0]: (X0=k3_tarski(sK23837_skl)|r2_hidden(sK5_skl(X0,sK23837_skl),X0)|k5_setfam_1(sK23836_skl,sK23837_skl)=np__0|sK6_skl(X0,sK23837_skl)=np__0)),
% 53.50/36.94 inference(resolution,[status(thm)],[f71152,f387230])).
% 53.50/36.94 fof(f387708,plain,(
% 53.50/36.94 k5_setfam_1(sK23836_skl,sK23837_skl)=k3_tarski(sK23837_skl)),
% 53.50/36.94 inference(resolution,[status(thm)],[f72565,f336032])).
% 53.50/36.94 fof(f387731,plain,(
% 53.50/36.94 ~k3_tarski(sK23837_skl)=np__0|r2_hidden(sK23838_skl,sK23837_skl)),
% 53.50/36.94 inference(backward_demodulation,[status(thm)],[f387708,f387219])).
% 53.50/36.94 fof(f387732,plain,(
% 53.50/36.94 ~k3_tarski(sK23837_skl)=np__0|~sK23838_skl=np__0),
% 53.50/36.94 inference(backward_demodulation,[status(thm)],[f387708,f387231])).
% 53.50/36.94 fof(f387820,plain,(
% 53.50/36.94 ![X0]: (X0=k3_tarski(sK23837_skl)|r2_hidden(sK5_skl(X0,sK23837_skl),X0)|k3_tarski(sK23837_skl)=np__0|sK6_skl(X0,sK23837_skl)=np__0)),
% 53.50/36.94 inference(forward_demodulation,[status(thm)],[f387708,f387563])).
% 53.50/36.94 fof(f387824,plain,(
% 53.50/36.94 np__0=k3_tarski(sK23837_skl)|k3_tarski(sK23837_skl)=np__0|sK6_skl(np__0,sK23837_skl)=np__0),
% 53.50/36.94 inference(resolution,[status(thm)],[f387820,f387214])).
% 53.50/36.94 fof(f387839,plain,(
% 53.50/36.94 np__0=k3_tarski(sK23837_skl)|sK6_skl(np__0,sK23837_skl)=np__0),
% 53.50/36.94 inference(duplicate_literals_removal,[status(thm)],[f387824])).
% 53.50/36.94 fof(f388019,plain,(
% 53.50/36.94 np__0=k3_tarski(sK23837_skl)|r2_hidden(sK5_skl(np__0,sK23837_skl),np__0)|r2_hidden(sK5_skl(np__0,sK23837_skl),np__0)|np__0=k3_tarski(sK23837_skl)),
% 53.50/36.94 inference(paramodulation,[status(thm)],[f387839,f71151])).
% 53.50/36.94 fof(f388022,plain,(
% 53.50/36.94 np__0=k3_tarski(sK23837_skl)|r2_hidden(sK5_skl(np__0,sK23837_skl),np__0)),
% 53.50/36.94 inference(duplicate_literals_removal,[status(thm)],[f388019])).
% 53.50/36.94 fof(f388023,plain,(
% 53.50/36.94 np__0=k3_tarski(sK23837_skl)),
% 53.50/36.94 inference(forward_subsumption_resolution,[status(thm)],[f388022,f387214])).
% 53.50/36.94 fof(f388029,plain,(
% 53.50/36.94 ~np__0=np__0|r2_hidden(sK23838_skl,sK23837_skl)),
% 53.50/36.94 inference(backward_demodulation,[status(thm)],[f388023,f387731])).
% 53.50/36.94 fof(f388031,plain,(
% 53.50/36.94 ~np__0=np__0|~sK23838_skl=np__0),
% 53.50/36.94 inference(backward_demodulation,[status(thm)],[f388023,f387732])).
% 53.50/36.94 fof(f388035,plain,(
% 53.50/36.94 r2_hidden(sK23838_skl,sK23837_skl)),
% 53.50/36.94 inference(trivial_equality_resolution,[status(thm)],[f388029])).
% 53.50/36.94 fof(f388036,plain,(
% 53.50/36.94 ~sK23838_skl=np__0),
% 53.50/36.94 inference(trivial_equality_resolution,[status(thm)],[f388031])).
% 53.50/36.94 fof(f388049,plain,(
% 53.50/36.94 ![X0]: (r2_hidden(X0,k3_tarski(sK23837_skl))|~r2_hidden(X0,sK23838_skl))),
% 53.50/36.94 inference(resolution,[status(thm)],[f388035,f366805])).
% 53.50/36.94 fof(f388054,plain,(
% 53.50/36.94 ![X0]: (r2_hidden(X0,np__0)|~r2_hidden(X0,sK23838_skl))),
% 53.50/36.94 inference(forward_demodulation,[status(thm)],[f388023,f388049])).
% 53.50/36.94 fof(f388055,plain,(
% 53.50/36.94 ![X0]: (~r2_hidden(X0,sK23838_skl))),
% 53.50/36.94 inference(forward_subsumption_resolution,[status(thm)],[f388054,f387214])).
% 53.50/36.94 fof(f388430,plain,(
% 53.50/36.94 k12_arytm_3=np__0),
% 53.50/36.94 inference(resolution,[status(thm)],[f79724,f387236])).
% 53.50/36.94 fof(f388532,plain,(
% 53.50/36.94 ~sK23838_skl=k12_arytm_3),
% 53.50/36.94 inference(backward_demodulation,[status(thm)],[f388430,f388036])).
% 53.50/36.94 fof(f388624,plain,(
% 53.50/36.94 ![X0]: (X0=k12_arytm_3|r2_hidden(sK22_skl(X0),X0))),
% 53.50/36.94 inference(forward_demodulation,[status(thm)],[f79726,f71207])).
% 53.50/36.94 fof(f388628,plain,(
% 53.50/36.94 sK23838_skl=k12_arytm_3),
% 53.50/36.94 inference(resolution,[status(thm)],[f388624,f388055])).
% 53.50/36.94 fof(f388669,plain,(
% 53.50/36.94 $false),
% 53.50/36.94 inference(forward_subsumption_resolution,[status(thm)],[f388628,f388532])).
% 53.50/36.94 % SZS output end CNFRefutation for theBenchmark.p
% 17.90/37.27 % Elapsed time: 26.343451 seconds
% 17.90/37.27 % CPU time: 94.722867 seconds
% 17.90/37.27 % Total memory used: 21.785 GB
% 17.90/37.27 % Net memory used: 21.622 GB
%------------------------------------------------------------------------------