%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU411+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 : n013.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:28 PM UTC 2026
% Result : Theorem 2.25s 0.76s
% Output : CNFRefutation 2.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 20
% Syntax : Number of formulae : 94 ( 21 unt; 11 def)
% Number of atoms : 375 ( 23 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 439 ( 158 ~; 150 |; 100 &)
% ( 16 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 12 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 114 ( 106 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ( ( m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ( ( m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( v12_waybel_0(B,A)
<=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r1_orders_2(A,D,C)
& r2_hidden(C,B) )
=> r2_hidden(D,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B,C] :
( C = k3_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,B)
& r2_hidden(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] :
( l1_orders_2(A)
=> m1_subset_1(k3_yellow_0(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B] : k3_xboole_0(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( ( l1_orders_2(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> r1_orders_2(A,k3_yellow_0(A),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k3_yellow_0(B),u1_struct_0(A))
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
& l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
& l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f42,plain,
( ~ r2_hidden(k3_yellow_0(sK1_skl),u1_struct_0(sK0_skl))
& m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl)
& v1_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
& l1_orders_2(sK1_skl)
& v1_lattice3(sK1_skl)
& v1_yellow_0(sK1_skl)
& v4_orders_2(sK1_skl)
& v3_orders_2(sK1_skl)
& v2_orders_2(sK1_skl)
& ~ v3_struct_0(sK1_skl)
& l1_orders_2(sK0_skl)
& v1_lattice3(sK0_skl)
& v1_yellow_0(sK0_skl)
& v4_orders_2(sK0_skl)
& v3_orders_2(sK0_skl)
& v2_orders_2(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f41]) ).
fof(f50,plain,
~ v3_struct_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f53,plain,
v4_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f54,plain,
v1_yellow_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f56,plain,
l1_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f57,plain,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f59,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f60,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl))),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f61,plain,
~ r2_hidden(k3_yellow_0(sK1_skl),u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f65,plain,
! [A] :
( ! [B] :
( ( v12_waybel_0(B,A)
<=> ! [C] :
( ! [D] :
( r2_hidden(D,B)
| ~ r1_orders_2(A,D,C)
| ~ r2_hidden(C,B)
| ~ m1_subset_1(D,u1_struct_0(A)) )
| ~ m1_subset_1(C,u1_struct_0(A)) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f66,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ? [D] :
( ~ r2_hidden(D,B)
& r1_orders_2(A,D,C)
& r2_hidden(C,B)
& m1_subset_1(D,u1_struct_0(A)) )
& m1_subset_1(C,u1_struct_0(A)) )
| v12_waybel_0(B,A) )
& ( ! [C] :
( ! [D] :
( r2_hidden(D,B)
| ~ r1_orders_2(A,D,C)
| ~ r2_hidden(C,B)
| ~ m1_subset_1(D,u1_struct_0(A)) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ v12_waybel_0(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_orders_2(A) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [A] :
( ! [B] :
( ( ( ( ~ r2_hidden(sK3_skl(B,A),B)
& r1_orders_2(A,sK3_skl(B,A),sK2_skl(B,A))
& r2_hidden(sK2_skl(B,A),B)
& m1_subset_1(sK3_skl(B,A),u1_struct_0(A))
& m1_subset_1(sK2_skl(B,A),u1_struct_0(A)) )
| v12_waybel_0(B,A) )
& ( ! [C] :
( ! [D] :
( r2_hidden(D,B)
| ~ r1_orders_2(A,D,C)
| ~ r2_hidden(C,B)
| ~ m1_subset_1(D,u1_struct_0(A)) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ v12_waybel_0(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l1_orders_2(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f66]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X3,X1)
| ~ r1_orders_2(X0,X3,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ v12_waybel_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f74,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)],[f6]) ).
fof(f75,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)],[f74]) ).
fof(f76,plain,
( ! [A] :
( r2_hidden(sK4_skl(A),A)
| A = k1_xboole_0 )
& ! [A] :
( ! [B] : ~ r2_hidden(B,A)
| A != k1_xboole_0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f75]) ).
fof(f78,plain,
! [X0] :
( r2_hidden(sK4_skl(X0),X0)
| X0 = k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| r2_hidden(D,C) )
& ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| ~ r2_hidden(D,C) ) )
| C = k3_xboole_0(A,B) )
& ( ! [D] :
( ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C) )
& ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| ~ r2_hidden(D,C) ) )
| C != k3_xboole_0(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f80,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| r2_hidden(D,C) )
& ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| ~ r2_hidden(D,C) ) )
| C = k3_xboole_0(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C) )
& ! [D] :
( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| ~ r2_hidden(D,C) ) )
| C != k3_xboole_0(A,B) ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f81,plain,
( ! [A,B,C] :
( ( ( ( r2_hidden(sK5_skl(C,B,A),B)
& r2_hidden(sK5_skl(C,B,A),A) )
| r2_hidden(sK5_skl(C,B,A),C) )
& ( ~ r2_hidden(sK5_skl(C,B,A),B)
| ~ r2_hidden(sK5_skl(C,B,A),A)
| ~ r2_hidden(sK5_skl(C,B,A),C) ) )
| C = k3_xboole_0(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C) )
& ! [D] :
( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| ~ r2_hidden(D,C) ) )
| C != k3_xboole_0(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(D,sK5_skl(C,B,A))],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0)
| X0 != k3_xboole_0(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f88,plain,
! [A] :
( m1_subset_1(k3_yellow_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f89,plain,
! [X0] :
( m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f100,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f101,plain,
! [A] : k3_xboole_0(A,A) = A,
inference(miniscoping,[status(thm)],[f21]) ).
fof(f102,plain,
! [X0] : k3_xboole_0(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f140,plain,
! [A] :
( ! [B] :
( r1_orders_2(A,k3_yellow_0(A),B)
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l1_orders_2(A)
| ~ v1_yellow_0(A)
| ~ v4_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f141,plain,
! [X0,X1] :
( r1_orders_2(X0,k3_yellow_0(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ v4_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f142,plain,
! [A,B,C] :
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f143,plain,
! [A,C] :
( m1_subset_1(A,C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f142]) ).
fof(f144,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f162,plain,
! [X0,X1,X2] :
( r2_hidden(X0,X1)
| ~ r2_hidden(X0,k3_xboole_0(k3_xboole_0(X1,X2),k3_xboole_0(X1,X2))) ),
inference(resolution,[status(thm)],[f82,f102]) ).
fof(f169,plain,
! [X0,X1,X2] :
( r2_hidden(X0,X1)
| ~ r2_hidden(X0,k3_xboole_0(X1,X2)) ),
inference(forward_demodulation,[status(thm)],[f102,f162]) ).
fof(f180,plain,
! [X0,X1] :
( r2_hidden(X1,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X1,X0)
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ m1_subset_1(X1,u1_struct_0(sK1_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f68,f60]) ).
fof(f181,definition,
( sQ0_spl
<=> l1_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( sQ0_spl
| ~ l1_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f184,definition,
( sQ1_spl
<=> v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f186,plain,
( sQ1_spl
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl) ),
inference(component_clause,[status(thm)],[f184]) ).
fof(f187,definition,
! [X0,X1] :
( sQ2_spl
<=> ( r2_hidden(X1,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X1,X0)
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ m1_subset_1(X1,u1_struct_0(sK1_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f188,plain,
! [X0,X1] :
( ~ sQ2_spl
| r2_hidden(X1,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X1,X0)
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ m1_subset_1(X1,u1_struct_0(sK1_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f187]) ).
fof(f190,plain,
( sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f180,f181,f184,f187]) ).
fof(f201,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f186,f59]) ).
fof(f202,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f201]) ).
fof(f203,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f56]) ).
fof(f204,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f203]) ).
fof(f259,definition,
( sQ8_spl
<=> k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( ~ sQ8_spl
| k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) = k1_xboole_0 ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f262,definition,
( sQ9_spl
<=> m1_subset_1(sK4_skl(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f290,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sK1_skl))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))) ),
inference(resolution,[status(thm)],[f144,f60]) ).
fof(f333,plain,
( k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) = k1_xboole_0
| m1_subset_1(sK4_skl(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f290,f78]) ).
fof(f336,plain,
( sQ8_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f333,f262,f259]) ).
fof(f356,plain,
! [X0,X1] :
( ~ sQ2_spl
| r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X0,X1)
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f188,f290]) ).
fof(f423,plain,
( ~ sQ8_spl
| ~ v1_xboole_0(k1_xboole_0) ),
inference(backward_demodulation,[status(thm)],[f260,f57]) ).
fof(f432,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f423,f100]) ).
fof(f433,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f432]) ).
fof(f508,plain,
! [X0] :
( ~ sQ2_spl
| k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) = k1_xboole_0
| r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X0,sK4_skl(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f356,f78]) ).
fof(f511,definition,
! [X0] :
( sQ27_spl
<=> ( r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X0,sK4_skl(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f512,plain,
! [X0] :
( ~ sQ27_spl
| r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r1_orders_2(sK1_skl,X0,sK4_skl(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))))
| ~ m1_subset_1(X0,u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f511]) ).
fof(f514,plain,
( ~ sQ2_spl
| sQ8_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f508,f511,f259,f187]) ).
fof(f687,definition,
( sQ32_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( ~ sQ32_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f707,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f50]) ).
fof(f708,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f707]) ).
fof(f1483,definition,
( sQ62_spl
<=> m1_subset_1(k3_yellow_0(sK1_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1485,plain,
( sQ62_spl
| ~ m1_subset_1(k3_yellow_0(sK1_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1483]) ).
fof(f1520,plain,
( sQ62_spl
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1485,f89]) ).
fof(f1521,plain,
( sQ62_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1520,f181,f1483]) ).
fof(f1737,definition,
( sQ82_spl
<=> r2_hidden(k3_yellow_0(sK1_skl),k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1738,plain,
( ~ sQ82_spl
| r2_hidden(k3_yellow_0(sK1_skl),k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))) ),
inference(component_clause,[status(thm)],[f1737]) ).
fof(f1743,definition,
( sQ84_spl
<=> v4_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1745,plain,
( sQ84_spl
| ~ v4_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1743]) ).
fof(f1746,definition,
( sQ85_spl
<=> v1_yellow_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1748,plain,
( sQ85_spl
| ~ v1_yellow_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f1746]) ).
fof(f1756,plain,
( sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1748,f54]) ).
fof(f1757,plain,
sQ85_spl,
inference(contradiction_clause,[status(thm)],[f1756]) ).
fof(f1758,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1745,f53]) ).
fof(f1759,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f1758]) ).
fof(f2242,plain,
( ~ sQ27_spl
| ~ m1_subset_1(sK4_skl(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ v1_yellow_0(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| v3_struct_0(sK1_skl)
| r2_hidden(k3_yellow_0(sK1_skl),k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ m1_subset_1(k3_yellow_0(sK1_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f512,f141]) ).
fof(f2249,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| ~ sQ85_spl
| ~ sQ84_spl
| sQ32_spl
| sQ82_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f2242,f1483,f1737,f687,f1743,f1746,f181,f262,f511]) ).
fof(f2377,plain,
( ~ sQ82_spl
| r2_hidden(k3_yellow_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1738,f169]) ).
fof(f2392,plain,
( ~ sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2377,f61]) ).
fof(f2393,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f2392]) ).
fof(f2394,plain,
$false,
inference(sat_refutation,[status(thm)],[f190,f202,f204,f336,f433,f514,f708,f1521,f1757,f1759,f2249,f2393]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU411+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.36 % Computer : n013.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 06:21:36 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 2.25/0.76 % Refutation found
% 2.25/0.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.25/0.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.25/0.78 % Elapsed time: 0.407418 seconds
% 2.25/0.78 % CPU time: 2.886552 seconds
% 2.25/0.78 % Total memory used: 147.140 MB
% 2.25/0.78 % Net memory used: 142.602 MB
%------------------------------------------------------------------------------