%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT359+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 01:02:56 PM UTC 2026
% Result : Theorem 1.12s 0.62s
% Output : CNFRefutation 1.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 28
% Syntax : Number of formulae : 146 ( 10 unt; 14 def)
% Number of atoms : 445 ( 73 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 511 ( 212 ~; 215 |; 43 &)
% ( 21 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 15 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 185 ( 181 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B,C,D] :
~ ( ! [E] :
( m1_subset_1(E,u1_struct_0(A))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(A))
=> ~ ( m1_subset_1(D,k1_altcat_1(A,E,F))
& r2_hidden(D,k1_altcat_1(A,E,F))
& F = C
& E = B ) ) )
& r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l2_altcat_1(A)
& ~ v3_struct_0(A) )
=> ! [B,C,D] :
~ ( ! [E] :
( m1_subset_1(E,u1_struct_0(A))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(A))
=> ~ ( m1_subset_1(D,k1_altcat_1(A,E,F))
& r2_hidden(D,k1_altcat_1(A,E,F))
& F = C
& E = B ) ) )
& r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f19,axiom,
! [A] :
( ( v1_funct_1(A)
& v1_relat_1(A) )
=> ! [B,C] : k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( l1_altcat_1(A)
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> k1_altcat_1(A,B,C) = k1_binop_1(u1_altcat_1(A),B,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
=> ( m1_pboole(B,A)
<=> k1_relat_1(B) = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( ( v1_funct_1(A)
& v1_relat_1(A) )
=> ! [B,C] :
( ( ~ r2_hidden(B,k1_relat_1(A))
=> ( C = k1_funct_1(A,B)
<=> C = k1_xboole_0 ) )
& ( r2_hidden(B,k1_relat_1(A))
=> ( C = k1_funct_1(A,B)
<=> r2_hidden(k4_tarski(B,C),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( l2_altcat_1(A)
=> l1_altcat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B] :
( m1_pboole(B,A)
=> ( v1_funct_1(B)
& v1_relat_1(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( l1_altcat_1(A)
=> m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A,B,C,D] :
( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))
<=> ( r2_hidden(B,D)
& r2_hidden(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,plain,
? [A] :
( ? [B,C,D] :
( ! [E] :
( ! [F] :
( ~ m1_subset_1(D,k1_altcat_1(A,E,F))
| ~ r2_hidden(D,k1_altcat_1(A,E,F))
| F != C
| E != B
| ~ m1_subset_1(F,u1_struct_0(A)) )
| ~ m1_subset_1(E,u1_struct_0(A)) )
& r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C)) )
& l2_altcat_1(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f76,plain,
( ! [E] :
( ! [F] :
( ~ m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,E,F))
| ~ r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,E,F))
| F != sK2_skl
| E != sK1_skl
| ~ m1_subset_1(F,u1_struct_0(sK0_skl)) )
| ~ m1_subset_1(E,u1_struct_0(sK0_skl)) )
& r2_hidden(sK3_skl,k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,sK2_skl))
& l2_altcat_1(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f75]) ).
fof(f77,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
l2_altcat_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
r2_hidden(sK3_skl,k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,sK2_skl)),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f80,plain,
! [X0,X1] :
( ~ m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,X0,X1))
| ~ r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,X0,X1))
| X1 != sK2_skl
| X0 != sK1_skl
| ~ m1_subset_1(X1,u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f128,plain,
! [A] :
( ! [B,C] : k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C))
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f129,plain,
! [X0,X1,X2] :
( k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [A] :
( ! [B] :
( ! [C] :
( k1_altcat_1(A,B,C) = k1_binop_1(u1_altcat_1(A),B,C)
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_altcat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f131,plain,
! [X0,X1,X2] :
( k1_altcat_1(X0,X1,X2) = k1_binop_1(u1_altcat_1(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [A,B] :
( ( m1_pboole(B,A)
<=> k1_relat_1(B) = A )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f133,plain,
! [A,B] :
( ( ( k1_relat_1(B) != A
| m1_pboole(B,A) )
& ( k1_relat_1(B) = A
| ~ m1_pboole(B,A) ) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(NNF_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
! [B] :
( ( ! [A] :
( k1_relat_1(B) != A
| m1_pboole(B,A) )
& ! [A] :
( k1_relat_1(B) = A
| ~ m1_pboole(B,A) ) )
| ~ v1_funct_1(B)
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( k1_relat_1(X0) = X1
| ~ m1_pboole(X0,X1)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
! [A] :
( ! [B,C] :
( ( ( C = k1_funct_1(A,B)
<=> C = k1_xboole_0 )
| r2_hidden(B,k1_relat_1(A)) )
& ( ( C = k1_funct_1(A,B)
<=> r2_hidden(k4_tarski(B,C),A) )
| ~ r2_hidden(B,k1_relat_1(A)) ) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f138,plain,
! [A] :
( ! [B,C] :
( ( ( ( C != k1_xboole_0
| C = k1_funct_1(A,B) )
& ( C = k1_xboole_0
| C != k1_funct_1(A,B) ) )
| r2_hidden(B,k1_relat_1(A)) )
& ( ( ( ~ r2_hidden(k4_tarski(B,C),A)
| C = k1_funct_1(A,B) )
& ( r2_hidden(k4_tarski(B,C),A)
| C != k1_funct_1(A,B) ) )
| ~ r2_hidden(B,k1_relat_1(A)) ) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(NNF_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [A] :
( ( ! [B] :
( ( ! [C] :
( C != k1_xboole_0
| C = k1_funct_1(A,B) )
& ! [C] :
( C = k1_xboole_0
| C != k1_funct_1(A,B) ) )
| r2_hidden(B,k1_relat_1(A)) )
& ! [B] :
( ( ! [C] :
( ~ r2_hidden(k4_tarski(B,C),A)
| C = k1_funct_1(A,B) )
& ! [C] :
( r2_hidden(k4_tarski(B,C),A)
| C != k1_funct_1(A,B) ) )
| ~ r2_hidden(B,k1_relat_1(A)) ) )
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f142,plain,
! [X0,X1,X2] :
( X2 = k1_xboole_0
| X2 != k1_funct_1(X0,X1)
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f147,plain,
! [A] :
( l1_altcat_1(A)
| ~ l2_altcat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f148,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [A,B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
| ~ m1_pboole(B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f150,plain,
! [B] :
( ( v1_funct_1(B)
& v1_relat_1(B) )
| ! [A] : ~ m1_pboole(B,A) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( v1_relat_1(X0)
| ~ m1_pboole(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [X0,X1] :
( v1_funct_1(X0)
| ~ m1_pboole(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f153,plain,
! [A] :
( m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)))
| ~ l1_altcat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f154,plain,
! [X0] :
( m1_pboole(u1_altcat_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f212,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f254,plain,
! [A,B,C,D] :
( ( ~ r2_hidden(B,D)
| ~ r2_hidden(A,C)
| r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) )
& ( ( r2_hidden(B,D)
& r2_hidden(A,C) )
| ~ r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) ) ),
inference(NNF_transformation,[status(thm)],[f69]) ).
fof(f255,plain,
( ! [A,B,C,D] :
( ~ r2_hidden(B,D)
| ~ r2_hidden(A,C)
| r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) )
& ! [A,B,C,D] :
( ( r2_hidden(B,D)
& r2_hidden(A,C) )
| ~ r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) ) ),
inference(miniscoping,[status(thm)],[f254]) ).
fof(f256,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X0,X2)
| ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f257,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X1,X3)
| ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f259,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f70]) ).
fof(f260,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f261,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f262,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f263,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f72]) ).
fof(f264,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f265,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f266,plain,
! [B] :
( ~ v1_xboole_0(B)
| ! [A] : ~ r2_hidden(A,B) ),
inference(miniscoping,[status(thm)],[f265]) ).
fof(f267,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f271,plain,
( ~ m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))
| ~ r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(destructive_equality_resolution,[status(thm)],[f80]) ).
fof(f274,plain,
! [X0,X1] :
( k1_funct_1(X0,X1) = k1_xboole_0
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f142]) ).
fof(f277,plain,
( ~ r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f271,f260]) ).
fof(f278,definition,
( sQ0_spl
<=> m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f279,plain,
( ~ sQ0_spl
| m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f278]) ).
fof(f280,plain,
( sQ0_spl
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f278]) ).
fof(f281,definition,
( sQ1_spl
<=> m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( ~ sQ1_spl
| m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f283,plain,
( sQ1_spl
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f284,definition,
( sQ2_spl
<=> r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( sQ2_spl
| ~ r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f277,f278,f281,f284]) ).
fof(f290,plain,
( sQ2_spl
| v1_xboole_0(k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))
| ~ m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f286,f262]) ).
fof(f291,definition,
( sQ3_spl
<=> m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ3_spl
| ~ m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f294,definition,
( sQ4_spl
<=> v1_xboole_0(k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f295,plain,
( ~ sQ4_spl
| v1_xboole_0(k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f294]) ).
fof(f297,plain,
( sQ2_spl
| sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f290,f291,f294,f284]) ).
fof(f298,plain,
( sQ1_spl
| ~ r2_hidden(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f283,f260]) ).
fof(f299,plain,
! [X0,X1,X2] :
( ~ l2_altcat_1(X1)
| k1_altcat_1(X1,X0,X2) = k1_binop_1(u1_altcat_1(X1),X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(resolution,[status(thm)],[f131,f148]) ).
fof(f301,plain,
! [X0] : ~ r2_hidden(X0,k1_xboole_0),
inference(resolution,[status(thm)],[f212,f267]) ).
fof(f313,plain,
( sQ3_spl
| ~ r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f293,f260]) ).
fof(f417,plain,
( ~ sQ4_spl
| k1_altcat_1(sK0_skl,sK1_skl,sK2_skl) = k1_xboole_0 ),
inference(resolution,[status(thm)],[f264,f295]) ).
fof(f443,plain,
! [X0,X1,X2,X3] :
( k1_binop_1(X0,X2,X3) = k1_funct_1(X0,k4_tarski(X2,X3))
| ~ v1_relat_1(X0)
| ~ m1_pboole(X0,X1) ),
inference(resolution,[status(thm)],[f152,f129]) ).
fof(f444,plain,
! [X0,X1,X2,X3] :
( k1_binop_1(X0,X2,X3) = k1_funct_1(X0,k4_tarski(X2,X3))
| ~ m1_pboole(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f443,f151]) ).
fof(f454,plain,
! [X0,X1] :
( k1_relat_1(X0) = X1
| ~ m1_pboole(X0,X1)
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f151]) ).
fof(f456,plain,
! [X0] :
( ~ l1_altcat_1(X0)
| k1_relat_1(u1_altcat_1(X0)) = k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(u1_altcat_1(X0)) ),
inference(resolution,[status(thm)],[f454,f154]) ).
fof(f466,plain,
! [X0,X1,X2] :
( ~ l1_altcat_1(X0)
| k1_binop_1(u1_altcat_1(X0),X1,X2) = k1_funct_1(u1_altcat_1(X0),k4_tarski(X1,X2)) ),
inference(resolution,[status(thm)],[f444,f154]) ).
fof(f469,plain,
! [X0,X1,X2] :
( ~ l2_altcat_1(X0)
| k1_binop_1(u1_altcat_1(X0),X1,X2) = k1_funct_1(u1_altcat_1(X0),k4_tarski(X1,X2)) ),
inference(resolution,[status(thm)],[f466,f148]) ).
fof(f471,plain,
! [X0,X1] : k1_binop_1(u1_altcat_1(sK0_skl),X0,X1) = k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1)),
inference(resolution,[status(thm)],[f469,f78]) ).
fof(f587,definition,
( sQ39_spl
<=> k1_relat_1(u1_altcat_1(sK0_skl)) = k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( ~ sQ39_spl
| k1_relat_1(u1_altcat_1(sK0_skl)) = k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f587]) ).
fof(f596,definition,
( sQ41_spl
<=> v1_relat_1(u1_altcat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( sQ41_spl
| ~ v1_relat_1(u1_altcat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f599,definition,
( sQ42_spl
<=> v1_funct_1(u1_altcat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( ~ sQ42_spl
| v1_funct_1(u1_altcat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f601,plain,
( sQ42_spl
| ~ v1_funct_1(u1_altcat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f603,plain,
! [X0] :
( sQ42_spl
| ~ m1_pboole(u1_altcat_1(sK0_skl),X0) ),
inference(resolution,[status(thm)],[f601,f152]) ).
fof(f606,definition,
( sQ43_spl
<=> l1_altcat_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( sQ43_spl
| ~ l1_altcat_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f606]) ).
fof(f613,plain,
( sQ43_spl
| ~ l2_altcat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f608,f148]) ).
fof(f614,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f613,f78]) ).
fof(f615,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f614]) ).
fof(f620,plain,
! [X0] :
( sQ41_spl
| ~ m1_pboole(u1_altcat_1(sK0_skl),X0) ),
inference(resolution,[status(thm)],[f598,f151]) ).
fof(f673,plain,
( sQ42_spl
| ~ l1_altcat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f603,f154]) ).
fof(f675,plain,
( sQ42_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f673,f606,f599]) ).
fof(f677,plain,
( ~ sQ42_spl
| ~ l1_altcat_1(sK0_skl)
| k1_relat_1(u1_altcat_1(sK0_skl)) = k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f600,f456]) ).
fof(f679,plain,
( ~ sQ42_spl
| ~ sQ43_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f677,f587,f606,f599]) ).
fof(f684,plain,
( sQ41_spl
| ~ l1_altcat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f620,f154]) ).
fof(f686,plain,
( sQ41_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f684,f606,f596]) ).
fof(f922,plain,
! [X0,X1] :
( ~ sQ39_spl
| r2_hidden(X0,u1_struct_0(sK0_skl))
| ~ r2_hidden(k4_tarski(X0,X1),k1_relat_1(u1_altcat_1(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f588,f256]) ).
fof(f926,plain,
! [X0,X1] :
( ~ sQ39_spl
| r2_hidden(X1,u1_struct_0(sK0_skl))
| ~ r2_hidden(k4_tarski(X0,X1),k1_relat_1(u1_altcat_1(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f588,f257]) ).
fof(f931,plain,
! [X0,X1] :
( ~ sQ39_spl
| k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1)) = k1_xboole_0
| ~ v1_funct_1(u1_altcat_1(sK0_skl))
| ~ v1_relat_1(u1_altcat_1(sK0_skl))
| r2_hidden(X0,u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f922,f274]) ).
fof(f933,definition,
! [X0,X1] :
( sQ82_spl
<=> ( k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1)) = k1_xboole_0
| r2_hidden(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f934,plain,
! [X0,X1] :
( ~ sQ82_spl
| k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1)) = k1_xboole_0
| r2_hidden(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f933]) ).
fof(f936,plain,
( ~ sQ39_spl
| ~ sQ42_spl
| ~ sQ41_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f931,f933,f596,f599,f587]) ).
fof(f944,plain,
! [X0,X1] :
( ~ sQ82_spl
| k1_binop_1(u1_altcat_1(sK0_skl),X0,X1) = k1_xboole_0
| r2_hidden(X0,u1_struct_0(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f471,f934]) ).
fof(f1535,definition,
( sQ142_spl
<=> l2_altcat_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1537,plain,
( sQ142_spl
| ~ l2_altcat_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f1535]) ).
fof(f1539,plain,
( sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1537,f78]) ).
fof(f1540,plain,
sQ142_spl,
inference(contradiction_clause,[status(thm)],[f1539]) ).
fof(f1717,plain,
! [X0,X1] :
( ~ sQ39_spl
| k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X1,X0)) = k1_xboole_0
| ~ v1_funct_1(u1_altcat_1(sK0_skl))
| ~ v1_relat_1(u1_altcat_1(sK0_skl))
| r2_hidden(X0,u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f926,f274]) ).
fof(f1719,definition,
! [X0,X1] :
( sQ154_spl
<=> ( k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X1,X0)) = k1_xboole_0
| r2_hidden(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1720,plain,
! [X0,X1] :
( ~ sQ154_spl
| k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X1,X0)) = k1_xboole_0
| r2_hidden(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1719]) ).
fof(f1722,plain,
( ~ sQ39_spl
| ~ sQ42_spl
| ~ sQ41_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f1717,f1719,f596,f599,f587]) ).
fof(f1724,plain,
! [X0,X1] :
( ~ sQ154_spl
| k1_binop_1(u1_altcat_1(sK0_skl),X1,X0) = k1_xboole_0
| r2_hidden(X0,u1_struct_0(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f471,f1720]) ).
fof(f1728,plain,
! [X0] :
( sQ1_spl
| ~ sQ154_spl
| k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl) = k1_xboole_0 ),
inference(resolution,[status(thm)],[f1724,f298]) ).
fof(f1786,plain,
( sQ1_spl
| ~ sQ154_spl
| r2_hidden(sK3_skl,k1_xboole_0) ),
inference(backward_demodulation,[status(thm)],[f1728,f79]) ).
fof(f1794,plain,
( sQ1_spl
| ~ sQ154_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1786,f301]) ).
fof(f1795,plain,
( sQ1_spl
| ~ sQ154_spl ),
inference(contradiction_clause,[status(thm)],[f1794]) ).
fof(f1796,plain,
( sQ0_spl
| ~ r2_hidden(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f280,f260]) ).
fof(f1797,plain,
! [X0] :
( ~ sQ1_spl
| ~ l2_altcat_1(sK0_skl)
| k1_altcat_1(sK0_skl,X0,sK2_skl) = k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f282,f299]) ).
fof(f1800,definition,
! [X0] :
( sQ164_spl
<=> ( k1_altcat_1(sK0_skl,X0,sK2_skl) = k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1801,plain,
! [X0] :
( ~ sQ164_spl
| k1_altcat_1(sK0_skl,X0,sK2_skl) = k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1800]) ).
fof(f1803,plain,
( ~ sQ1_spl
| ~ sQ142_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f1797,f1800,f1535,f281]) ).
fof(f1819,definition,
( sQ167_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f1820,plain,
( ~ sQ167_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1819]) ).
fof(f1826,plain,
( ~ sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1820,f77]) ).
fof(f1827,plain,
~ sQ167_spl,
inference(contradiction_clause,[status(thm)],[f1826]) ).
fof(f1842,plain,
! [X0] :
( ~ sQ82_spl
| sQ0_spl
| k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,X0) = k1_xboole_0 ),
inference(resolution,[status(thm)],[f1796,f944]) ).
fof(f2182,plain,
( ~ sQ82_spl
| sQ0_spl
| r2_hidden(sK3_skl,k1_xboole_0) ),
inference(backward_demodulation,[status(thm)],[f1842,f79]) ).
fof(f2187,plain,
( ~ sQ82_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2182,f301]) ).
fof(f2188,plain,
( ~ sQ82_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f2187]) ).
fof(f2786,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| k1_altcat_1(sK0_skl,sK1_skl,sK2_skl) = k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1801,f279]) ).
fof(f2794,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f2786,f79]) ).
fof(f2798,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2794,f313]) ).
fof(f2799,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f2798]) ).
fof(f2809,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| ~ sQ4_spl
| r2_hidden(sK3_skl,k1_xboole_0) ),
inference(forward_demodulation,[status(thm)],[f417,f2794]) ).
fof(f2810,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2809,f301]) ).
fof(f2811,plain,
( ~ sQ0_spl
| ~ sQ164_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f2810]) ).
fof(f2812,plain,
$false,
inference(sat_refutation,[status(thm)],[f287,f297,f615,f675,f679,f686,f936,f1540,f1722,f1795,f1803,f1827,f2188,f2799,f2811]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT359+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 23:49:12 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.14/0.36 % Drodi V4.1.1
% 1.12/0.62 % Refutation found
% 1.12/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.12/0.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.12/0.63 % Elapsed time: 0.277926 seconds
% 1.12/0.63 % CPU time: 1.864626 seconds
% 1.12/0.63 % Total memory used: 146.476 MB
% 1.12/0.63 % Net memory used: 143.999 MB
%------------------------------------------------------------------------------