%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU430+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:20:35 PM UTC 2026
% Result : Theorem 123.01s 40.27s
% Output : CNFRefutation 66.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 6
% Syntax : Number of formulae : 56 ( 14 unt; 0 def)
% Number of atoms : 176 ( 75 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 188 ( 68 ~; 80 |; 28 &)
% ( 6 <=>; 5 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 92 ( 77 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [A,B] :
( B = k3_tarski(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
? [A] : v1_xboole_0(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f669,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> k5_setfam_1(A,B) = k3_tarski(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71112,conjecture,
! [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 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71113,negated_conjecture,
~ ! [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 ) ) ),
inference(negated_conjecture,[status(cth)],[f71112]) ).
fof(f71144,plain,
! [A,B] :
( ( ? [C] :
( ( ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) )
| r2_hidden(C,B) )
& ( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
| ~ r2_hidden(C,B) ) )
| B = k3_tarski(A) )
& ( ! [C] :
( ( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
| r2_hidden(C,B) )
& ( ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) )
| ~ r2_hidden(C,B) ) )
| B != k3_tarski(A) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f71145,plain,
( ! [A,B] :
( ? [C] :
( ( ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) )
| r2_hidden(C,B) )
& ( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
| ~ r2_hidden(C,B) ) )
| B = k3_tarski(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
| r2_hidden(C,B) )
& ! [C] :
( ? [D] :
( r2_hidden(D,A)
& r2_hidden(C,D) )
| ~ r2_hidden(C,B) ) )
| B != k3_tarski(A) ) ),
inference(miniscoping,[status(thm)],[f71144]) ).
fof(f71146,plain,
( ! [A,B] :
( ( ( ( r2_hidden(sK6_skl(B,A),A)
& r2_hidden(sK5_skl(B,A),sK6_skl(B,A)) )
| r2_hidden(sK5_skl(B,A),B) )
& ( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(sK5_skl(B,A),D) )
| ~ r2_hidden(sK5_skl(B,A),B) ) )
| B = k3_tarski(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ r2_hidden(D,A)
| ~ r2_hidden(C,D) )
| r2_hidden(C,B) )
& ! [C] :
( ( r2_hidden(sK4_skl(C,B,A),A)
& r2_hidden(C,sK4_skl(C,B,A)) )
| ~ r2_hidden(C,B) ) )
| B != k3_tarski(A) ) ),
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]) ).
fof(f71149,plain,
! [X0,X1,X2,X3] :
( ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X3)
| r2_hidden(X2,X0)
| X0 != k3_tarski(X1) ),
inference(cnf_transformation,[status(thm)],[f71146]) ).
fof(f71151,plain,
! [X0,X1] :
( r2_hidden(sK5_skl(X0,X1),sK6_skl(X0,X1))
| r2_hidden(sK5_skl(X0,X1),X0)
| X0 = k3_tarski(X1) ),
inference(cnf_transformation,[status(thm)],[f71146]) ).
fof(f71152,plain,
! [X0,X1] :
( r2_hidden(sK6_skl(X0,X1),X1)
| r2_hidden(sK5_skl(X0,X1),X0)
| X0 = k3_tarski(X1) ),
inference(cnf_transformation,[status(thm)],[f71146]) ).
fof(f71193,plain,
v1_xboole_0(sK20_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25]) ).
fof(f71194,plain,
v1_xboole_0(sK20_skl),
inference(cnf_transformation,[status(thm)],[f71193]) ).
fof(f71203,plain,
! [A] :
( ( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(NNF_transformation,[status(thm)],[f29]) ).
fof(f71204,plain,
( ! [A] :
( ? [B] : r2_hidden(B,A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(miniscoping,[status(thm)],[f71203]) ).
fof(f71205,plain,
( ! [A] :
( r2_hidden(sK22_skl(A),A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f71204]) ).
fof(f71206,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| X0 != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f71205]) ).
fof(f71207,plain,
! [X0] :
( r2_hidden(sK22_skl(X0),X0)
| X0 = k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f71205]) ).
fof(f71235,plain,
! [A] :
( ( A != k1_xboole_0
| v1_xboole_0(A) )
& ( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(NNF_transformation,[status(thm)],[f33]) ).
fof(f71236,plain,
( ! [A] :
( A != k1_xboole_0
| v1_xboole_0(A) )
& ! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(miniscoping,[status(thm)],[f71235]) ).
fof(f71237,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f71236]) ).
fof(f72564,plain,
! [A,B] :
( k5_setfam_1(A,B) = k3_tarski(B)
| ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f669]) ).
fof(f72565,plain,
! [X0,X1] :
( k5_setfam_1(X1,X0) = k3_tarski(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1))) ),
inference(cnf_transformation,[status(thm)],[f72564]) ).
fof(f336029,plain,
? [A,B] :
( ( k5_setfam_1(A,B) = k1_xboole_0
<~> ! [C] :
( C = k1_xboole_0
| ~ r2_hidden(C,B) ) )
& m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f71113]) ).
fof(f336030,plain,
? [A,B] :
( ( ? [C] :
( C != k1_xboole_0
& r2_hidden(C,B) )
| k5_setfam_1(A,B) != k1_xboole_0 )
& ( ! [C] :
( C = k1_xboole_0
| ~ r2_hidden(C,B) )
| k5_setfam_1(A,B) = k1_xboole_0 )
& m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ),
inference(NNF_transformation,[status(thm)],[f336029]) ).
fof(f336031,plain,
( ( ( sK23838_skl != k1_xboole_0
& r2_hidden(sK23838_skl,sK23837_skl) )
| k5_setfam_1(sK23836_skl,sK23837_skl) != k1_xboole_0 )
& ( ! [C] :
( C = k1_xboole_0
| ~ r2_hidden(C,sK23837_skl) )
| k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0 )
& m1_subset_1(sK23837_skl,k1_zfmisc_1(k1_zfmisc_1(sK23836_skl))) ),
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]) ).
fof(f336032,plain,
m1_subset_1(sK23837_skl,k1_zfmisc_1(k1_zfmisc_1(sK23836_skl))),
inference(cnf_transformation,[status(thm)],[f336031]) ).
fof(f336033,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ r2_hidden(X0,sK23837_skl)
| k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f336031]) ).
fof(f336034,plain,
( r2_hidden(sK23838_skl,sK23837_skl)
| k5_setfam_1(sK23836_skl,sK23837_skl) != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f336031]) ).
fof(f336035,plain,
( sK23838_skl != k1_xboole_0
| k5_setfam_1(sK23836_skl,sK23837_skl) != k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f336031]) ).
fof(f366805,plain,
! [X0,X1,X2] :
( ~ r2_hidden(X2,X1)
| ~ r2_hidden(X0,X2)
| r2_hidden(X0,k3_tarski(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f71149]) ).
fof(f366808,plain,
! [X0] : ~ r2_hidden(X0,k1_xboole_0),
inference(destructive_equality_resolution,[status(thm)],[f71206]) ).
fof(f387170,plain,
sK20_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f71237,f71194]) ).
fof(f387294,plain,
! [X0] :
( sK6_skl(X0,sK23837_skl) = k1_xboole_0
| k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0
| r2_hidden(sK5_skl(X0,sK23837_skl),X0)
| X0 = k3_tarski(sK23837_skl) ),
inference(resolution,[status(thm)],[f71152,f336033]) ).
fof(f387305,plain,
( sK6_skl(k1_xboole_0,sK23837_skl) = k1_xboole_0
| k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0
| k1_xboole_0 = k3_tarski(sK23837_skl) ),
inference(resolution,[status(thm)],[f387294,f366808]) ).
fof(f387358,plain,
( k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0
| k1_xboole_0 = k3_tarski(sK23837_skl)
| r2_hidden(sK5_skl(k1_xboole_0,sK23837_skl),k1_xboole_0)
| r2_hidden(sK5_skl(k1_xboole_0,sK23837_skl),k1_xboole_0)
| k1_xboole_0 = k3_tarski(sK23837_skl) ),
inference(paramodulation,[status(thm)],[f387305,f71151]) ).
fof(f387361,plain,
( k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0
| r2_hidden(sK5_skl(k1_xboole_0,sK23837_skl),k1_xboole_0)
| k1_xboole_0 = k3_tarski(sK23837_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f387358]) ).
fof(f387362,plain,
( k5_setfam_1(sK23836_skl,sK23837_skl) = k1_xboole_0
| k1_xboole_0 = k3_tarski(sK23837_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f387361,f366808]) ).
fof(f387394,plain,
k5_setfam_1(sK23836_skl,sK23837_skl) = k3_tarski(sK23837_skl),
inference(resolution,[status(thm)],[f72565,f336032]) ).
fof(f387399,plain,
( k3_tarski(sK23837_skl) = k1_xboole_0
| k1_xboole_0 = k3_tarski(sK23837_skl) ),
inference(backward_demodulation,[status(thm)],[f387394,f387362]) ).
fof(f387418,plain,
( r2_hidden(sK23838_skl,sK23837_skl)
| k3_tarski(sK23837_skl) != k1_xboole_0 ),
inference(backward_demodulation,[status(thm)],[f387394,f336034]) ).
fof(f387420,plain,
( sK23838_skl != k1_xboole_0
| k3_tarski(sK23837_skl) != k1_xboole_0 ),
inference(backward_demodulation,[status(thm)],[f387394,f336035]) ).
fof(f387421,plain,
k1_xboole_0 = k3_tarski(sK23837_skl),
inference(duplicate_literals_removal,[status(thm)],[f387399]) ).
fof(f387423,plain,
! [X0,X1] :
( ~ r2_hidden(X1,sK23837_skl)
| ~ r2_hidden(X0,X1)
| r2_hidden(X0,k1_xboole_0) ),
inference(paramodulation,[status(thm)],[f387421,f366805]) ).
fof(f387426,plain,
! [X0,X1] :
( ~ r2_hidden(X1,sK23837_skl)
| ~ r2_hidden(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f387423,f366808]) ).
fof(f387429,plain,
( r2_hidden(sK23838_skl,sK23837_skl)
| k1_xboole_0 != k1_xboole_0 ),
inference(forward_demodulation,[status(thm)],[f387421,f387418]) ).
fof(f387430,plain,
r2_hidden(sK23838_skl,sK23837_skl),
inference(trivial_equality_resolution,[status(thm)],[f387429]) ).
fof(f387622,plain,
! [X0] : ~ r2_hidden(X0,sK23838_skl),
inference(resolution,[status(thm)],[f387426,f387430]) ).
fof(f387634,plain,
( sK23838_skl != k1_xboole_0
| k1_xboole_0 != k1_xboole_0 ),
inference(forward_demodulation,[status(thm)],[f387421,f387420]) ).
fof(f387635,plain,
sK23838_skl != k1_xboole_0,
inference(trivial_equality_resolution,[status(thm)],[f387634]) ).
fof(f387785,plain,
sK23838_skl != sK20_skl,
inference(backward_demodulation,[status(thm)],[f387170,f387635]) ).
fof(f387827,plain,
! [X0] :
( r2_hidden(sK22_skl(X0),X0)
| X0 = sK20_skl ),
inference(forward_demodulation,[status(thm)],[f387170,f71207]) ).
fof(f387828,plain,
sK23838_skl = sK20_skl,
inference(resolution,[status(thm)],[f387827,f387622]) ).
fof(f387886,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f387828,f387785]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU430+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.36 % Computer : n001.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Mon Sep 21 06:34:47 UTC 2026
% 0.10/5.37 % CPUTime :
% 22.06/27.38 % Drodi V4.1.1
% 123.01/40.27 % Refutation found
% 123.01/40.27 % SZS status Theorem for theBenchmark: Theorem is valid
% 123.01/40.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 66.24/42.36 % Elapsed time: 36.237849 seconds
% 66.24/42.36 % CPU time: 126.021628 seconds
% 66.24/42.36 % Total memory used: 21.814 GB
% 66.24/42.36 % Net memory used: 21.647 GB
%------------------------------------------------------------------------------