%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT358+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 : n019.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:55 PM UTC 2026
% Result : Theorem 3.82s 0.98s
% Output : CNFRefutation 3.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 67
% Syntax : Number of formulae : 307 ( 58 unt; 55 def)
% Number of atoms : 1685 ( 23 equ)
% Maximal formula atoms : 50 ( 5 avg)
% Number of connectives : 2422 (1044 ~;1093 |; 188 &)
% ( 58 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 58 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 73 ( 71 usr; 56 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-5 aty)
% Number of variables : 185 ( 180 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( l1_orders_2(C)
& v3_lattice3(C)
& v2_lattice3(C)
& v1_lattice3(C)
& v4_orders_2(C)
& v3_orders_2(C)
& v2_orders_2(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(D,A,B)
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
& v18_waybel_0(E,B,C)
& v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_1(E) )
=> k2_waybel34(C,A,k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E)) = k7_funct_2(u1_struct_0(C),u1_struct_0(B),u1_struct_0(A),k2_waybel34(C,B,E),k2_waybel34(B,A,D)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( l1_orders_2(C)
& v3_lattice3(C)
& v2_lattice3(C)
& v1_lattice3(C)
& v4_orders_2(C)
& v3_orders_2(C)
& v2_orders_2(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(D,A,B)
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
& v18_waybel_0(E,B,C)
& v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_1(E) )
=> k2_waybel34(C,A,k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E)) = k7_funct_2(u1_struct_0(C),u1_struct_0(B),u1_struct_0(A),k2_waybel34(C,B,E),k2_waybel34(B,A,D)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f21,axiom,
! [A] :
( l1_orders_2(A)
=> ( v1_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( l1_orders_2(A)
=> ( ( v3_lattice3(A)
& ~ v3_struct_0(A) )
=> ( v2_lattice3(A)
& v1_lattice3(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C) )
=> ( ( v18_waybel_0(C,B,A)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [A,B,C] :
( ( m1_relset_1(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(C)
& l1_orders_2(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& l1_orders_2(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ( m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k2_waybel34(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A,B,C,D,E] :
( ( m1_relset_1(E,B,C)
& v1_funct_2(E,B,C)
& v1_funct_1(E)
& m1_relset_1(D,A,B)
& v1_funct_2(D,A,B)
& v1_funct_1(D)
& ~ v1_xboole_0(B) )
=> ( m2_relset_1(k7_funct_2(A,B,C,D,E),A,C)
& v1_funct_2(k7_funct_2(A,B,C,D,E),A,C)
& v1_funct_1(k7_funct_2(A,B,C,D,E)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( l1_orders_2(C)
& ~ v3_struct_0(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_1(E) )
=> ( ( v18_waybel_0(E,B,C)
& v18_waybel_0(D,A,B) )
=> v18_waybel_0(k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),A,C) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [A] :
( ( l1_orders_2(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( ( l1_orders_2(C)
& v4_orders_2(C)
& v3_orders_2(C)
& v2_orders_2(C)
& ~ v3_struct_0(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(F,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(F) )
=> ! [G] :
( ( m2_relset_1(G,u1_struct_0(C),u1_struct_0(B))
& v1_funct_2(G,u1_struct_0(C),u1_struct_0(B))
& v1_funct_1(G) )
=> ( ( v3_waybel_1(k1_waybel_1(B,C,E,G),B,C)
& v3_waybel_1(k1_waybel_1(A,B,D,F),A,B) )
=> v3_waybel_1(k1_waybel_1(A,C,k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),k7_funct_2(u1_struct_0(C),u1_struct_0(B),u1_struct_0(A),G,F)),A,C) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( k2_waybel34(C,A,k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E)) != k7_funct_2(u1_struct_0(C),u1_struct_0(B),u1_struct_0(A),k2_waybel34(C,B,E),k2_waybel34(B,A,D))
& m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
& v18_waybel_0(E,B,C)
& v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
& v1_funct_1(E) )
& m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(D,A,B)
& v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(D) )
& l1_orders_2(C)
& v3_lattice3(C)
& v2_lattice3(C)
& v1_lattice3(C)
& v4_orders_2(C)
& v3_orders_2(C)
& v2_orders_2(C) )
& l1_orders_2(B)
& v3_lattice3(B)
& v2_lattice3(B)
& v1_lattice3(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
& l1_orders_2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f119,plain,
( k2_waybel34(sK2_skl,sK0_skl,k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl)) != k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
& m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
& v18_waybel_0(sK4_skl,sK1_skl,sK2_skl)
& v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
& v1_funct_1(sK4_skl)
& m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v18_waybel_0(sK3_skl,sK0_skl,sK1_skl)
& v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v1_funct_1(sK3_skl)
& l1_orders_2(sK2_skl)
& v3_lattice3(sK2_skl)
& v2_lattice3(sK2_skl)
& v1_lattice3(sK2_skl)
& v4_orders_2(sK2_skl)
& v3_orders_2(sK2_skl)
& v2_orders_2(sK2_skl)
& l1_orders_2(sK1_skl)
& v3_lattice3(sK1_skl)
& v2_lattice3(sK1_skl)
& v1_lattice3(sK1_skl)
& v4_orders_2(sK1_skl)
& v3_orders_2(sK1_skl)
& v2_orders_2(sK1_skl)
& l1_orders_2(sK0_skl)
& v3_lattice3(sK0_skl)
& v2_lattice3(sK0_skl)
& v1_lattice3(sK0_skl)
& v4_orders_2(sK0_skl)
& v3_orders_2(sK0_skl)
& v2_orders_2(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl),skolemize(E,sK4_skl)],[f118]) ).
fof(f120,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f122,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f124,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f125,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f126,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f127,plain,
v2_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f128,plain,
v3_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f129,plain,
v4_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f131,plain,
v2_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f132,plain,
v3_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f133,plain,
l1_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f134,plain,
v2_orders_2(sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f135,plain,
v3_orders_2(sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f136,plain,
v4_orders_2(sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f138,plain,
v2_lattice3(sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f139,plain,
v3_lattice3(sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f140,plain,
l1_orders_2(sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f141,plain,
v1_funct_1(sK3_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f142,plain,
v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f143,plain,
v18_waybel_0(sK3_skl,sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f144,plain,
m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f145,plain,
v1_funct_1(sK4_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f146,plain,
v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f147,plain,
v18_waybel_0(sK4_skl,sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f148,plain,
m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f149,plain,
k2_waybel34(sK2_skl,sK0_skl,k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl)) != k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f227,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v1_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f228,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f254,plain,
! [A] :
( ( v2_lattice3(A)
& v1_lattice3(A)
& ~ v3_struct_0(A) )
| ~ v3_lattice3(A)
| v3_struct_0(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f256,plain,
! [X0] :
( v1_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f283,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f284,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f315,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( D = k2_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,D,C),A,B) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f316,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| D = k2_waybel34(A,B,C) )
& ( v3_waybel_1(k1_waybel_1(A,B,D,C),A,B)
| D != k2_waybel34(A,B,C) ) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ v18_waybel_0(C,B,A)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B) )
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(NNF_transformation,[status(thm)],[f315]) ).
fof(f317,plain,
! [X0,X1,X2,X3] :
( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 != k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
! [X0,X1,X2,X3] :
( ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 = k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f322,plain,
! [A,B,C] :
( ( m2_relset_1(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(k2_waybel34(A,B,C),u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(k2_waybel34(A,B,C)) )
| ~ m1_relset_1(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(C,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(C)
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v1_lattice3(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v1_lattice3(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f323,plain,
! [X0,X1,X2] :
( v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f324,plain,
! [X0,X1,X2] :
( v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f325,plain,
! [X0,X1,X2] :
( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f328,plain,
! [A,B,C,D,E] :
( ( m2_relset_1(k7_funct_2(A,B,C,D,E),A,C)
& v1_funct_2(k7_funct_2(A,B,C,D,E),A,C)
& v1_funct_1(k7_funct_2(A,B,C,D,E)) )
| ~ m1_relset_1(E,B,C)
| ~ v1_funct_2(E,B,C)
| ~ v1_funct_1(E)
| ~ m1_relset_1(D,A,B)
| ~ v1_funct_2(D,A,B)
| ~ v1_funct_1(D)
| v1_xboole_0(B) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f329,plain,
! [X0,X1,X2,X3,X4] :
( v1_funct_1(k7_funct_2(X2,X0,X4,X1,X3))
| ~ m1_relset_1(X3,X0,X4)
| ~ v1_funct_2(X3,X0,X4)
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X1,X2,X0)
| ~ v1_funct_2(X1,X2,X0)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f330,plain,
! [X0,X1,X2,X3,X4] :
( v1_funct_2(k7_funct_2(X2,X0,X4,X1,X3),X2,X4)
| ~ m1_relset_1(X3,X0,X4)
| ~ v1_funct_2(X3,X0,X4)
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X1,X2,X0)
| ~ v1_funct_2(X1,X2,X0)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f331,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k7_funct_2(X2,X0,X4,X1,X3),X2,X4)
| ~ m1_relset_1(X3,X0,X4)
| ~ v1_funct_2(X3,X0,X4)
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X1,X2,X0)
| ~ v1_funct_2(X1,X2,X0)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f332,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f333,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f388,plain,
! [A] :
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f389,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f524,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f106]) ).
fof(f525,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f524]) ).
fof(f526,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f525]) ).
fof(f527,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X0,X1,X2)
| m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f525]) ).
fof(f532,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( v18_waybel_0(k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),A,C)
| ~ v18_waybel_0(E,B,C)
| ~ v18_waybel_0(D,A,B)
| ~ m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
| ~ v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ l1_orders_2(C)
| v3_struct_0(C) )
| ~ l1_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f109]) ).
fof(f533,plain,
! [X0,X1,X2,X3,X4] :
( v18_waybel_0(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2)
| ~ v18_waybel_0(X4,X1,X2)
| ~ v18_waybel_0(X3,X0,X1)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f532]) ).
fof(f551,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ! [G] :
( v3_waybel_1(k1_waybel_1(A,C,k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E),k7_funct_2(u1_struct_0(C),u1_struct_0(B),u1_struct_0(A),G,F)),A,C)
| ~ v3_waybel_1(k1_waybel_1(B,C,E,G),B,C)
| ~ v3_waybel_1(k1_waybel_1(A,B,D,F),A,B)
| ~ m2_relset_1(G,u1_struct_0(C),u1_struct_0(B))
| ~ v1_funct_2(G,u1_struct_0(C),u1_struct_0(B))
| ~ v1_funct_1(G) )
| ~ m2_relset_1(F,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(F,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(F) )
| ~ m2_relset_1(E,u1_struct_0(B),u1_struct_0(C))
| ~ v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(D) )
| ~ l1_orders_2(C)
| ~ v4_orders_2(C)
| ~ v3_orders_2(C)
| ~ v2_orders_2(C)
| v3_struct_0(C) )
| ~ l1_orders_2(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| v3_struct_0(B) )
| ~ l1_orders_2(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f116]) ).
fof(f552,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( v3_waybel_1(k1_waybel_1(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5)),X0,X2)
| ~ v3_waybel_1(k1_waybel_1(X1,X2,X4,X6),X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X5),X0,X1)
| ~ m2_relset_1(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_2(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_1(X6)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v2_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f551]) ).
fof(f556,plain,
! [X0] :
( ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v1_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f256,f284]) ).
fof(f558,plain,
! [X0] :
( ~ v2_lattice3(X0)
| v1_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f556]) ).
fof(f563,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(resolution,[status(thm)],[f323,f526]) ).
fof(f573,plain,
( ~ v2_lattice3(sK2_skl)
| v1_lattice3(sK2_skl)
| ~ v3_lattice3(sK2_skl) ),
inference(resolution,[status(thm)],[f558,f140]) ).
fof(f574,plain,
( ~ v2_lattice3(sK1_skl)
| v1_lattice3(sK1_skl)
| ~ v3_lattice3(sK1_skl) ),
inference(resolution,[status(thm)],[f558,f133]) ).
fof(f575,plain,
( ~ v2_lattice3(sK0_skl)
| v1_lattice3(sK0_skl)
| ~ v3_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f558,f126]) ).
fof(f586,definition,
( sQ3_spl
<=> v3_lattice3(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( sQ3_spl
| ~ v3_lattice3(sK2_skl) ),
inference(component_clause,[status(thm)],[f586]) ).
fof(f589,definition,
( sQ4_spl
<=> v1_lattice3(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f592,definition,
( sQ5_spl
<=> v2_lattice3(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f594,plain,
( sQ5_spl
| ~ v2_lattice3(sK2_skl) ),
inference(component_clause,[status(thm)],[f592]) ).
fof(f595,plain,
( ~ sQ5_spl
| sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f573,f586,f589,f592]) ).
fof(f596,definition,
( sQ6_spl
<=> v3_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( sQ6_spl
| ~ v3_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f599,definition,
( sQ7_spl
<=> v1_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f602,definition,
( sQ8_spl
<=> v2_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ8_spl
| ~ v2_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f605,plain,
( ~ sQ8_spl
| sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f574,f596,f599,f602]) ).
fof(f606,definition,
( sQ9_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( sQ9_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f606]) ).
fof(f609,definition,
( sQ10_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f612,definition,
( sQ11_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f614,plain,
( sQ11_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( ~ sQ11_spl
| sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f575,f606,f609,f612]) ).
fof(f616,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f614,f124]) ).
fof(f617,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f618,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f608,f125]) ).
fof(f619,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f618]) ).
fof(f620,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f604,f131]) ).
fof(f621,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f620]) ).
fof(f622,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f132]) ).
fof(f623,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f622]) ).
fof(f624,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f594,f138]) ).
fof(f625,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f624]) ).
fof(f626,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f588,f139]) ).
fof(f627,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f626]) ).
fof(f740,plain,
( v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK2_skl)
| ~ v2_lattice3(sK2_skl)
| ~ v1_lattice3(sK2_skl)
| ~ v4_orders_2(sK2_skl)
| ~ v3_orders_2(sK2_skl)
| ~ v2_orders_2(sK2_skl) ),
inference(resolution,[status(thm)],[f563,f148]) ).
fof(f741,plain,
( v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f563,f144]) ).
fof(f745,definition,
( sQ12_spl
<=> v2_orders_2(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( sQ12_spl
| ~ v2_orders_2(sK2_skl) ),
inference(component_clause,[status(thm)],[f745]) ).
fof(f748,definition,
( sQ13_spl
<=> v3_orders_2(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f750,plain,
( sQ13_spl
| ~ v3_orders_2(sK2_skl) ),
inference(component_clause,[status(thm)],[f748]) ).
fof(f751,definition,
( sQ14_spl
<=> v4_orders_2(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( sQ14_spl
| ~ v4_orders_2(sK2_skl) ),
inference(component_clause,[status(thm)],[f751]) ).
fof(f754,definition,
( sQ15_spl
<=> l1_orders_2(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( sQ15_spl
| ~ l1_orders_2(sK2_skl) ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f757,definition,
( sQ16_spl
<=> v2_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f759,plain,
( sQ16_spl
| ~ v2_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f757]) ).
fof(f760,definition,
( sQ17_spl
<=> v3_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( sQ17_spl
| ~ v3_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f760]) ).
fof(f763,definition,
( sQ18_spl
<=> v4_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( sQ18_spl
| ~ v4_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f763]) ).
fof(f766,definition,
( sQ19_spl
<=> l1_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f768,plain,
( sQ19_spl
| ~ l1_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f766]) ).
fof(f769,definition,
( sQ20_spl
<=> v1_funct_1(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f771,plain,
( sQ20_spl
| ~ v1_funct_1(sK4_skl) ),
inference(component_clause,[status(thm)],[f769]) ).
fof(f772,definition,
( sQ21_spl
<=> v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f774,plain,
( sQ21_spl
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f775,definition,
( sQ22_spl
<=> v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f778,plain,
( sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f740,f745,f748,f751,f589,f592,f754,f757,f760,f763,f599,f602,f766,f769,f772,f775]) ).
fof(f779,definition,
( sQ23_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f781,plain,
( sQ23_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f779]) ).
fof(f782,definition,
( sQ24_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( sQ24_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f782]) ).
fof(f785,definition,
( sQ25_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( sQ25_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f785]) ).
fof(f788,definition,
( sQ26_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( sQ26_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f791,definition,
( sQ27_spl
<=> v1_funct_1(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f793,plain,
( sQ27_spl
| ~ v1_funct_1(sK3_skl) ),
inference(component_clause,[status(thm)],[f791]) ).
fof(f794,definition,
( sQ28_spl
<=> v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f796,plain,
( sQ28_spl
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,definition,
( sQ29_spl
<=> v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f741,f757,f760,f763,f599,f602,f766,f779,f782,f785,f609,f612,f788,f791,f794,f797]) ).
fof(f801,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f768,f133]) ).
fof(f802,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f801]) ).
fof(f803,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f765,f129]) ).
fof(f804,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f803]) ).
fof(f805,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f762,f128]) ).
fof(f806,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f805]) ).
fof(f807,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f127]) ).
fof(f808,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f807]) ).
fof(f809,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f142]) ).
fof(f810,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f809]) ).
fof(f811,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f793,f141]) ).
fof(f812,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f811]) ).
fof(f813,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f790,f126]) ).
fof(f814,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f813]) ).
fof(f815,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f787,f122]) ).
fof(f816,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f815]) ).
fof(f817,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f784,f121]) ).
fof(f818,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f817]) ).
fof(f819,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f120]) ).
fof(f820,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f819]) ).
fof(f828,definition,
( sQ30_spl
<=> v18_waybel_0(sK4_skl,sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f830,plain,
( sQ30_spl
| ~ v18_waybel_0(sK4_skl,sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f835,definition,
( sQ32_spl
<=> v18_waybel_0(sK3_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f837,plain,
( sQ32_spl
| ~ v18_waybel_0(sK3_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f835]) ).
fof(f842,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f774,f146]) ).
fof(f843,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f842]) ).
fof(f844,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f771,f145]) ).
fof(f845,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f844]) ).
fof(f846,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f756,f140]) ).
fof(f847,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f846]) ).
fof(f848,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f753,f136]) ).
fof(f849,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f848]) ).
fof(f850,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f135]) ).
fof(f851,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f850]) ).
fof(f852,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f747,f134]) ).
fof(f853,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f852]) ).
fof(f854,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f837,f143]) ).
fof(f855,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f854]) ).
fof(f856,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f830,f147]) ).
fof(f857,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f856]) ).
fof(f1223,definition,
( sQ61_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1224,plain,
( ~ sQ61_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f1223]) ).
fof(f1226,definition,
( sQ62_spl
<=> v3_struct_0(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1227,plain,
( ~ sQ62_spl
| v3_struct_0(sK2_skl) ),
inference(component_clause,[status(thm)],[f1226]) ).
fof(f1236,definition,
( sQ65_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1237,plain,
( ~ sQ65_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1236]) ).
fof(f1247,plain,
( ~ sQ61_spl
| ~ v1_lattice3(sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1224,f228]) ).
fof(f1249,plain,
( ~ sQ61_spl
| ~ sQ7_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1247,f766,f599,f1223]) ).
fof(f1270,plain,
( ~ sQ65_spl
| ~ v1_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1237,f228]) ).
fof(f1272,plain,
( ~ sQ65_spl
| ~ sQ10_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1270,f788,f609,f1236]) ).
fof(f1309,plain,
( ~ sQ62_spl
| ~ v1_lattice3(sK2_skl)
| ~ l1_orders_2(sK2_skl) ),
inference(resolution,[status(thm)],[f1227,f228]) ).
fof(f1311,plain,
( ~ sQ62_spl
| ~ sQ4_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1309,f754,f589,f1226]) ).
fof(f2309,plain,
! [X0,X1,X2,X3] :
( v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 != k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f317,f558]) ).
fof(f2334,plain,
! [X0,X1,X2,X3] :
( ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 = k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f318,f558]) ).
fof(f3250,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4) = k2_waybel34(X0,X2,k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4))
| ~ v18_waybel_0(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),X2,X0)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ l1_orders_2(X2)
| ~ v2_lattice3(X2)
| ~ v1_lattice3(X2)
| ~ v4_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v2_orders_2(X2)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_waybel_1(k1_waybel_1(X1,X2,X4,X6),X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X5),X0,X1)
| ~ m2_relset_1(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_2(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_1(X6)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v2_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f552,f2334]) ).
fof(f3251,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4) = k2_waybel34(X0,X2,k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4))
| ~ v18_waybel_0(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),X2,X0)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ v2_lattice3(X2)
| ~ v1_lattice3(X2)
| ~ v2_lattice3(X0)
| ~ v3_waybel_1(k1_waybel_1(X1,X2,X4,X6),X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X5),X0,X1)
| ~ m2_relset_1(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_2(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_1(X6)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v2_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3250]) ).
fof(f3252,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4) = k2_waybel34(X0,X2,k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4))
| ~ v18_waybel_0(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),X2,X0)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ v2_lattice3(X2)
| ~ v1_lattice3(X2)
| ~ v2_lattice3(X0)
| ~ v3_waybel_1(k1_waybel_1(X1,X2,X4,X6),X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X5),X0,X1)
| ~ m2_relset_1(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_2(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_1(X6)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v2_orders_2(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3251,f284]) ).
fof(f3253,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4) = k2_waybel34(X0,X2,k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4))
| ~ v18_waybel_0(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),X2,X0)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5),u1_struct_0(X2),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(X2),u1_struct_0(X1),u1_struct_0(X0),X6,X5))
| ~ v2_lattice3(X2)
| ~ v1_lattice3(X2)
| ~ v2_lattice3(X0)
| ~ v3_waybel_1(k1_waybel_1(X1,X2,X4,X6),X1,X2)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X5),X0,X1)
| ~ m2_relset_1(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_2(X6,u1_struct_0(X2),u1_struct_0(X1))
| ~ v1_funct_1(X6)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v2_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3252,f284]) ).
fof(f3254,plain,
( ~ m2_relset_1(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),u1_struct_0(sK2_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),u1_struct_0(sK2_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)))
| ~ v18_waybel_0(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),sK0_skl,sK2_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v3_lattice3(sK2_skl)
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),u1_struct_0(sK0_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),u1_struct_0(sK0_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl))
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v2_lattice3(sK2_skl)
| ~ v3_waybel_1(k1_waybel_1(sK1_skl,sK0_skl,k2_waybel34(sK1_skl,sK0_skl,sK3_skl),sK3_skl),sK1_skl,sK0_skl)
| ~ v3_waybel_1(k1_waybel_1(sK2_skl,sK1_skl,k2_waybel34(sK2_skl,sK1_skl,sK4_skl),sK4_skl),sK2_skl,sK1_skl)
| ~ m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| ~ m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
| ~ m2_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl))
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| ~ l1_orders_2(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(sK2_skl)
| ~ v4_orders_2(sK2_skl)
| ~ v3_orders_2(sK2_skl)
| ~ v2_orders_2(sK2_skl) ),
inference(resolution,[status(thm)],[f3253,f149]) ).
fof(f3255,definition,
( sQ95_spl
<=> v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f3257,plain,
( sQ95_spl
| ~ v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3255]) ).
fof(f3258,definition,
( sQ96_spl
<=> m2_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f3260,plain,
( sQ96_spl
| ~ m2_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3258]) ).
fof(f3261,definition,
( sQ97_spl
<=> v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f3263,plain,
( sQ97_spl
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3261]) ).
fof(f3264,definition,
( sQ98_spl
<=> m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f3266,plain,
( sQ98_spl
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3264]) ).
fof(f3267,definition,
( sQ99_spl
<=> m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f3269,plain,
( sQ99_spl
| ~ m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
inference(component_clause,[status(thm)],[f3267]) ).
fof(f3270,definition,
( sQ100_spl
<=> m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f3272,plain,
( sQ100_spl
| ~ m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3270]) ).
fof(f3273,definition,
( sQ101_spl
<=> v3_waybel_1(k1_waybel_1(sK2_skl,sK1_skl,k2_waybel34(sK2_skl,sK1_skl,sK4_skl),sK4_skl),sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f3275,plain,
( sQ101_spl
| ~ v3_waybel_1(k1_waybel_1(sK2_skl,sK1_skl,k2_waybel34(sK2_skl,sK1_skl,sK4_skl),sK4_skl),sK2_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f3273]) ).
fof(f3276,definition,
( sQ102_spl
<=> v3_waybel_1(k1_waybel_1(sK1_skl,sK0_skl,k2_waybel34(sK1_skl,sK0_skl,sK3_skl),sK3_skl),sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f3278,plain,
( sQ102_spl
| ~ v3_waybel_1(k1_waybel_1(sK1_skl,sK0_skl,k2_waybel34(sK1_skl,sK0_skl,sK3_skl),sK3_skl),sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f3276]) ).
fof(f3279,definition,
( sQ103_spl
<=> v1_funct_1(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f3281,plain,
( sQ103_spl
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f3279]) ).
fof(f3282,definition,
( sQ104_spl
<=> v1_funct_2(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),u1_struct_0(sK0_skl),u1_struct_0(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f3284,plain,
( sQ104_spl
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),u1_struct_0(sK0_skl),u1_struct_0(sK2_skl)) ),
inference(component_clause,[status(thm)],[f3282]) ).
fof(f3285,definition,
( sQ105_spl
<=> m2_relset_1(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),u1_struct_0(sK0_skl),u1_struct_0(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f3287,plain,
( sQ105_spl
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),u1_struct_0(sK0_skl),u1_struct_0(sK2_skl)) ),
inference(component_clause,[status(thm)],[f3285]) ).
fof(f3288,definition,
( sQ106_spl
<=> v18_waybel_0(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f3290,plain,
( sQ106_spl
| ~ v18_waybel_0(k7_funct_2(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl),u1_struct_0(sK2_skl),sK3_skl,sK4_skl),sK0_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f3288]) ).
fof(f3291,definition,
( sQ107_spl
<=> v1_funct_1(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f3293,plain,
( sQ107_spl
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl))) ),
inference(component_clause,[status(thm)],[f3291]) ).
fof(f3294,definition,
( sQ108_spl
<=> v1_funct_2(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),u1_struct_0(sK2_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f3296,plain,
( sQ108_spl
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),u1_struct_0(sK2_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3294]) ).
fof(f3297,definition,
( sQ109_spl
<=> m2_relset_1(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),u1_struct_0(sK2_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f3299,plain,
( sQ109_spl
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl),k2_waybel34(sK2_skl,sK1_skl,sK4_skl),k2_waybel34(sK1_skl,sK0_skl,sK3_skl)),u1_struct_0(sK2_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3297]) ).
fof(f3300,plain,
( ~ sQ109_spl
| ~ sQ108_spl
| ~ sQ107_spl
| ~ sQ106_spl
| ~ sQ9_spl
| ~ sQ3_spl
| ~ sQ105_spl
| ~ sQ104_spl
| ~ sQ103_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ5_spl
| ~ sQ102_spl
| ~ sQ101_spl
| ~ sQ100_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ99_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ98_spl
| ~ sQ97_spl
| ~ sQ29_spl
| ~ sQ96_spl
| ~ sQ95_spl
| ~ sQ22_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| sQ61_spl
| ~ sQ15_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f3254,f745,f748,f751,f754,f1223,f757,f760,f763,f766,f779,f782,f785,f788,f775,f3255,f3258,f797,f3261,f3264,f769,f772,f3267,f791,f794,f3270,f3273,f3276,f592,f609,f612,f3279,f3282,f3285,f586,f606,f3288,f3291,f3294,f3297]) ).
fof(f3301,plain,
( sQ109_spl
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
| ~ m1_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl))
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3299,f331]) ).
fof(f3302,definition,
( sQ110_spl
<=> v1_xboole_0(u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f3303,plain,
( ~ sQ110_spl
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3302]) ).
fof(f3305,definition,
( sQ111_spl
<=> m1_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f3306,plain,
( ~ sQ111_spl
| m1_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3305]) ).
fof(f3307,plain,
( sQ111_spl
| ~ m1_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3305]) ).
fof(f3308,definition,
( sQ112_spl
<=> m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f3309,plain,
( ~ sQ112_spl
| m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3308]) ).
fof(f3310,plain,
( sQ112_spl
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3308]) ).
fof(f3311,plain,
( sQ109_spl
| ~ sQ112_spl
| ~ sQ97_spl
| ~ sQ29_spl
| ~ sQ111_spl
| ~ sQ95_spl
| ~ sQ22_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f3301,f3302,f775,f3255,f3305,f797,f3261,f3308,f3297]) ).
fof(f3312,plain,
( sQ97_spl
| ~ m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f3263,f324]) ).
fof(f3313,definition,
( sQ113_spl
<=> m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f3315,plain,
( sQ113_spl
| ~ m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3313]) ).
fof(f3316,plain,
( sQ97_spl
| ~ sQ113_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f3312,f757,f760,f763,f599,f602,f766,f779,f782,f785,f609,f612,f788,f791,f794,f3313,f3261]) ).
fof(f3342,plain,
( sQ113_spl
| ~ m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3315,f526]) ).
fof(f3343,plain,
( sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3342,f144]) ).
fof(f3344,plain,
sQ113_spl,
inference(contradiction_clause,[status(thm)],[f3343]) ).
fof(f3345,plain,
( sQ95_spl
| ~ m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK2_skl)
| ~ v2_lattice3(sK2_skl)
| ~ v1_lattice3(sK2_skl)
| ~ v4_orders_2(sK2_skl)
| ~ v3_orders_2(sK2_skl)
| ~ v2_orders_2(sK2_skl) ),
inference(resolution,[status(thm)],[f3257,f324]) ).
fof(f3346,definition,
( sQ114_spl
<=> m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f3348,plain,
( sQ114_spl
| ~ m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
inference(component_clause,[status(thm)],[f3346]) ).
fof(f3349,plain,
( sQ95_spl
| ~ sQ114_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f3345,f745,f748,f751,f589,f592,f754,f757,f760,f763,f599,f602,f766,f769,f772,f3346,f3255]) ).
fof(f3350,plain,
( ~ sQ110_spl
| ~ l1_struct_0(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f3303,f389]) ).
fof(f3359,definition,
( sQ115_spl
<=> l1_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f3361,plain,
( sQ115_spl
| ~ l1_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f3359]) ).
fof(f3362,plain,
( ~ sQ110_spl
| ~ sQ115_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f3350,f1223,f3359,f3302]) ).
fof(f3363,plain,
( sQ115_spl
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f3361,f333]) ).
fof(f3364,plain,
( sQ115_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f3363,f766,f3359]) ).
fof(f3552,plain,
( sQ114_spl
| ~ m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl)) ),
inference(resolution,[status(thm)],[f3348,f526]) ).
fof(f3553,plain,
( sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3552,f148]) ).
fof(f3554,plain,
sQ114_spl,
inference(contradiction_clause,[status(thm)],[f3553]) ).
fof(f3655,plain,
( sQ108_spl
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
| ~ m1_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl))
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3296,f330]) ).
fof(f3656,plain,
( sQ108_spl
| ~ sQ112_spl
| ~ sQ97_spl
| ~ sQ29_spl
| ~ sQ111_spl
| ~ sQ95_spl
| ~ sQ22_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f3655,f3302,f775,f3255,f3305,f797,f3261,f3308,f3294]) ).
fof(f3670,plain,
( sQ112_spl
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f3310,f526]) ).
fof(f3698,plain,
( sQ107_spl
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
| ~ m1_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl))
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3293,f329]) ).
fof(f3699,plain,
( sQ107_spl
| ~ sQ112_spl
| ~ sQ97_spl
| ~ sQ29_spl
| ~ sQ111_spl
| ~ sQ95_spl
| ~ sQ22_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f3698,f3302,f775,f3255,f3305,f797,f3261,f3308,f3291]) ).
fof(f3700,plain,
( sQ111_spl
| ~ m2_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3307,f526]) ).
fof(f3701,plain,
( sQ112_spl
| ~ m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f3670,f325]) ).
fof(f3702,plain,
( sQ112_spl
| ~ sQ113_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f3701,f757,f760,f763,f599,f602,f766,f779,f782,f785,f609,f612,f788,f791,f794,f3313,f3308]) ).
fof(f3717,plain,
( sQ111_spl
| ~ m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK2_skl)
| ~ v2_lattice3(sK2_skl)
| ~ v1_lattice3(sK2_skl)
| ~ v4_orders_2(sK2_skl)
| ~ v3_orders_2(sK2_skl)
| ~ v2_orders_2(sK2_skl) ),
inference(resolution,[status(thm)],[f3700,f325]) ).
fof(f3718,plain,
( sQ111_spl
| ~ sQ114_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f3717,f745,f748,f751,f589,f592,f754,f757,f760,f763,f599,f602,f766,f769,f772,f3346,f3305]) ).
fof(f3719,plain,
( sQ106_spl
| ~ v18_waybel_0(sK4_skl,sK1_skl,sK2_skl)
| ~ v18_waybel_0(sK3_skl,sK0_skl,sK1_skl)
| ~ m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| ~ l1_orders_2(sK2_skl)
| v3_struct_0(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| v3_struct_0(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f3290,f533]) ).
fof(f3720,plain,
( sQ106_spl
| ~ sQ30_spl
| ~ sQ32_spl
| ~ sQ99_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ100_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ15_spl
| sQ62_spl
| ~ sQ19_spl
| sQ61_spl
| ~ sQ26_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f3719,f1236,f788,f1223,f766,f1226,f754,f791,f794,f3270,f769,f772,f3267,f835,f828,f3288]) ).
fof(f3721,plain,
( sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3269,f148]) ).
fof(f3722,plain,
sQ99_spl,
inference(contradiction_clause,[status(thm)],[f3721]) ).
fof(f3723,plain,
( sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3272,f144]) ).
fof(f3724,plain,
sQ100_spl,
inference(contradiction_clause,[status(thm)],[f3723]) ).
fof(f3923,plain,
( ~ sQ112_spl
| m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f3309,f527]) ).
fof(f4027,plain,
( sQ105_spl
| ~ m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3287,f331]) ).
fof(f4028,plain,
( sQ105_spl
| ~ sQ114_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ113_spl
| ~ sQ28_spl
| ~ sQ27_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f4027,f3302,f791,f794,f3313,f769,f772,f3346,f3285]) ).
fof(f4044,plain,
( ~ sQ111_spl
| m2_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3306,f527]) ).
fof(f4092,plain,
( sQ104_spl
| ~ m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3284,f330]) ).
fof(f4093,plain,
( sQ104_spl
| ~ sQ114_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ113_spl
| ~ sQ28_spl
| ~ sQ27_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f4092,f3302,f791,f794,f3313,f769,f772,f3346,f3282]) ).
fof(f4243,plain,
( sQ103_spl
| ~ m1_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ m1_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| v1_xboole_0(u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f3281,f329]) ).
fof(f4244,plain,
( sQ103_spl
| ~ sQ114_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ113_spl
| ~ sQ28_spl
| ~ sQ27_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f4243,f3302,f791,f794,f3313,f769,f772,f3346,f3279]) ).
fof(f4260,plain,
( sQ102_spl
| k2_waybel34(sK1_skl,sK0_skl,sK3_skl) != k2_waybel34(sK1_skl,sK0_skl,sK3_skl)
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK3_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK3_skl))
| ~ v18_waybel_0(sK3_skl,sK0_skl,sK1_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v3_lattice3(sK1_skl)
| ~ m2_relset_1(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK3_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK3_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f3278,f2309]) ).
fof(f4261,definition,
( sQ161_spl
<=> k2_waybel34(sK1_skl,sK0_skl,sK3_skl) = k2_waybel34(sK1_skl,sK0_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f4263,plain,
( sQ161_spl
| k2_waybel34(sK1_skl,sK0_skl,sK3_skl) != k2_waybel34(sK1_skl,sK0_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f4261]) ).
fof(f4264,plain,
( sQ102_spl
| ~ sQ161_spl
| ~ sQ98_spl
| ~ sQ97_spl
| ~ sQ29_spl
| ~ sQ32_spl
| ~ sQ9_spl
| ~ sQ6_spl
| ~ sQ100_spl
| ~ sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ25_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f4260,f757,f760,f763,f602,f766,f779,f782,f785,f609,f612,f788,f791,f794,f3270,f596,f606,f835,f797,f3261,f3264,f4261,f3276]) ).
fof(f4265,plain,
( sQ98_spl
| ~ sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3266,f3923]) ).
fof(f4266,plain,
( sQ98_spl
| ~ sQ112_spl ),
inference(contradiction_clause,[status(thm)],[f4265]) ).
fof(f4267,plain,
( sQ161_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4263]) ).
fof(f4268,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f4267]) ).
fof(f4269,plain,
( sQ96_spl
| ~ sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3260,f4044]) ).
fof(f4270,plain,
( sQ96_spl
| ~ sQ111_spl ),
inference(contradiction_clause,[status(thm)],[f4269]) ).
fof(f4273,plain,
( sQ101_spl
| k2_waybel34(sK2_skl,sK1_skl,sK4_skl) != k2_waybel34(sK2_skl,sK1_skl,sK4_skl)
| ~ m2_relset_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(k2_waybel34(sK2_skl,sK1_skl,sK4_skl),u1_struct_0(sK2_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(k2_waybel34(sK2_skl,sK1_skl,sK4_skl))
| ~ v18_waybel_0(sK4_skl,sK1_skl,sK2_skl)
| ~ v3_lattice3(sK1_skl)
| ~ v3_lattice3(sK2_skl)
| ~ m2_relset_1(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_2(sK4_skl,u1_struct_0(sK1_skl),u1_struct_0(sK2_skl))
| ~ v1_funct_1(sK4_skl)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK2_skl)
| ~ v2_lattice3(sK2_skl)
| ~ v4_orders_2(sK2_skl)
| ~ v3_orders_2(sK2_skl)
| ~ v2_orders_2(sK2_skl) ),
inference(resolution,[status(thm)],[f3275,f2309]) ).
fof(f4274,definition,
( sQ162_spl
<=> k2_waybel34(sK2_skl,sK1_skl,sK4_skl) = k2_waybel34(sK2_skl,sK1_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f4276,plain,
( sQ162_spl
| k2_waybel34(sK2_skl,sK1_skl,sK4_skl) != k2_waybel34(sK2_skl,sK1_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f4274]) ).
fof(f4277,plain,
( sQ101_spl
| ~ sQ162_spl
| ~ sQ96_spl
| ~ sQ95_spl
| ~ sQ22_spl
| ~ sQ30_spl
| ~ sQ6_spl
| ~ sQ3_spl
| ~ sQ99_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ18_spl
| ~ sQ17_spl
| ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ5_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f4273,f745,f748,f751,f592,f754,f757,f760,f763,f599,f602,f766,f769,f772,f3267,f586,f596,f828,f775,f3255,f3258,f4274,f3273]) ).
fof(f4278,plain,
( sQ162_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4276]) ).
fof(f4279,plain,
sQ162_spl,
inference(contradiction_clause,[status(thm)],[f4278]) ).
fof(f4280,plain,
$false,
inference(sat_refutation,[status(thm)],[f595,f605,f615,f617,f619,f621,f623,f625,f627,f778,f800,f802,f804,f806,f808,f810,f812,f814,f816,f818,f820,f843,f845,f847,f849,f851,f853,f855,f857,f1249,f1272,f1311,f3300,f3311,f3316,f3344,f3349,f3362,f3364,f3554,f3656,f3699,f3702,f3718,f3720,f3722,f3724,f4028,f4093,f4244,f4264,f4266,f4268,f4270,f4277,f4279]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT358+1 : 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 : n019.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 : Sun Sep 20 23:48:50 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 3.82/0.98 % Refutation found
% 3.82/0.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.82/0.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.13/1.01 % Elapsed time: 0.637114 seconds
% 1.13/1.01 % CPU time: 4.694393 seconds
% 1.13/1.01 % Total memory used: 186.684 MB
% 1.13/1.01 % Net memory used: 184.284 MB
%------------------------------------------------------------------------------