%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU412+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 107.08s 18.94s
% Output : CNFRefutation 107.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 15
% Syntax : Number of formulae : 122 ( 13 unt; 0 def)
% Number of atoms : 517 ( 37 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 691 ( 296 ~; 284 |; 88 &)
% ( 7 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-6 aty)
% Number of variables : 263 ( 251 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A,B,C] :
( l1_orders_2(C)
=> ! [D] :
( l1_orders_2(D)
=> ~ ( ~ ( r2_hidden(B,k4_xboole_0(u1_struct_0(D),u1_struct_0(C)))
& r2_hidden(A,k4_xboole_0(u1_struct_0(C),u1_struct_0(D))) )
& ~ ( r2_hidden(B,u1_struct_0(D))
& r2_hidden(A,u1_struct_0(D)) )
& ~ ( r2_hidden(B,u1_struct_0(C))
& r2_hidden(A,u1_struct_0(C)) )
& m1_subset_1(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),k1_zfmisc_1(u1_struct_0(C)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),C)
& r2_hidden(k4_tarski(A,B),u1_orders_2(k1_latsum_1(C,D))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A,B,C] :
( l1_orders_2(C)
=> ! [D] :
( l1_orders_2(D)
=> ~ ( ~ ( r2_hidden(B,k4_xboole_0(u1_struct_0(D),u1_struct_0(C)))
& r2_hidden(A,k4_xboole_0(u1_struct_0(C),u1_struct_0(D))) )
& ~ ( r2_hidden(B,u1_struct_0(D))
& r2_hidden(A,u1_struct_0(D)) )
& ~ ( r2_hidden(B,u1_struct_0(C))
& r2_hidden(A,u1_struct_0(C)) )
& m1_subset_1(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),k1_zfmisc_1(u1_struct_0(C)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),C)
& r2_hidden(k4_tarski(A,B),u1_orders_2(k1_latsum_1(C,D))) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f7,axiom,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( ( l1_orders_2(C)
& v1_orders_2(C) )
=> ( C = k1_latsum_1(A,B)
<=> ( u1_orders_2(C) = k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))
& u1_struct_0(C) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B,C] :
( C = k2_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,B)
| r2_hidden(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B,C] :
( C = k4_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( ~ r2_hidden(D,B)
& r2_hidden(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] :
( ( l1_orders_2(B)
& l1_orders_2(A) )
=> ( l1_orders_2(k1_latsum_1(A,B))
& v1_orders_2(k1_latsum_1(A,B)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( l1_orders_2(A)
=> m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C,D] :
( ( r2_hidden(C,u1_struct_0(B))
& r2_hidden(k4_tarski(C,D),u1_orders_2(k1_latsum_1(A,B)))
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(A)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),A) )
=> r2_hidden(D,u1_struct_0(B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,plain,
? [A,B,C] :
( ? [D] :
( ( ~ r2_hidden(B,k4_xboole_0(u1_struct_0(D),u1_struct_0(C)))
| ~ r2_hidden(A,k4_xboole_0(u1_struct_0(C),u1_struct_0(D))) )
& ( ~ r2_hidden(B,u1_struct_0(D))
| ~ r2_hidden(A,u1_struct_0(D)) )
& ( ~ r2_hidden(B,u1_struct_0(C))
| ~ r2_hidden(A,u1_struct_0(C)) )
& m1_subset_1(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),k1_zfmisc_1(u1_struct_0(C)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),C)
& r2_hidden(k4_tarski(A,B),u1_orders_2(k1_latsum_1(C,D)))
& l1_orders_2(D) )
& l1_orders_2(C) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f60,plain,
? [C] :
( ? [D] :
( ? [A,B] :
( ( ~ r2_hidden(B,k4_xboole_0(u1_struct_0(D),u1_struct_0(C)))
| ~ r2_hidden(A,k4_xboole_0(u1_struct_0(C),u1_struct_0(D))) )
& ( ~ r2_hidden(B,u1_struct_0(D))
| ~ r2_hidden(A,u1_struct_0(D)) )
& ( ~ r2_hidden(B,u1_struct_0(C))
| ~ r2_hidden(A,u1_struct_0(C)) )
& m1_subset_1(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),k1_zfmisc_1(u1_struct_0(C)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(C),u1_struct_0(D)),C)
& r2_hidden(k4_tarski(A,B),u1_orders_2(k1_latsum_1(C,D))) )
& l1_orders_2(D) )
& l1_orders_2(C) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
( ( ~ r2_hidden(sK3_skl,k4_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)))
| ~ r2_hidden(sK2_skl,k4_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))) )
& ( ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ r2_hidden(sK2_skl,u1_struct_0(sK1_skl)) )
& ( ~ r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK2_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(sK0_skl)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK0_skl)
& r2_hidden(k4_tarski(sK2_skl,sK3_skl),u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)))
& l1_orders_2(sK1_skl)
& l1_orders_2(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(C,sK0_skl),skolemize(D,sK1_skl),skolemize(A,sK2_skl),skolemize(B,sK3_skl)],[f60]) ).
fof(f62,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
l1_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f64,plain,
r2_hidden(k4_tarski(sK2_skl,sK3_skl),u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f65,plain,
v13_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK0_skl),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f66,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK0_skl))),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f67,plain,
( ~ r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK3_skl,u1_struct_0(sK0_skl)) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f68,plain,
( ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ r2_hidden(sK2_skl,u1_struct_0(sK1_skl)) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f69,plain,
( ~ r2_hidden(sK2_skl,k4_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))
| ~ r2_hidden(sK3_skl,k4_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f78,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f79,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = k1_latsum_1(A,B)
<=> ( u1_orders_2(C) = k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))
& u1_struct_0(C) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) ) )
| ~ l1_orders_2(C)
| ~ v1_orders_2(C) )
| ~ l1_orders_2(B) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f80,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( u1_orders_2(C) != k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))
| u1_struct_0(C) != k2_xboole_0(u1_struct_0(A),u1_struct_0(B))
| C = k1_latsum_1(A,B) )
& ( ( u1_orders_2(C) = k2_xboole_0(k2_xboole_0(u1_orders_2(A),u1_orders_2(B)),k7_relset_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(B),u1_struct_0(B),u1_orders_2(A),u1_orders_2(B)))
& u1_struct_0(C) = k2_xboole_0(u1_struct_0(A),u1_struct_0(B)) )
| C != k1_latsum_1(A,B) ) )
| ~ l1_orders_2(C)
| ~ v1_orders_2(C) )
| ~ l1_orders_2(B) )
| ~ l1_orders_2(A) ),
inference(NNF_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ l1_orders_2(X1)
| X0 != k1_latsum_1(X1,X2)
| ~ l1_orders_2(X2)
| ~ v1_orders_2(X0)
| u1_struct_0(X0) = k2_xboole_0(u1_struct_0(X1),u1_struct_0(X2))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f84,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 = k2_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 != k2_xboole_0(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f85,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 = k2_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 != k2_xboole_0(A,B) ) ),
inference(miniscoping,[status(thm)],[f84]) ).
fof(f86,plain,
( ! [A,B,C] :
( ( ( r2_hidden(sK4_skl(C,B,A),B)
| r2_hidden(sK4_skl(C,B,A),A)
| r2_hidden(sK4_skl(C,B,A),C) )
& ( ( ~ r2_hidden(sK4_skl(C,B,A),B)
& ~ r2_hidden(sK4_skl(C,B,A),A) )
| ~ r2_hidden(sK4_skl(C,B,A),C) ) )
| C = k2_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 != k2_xboole_0(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(D,sK4_skl(C,B,A))],[f85]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( X2 != k2_xboole_0(X3,X1)
| r2_hidden(X0,X3)
| ~ r2_hidden(X0,X2)
| r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f93,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 = k4_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 != k4_xboole_0(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f94,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 = k4_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 != k4_xboole_0(A,B) ) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f95,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 = k4_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 != k4_xboole_0(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(D,sK5_skl(C,B,A))],[f94]) ).
fof(f98,plain,
! [X0,X1,X2,X3] :
( ~ r2_hidden(X3,X1)
| r2_hidden(X3,X2)
| r2_hidden(X3,X0)
| X0 != k4_xboole_0(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f105,plain,
! [A,B] :
( ( l1_orders_2(k1_latsum_1(A,B))
& v1_orders_2(k1_latsum_1(A,B)) )
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f106,plain,
! [X0,X1] :
( v1_orders_2(k1_latsum_1(X0,X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [X0,X1] :
( ~ l1_orders_2(X1)
| l1_orders_2(k1_latsum_1(X1,X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f114,plain,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X0,X1,X2)
| m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
! [A] :
( m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f117,plain,
! [X0] :
( ~ l1_orders_2(X0)
| m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f154,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)],[f45]) ).
fof(f155,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)],[f154]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( ~ r2_hidden(k4_tarski(X0,X2),k2_zfmisc_1(X1,X3))
| r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,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)],[f155]) ).
fof(f159,plain,
! [A] :
( ! [B] :
( ! [C,D] :
( r2_hidden(D,u1_struct_0(B))
| ~ r2_hidden(C,u1_struct_0(B))
| ~ r2_hidden(k4_tarski(C,D),u1_orders_2(k1_latsum_1(A,B)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(A)))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),A) )
| ~ l1_orders_2(B) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f160,plain,
! [A] :
( ! [B] :
( ! [D] :
( r2_hidden(D,u1_struct_0(B))
| ! [C] :
( ~ r2_hidden(C,u1_struct_0(B))
| ~ r2_hidden(k4_tarski(C,D),u1_orders_2(k1_latsum_1(A,B)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(A)))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),A) ) )
| ~ l1_orders_2(B) )
| ~ l1_orders_2(A) ),
inference(miniscoping,[status(thm)],[f159]) ).
fof(f161,plain,
! [X0,X1,X2,X3] :
( ~ m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
| ~ r2_hidden(k4_tarski(X2,X3),u1_orders_2(k1_latsum_1(X0,X1)))
| ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| r2_hidden(X3,u1_struct_0(X1))
| ~ r2_hidden(X2,u1_struct_0(X1))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f164,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f167,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| v1_xboole_0(X1)
| r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f174,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)],[f54]) ).
fof(f175,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)],[f174]) ).
fof(f176,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)],[f175]) ).
fof(f177,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f178,plain,
! [C] :
( ~ v1_xboole_0(C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ! [A] : ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f182,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f183,plain,
! [B] :
( ~ v1_xboole_0(B)
| ! [A] : ~ r2_hidden(A,B) ),
inference(miniscoping,[status(thm)],[f182]) ).
fof(f184,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f292,plain,
v13_waybel_0(k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)),sK0_skl),
inference(forward_demodulation,[status(thm)],[f78,f65]) ).
fof(f324,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X2,X0)
| ~ m1_subset_1(k4_tarski(X2,X3),k2_zfmisc_1(X0,X1))
| v1_xboole_0(k2_zfmisc_1(X0,X1)) ),
inference(resolution,[status(thm)],[f167,f156]) ).
fof(f327,plain,
( ~ r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f167,f67]) ).
fof(f335,plain,
( ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK3_skl,u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f327,f184]) ).
fof(f338,plain,
! [X0,X1,X2,X3] :
( v1_xboole_0(k2_zfmisc_1(X3,X1))
| ~ m1_subset_1(k4_tarski(X2,X0),k2_zfmisc_1(X3,X1))
| r2_hidden(X0,X1) ),
inference(resolution,[status(thm)],[f157,f167]) ).
fof(f446,plain,
! [X0,X1,X2] :
( r2_hidden(X0,k4_xboole_0(X2,X1))
| ~ r2_hidden(X0,X2)
| r2_hidden(X0,X1) ),
inference(equality_resolution,[status(thm)],[f98]) ).
fof(f461,plain,
! [X0,X1,X2,X3] :
( ~ v13_waybel_0(k3_xboole_0(u1_struct_0(X2),u1_struct_0(X3)),X2)
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(X3),u1_struct_0(X2)),k1_zfmisc_1(u1_struct_0(X2)))
| r2_hidden(X1,u1_struct_0(X3))
| ~ l1_orders_2(X2)
| ~ r2_hidden(X0,u1_struct_0(X3))
| ~ l1_orders_2(X3)
| ~ r2_hidden(k4_tarski(X0,X1),u1_orders_2(k1_latsum_1(X2,X3))) ),
inference(paramodulation,[status(thm)],[f78,f161]) ).
fof(f578,plain,
! [X0,X1,X2,X3] :
( ~ r2_hidden(X0,X3)
| ~ m2_relset_1(X3,X1,X2)
| m1_subset_1(X0,k2_zfmisc_1(X1,X2)) ),
inference(resolution,[status(thm)],[f115,f176]) ).
fof(f579,plain,
! [X0,X1,X2,X3] :
( ~ r2_hidden(X3,X0)
| ~ v1_xboole_0(k2_zfmisc_1(X1,X2))
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[status(thm)],[f115,f179]) ).
fof(f580,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)),k1_zfmisc_1(u1_struct_0(sK0_skl))),
inference(forward_demodulation,[status(thm)],[f78,f66]) ).
fof(f1340,plain,
( r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| ~ r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK3_skl,k4_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))) ),
inference(resolution,[status(thm)],[f446,f69]) ).
fof(f1365,plain,
( ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| ~ r2_hidden(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1340,f446]) ).
fof(f1367,plain,
( r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1365,f68]) ).
fof(f1368,plain,
( ~ r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1367,f67]) ).
fof(f1479,plain,
! [X0,X1,X2,X3] :
( ~ l1_orders_2(X3)
| ~ v1_orders_2(X3)
| ~ r2_hidden(X2,u1_struct_0(X3))
| k1_latsum_1(X0,X1) != X3
| r2_hidden(X2,u1_struct_0(X0))
| r2_hidden(X2,u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f81,f87]) ).
fof(f1782,plain,
! [X0,X1] :
( ~ v13_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK0_skl)
| r2_hidden(X1,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK0_skl)
| ~ r2_hidden(X0,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ r2_hidden(k4_tarski(X0,X1),u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))) ),
inference(resolution,[status(thm)],[f461,f580]) ).
fof(f1789,plain,
! [X0,X1] :
( ~ v13_waybel_0(k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)),sK0_skl)
| r2_hidden(X1,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK0_skl)
| ~ r2_hidden(X0,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ r2_hidden(k4_tarski(X0,X1),u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))) ),
inference(forward_demodulation,[status(thm)],[f78,f1782]) ).
fof(f1790,plain,
! [X0,X1] :
( ~ l1_orders_2(sK0_skl)
| r2_hidden(X1,u1_struct_0(sK1_skl))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)),sK0_skl)
| ~ r2_hidden(X0,u1_struct_0(sK1_skl))
| ~ r2_hidden(k4_tarski(X0,X1),u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1789,f63]) ).
fof(f1894,plain,
! [X0,X1,X2,X3,X4] :
( v1_xboole_0(k2_zfmisc_1(X1,X2))
| r2_hidden(X4,X2)
| ~ r2_hidden(k4_tarski(X3,X4),X0)
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[status(thm)],[f578,f338]) ).
fof(f1895,plain,
! [X0,X1,X2,X3,X4] :
( r2_hidden(X3,X1)
| v1_xboole_0(k2_zfmisc_1(X1,X2))
| ~ r2_hidden(k4_tarski(X3,X4),X0)
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[status(thm)],[f578,f324]) ).
fof(f1900,plain,
! [X0,X1,X2,X3,X4] :
( r2_hidden(X0,X3)
| ~ m2_relset_1(X2,X3,X4)
| ~ r2_hidden(k4_tarski(X0,X1),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f1895,f579]) ).
fof(f1901,plain,
! [X0,X1,X2,X3,X4] :
( ~ m2_relset_1(X2,X4,X3)
| r2_hidden(X1,X3)
| ~ r2_hidden(k4_tarski(X0,X1),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f1894,f579]) ).
fof(f2162,plain,
! [X0,X1] :
( r2_hidden(sK2_skl,X0)
| ~ m2_relset_1(u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)),X0,X1) ),
inference(resolution,[status(thm)],[f1900,f64]) ).
fof(f2169,plain,
! [X0,X1] :
( ~ m2_relset_1(u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)),X1,X0)
| r2_hidden(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f1901,f64]) ).
fof(f2341,plain,
( r2_hidden(sK2_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl)))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f2162,f117]) ).
fof(f2456,plain,
( ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(k1_latsum_1(sK0_skl,sK1_skl))) ),
inference(resolution,[status(thm)],[f2169,f117]) ).
fof(f3414,plain,
! [X0,X1] :
( ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| k1_latsum_1(X0,X1) != k1_latsum_1(sK0_skl,sK1_skl)
| r2_hidden(sK3_skl,u1_struct_0(X0))
| r2_hidden(sK3_skl,u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f1479,f2456]) ).
fof(f3417,plain,
! [X0,X1] :
( ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| k1_latsum_1(X0,X1) != k1_latsum_1(sK0_skl,sK1_skl)
| r2_hidden(sK2_skl,u1_struct_0(X0))
| r2_hidden(sK2_skl,u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f1479,f2341]) ).
fof(f3437,plain,
! [X0,X1] :
( ~ l1_orders_2(X1)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(X0))
| r2_hidden(sK3_skl,u1_struct_0(X1))
| k1_latsum_1(sK0_skl,sK1_skl) != k1_latsum_1(X0,X1)
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ l1_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3414]) ).
fof(f3438,plain,
! [X0,X1] :
( ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK2_skl,u1_struct_0(X1))
| ~ l1_orders_2(X1)
| k1_latsum_1(sK0_skl,sK1_skl) != k1_latsum_1(X1,X0)
| r2_hidden(sK2_skl,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f3417]) ).
fof(f3440,plain,
( ~ l1_orders_2(sK1_skl)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ l1_orders_2(sK0_skl) ),
inference(equality_resolution,[status(thm)],[f3437]) ).
fof(f3441,plain,
( r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3440,f62]) ).
fof(f3442,plain,
( r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK0_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3441,f63]) ).
fof(f3443,plain,
( ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3442,f335]) ).
fof(f4193,plain,
( ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl)
| r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(equality_resolution,[status(thm)],[f3438]) ).
fof(f4194,plain,
( ~ l1_orders_2(sK0_skl)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ l1_orders_2(sK1_skl)
| r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| r2_hidden(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4193,f107]) ).
fof(f4195,plain,
( r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK0_skl)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4194,f63]) ).
fof(f4196,plain,
( ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f4195,f68]) ).
fof(f4216,plain,
( m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK0_skl)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f4195,f164]) ).
fof(f4221,plain,
( r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4216,f62]) ).
fof(f4228,plain,
( r2_hidden(sK2_skl,u1_struct_0(sK0_skl))
| ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4196,f62]) ).
fof(f4257,plain,
( ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f3443,f4263]) ).
fof(f4263,plain,
( ~ r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4228,f1368]) ).
fof(f4477,plain,
( ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ l1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f4257,f106]) ).
fof(f4479,plain,
( ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4477,f107]) ).
fof(f4480,plain,
( ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4479,f63]) ).
fof(f11387,plain,
! [X0,X1] :
( ~ r2_hidden(X0,u1_struct_0(sK1_skl))
| r2_hidden(X1,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK0_skl)
| ~ r2_hidden(k4_tarski(X0,X1),u1_orders_2(k1_latsum_1(sK0_skl,sK1_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1790,f292]) ).
fof(f11388,plain,
( ~ r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f11387,f64]) ).
fof(f11391,plain,
( ~ r2_hidden(sK2_skl,u1_struct_0(sK1_skl))
| r2_hidden(sK3_skl,u1_struct_0(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f11388,f62]) ).
fof(f11394,plain,
( m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f4221,f11396]) ).
fof(f11396,plain,
~ r2_hidden(sK2_skl,u1_struct_0(sK1_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f11391,f68]) ).
fof(f11805,plain,
( ~ l1_orders_2(sK0_skl)
| ~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f11394,f4480]) ).
fof(f11809,plain,
~ v1_orders_2(k1_latsum_1(sK0_skl,sK1_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f11805,f62]) ).
fof(f11813,plain,
( ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f11809,f106]) ).
fof(f11814,plain,
~ l1_orders_2(sK1_skl),
inference(forward_subsumption_resolution,[status(thm)],[f11813,f62]) ).
fof(f11815,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f11814,f63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU412+1 : 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.37 % Computer : n004.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 06:22:10 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 107.08/18.94 % Refutation found
% 107.08/18.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 107.08/18.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.34/19.02 % Elapsed time: 13.623019 seconds
% 6.34/19.02 % CPU time: 107.857315 seconds
% 6.34/19.02 % Total memory used: 561.867 MB
% 6.34/19.02 % Net memory used: 497.751 MB
%------------------------------------------------------------------------------