%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU411+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 162.05s 21.40s
% Output : CNFRefutation 162.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 23
% Syntax : Number of formulae : 122 ( 53 unt; 0 def)
% Number of atoms : 385 ( 49 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 423 ( 160 ~; 144 |; 93 &)
% ( 5 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-2 aty)
% Number of variables : 199 ( 191 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
? [A] : v1_xboole_0(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( v1_xboole_0(A)
<=> A = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A,B] : k3_xboole_0(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [A] : k3_xboole_0(A,k1_xboole_0) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] : k4_xboole_0(A,k1_xboole_0) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [A,B] :
( r1_tarski(A,B)
=> k2_xboole_0(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A,B] : r1_tarski(k3_xboole_0(A,B),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [A,B,C] :
( r1_tarski(A,B)
=> r1_tarski(k4_xboole_0(C,B),k4_xboole_0(C,A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,axiom,
! [A,B] : k4_xboole_0(A,k4_xboole_0(A,B)) = k3_xboole_0(A,B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,axiom,
! [A,B,C] : k4_xboole_0(A,k4_xboole_0(B,C)) = k2_xboole_0(k4_xboole_0(A,B),k3_xboole_0(A,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,axiom,
! [A,B] : r1_xboole_0(k4_xboole_0(A,B),B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [A,B,C] :
( r1_xboole_0(A,B)
=> r1_xboole_0(A,k4_xboole_0(B,C)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f242,axiom,
! [A,B] :
~ ( r2_hidden(A,B)
& r1_xboole_0(k1_tarski(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,axiom,
! [A,B] :
( k4_xboole_0(A,k1_tarski(B)) = A
<=> ~ r2_hidden(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f447,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(f449,axiom,
? [A] :
( v1_relat_1(A)
& v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3802,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(f3842,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(f3932,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(f4449,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( r2_hidden(C,k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
=> m1_subset_1(C,u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4457,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(f4458,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)],[f4457]) ).
fof(f4538,plain,
v1_xboole_0(sK20_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25]) ).
fof(f4539,plain,
v1_xboole_0(sK20_skl),
inference(cnf_transformation,[status(thm)],[f4538]) ).
fof(f4548,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(f4549,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)],[f4548]) ).
fof(f4550,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))],[f4549]) ).
fof(f4552,plain,
! [X0] :
( r2_hidden(sK22_skl(X0),X0)
| X0 = k1_xboole_0 ),
inference(cnf_transformation,[status(thm)],[f4550]) ).
fof(f4580,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(f4581,plain,
( ! [A] :
( A != k1_xboole_0
| v1_xboole_0(A) )
& ! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ) ),
inference(miniscoping,[status(thm)],[f4580]) ).
fof(f4582,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f4581]) ).
fof(f4667,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f4668,plain,
! [A] : k3_xboole_0(A,A) = A,
inference(miniscoping,[status(thm)],[f58]) ).
fof(f4669,plain,
! [X0] : k3_xboole_0(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f4668]) ).
fof(f4672,plain,
! [X0] : k3_xboole_0(X0,k1_xboole_0) = k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f4673,plain,
! [X0] : k4_xboole_0(X0,k1_xboole_0) = X0,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f4705,plain,
! [A,B] :
( k2_xboole_0(A,B) = B
| ~ r1_tarski(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f4706,plain,
! [X0,X1] :
( k2_xboole_0(X0,X1) = X1
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4705]) ).
fof(f4718,plain,
! [X0,X1] : r1_tarski(k3_xboole_0(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f4751,plain,
! [A,B,C] :
( r1_tarski(k4_xboole_0(C,B),k4_xboole_0(C,A))
| ~ r1_tarski(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f103]) ).
fof(f4752,plain,
! [A,B] :
( ! [C] : r1_tarski(k4_xboole_0(C,B),k4_xboole_0(C,A))
| ~ r1_tarski(A,B) ),
inference(miniscoping,[status(thm)],[f4751]) ).
fof(f4753,plain,
! [X0,X1,X2] :
( r1_tarski(k4_xboole_0(X2,X1),k4_xboole_0(X2,X0))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4752]) ).
fof(f4776,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f4780,plain,
! [X0,X1,X2] : k4_xboole_0(X0,k4_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k3_xboole_0(X0,X2)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f4847,plain,
! [X0,X1] : r1_xboole_0(k4_xboole_0(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f4848,plain,
! [A,B,C] :
( r1_xboole_0(A,k4_xboole_0(B,C))
| ~ r1_xboole_0(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f149]) ).
fof(f4849,plain,
! [A,B] :
( ! [C] : r1_xboole_0(A,k4_xboole_0(B,C))
| ~ r1_xboole_0(A,B) ),
inference(miniscoping,[status(thm)],[f4848]) ).
fof(f4850,plain,
! [X0,X1,X2] :
( r1_xboole_0(X0,k4_xboole_0(X1,X2))
| ~ r1_xboole_0(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4849]) ).
fof(f5053,plain,
! [A,B] :
( ~ r2_hidden(A,B)
| ~ r1_xboole_0(k1_tarski(A),B) ),
inference(pre_NNF_transformation,[status(thm)],[f242]) ).
fof(f5054,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r1_xboole_0(k1_tarski(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f5053]) ).
fof(f5078,plain,
! [A,B] :
( ( r2_hidden(B,A)
| k4_xboole_0(A,k1_tarski(B)) = A )
& ( ~ r2_hidden(B,A)
| k4_xboole_0(A,k1_tarski(B)) != A ) ),
inference(NNF_transformation,[status(thm)],[f253]) ).
fof(f5079,plain,
( ! [A,B] :
( r2_hidden(B,A)
| k4_xboole_0(A,k1_tarski(B)) = A )
& ! [A,B] :
( ~ r2_hidden(B,A)
| k4_xboole_0(A,k1_tarski(B)) != A ) ),
inference(miniscoping,[status(thm)],[f5078]) ).
fof(f5081,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| k4_xboole_0(X0,k1_tarski(X1)) = X0 ),
inference(cnf_transformation,[status(thm)],[f5079]) ).
fof(f5571,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)],[f447]) ).
fof(f5572,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)],[f5571]) ).
fof(f5573,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)],[f5572]) ).
fof(f5577,plain,
( v1_relat_1(sK87_skl)
& v1_xboole_0(sK87_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87_skl]),skolemize(A,sK87_skl)],[f449]) ).
fof(f5578,plain,
v1_xboole_0(sK87_skl),
inference(cnf_transformation,[status(thm)],[f5577]) ).
fof(f15613,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)],[f3802]) ).
fof(f15614,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)],[f15613]) ).
fof(f15782,plain,
! [A] :
( m1_subset_1(k3_yellow_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3842]) ).
fof(f15783,plain,
! [X0] :
( m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f15782]) ).
fof(f16230,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)],[f3932]) ).
fof(f16231,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)],[f16230]) ).
fof(f16232,plain,
! [A] :
( ! [B] :
( ( ( ( ~ r2_hidden(sK1012_skl(B,A),B)
& r1_orders_2(A,sK1012_skl(B,A),sK1011_skl(B,A))
& r2_hidden(sK1011_skl(B,A),B)
& m1_subset_1(sK1012_skl(B,A),u1_struct_0(A))
& m1_subset_1(sK1011_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,[sK1011_skl,sK1012_skl]),skolemize(C,sK1011_skl(B,A)),skolemize(D,sK1012_skl(B,A))],[f16231]) ).
fof(f16233,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)],[f16232]) ).
fof(f18571,plain,
! [A] :
( ! [B] :
( ! [C] :
( m1_subset_1(C,u1_struct_0(A))
| ~ r2_hidden(C,k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
| ~ l1_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4449]) ).
fof(f18572,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f18571]) ).
fof(f18596,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)],[f4458]) ).
fof(f18597,plain,
( ~ r2_hidden(k3_yellow_0(sK1193_skl),u1_struct_0(sK1192_skl))
& m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),sK1193_skl)
& v1_waybel_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),sK1193_skl)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
& l1_orders_2(sK1193_skl)
& v1_lattice3(sK1193_skl)
& v1_yellow_0(sK1193_skl)
& v4_orders_2(sK1193_skl)
& v3_orders_2(sK1193_skl)
& v2_orders_2(sK1193_skl)
& ~ v3_struct_0(sK1193_skl)
& l1_orders_2(sK1192_skl)
& v1_lattice3(sK1192_skl)
& v1_yellow_0(sK1192_skl)
& v4_orders_2(sK1192_skl)
& v3_orders_2(sK1192_skl)
& v2_orders_2(sK1192_skl)
& ~ v3_struct_0(sK1192_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1192_skl,sK1193_skl]),skolemize(A,sK1192_skl),skolemize(B,sK1193_skl)],[f18596]) ).
fof(f18598,plain,
~ v3_struct_0(sK1192_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18604,plain,
l1_orders_2(sK1192_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18605,plain,
~ v3_struct_0(sK1193_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18608,plain,
v4_orders_2(sK1193_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18609,plain,
v1_yellow_0(sK1193_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18611,plain,
l1_orders_2(sK1193_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18612,plain,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18614,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),sK1193_skl),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18615,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl))),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f18616,plain,
~ r2_hidden(k3_yellow_0(sK1193_skl),u1_struct_0(sK1192_skl)),
inference(cnf_transformation,[status(thm)],[f18597]) ).
fof(f21029,plain,
sK87_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f4582,f5578]) ).
fof(f21030,plain,
sK20_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f4582,f4539]) ).
fof(f21052,plain,
sK20_skl = k1_xboole_0,
inference(backward_demodulation,[status(thm)],[f21055,f21029]) ).
fof(f21055,plain,
sK20_skl = sK87_skl,
inference(forward_demodulation,[status(thm)],[f21029,f21030]) ).
fof(f21057,plain,
! [X0] : k3_xboole_0(X0,sK20_skl) = k1_xboole_0,
inference(forward_demodulation,[status(thm)],[f21052,f4672]) ).
fof(f21058,plain,
! [X0] : k3_xboole_0(X0,sK20_skl) = sK20_skl,
inference(forward_demodulation,[status(thm)],[f21052,f21057]) ).
fof(f21130,plain,
! [X0] : r1_tarski(sK20_skl,X0),
inference(paramodulation,[status(thm)],[f21058,f4718]) ).
fof(f21767,plain,
! [X0] :
( r2_hidden(sK22_skl(X0),X0)
| X0 = sK20_skl ),
inference(forward_demodulation,[status(thm)],[f21052,f4552]) ).
fof(f22575,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X2,X1)
| ~ r1_orders_2(X0,X2,X3)
| ~ r2_hidden(X3,X1)
| ~ 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(forward_subsumption_resolution,[status(thm)],[f16233,f5573]) ).
fof(f22576,plain,
! [X0,X1] :
( r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r1_orders_2(sK1193_skl,X0,X1)
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl)))
| ~ l1_orders_2(sK1193_skl) ),
inference(resolution,[status(thm)],[f22575,f18614]) ).
fof(f22577,plain,
! [X0,X1] :
( r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r1_orders_2(sK1193_skl,X0,X1)
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)),k1_zfmisc_1(u1_struct_0(sK1193_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f22576,f18611]) ).
fof(f22638,plain,
! [X0,X1] :
( r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r1_orders_2(sK1193_skl,X0,X1)
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ m1_subset_1(X0,u1_struct_0(sK1193_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f22577,f18615]) ).
fof(f22639,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ l1_orders_2(sK1193_skl)
| ~ v1_yellow_0(sK1193_skl)
| ~ v4_orders_2(sK1193_skl)
| v3_struct_0(sK1193_skl)
| r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ m1_subset_1(k3_yellow_0(sK1193_skl),u1_struct_0(sK1193_skl)) ),
inference(resolution,[status(thm)],[f22638,f15614]) ).
fof(f22640,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ l1_orders_2(sK1193_skl)
| ~ v1_yellow_0(sK1193_skl)
| ~ v4_orders_2(sK1193_skl)
| v3_struct_0(sK1193_skl)
| r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f22639,f15783]) ).
fof(f23637,plain,
! [X0] : k4_xboole_0(X0,sK20_skl) = X0,
inference(forward_demodulation,[status(thm)],[f21052,f4673]) ).
fof(f24232,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ l1_orders_2(sK1193_skl)
| ~ v1_yellow_0(sK1193_skl)
| ~ v4_orders_2(sK1193_skl)
| r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f22640,f18605]) ).
fof(f24454,plain,
! [X0,X1] :
( m1_subset_1(X1,u1_struct_0(X0))
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(X0),u1_struct_0(sK1192_skl)))
| v3_struct_0(sK1192_skl)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f18572,f18604]) ).
fof(f24456,plain,
! [X0,X1] :
( m1_subset_1(X1,u1_struct_0(X0))
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(X0),u1_struct_0(sK1192_skl)))
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f24454,f18598]) ).
fof(f24929,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1193_skl),u1_struct_0(sK1192_skl)))
| v3_struct_0(sK1193_skl) ),
inference(resolution,[status(thm)],[f24456,f18611]) ).
fof(f24931,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| v3_struct_0(sK1193_skl) ),
inference(forward_demodulation,[status(thm)],[f4667,f24929]) ).
fof(f24932,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(sK1193_skl))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f24931,f18605]) ).
fof(f25395,plain,
! [X0] :
( ~ l1_orders_2(sK1193_skl)
| ~ v1_yellow_0(sK1193_skl)
| ~ v4_orders_2(sK1193_skl)
| r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(backward_subsumption_resolution,[status(thm)],[f24232,f24932]) ).
fof(f25398,plain,
! [X0] :
( ~ l1_orders_2(sK1193_skl)
| ~ v1_yellow_0(sK1193_skl)
| r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f25395,f18608]) ).
fof(f25801,plain,
! [X0,X1] :
( r1_tarski(k4_xboole_0(X1,X0),X1)
| ~ r1_tarski(sK20_skl,X0) ),
inference(paramodulation,[status(thm)],[f23637,f4753]) ).
fof(f25805,plain,
! [X0,X1] : r1_tarski(k4_xboole_0(X0,X1),X0),
inference(forward_subsumption_resolution,[status(thm)],[f25801,f21130]) ).
fof(f25884,plain,
! [X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),X0) = X0,
inference(resolution,[status(thm)],[f25805,f4706]) ).
fof(f27996,plain,
! [X0] :
( ~ l1_orders_2(sK1193_skl)
| r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f25398,f18609]) ).
fof(f28691,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X0)) = k2_xboole_0(k4_xboole_0(X0,X1),X0),
inference(paramodulation,[status(thm)],[f4669,f4780]) ).
fof(f28744,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f25884,f28691]) ).
fof(f32736,plain,
! [X0,X1] : r1_xboole_0(X0,k4_xboole_0(X1,X0)),
inference(paramodulation,[status(thm)],[f28744,f4847]) ).
fof(f48872,plain,
k4_xboole_0(u1_struct_0(sK1192_skl),k1_tarski(k3_yellow_0(sK1193_skl))) = u1_struct_0(sK1192_skl),
inference(resolution,[status(thm)],[f5081,f18616]) ).
fof(f49030,plain,
r1_xboole_0(k1_tarski(k3_yellow_0(sK1193_skl)),u1_struct_0(sK1192_skl)),
inference(paramodulation,[status(thm)],[f48872,f32736]) ).
fof(f49088,plain,
! [X0] : r1_xboole_0(k1_tarski(k3_yellow_0(sK1193_skl)),k4_xboole_0(u1_struct_0(sK1192_skl),X0)),
inference(resolution,[status(thm)],[f49030,f4850]) ).
fof(f55345,plain,
! [X0] : ~ r2_hidden(k3_yellow_0(sK1193_skl),k4_xboole_0(u1_struct_0(sK1192_skl),X0)),
inference(resolution,[status(thm)],[f49088,f5054]) ).
fof(f55399,plain,
! [X0] : ~ r2_hidden(k3_yellow_0(sK1193_skl),k3_xboole_0(u1_struct_0(sK1192_skl),X0)),
inference(paramodulation,[status(thm)],[f4776,f55345]) ).
fof(f55992,plain,
! [X0] :
( ~ l1_orders_2(sK1193_skl)
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))) ),
inference(backward_subsumption_resolution,[status(thm)],[f27996,f55399]) ).
fof(f56021,plain,
! [X0] : ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f55992,f18611]) ).
fof(f56040,plain,
k3_xboole_0(u1_struct_0(sK1192_skl),u1_struct_0(sK1193_skl)) = sK20_skl,
inference(resolution,[status(thm)],[f56021,f21767]) ).
fof(f57879,plain,
~ v1_xboole_0(sK20_skl),
inference(backward_demodulation,[status(thm)],[f56040,f18612]) ).
fof(f57994,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f57879,f4539]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU411+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n016.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 06:26:54 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.55/0.83 % Drodi V4.1.1
% 162.05/21.40 % Refutation found
% 162.05/21.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 162.05/21.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 35.18/21.54 % Elapsed time: 21.165308 seconds
% 35.18/21.54 % CPU time: 163.329767 seconds
% 35.18/21.54 % Total memory used: 1.154 GB
% 35.18/21.54 % Net memory used: 1.090 GB
%------------------------------------------------------------------------------