%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT355+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 : n015.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:54 PM UTC 2026
% Result : Theorem 70.45s 9.46s
% Output : CNFRefutation 57.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 168
% Syntax : Number of formulae : 755 ( 214 unt; 136 def)
% Number of atoms : 2875 ( 54 equ)
% Maximal formula atoms : 43 ( 3 avg)
% Number of connectives : 3451 (1331 ~;1378 |; 559 &)
% ( 143 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 181 ( 179 usr; 137 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 18 con; 0-4 aty)
% Number of variables : 216 ( 198 !; 18 ?)
% 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] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> k1_waybel34(k7_lattice3(A),k7_lattice3(B),k3_waybel34(A,B,C)) = k2_waybel34(B,A,C) ) ) ),
file('/export/starexec/sandbox2/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] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> k1_waybel34(k7_lattice3(A),k7_lattice3(B),k3_waybel34(A,B,C)) = k2_waybel34(B,A,C) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f23,axiom,
! [A] :
( l1_orders_2(A)
=> ( v1_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,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(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( ( v17_waybel_0(C,A,B)
& v3_lattice3(B)
& v3_lattice3(A) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(D) )
=> ( D = k1_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [A] :
( l1_orders_2(A)
=> ! [B] :
( l1_orders_2(B)
=> ! [C] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> k3_waybel34(A,B,C) = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A,B,C] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C)
& l1_orders_2(B)
& l1_orders_2(A) )
=> ( m2_relset_1(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_2(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_1(k3_waybel34(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,axiom,
! [A] :
( l1_orders_2(A)
=> ( l1_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,axiom,
? [A] : l1_orders_2(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_orders_2(A) )
=> ( v2_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [A] :
( ( l1_orders_2(A)
& v3_orders_2(A) )
=> ( v3_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,axiom,
! [A] :
( ( l1_orders_2(A)
& v4_orders_2(A) )
=> ( v4_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [A,B,C] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(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) )
=> ( v5_orders_3(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v4_waybel_1(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v21_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v19_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v17_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v1_partfun1(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_2(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& ~ v1_xboole_0(k3_waybel34(A,B,C))
& v1_funct_1(k3_waybel34(A,B,C))
& v1_relat_1(k3_waybel34(A,B,C)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [A] :
( ( l1_orders_2(A)
& v3_lattice3(A)
& ~ v3_struct_0(A) )
=> ( v3_yellow_0(k7_lattice3(A))
& v2_yellow_0(k7_lattice3(A))
& v1_yellow_0(k7_lattice3(A))
& v3_lattice3(k7_lattice3(A))
& v2_lattice3(k7_lattice3(A))
& v1_lattice3(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,axiom,
? [A] :
( v16_waybel_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,axiom,
? [A] :
( v25_waybel_0(A)
& v24_waybel_0(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,axiom,
? [A] :
( v3_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,axiom,
? [A] :
( v3_realset2(A)
& v11_waybel_1(A)
& v10_waybel_1(A)
& v9_waybel_1(A)
& v2_waybel_1(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& ~ v1_yellow_3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v16_waybel_0(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
? [A] :
( v25_waybel_0(A)
& v24_waybel_0(A)
& v16_waybel_0(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,axiom,
? [A] :
( v3_waybel_8(A)
& v2_waybel_8(A)
& v1_waybel_8(A)
& v3_realset2(A)
& v3_waybel_3(A)
& v2_waybel_3(A)
& v11_waybel_1(A)
& v10_waybel_1(A)
& v9_waybel_1(A)
& v2_waybel_1(A)
& ~ v1_yellow_3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v16_waybel_0(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
? [A] :
( v3_realset2(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,axiom,
? [A] :
( v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,axiom,
? [A] :
( v2_waybel_2(A)
& v1_waybel_2(A)
& v3_realset2(A)
& v11_waybel_1(A)
& v10_waybel_1(A)
& v9_waybel_1(A)
& v2_waybel_1(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& ~ v1_yellow_3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v16_waybel_0(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
? [A] :
( v3_waybel_3(A)
& v2_waybel_3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,axiom,
? [A] :
( v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v3_lattice3(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,axiom,
? [A] :
( v2_funct_1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
? [A] :
( v11_waybel_1(A)
& v10_waybel_1(A)
& v9_waybel_1(A)
& v2_waybel_1(A)
& v3_yellow_0(A)
& v2_yellow_0(A)
& v1_yellow_0(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,axiom,
? [A] :
( v9_waybel_1(A)
& v2_waybel_1(A)
& v2_yellow_0(A)
& v2_lattice3(A)
& v1_lattice3(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& v1_orders_2(A)
& ~ v3_struct_0(A)
& l1_orders_2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,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] :
( ( m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_2(E,u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,u1_struct_0(k7_lattice3(B)),u1_struct_0(k7_lattice3(A)))
& v1_funct_2(F,u1_struct_0(k7_lattice3(B)),u1_struct_0(k7_lattice3(A)))
& v1_funct_1(F) )
=> ( ( D = F
& C = E )
=> ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
<=> v3_waybel_1(k1_waybel_1(k7_lattice3(B),k7_lattice3(A),F,E),k7_lattice3(B),k7_lattice3(A)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_waybel34(k7_lattice3(A),k7_lattice3(B),k3_waybel34(A,B,C)) != k2_waybel34(B,A,C)
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v18_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(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(f200,plain,
( k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),k3_waybel34(sK0_skl,sK1_skl,sK2_skl)) != k2_waybel34(sK1_skl,sK0_skl,sK2_skl)
& m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v18_waybel_0(sK2_skl,sK0_skl,sK1_skl)
& v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v1_funct_1(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]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f199]) ).
fof(f201,plain,
v2_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
v3_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
v4_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f204,plain,
v1_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f205,plain,
v2_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f206,plain,
v3_lattice3(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f207,plain,
l1_orders_2(sK0_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f208,plain,
v2_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f209,plain,
v3_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f210,plain,
v4_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f211,plain,
v1_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f212,plain,
v2_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f213,plain,
v3_lattice3(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f214,plain,
l1_orders_2(sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f215,plain,
v1_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f216,plain,
v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f217,plain,
v18_waybel_0(sK2_skl,sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f218,plain,
m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f219,plain,
k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),k3_waybel34(sK0_skl,sK1_skl,sK2_skl)) != k2_waybel34(sK1_skl,sK0_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f309,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v1_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f310,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v1_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f309]) ).
fof(f354,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)],[f33]) ).
fof(f357,plain,
! [X0] :
( v2_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f383,plain,
! [A] :
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f384,plain,
! [X0] :
( ~ v3_struct_0(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f586,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( D = k1_waybel34(A,B,C)
<=> v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ 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)],[f72]) ).
fof(f587,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| D = k1_waybel34(A,B,C) )
& ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
| D != k1_waybel34(A,B,C) ) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ v17_waybel_0(C,A,B)
| ~ v3_lattice3(B)
| ~ v3_lattice3(A)
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ 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)],[f586]) ).
fof(f589,plain,
! [X0,X1,X2,X3] :
( ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| X3 = k1_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f587]) ).
fof(f590,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)],[f73]) ).
fof(f591,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)],[f590]) ).
fof(f592,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)],[f591]) ).
fof(f594,plain,
! [A] :
( ! [B] :
( ! [C] :
( k3_waybel34(A,B,C) = C
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C) )
| ~ l1_orders_2(B) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f595,plain,
! [X0,X1,X2] :
( k3_waybel34(X0,X1,X2) = X2
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f594]) ).
fof(f608,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)],[f84]) ).
fof(f609,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)],[f608]) ).
fof(f610,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)],[f608]) ).
fof(f611,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)],[f608]) ).
fof(f612,plain,
! [A,B,C] :
( ( m2_relset_1(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_2(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_1(k3_waybel34(A,B,C)) )
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ l1_orders_2(B)
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f614,plain,
! [X0,X1,X2] :
( v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f612]) ).
fof(f615,plain,
! [X0,X1,X2] :
( m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f612]) ).
fof(f620,plain,
! [A] :
( ( l1_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f622,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f629,plain,
l1_orders_2(sK3_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f99]) ).
fof(f630,plain,
l1_orders_2(sK3_skl),
inference(cnf_transformation,[status(thm)],[f629]) ).
fof(f738,plain,
! [A] :
( ( v2_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v2_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f122]) ).
fof(f740,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f738]) ).
fof(f765,plain,
! [A] :
( ( v3_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v3_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f127]) ).
fof(f767,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f765]) ).
fof(f785,plain,
! [A] :
( ( v4_orders_2(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v4_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f131]) ).
fof(f787,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f785]) ).
fof(f788,plain,
! [A,B,C] :
( ( v5_orders_3(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v4_waybel_1(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v21_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v19_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v17_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v1_partfun1(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& v1_funct_2(k3_waybel34(A,B,C),u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
& ~ v1_xboole_0(k3_waybel34(A,B,C))
& v1_funct_1(k3_waybel34(A,B,C))
& v1_relat_1(k3_waybel34(A,B,C)) )
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v18_waybel_0(C,A,B)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(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)],[f132]) ).
fof(f794,plain,
! [X0,X1,X2] :
( v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f788]) ).
fof(f840,plain,
! [A] :
( ( v3_yellow_0(k7_lattice3(A))
& v2_yellow_0(k7_lattice3(A))
& v1_yellow_0(k7_lattice3(A))
& v3_lattice3(k7_lattice3(A))
& v2_lattice3(k7_lattice3(A))
& v1_lattice3(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v3_lattice3(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f144]) ).
fof(f843,plain,
! [X0] :
( v1_lattice3(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f840]) ).
fof(f845,plain,
! [X0] :
( v3_lattice3(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f840]) ).
fof(f889,plain,
( v16_waybel_0(sK10_skl)
& v4_orders_2(sK10_skl)
& v3_orders_2(sK10_skl)
& v2_orders_2(sK10_skl)
& ~ v3_struct_0(sK10_skl)
& l1_orders_2(sK10_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f155]) ).
fof(f890,plain,
l1_orders_2(sK10_skl),
inference(cnf_transformation,[status(thm)],[f889]) ).
fof(f891,plain,
~ v3_struct_0(sK10_skl),
inference(cnf_transformation,[status(thm)],[f889]) ).
fof(f892,plain,
v2_orders_2(sK10_skl),
inference(cnf_transformation,[status(thm)],[f889]) ).
fof(f893,plain,
v3_orders_2(sK10_skl),
inference(cnf_transformation,[status(thm)],[f889]) ).
fof(f894,plain,
v4_orders_2(sK10_skl),
inference(cnf_transformation,[status(thm)],[f889]) ).
fof(f895,plain,
v16_waybel_0(sK10_skl),
inference(cnf_transformation,[status(thm)],[f889]) ).
fof(f896,plain,
( v25_waybel_0(sK11_skl)
& v24_waybel_0(sK11_skl)
& v3_yellow_0(sK11_skl)
& v2_yellow_0(sK11_skl)
& v1_yellow_0(sK11_skl)
& v3_lattice3(sK11_skl)
& v2_lattice3(sK11_skl)
& v1_lattice3(sK11_skl)
& v4_orders_2(sK11_skl)
& v3_orders_2(sK11_skl)
& v2_orders_2(sK11_skl)
& v1_orders_2(sK11_skl)
& ~ v3_struct_0(sK11_skl)
& l1_orders_2(sK11_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f156]) ).
fof(f898,plain,
~ v3_struct_0(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f900,plain,
v2_orders_2(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f901,plain,
v3_orders_2(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f902,plain,
v4_orders_2(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f903,plain,
v1_lattice3(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f904,plain,
v2_lattice3(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f905,plain,
v3_lattice3(sK11_skl),
inference(cnf_transformation,[status(thm)],[f896]) ).
fof(f917,plain,
( v3_lattice3(sK14_skl)
& v4_orders_2(sK14_skl)
& v3_orders_2(sK14_skl)
& v2_orders_2(sK14_skl)
& v1_orders_2(sK14_skl)
& ~ v3_struct_0(sK14_skl)
& l1_orders_2(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f159]) ).
fof(f919,plain,
~ v3_struct_0(sK14_skl),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f921,plain,
v2_orders_2(sK14_skl),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f922,plain,
v3_orders_2(sK14_skl),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f923,plain,
v4_orders_2(sK14_skl),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f924,plain,
v3_lattice3(sK14_skl),
inference(cnf_transformation,[status(thm)],[f917]) ).
fof(f966,plain,
( v3_realset2(sK22_skl)
& v11_waybel_1(sK22_skl)
& v10_waybel_1(sK22_skl)
& v9_waybel_1(sK22_skl)
& v2_waybel_1(sK22_skl)
& v3_lattice3(sK22_skl)
& v2_lattice3(sK22_skl)
& v1_lattice3(sK22_skl)
& ~ v1_yellow_3(sK22_skl)
& v25_waybel_0(sK22_skl)
& v24_waybel_0(sK22_skl)
& v16_waybel_0(sK22_skl)
& v3_yellow_0(sK22_skl)
& v2_yellow_0(sK22_skl)
& v1_yellow_0(sK22_skl)
& v4_orders_2(sK22_skl)
& v3_orders_2(sK22_skl)
& v2_orders_2(sK22_skl)
& v1_orders_2(sK22_skl)
& ~ v3_struct_0(sK22_skl)
& l1_orders_2(sK22_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f167]) ).
fof(f975,plain,
v3_yellow_0(sK22_skl),
inference(cnf_transformation,[status(thm)],[f966]) ).
fof(f982,plain,
v3_lattice3(sK22_skl),
inference(cnf_transformation,[status(thm)],[f966]) ).
fof(f988,plain,
( v25_waybel_0(sK23_skl)
& v24_waybel_0(sK23_skl)
& v16_waybel_0(sK23_skl)
& v3_yellow_0(sK23_skl)
& v2_yellow_0(sK23_skl)
& v1_yellow_0(sK23_skl)
& v3_lattice3(sK23_skl)
& v2_lattice3(sK23_skl)
& v1_lattice3(sK23_skl)
& v4_orders_2(sK23_skl)
& v3_orders_2(sK23_skl)
& v2_orders_2(sK23_skl)
& ~ v3_struct_0(sK23_skl)
& l1_orders_2(sK23_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f168]) ).
fof(f989,plain,
l1_orders_2(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f990,plain,
~ v3_struct_0(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f991,plain,
v2_orders_2(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f992,plain,
v3_orders_2(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f993,plain,
v4_orders_2(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f994,plain,
v1_lattice3(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f995,plain,
v2_lattice3(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f996,plain,
v3_lattice3(sK23_skl),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f1003,plain,
( v3_waybel_8(sK24_skl)
& v2_waybel_8(sK24_skl)
& v1_waybel_8(sK24_skl)
& v3_realset2(sK24_skl)
& v3_waybel_3(sK24_skl)
& v2_waybel_3(sK24_skl)
& v11_waybel_1(sK24_skl)
& v10_waybel_1(sK24_skl)
& v9_waybel_1(sK24_skl)
& v2_waybel_1(sK24_skl)
& ~ v1_yellow_3(sK24_skl)
& v25_waybel_0(sK24_skl)
& v24_waybel_0(sK24_skl)
& v16_waybel_0(sK24_skl)
& v3_yellow_0(sK24_skl)
& v2_yellow_0(sK24_skl)
& v1_yellow_0(sK24_skl)
& v3_lattice3(sK24_skl)
& v2_lattice3(sK24_skl)
& v1_lattice3(sK24_skl)
& v4_orders_2(sK24_skl)
& v3_orders_2(sK24_skl)
& v2_orders_2(sK24_skl)
& v1_orders_2(sK24_skl)
& ~ v3_struct_0(sK24_skl)
& l1_orders_2(sK24_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(A,sK24_skl)],[f169]) ).
fof(f1004,plain,
l1_orders_2(sK24_skl),
inference(cnf_transformation,[status(thm)],[f1003]) ).
fof(f1005,plain,
~ v3_struct_0(sK24_skl),
inference(cnf_transformation,[status(thm)],[f1003]) ).
fof(f1012,plain,
v3_lattice3(sK24_skl),
inference(cnf_transformation,[status(thm)],[f1003]) ).
fof(f1015,plain,
v3_yellow_0(sK24_skl),
inference(cnf_transformation,[status(thm)],[f1003]) ).
fof(f1030,plain,
( v3_realset2(sK25_skl)
& v3_lattice3(sK25_skl)
& v2_lattice3(sK25_skl)
& v1_lattice3(sK25_skl)
& v4_orders_2(sK25_skl)
& v3_orders_2(sK25_skl)
& v2_orders_2(sK25_skl)
& v1_orders_2(sK25_skl)
& ~ v3_struct_0(sK25_skl)
& l1_orders_2(sK25_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(A,sK25_skl)],[f170]) ).
fof(f1031,plain,
l1_orders_2(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1032,plain,
~ v3_struct_0(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1034,plain,
v2_orders_2(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1035,plain,
v3_orders_2(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1036,plain,
v4_orders_2(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1037,plain,
v1_lattice3(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1038,plain,
v2_lattice3(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1039,plain,
v3_lattice3(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1040,plain,
v3_realset2(sK25_skl),
inference(cnf_transformation,[status(thm)],[f1030]) ).
fof(f1045,plain,
( v3_lattice3(sK27_skl)
& v2_lattice3(sK27_skl)
& v1_lattice3(sK27_skl)
& v4_orders_2(sK27_skl)
& v3_orders_2(sK27_skl)
& v2_orders_2(sK27_skl)
& v1_orders_2(sK27_skl)
& ~ v3_struct_0(sK27_skl)
& l1_orders_2(sK27_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(A,sK27_skl)],[f172]) ).
fof(f1046,plain,
l1_orders_2(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1047,plain,
~ v3_struct_0(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1049,plain,
v2_orders_2(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1050,plain,
v3_orders_2(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1051,plain,
v4_orders_2(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1052,plain,
v1_lattice3(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1053,plain,
v2_lattice3(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1054,plain,
v3_lattice3(sK27_skl),
inference(cnf_transformation,[status(thm)],[f1045]) ).
fof(f1062,plain,
( v2_waybel_2(sK29_skl)
& v1_waybel_2(sK29_skl)
& v3_realset2(sK29_skl)
& v11_waybel_1(sK29_skl)
& v10_waybel_1(sK29_skl)
& v9_waybel_1(sK29_skl)
& v2_waybel_1(sK29_skl)
& v3_lattice3(sK29_skl)
& v2_lattice3(sK29_skl)
& v1_lattice3(sK29_skl)
& ~ v1_yellow_3(sK29_skl)
& v25_waybel_0(sK29_skl)
& v24_waybel_0(sK29_skl)
& v16_waybel_0(sK29_skl)
& v3_yellow_0(sK29_skl)
& v2_yellow_0(sK29_skl)
& v1_yellow_0(sK29_skl)
& v4_orders_2(sK29_skl)
& v3_orders_2(sK29_skl)
& v2_orders_2(sK29_skl)
& v1_orders_2(sK29_skl)
& ~ v3_struct_0(sK29_skl)
& l1_orders_2(sK29_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f174]) ).
fof(f1063,plain,
l1_orders_2(sK29_skl),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f1064,plain,
~ v3_struct_0(sK29_skl),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f1071,plain,
v3_yellow_0(sK29_skl),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f1072,plain,
v16_waybel_0(sK29_skl),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f1078,plain,
v3_lattice3(sK29_skl),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f1086,plain,
( v3_waybel_3(sK30_skl)
& v2_waybel_3(sK30_skl)
& v25_waybel_0(sK30_skl)
& v24_waybel_0(sK30_skl)
& v3_yellow_0(sK30_skl)
& v2_yellow_0(sK30_skl)
& v1_yellow_0(sK30_skl)
& v3_lattice3(sK30_skl)
& v2_lattice3(sK30_skl)
& v1_lattice3(sK30_skl)
& v4_orders_2(sK30_skl)
& v3_orders_2(sK30_skl)
& v2_orders_2(sK30_skl)
& v1_orders_2(sK30_skl)
& ~ v3_struct_0(sK30_skl)
& l1_orders_2(sK30_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(A,sK30_skl)],[f175]) ).
fof(f1087,plain,
l1_orders_2(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1088,plain,
~ v3_struct_0(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1090,plain,
v2_orders_2(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1091,plain,
v3_orders_2(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1092,plain,
v4_orders_2(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1093,plain,
v1_lattice3(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1094,plain,
v2_lattice3(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1095,plain,
v3_lattice3(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1103,plain,
( v3_yellow_0(sK31_skl)
& v2_yellow_0(sK31_skl)
& v1_yellow_0(sK31_skl)
& v3_lattice3(sK31_skl)
& v2_lattice3(sK31_skl)
& v1_lattice3(sK31_skl)
& v4_orders_2(sK31_skl)
& v3_orders_2(sK31_skl)
& v2_orders_2(sK31_skl)
& ~ v3_struct_0(sK31_skl)
& l1_orders_2(sK31_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl]),skolemize(A,sK31_skl)],[f176]) ).
fof(f1104,plain,
l1_orders_2(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1105,plain,
~ v3_struct_0(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1106,plain,
v2_orders_2(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1107,plain,
v3_orders_2(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1108,plain,
v4_orders_2(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1109,plain,
v1_lattice3(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1110,plain,
v2_lattice3(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1111,plain,
v3_lattice3(sK31_skl),
inference(cnf_transformation,[status(thm)],[f1103]) ).
fof(f1120,plain,
( v2_funct_1(sK33_skl)
& v1_funct_1(sK33_skl)
& v1_relat_1(sK33_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(A,sK33_skl)],[f178]) ).
fof(f1121,plain,
v1_relat_1(sK33_skl),
inference(cnf_transformation,[status(thm)],[f1120]) ).
fof(f1122,plain,
v1_funct_1(sK33_skl),
inference(cnf_transformation,[status(thm)],[f1120]) ).
fof(f1143,plain,
( v11_waybel_1(sK37_skl)
& v10_waybel_1(sK37_skl)
& v9_waybel_1(sK37_skl)
& v2_waybel_1(sK37_skl)
& v3_yellow_0(sK37_skl)
& v2_yellow_0(sK37_skl)
& v1_yellow_0(sK37_skl)
& v2_lattice3(sK37_skl)
& v1_lattice3(sK37_skl)
& v4_orders_2(sK37_skl)
& v3_orders_2(sK37_skl)
& v2_orders_2(sK37_skl)
& v1_orders_2(sK37_skl)
& ~ v3_struct_0(sK37_skl)
& l1_orders_2(sK37_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl]),skolemize(A,sK37_skl)],[f182]) ).
fof(f1144,plain,
l1_orders_2(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1145,plain,
~ v3_struct_0(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1152,plain,
v1_yellow_0(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1154,plain,
v3_yellow_0(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1157,plain,
v10_waybel_1(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1174,plain,
( v9_waybel_1(sK40_skl)
& v2_waybel_1(sK40_skl)
& v2_yellow_0(sK40_skl)
& v2_lattice3(sK40_skl)
& v1_lattice3(sK40_skl)
& v4_orders_2(sK40_skl)
& v3_orders_2(sK40_skl)
& v2_orders_2(sK40_skl)
& v1_orders_2(sK40_skl)
& ~ v3_struct_0(sK40_skl)
& l1_orders_2(sK40_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(A,sK40_skl)],[f185]) ).
fof(f1175,plain,
l1_orders_2(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1176,plain,
~ v3_struct_0(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1178,plain,
v2_orders_2(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1179,plain,
v3_orders_2(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1180,plain,
v4_orders_2(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1181,plain,
v1_lattice3(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1182,plain,
v2_lattice3(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1183,plain,
v2_yellow_0(sK40_skl),
inference(cnf_transformation,[status(thm)],[f1174]) ).
fof(f1190,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)],[f188]) ).
fof(f1191,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)],[f1190]) ).
fof(f1192,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1191]) ).
fof(f1204,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( v3_waybel_1(k1_waybel_1(A,B,C,D),A,B)
<=> v3_waybel_1(k1_waybel_1(k7_lattice3(B),k7_lattice3(A),F,E),k7_lattice3(B),k7_lattice3(A)) )
| D != F
| C != E
| ~ m2_relset_1(F,u1_struct_0(k7_lattice3(B)),u1_struct_0(k7_lattice3(A)))
| ~ v1_funct_2(F,u1_struct_0(k7_lattice3(B)),u1_struct_0(k7_lattice3(A)))
| ~ v1_funct_1(F) )
| ~ m2_relset_1(E,u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
| ~ v1_funct_2(E,u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(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)],[f193]) ).
fof(f1205,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( ( ~ v3_waybel_1(k1_waybel_1(k7_lattice3(B),k7_lattice3(A),F,E),k7_lattice3(B),k7_lattice3(A))
| v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) )
& ( v3_waybel_1(k1_waybel_1(k7_lattice3(B),k7_lattice3(A),F,E),k7_lattice3(B),k7_lattice3(A))
| ~ v3_waybel_1(k1_waybel_1(A,B,C,D),A,B) ) )
| D != F
| C != E
| ~ m2_relset_1(F,u1_struct_0(k7_lattice3(B)),u1_struct_0(k7_lattice3(A)))
| ~ v1_funct_2(F,u1_struct_0(k7_lattice3(B)),u1_struct_0(k7_lattice3(A)))
| ~ v1_funct_1(F) )
| ~ m2_relset_1(E,u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
| ~ v1_funct_2(E,u1_struct_0(k7_lattice3(A)),u1_struct_0(k7_lattice3(B)))
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_2(D,u1_struct_0(B),u1_struct_0(A))
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(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(NNF_transformation,[status(thm)],[f1204]) ).
fof(f1206,plain,
! [X0,X1,X2,X3,X4,X5] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| X3 != X5
| X2 != X4
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(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)],[f1205]) ).
fof(f1223,plain,
! [X0,X1,X2] :
( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ 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(destructive_equality_resolution,[status(thm)],[f592]) ).
fof(f1224,plain,
! [X0,X1,X4,X5] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X5,X4),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X4,X5),X0,X1)
| ~ m2_relset_1(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X5,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X4,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X4)
| ~ 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(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ 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(destructive_equality_resolution,[status(thm)],[f1206]) ).
fof(f1225,plain,
! [X0,X1,X2,X3] :
( v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X3,X2),k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(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)],[f1224]) ).
fof(f1228,plain,
! [X0,X1] :
( k3_waybel34(X0,X1,sK2_skl) = sK2_skl
| ~ m2_relset_1(sK2_skl,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK2_skl,u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f595,f215]) ).
fof(f1230,plain,
( k3_waybel34(sK0_skl,sK1_skl,sK2_skl) = sK2_skl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1228,f216]) ).
fof(f1231,definition,
( sQ0_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1233,plain,
( sQ0_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1231]) ).
fof(f1234,definition,
( sQ1_spl
<=> l1_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1236,plain,
( sQ1_spl
| ~ l1_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1234]) ).
fof(f1237,definition,
( sQ2_spl
<=> m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1239,plain,
( sQ2_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1237]) ).
fof(f1240,definition,
( sQ3_spl
<=> k3_waybel34(sK0_skl,sK1_skl,sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1241,plain,
( ~ sQ3_spl
| k3_waybel34(sK0_skl,sK1_skl,sK2_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f1240]) ).
fof(f1243,plain,
( sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1230,f1231,f1234,f1237,f1240]) ).
fof(f1245,plain,
! [X0,X1,X2,X3,X4] :
( k3_waybel34(X3,X4,k2_waybel34(X0,X1,X2)) = k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X3),u1_struct_0(X4))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X3),u1_struct_0(X4))
| ~ l1_orders_2(X4)
| ~ l1_orders_2(X3)
| ~ 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(resolution,[status(thm)],[f609,f595]) ).
fof(f1247,plain,
( ~ sQ3_spl
| v1_funct_2(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl)))
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1241,f614]) ).
fof(f1248,definition,
( sQ4_spl
<=> v1_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1250,plain,
( sQ4_spl
| ~ v1_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f1248]) ).
fof(f1251,definition,
( sQ5_spl
<=> v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1253,plain,
( sQ5_spl
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1251]) ).
fof(f1254,definition,
( sQ6_spl
<=> m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1256,plain,
( sQ6_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1254]) ).
fof(f1257,definition,
( sQ7_spl
<=> v1_funct_2(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1260,plain,
( ~ sQ3_spl
| sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1247,f1231,f1234,f1248,f1251,f1254,f1257,f1240]) ).
fof(f1261,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1236,f214]) ).
fof(f1262,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1261]) ).
fof(f1263,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1233,f207]) ).
fof(f1264,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1263]) ).
fof(f1265,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1239,f218]) ).
fof(f1266,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1265]) ).
fof(f1269,plain,
( ~ sQ3_spl
| m2_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl)))
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_skl)
| ~ l1_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1241,f615]) ).
fof(f1270,definition,
( sQ8_spl
<=> m2_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1273,plain,
( ~ sQ3_spl
| sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1269,f1231,f1234,f1248,f1251,f1254,f1270,f1240]) ).
fof(f1284,plain,
( sQ6_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f1256,f1192]) ).
fof(f1285,plain,
( sQ6_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1284,f1237,f1254]) ).
fof(f1286,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1253,f216]) ).
fof(f1287,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1286]) ).
fof(f1288,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1250,f215]) ).
fof(f1289,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1288]) ).
fof(f1290,plain,
( ~ sQ3_spl
| k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl) != k2_waybel34(sK1_skl,sK0_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f1241,f219]) ).
fof(f1299,definition,
( sQ12_spl
<=> l1_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1301,plain,
( sQ12_spl
| ~ l1_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1299]) ).
fof(f1302,definition,
( sQ13_spl
<=> l1_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1304,plain,
( sQ13_spl
| ~ l1_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1325,plain,
( sQ13_spl
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1304,f622]) ).
fof(f1326,plain,
( sQ13_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1325,f1234,f1302]) ).
fof(f1327,plain,
( sQ12_spl
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1301,f622]) ).
fof(f1328,plain,
( sQ12_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1327,f1231,f1299]) ).
fof(f1404,definition,
( sQ28_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1406,plain,
( sQ28_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1404]) ).
fof(f1407,definition,
( sQ29_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1409,plain,
( sQ29_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1407]) ).
fof(f1410,definition,
( sQ30_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1412,plain,
( sQ30_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1410]) ).
fof(f1413,definition,
( sQ31_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1415,plain,
( sQ31_spl
| ~ v1_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1413]) ).
fof(f1416,definition,
( sQ32_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1418,plain,
( sQ32_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1416]) ).
fof(f1419,definition,
( sQ33_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1421,plain,
( sQ33_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1419]) ).
fof(f1422,definition,
( sQ34_spl
<=> v2_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1424,plain,
( sQ34_spl
| ~ v2_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1422]) ).
fof(f1425,definition,
( sQ35_spl
<=> v3_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( sQ35_spl
| ~ v3_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1425]) ).
fof(f1428,definition,
( sQ36_spl
<=> v4_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1430,plain,
( sQ36_spl
| ~ v4_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,definition,
( sQ37_spl
<=> v1_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1433,plain,
( sQ37_spl
| ~ v1_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f1431]) ).
fof(f1434,definition,
( sQ38_spl
<=> v2_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( sQ38_spl
| ~ v2_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f1434]) ).
fof(f1437,definition,
( sQ39_spl
<=> v3_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1439,plain,
( sQ39_spl
| ~ v3_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f1437]) ).
fof(f1461,plain,
( v17_waybel_0(k3_waybel34(sK0_skl,sK1_skl,sK2_skl),k7_lattice3(sK0_skl),k7_lattice3(sK1_skl))
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(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(resolution,[status(thm)],[f794,f217]) ).
fof(f1464,definition,
( sQ44_spl
<=> v17_waybel_0(k3_waybel34(sK0_skl,sK1_skl,sK2_skl),k7_lattice3(sK0_skl),k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1465,plain,
( ~ sQ44_spl
| v17_waybel_0(k3_waybel34(sK0_skl,sK1_skl,sK2_skl),k7_lattice3(sK0_skl),k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1464]) ).
fof(f1467,plain,
( sQ44_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ1_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| ~ sQ0_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f1461,f1404,f1407,f1410,f1413,f1416,f1419,f1231,f1422,f1425,f1428,f1431,f1434,f1437,f1234,f1248,f1251,f1254,f1464]) ).
fof(f1468,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1439,f213]) ).
fof(f1469,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1468]) ).
fof(f1470,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1436,f212]) ).
fof(f1471,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1470]) ).
fof(f1472,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1433,f211]) ).
fof(f1473,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f1472]) ).
fof(f1474,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1430,f210]) ).
fof(f1475,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1474]) ).
fof(f1476,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1427,f209]) ).
fof(f1477,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f1476]) ).
fof(f1478,plain,
( sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1424,f208]) ).
fof(f1479,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1478]) ).
fof(f1480,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1421,f206]) ).
fof(f1481,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1480]) ).
fof(f1482,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1418,f205]) ).
fof(f1483,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1482]) ).
fof(f1484,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1415,f204]) ).
fof(f1485,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f1484]) ).
fof(f1486,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1412,f203]) ).
fof(f1487,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1486]) ).
fof(f1488,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1409,f202]) ).
fof(f1489,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f1488]) ).
fof(f1490,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1406,f201]) ).
fof(f1491,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f1490]) ).
fof(f1492,plain,
( ~ sQ44_spl
| ~ sQ3_spl
| v17_waybel_0(sK2_skl,k7_lattice3(sK0_skl),k7_lattice3(sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f1241,f1465]) ).
fof(f1501,definition,
( sQ47_spl
<=> v4_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1503,plain,
( sQ47_spl
| ~ v4_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1501]) ).
fof(f1504,definition,
( sQ48_spl
<=> v1_lattice3(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1506,plain,
( sQ48_spl
| ~ v1_lattice3(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1504]) ).
fof(f1507,definition,
( sQ49_spl
<=> v2_lattice3(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1509,plain,
( sQ49_spl
| ~ v2_lattice3(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1507]) ).
fof(f1510,definition,
( sQ50_spl
<=> v3_lattice3(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( sQ50_spl
| ~ v3_lattice3(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1510]) ).
fof(f1513,definition,
( sQ51_spl
<=> v2_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1515,plain,
( sQ51_spl
| ~ v2_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1513]) ).
fof(f1516,definition,
( sQ52_spl
<=> v3_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1518,plain,
( sQ52_spl
| ~ v3_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1516]) ).
fof(f1519,definition,
( sQ53_spl
<=> v4_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1521,plain,
( sQ53_spl
| ~ v4_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1519]) ).
fof(f1522,definition,
( sQ54_spl
<=> v1_lattice3(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1524,plain,
( sQ54_spl
| ~ v1_lattice3(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1522]) ).
fof(f1525,definition,
( sQ55_spl
<=> v2_lattice3(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1527,plain,
( sQ55_spl
| ~ v2_lattice3(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1525]) ).
fof(f1528,definition,
( sQ56_spl
<=> v3_lattice3(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1530,plain,
( sQ56_spl
| ~ v3_lattice3(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1528]) ).
fof(f1539,plain,
( sQ56_spl
| ~ l1_orders_2(sK1_skl)
| ~ v3_lattice3(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1530,f845]) ).
fof(f1541,definition,
( sQ59_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1542,plain,
( ~ sQ59_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f1541]) ).
fof(f1544,plain,
( sQ56_spl
| ~ sQ1_spl
| ~ sQ39_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1539,f1541,f1437,f1234,f1528]) ).
fof(f1552,plain,
( ~ sQ59_spl
| ~ v2_lattice3(sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1542,f384]) ).
fof(f1554,plain,
( ~ sQ59_spl
| ~ sQ38_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f1552,f1234,f1434,f1541]) ).
fof(f1559,plain,
! [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)
| k3_waybel34(X0,X1,k2_waybel34(X0,X1,X2)) = k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ 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(resolution,[status(thm)],[f1245,f610]) ).
fof(f1560,plain,
! [X0,X1,X2] :
( k3_waybel34(X0,X1,k2_waybel34(X0,X1,X2)) = k2_waybel34(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(duplicate_literals_removal,[status(thm)],[f1559]) ).
fof(f1561,plain,
! [X0,X1,X2] :
( k3_waybel34(X0,X1,k2_waybel34(X0,X1,X2)) = 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(forward_subsumption_resolution,[status(thm)],[f1560,f611]) ).
fof(f1562,plain,
( sQ54_spl
| ~ l1_orders_2(sK1_skl)
| ~ v3_lattice3(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1524,f843]) ).
fof(f1566,plain,
( sQ54_spl
| ~ sQ1_spl
| ~ sQ39_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1562,f1541,f1437,f1234,f1522]) ).
fof(f1568,definition,
( sQ62_spl
<=> v3_struct_0(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1569,plain,
( ~ sQ62_spl
| v3_struct_0(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1568]) ).
fof(f1579,plain,
( sQ53_spl
| ~ l1_orders_2(sK1_skl)
| ~ v4_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1521,f787]) ).
fof(f1580,plain,
( sQ53_spl
| ~ sQ1_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f1579,f1428,f1234,f1519]) ).
fof(f1598,plain,
( sQ51_spl
| ~ l1_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1515,f740]) ).
fof(f1599,plain,
( sQ51_spl
| ~ sQ1_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f1598,f1422,f1234,f1513]) ).
fof(f1600,plain,
( sQ52_spl
| ~ l1_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1518,f767]) ).
fof(f1601,plain,
( sQ52_spl
| ~ sQ1_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f1600,f1425,f1234,f1516]) ).
fof(f1611,plain,
( sQ55_spl
| ~ v3_lattice3(k7_lattice3(sK1_skl))
| v3_struct_0(k7_lattice3(sK1_skl))
| ~ l1_orders_2(k7_lattice3(sK1_skl)) ),
inference(resolution,[status(thm)],[f1527,f357]) ).
fof(f1616,plain,
( sQ55_spl
| ~ sQ56_spl
| sQ62_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1611,f1302,f1568,f1528,f1525]) ).
fof(f1621,plain,
( ~ sQ62_spl
| ~ v1_lattice3(k7_lattice3(sK1_skl))
| ~ l1_orders_2(k7_lattice3(sK1_skl)) ),
inference(resolution,[status(thm)],[f1569,f310]) ).
fof(f1626,plain,
( ~ sQ62_spl
| ~ sQ54_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f1621,f1302,f1522,f1568]) ).
fof(f1634,plain,
( sQ50_spl
| ~ l1_orders_2(sK0_skl)
| ~ v3_lattice3(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1512,f845]) ).
fof(f1636,definition,
( sQ67_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1637,plain,
( ~ sQ67_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1636]) ).
fof(f1639,plain,
( sQ50_spl
| ~ sQ0_spl
| ~ sQ33_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1634,f1636,f1419,f1231,f1510]) ).
fof(f1647,plain,
( ~ sQ67_spl
| ~ v2_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1637,f384]) ).
fof(f1649,plain,
( ~ sQ67_spl
| ~ sQ32_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1647,f1231,f1416,f1636]) ).
fof(f1700,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| k3_waybel34(X0,X1,k2_waybel34(X0,X1,X2)) = 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)],[f1561,f1192]) ).
fof(f1709,definition,
( sQ85_spl
<=> k3_waybel34(sK1_skl,sK0_skl,k2_waybel34(sK1_skl,sK0_skl,sK2_skl)) = k2_waybel34(sK1_skl,sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1710,plain,
( ~ sQ85_spl
| k3_waybel34(sK1_skl,sK0_skl,k2_waybel34(sK1_skl,sK0_skl,sK2_skl)) = k2_waybel34(sK1_skl,sK0_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f1709]) ).
fof(f1714,plain,
( sQ48_spl
| ~ l1_orders_2(sK0_skl)
| ~ v3_lattice3(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1506,f843]) ).
fof(f1718,plain,
( sQ48_spl
| ~ sQ0_spl
| ~ sQ33_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1714,f1636,f1419,f1231,f1504]) ).
fof(f1720,definition,
( sQ86_spl
<=> v3_struct_0(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1721,plain,
( ~ sQ86_spl
| v3_struct_0(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1720]) ).
fof(f1762,plain,
( sQ47_spl
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1503,f787]) ).
fof(f1763,plain,
( sQ47_spl
| ~ sQ0_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1762,f1410,f1231,f1501]) ).
fof(f1776,plain,
( sQ49_spl
| ~ v3_lattice3(k7_lattice3(sK0_skl))
| v3_struct_0(k7_lattice3(sK0_skl))
| ~ l1_orders_2(k7_lattice3(sK0_skl)) ),
inference(resolution,[status(thm)],[f1509,f357]) ).
fof(f1781,plain,
( sQ49_spl
| ~ sQ50_spl
| sQ86_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1776,f1299,f1720,f1510,f1507]) ).
fof(f1788,plain,
( ~ sQ86_spl
| ~ v1_lattice3(k7_lattice3(sK0_skl))
| ~ l1_orders_2(k7_lattice3(sK0_skl)) ),
inference(resolution,[status(thm)],[f1721,f310]) ).
fof(f1793,plain,
( ~ sQ86_spl
| ~ sQ48_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1788,f1299,f1504,f1720]) ).
fof(f1893,plain,
! [X0,X1] :
( ~ m2_relset_1(sK2_skl,u1_struct_0(X1),u1_struct_0(X0))
| k3_waybel34(X0,X1,k2_waybel34(X0,X1,sK2_skl)) = k2_waybel34(X0,X1,sK2_skl)
| ~ v1_funct_2(sK2_skl,u1_struct_0(X1),u1_struct_0(X0))
| ~ 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)],[f1700,f215]) ).
fof(f2151,plain,
( ~ sQ85_spl
| m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl))
| ~ l1_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(paramodulation,[status(thm)],[f1710,f615]) ).
fof(f2152,plain,
( ~ sQ85_spl
| v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl))
| ~ l1_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(paramodulation,[status(thm)],[f1710,f614]) ).
fof(f2153,definition,
( sQ154_spl
<=> v18_waybel_0(sK2_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f2155,plain,
( sQ154_spl
| ~ v18_waybel_0(sK2_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f2153]) ).
fof(f2176,definition,
( sQ161_spl
<=> v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f2184,definition,
( sQ163_spl
<=> m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f2186,plain,
( sQ163_spl
| ~ m1_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2184]) ).
fof(f2191,definition,
( sQ165_spl
<=> v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f2193,plain,
( sQ165_spl
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f2191]) ).
fof(f2194,definition,
( sQ166_spl
<=> v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f2196,plain,
( sQ166_spl
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2194]) ).
fof(f2197,definition,
( sQ167_spl
<=> m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f2199,plain,
( sQ167_spl
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2197]) ).
fof(f2205,definition,
( sQ169_spl
<=> m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f2208,plain,
( ~ sQ85_spl
| sQ169_spl
| ~ sQ163_spl
| ~ sQ166_spl
| ~ sQ165_spl
| ~ sQ0_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f2151,f1234,f1231,f2191,f2194,f2184,f2205,f1709]) ).
fof(f2209,plain,
( ~ sQ85_spl
| sQ161_spl
| ~ sQ163_spl
| ~ sQ166_spl
| ~ sQ165_spl
| ~ sQ0_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f2152,f1234,f1231,f2191,f2194,f2184,f2176,f1709]) ).
fof(f2210,plain,
( sQ154_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2155,f217]) ).
fof(f2211,plain,
sQ154_spl,
inference(contradiction_clause,[status(thm)],[f2210]) ).
fof(f2243,definition,
( sQ171_spl
<=> l1_orders_2(sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f2245,plain,
( sQ171_spl
| ~ l1_orders_2(sK24_skl) ),
inference(component_clause,[status(thm)],[f2243]) ).
fof(f2250,plain,
( sQ171_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2245,f1004]) ).
fof(f2251,plain,
sQ171_spl,
inference(contradiction_clause,[status(thm)],[f2250]) ).
fof(f2266,plain,
( ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| k3_waybel34(sK1_skl,sK0_skl,k2_waybel34(sK1_skl,sK0_skl,sK2_skl)) = k2_waybel34(sK1_skl,sK0_skl,sK2_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)],[f1893,f216]) ).
fof(f2273,plain,
( ~ sQ2_spl
| sQ85_spl
| ~ sQ0_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f2266,f1422,f1425,f1428,f1431,f1434,f1234,f1404,f1407,f1410,f1413,f1416,f1231,f1709,f1237]) ).
fof(f2377,definition,
( sQ181_spl
<=> v3_struct_0(sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f2378,plain,
( ~ sQ181_spl
| v3_struct_0(sK24_skl) ),
inference(component_clause,[status(thm)],[f2377]) ).
fof(f2412,plain,
( ~ sQ181_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2378,f1005]) ).
fof(f2413,plain,
~ sQ181_spl,
inference(contradiction_clause,[status(thm)],[f2412]) ).
fof(f2414,plain,
( sQ165_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_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)],[f2193,f609]) ).
fof(f2415,plain,
( sQ165_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f2414,f1422,f1425,f1428,f1431,f1434,f1234,f1404,f1407,f1410,f1413,f1416,f1231,f1248,f1251,f1254,f2191]) ).
fof(f2528,definition,
( sQ199_spl
<=> l1_orders_2(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f2530,plain,
( sQ199_spl
| ~ l1_orders_2(sK25_skl) ),
inference(component_clause,[status(thm)],[f2528]) ).
fof(f2535,plain,
( sQ199_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2530,f1031]) ).
fof(f2536,plain,
sQ199_spl,
inference(contradiction_clause,[status(thm)],[f2535]) ).
fof(f2686,definition,
( sQ226_spl
<=> l1_orders_2(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f2688,plain,
( sQ226_spl
| ~ l1_orders_2(sK27_skl) ),
inference(component_clause,[status(thm)],[f2686]) ).
fof(f2693,plain,
( sQ226_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2688,f1046]) ).
fof(f2694,plain,
sQ226_spl,
inference(contradiction_clause,[status(thm)],[f2693]) ).
fof(f2703,plain,
( sQ163_spl
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f2186,f1192]) ).
fof(f2704,plain,
( sQ166_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_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)],[f2196,f610]) ).
fof(f2705,plain,
( sQ166_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f2704,f1422,f1425,f1428,f1431,f1434,f1234,f1404,f1407,f1410,f1413,f1416,f1231,f1248,f1251,f1254,f2194]) ).
fof(f2803,definition,
( sQ238_spl
<=> l1_orders_2(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition]) ).
fof(f2805,plain,
( sQ238_spl
| ~ l1_orders_2(sK29_skl) ),
inference(component_clause,[status(thm)],[f2803]) ).
fof(f2810,plain,
( sQ238_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2805,f1063]) ).
fof(f2811,plain,
sQ238_spl,
inference(contradiction_clause,[status(thm)],[f2810]) ).
fof(f3085,definition,
( sQ272_spl
<=> v3_struct_0(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ272_spl])],[split_symbol_definition]) ).
fof(f3086,plain,
( ~ sQ272_spl
| v3_struct_0(sK29_skl) ),
inference(component_clause,[status(thm)],[f3085]) ).
fof(f3120,plain,
( ~ sQ272_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3086,f1064]) ).
fof(f3121,plain,
~ sQ272_spl,
inference(contradiction_clause,[status(thm)],[f3120]) ).
fof(f3177,definition,
( sQ284_spl
<=> l1_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f3179,plain,
( sQ284_spl
| ~ l1_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f3177]) ).
fof(f3184,plain,
( sQ284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3179,f1087]) ).
fof(f3185,plain,
sQ284_spl,
inference(contradiction_clause,[status(thm)],[f3184]) ).
fof(f3469,plain,
( sQ167_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_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)],[f2199,f611]) ).
fof(f3471,plain,
( sQ167_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f3469,f1422,f1425,f1428,f1431,f1434,f1234,f1404,f1407,f1410,f1413,f1416,f1231,f1248,f1251,f1254,f2197]) ).
fof(f3556,definition,
( sQ323_spl
<=> v3_yellow_0(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f3558,plain,
( sQ323_spl
| ~ v3_yellow_0(sK29_skl) ),
inference(component_clause,[status(thm)],[f3556]) ).
fof(f3563,definition,
( sQ325_spl
<=> v3_yellow_0(sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f3565,plain,
( sQ325_spl
| ~ v3_yellow_0(sK24_skl) ),
inference(component_clause,[status(thm)],[f3563]) ).
fof(f3570,definition,
( sQ327_spl
<=> v3_yellow_0(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f3572,plain,
( sQ327_spl
| ~ v3_yellow_0(sK22_skl) ),
inference(component_clause,[status(thm)],[f3570]) ).
fof(f3579,plain,
( sQ323_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3558,f1071]) ).
fof(f3580,plain,
sQ323_spl,
inference(contradiction_clause,[status(thm)],[f3579]) ).
fof(f3581,plain,
( sQ325_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3565,f1015]) ).
fof(f3582,plain,
sQ325_spl,
inference(contradiction_clause,[status(thm)],[f3581]) ).
fof(f3583,plain,
( sQ327_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3572,f975]) ).
fof(f3584,plain,
sQ327_spl,
inference(contradiction_clause,[status(thm)],[f3583]) ).
fof(f3592,definition,
( sQ329_spl
<=> v2_orders_2(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition]) ).
fof(f3594,plain,
( sQ329_spl
| ~ v2_orders_2(sK25_skl) ),
inference(component_clause,[status(thm)],[f3592]) ).
fof(f3595,definition,
( sQ330_spl
<=> v1_lattice3(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f3597,plain,
( sQ330_spl
| ~ v1_lattice3(sK25_skl) ),
inference(component_clause,[status(thm)],[f3595]) ).
fof(f3598,definition,
( sQ331_spl
<=> v2_lattice3(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition]) ).
fof(f3600,plain,
( sQ331_spl
| ~ v2_lattice3(sK25_skl) ),
inference(component_clause,[status(thm)],[f3598]) ).
fof(f3610,definition,
( sQ335_spl
<=> v3_struct_0(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f3611,plain,
( ~ sQ335_spl
| v3_struct_0(sK25_skl) ),
inference(component_clause,[status(thm)],[f3610]) ).
fof(f3616,plain,
( ~ sQ335_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3611,f1032]) ).
fof(f3617,plain,
~ sQ335_spl,
inference(contradiction_clause,[status(thm)],[f3616]) ).
fof(f3637,definition,
( sQ338_spl
<=> v4_orders_2(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f3639,plain,
( sQ338_spl
| ~ v4_orders_2(sK25_skl) ),
inference(component_clause,[status(thm)],[f3637]) ).
fof(f3641,definition,
( sQ339_spl
<=> v3_orders_2(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition]) ).
fof(f3643,plain,
( sQ339_spl
| ~ v3_orders_2(sK25_skl) ),
inference(component_clause,[status(thm)],[f3641]) ).
fof(f3668,definition,
( sQ341_spl
<=> v3_lattice3(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition]) ).
fof(f3670,plain,
( sQ341_spl
| ~ v3_lattice3(sK25_skl) ),
inference(component_clause,[status(thm)],[f3668]) ).
fof(f3684,plain,
( sQ341_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3670,f1039]) ).
fof(f3685,plain,
sQ341_spl,
inference(contradiction_clause,[status(thm)],[f3684]) ).
fof(f3688,plain,
( sQ329_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3594,f1034]) ).
fof(f3689,plain,
sQ329_spl,
inference(contradiction_clause,[status(thm)],[f3688]) ).
fof(f3690,plain,
( sQ338_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3639,f1036]) ).
fof(f3691,plain,
sQ338_spl,
inference(contradiction_clause,[status(thm)],[f3690]) ).
fof(f3692,plain,
( sQ339_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3643,f1035]) ).
fof(f3693,plain,
sQ339_spl,
inference(contradiction_clause,[status(thm)],[f3692]) ).
fof(f3694,plain,
( sQ330_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3597,f1037]) ).
fof(f3695,plain,
sQ330_spl,
inference(contradiction_clause,[status(thm)],[f3694]) ).
fof(f3696,plain,
( sQ331_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3600,f1038]) ).
fof(f3697,plain,
sQ331_spl,
inference(contradiction_clause,[status(thm)],[f3696]) ).
fof(f3737,definition,
( sQ345_spl
<=> v3_realset2(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition]) ).
fof(f3739,plain,
( sQ345_spl
| ~ v3_realset2(sK25_skl) ),
inference(component_clause,[status(thm)],[f3737]) ).
fof(f3829,definition,
( sQ352_spl
<=> l1_orders_2(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition]) ).
fof(f3831,plain,
( sQ352_spl
| ~ l1_orders_2(sK37_skl) ),
inference(component_clause,[status(thm)],[f3829]) ).
fof(f3836,plain,
( sQ352_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3831,f1144]) ).
fof(f3837,plain,
sQ352_spl,
inference(contradiction_clause,[status(thm)],[f3836]) ).
fof(f3950,plain,
( sQ163_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_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)],[f2703,f611]) ).
fof(f3952,plain,
( sQ163_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f3950,f1422,f1425,f1428,f1431,f1434,f1234,f1404,f1407,f1410,f1413,f1416,f1231,f1248,f1251,f1254,f2184]) ).
fof(f3957,plain,
( sQ345_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3739,f1040]) ).
fof(f3958,plain,
sQ345_spl,
inference(contradiction_clause,[status(thm)],[f3957]) ).
fof(f4016,definition,
( sQ381_spl
<=> v3_yellow_0(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f4018,plain,
( sQ381_spl
| ~ v3_yellow_0(sK37_skl) ),
inference(component_clause,[status(thm)],[f4016]) ).
fof(f4036,definition,
( sQ384_spl
<=> v3_struct_0(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f4037,plain,
( ~ sQ384_spl
| v3_struct_0(sK37_skl) ),
inference(component_clause,[status(thm)],[f4036]) ).
fof(f4053,plain,
( ~ sQ384_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4037,f1145]) ).
fof(f4054,plain,
~ sQ384_spl,
inference(contradiction_clause,[status(thm)],[f4053]) ).
fof(f4055,plain,
( sQ381_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4018,f1154]) ).
fof(f4056,plain,
sQ381_spl,
inference(contradiction_clause,[status(thm)],[f4055]) ).
fof(f4103,definition,
( sQ395_spl
<=> l1_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition]) ).
fof(f4105,plain,
( sQ395_spl
| ~ l1_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f4103]) ).
fof(f4110,plain,
( sQ395_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4105,f1175]) ).
fof(f4111,plain,
sQ395_spl,
inference(contradiction_clause,[status(thm)],[f4110]) ).
fof(f4558,definition,
( sQ455_spl
<=> v1_yellow_0(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ455_spl])],[split_symbol_definition]) ).
fof(f4560,plain,
( sQ455_spl
| ~ v1_yellow_0(sK37_skl) ),
inference(component_clause,[status(thm)],[f4558]) ).
fof(f4573,plain,
( sQ455_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4560,f1152]) ).
fof(f4574,plain,
sQ455_spl,
inference(contradiction_clause,[status(thm)],[f4573]) ).
fof(f5503,definition,
( sQ584_spl
<=> v2_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition]) ).
fof(f5505,plain,
( sQ584_spl
| ~ v2_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f5503]) ).
fof(f5506,definition,
( sQ585_spl
<=> l1_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition]) ).
fof(f5508,plain,
( sQ585_spl
| ~ l1_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f5506]) ).
fof(f5514,plain,
( sQ585_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5508,f1104]) ).
fof(f5515,plain,
sQ585_spl,
inference(contradiction_clause,[status(thm)],[f5514]) ).
fof(f5573,definition,
( sQ591_spl
<=> v3_struct_0(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition]) ).
fof(f5574,plain,
( ~ sQ591_spl
| v3_struct_0(sK31_skl) ),
inference(component_clause,[status(thm)],[f5573]) ).
fof(f5576,definition,
( sQ592_spl
<=> v3_lattice3(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition]) ).
fof(f5578,plain,
( sQ592_spl
| ~ v3_lattice3(sK31_skl) ),
inference(component_clause,[status(thm)],[f5576]) ).
fof(f5580,definition,
( sQ593_spl
<=> v1_lattice3(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ593_spl])],[split_symbol_definition]) ).
fof(f5582,plain,
( sQ593_spl
| ~ v1_lattice3(sK31_skl) ),
inference(component_clause,[status(thm)],[f5580]) ).
fof(f5608,definition,
( sQ598_spl
<=> v2_lattice3(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ598_spl])],[split_symbol_definition]) ).
fof(f5610,plain,
( sQ598_spl
| ~ v2_lattice3(sK31_skl) ),
inference(component_clause,[status(thm)],[f5608]) ).
fof(f5619,plain,
( sQ592_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5578,f1111]) ).
fof(f5620,plain,
sQ592_spl,
inference(contradiction_clause,[status(thm)],[f5619]) ).
fof(f5621,plain,
( ~ sQ591_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5574,f1105]) ).
fof(f5622,plain,
~ sQ591_spl,
inference(contradiction_clause,[status(thm)],[f5621]) ).
fof(f5746,definition,
( sQ624_spl
<=> v3_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f5748,plain,
( sQ624_spl
| ~ v3_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f5746]) ).
fof(f5755,definition,
( sQ625_spl
<=> v4_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f5757,plain,
( sQ625_spl
| ~ v4_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f5755]) ).
fof(f5788,plain,
( sQ625_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5757,f1108]) ).
fof(f5789,plain,
sQ625_spl,
inference(contradiction_clause,[status(thm)],[f5788]) ).
fof(f5790,plain,
( sQ624_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5748,f1107]) ).
fof(f5791,plain,
sQ624_spl,
inference(contradiction_clause,[status(thm)],[f5790]) ).
fof(f5792,plain,
( sQ598_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5610,f1110]) ).
fof(f5793,plain,
sQ598_spl,
inference(contradiction_clause,[status(thm)],[f5792]) ).
fof(f5794,plain,
( sQ593_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5582,f1109]) ).
fof(f5795,plain,
sQ593_spl,
inference(contradiction_clause,[status(thm)],[f5794]) ).
fof(f5796,plain,
( sQ584_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5505,f1106]) ).
fof(f5797,plain,
sQ584_spl,
inference(contradiction_clause,[status(thm)],[f5796]) ).
fof(f5890,definition,
( sQ641_spl
<=> v10_waybel_1(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition]) ).
fof(f5892,plain,
( sQ641_spl
| ~ v10_waybel_1(sK37_skl) ),
inference(component_clause,[status(thm)],[f5890]) ).
fof(f5904,plain,
( sQ641_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5892,f1157]) ).
fof(f5905,plain,
sQ641_spl,
inference(contradiction_clause,[status(thm)],[f5904]) ).
fof(f5924,definition,
( sQ644_spl
<=> v2_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f5926,plain,
( sQ644_spl
| ~ v2_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f5924]) ).
fof(f5987,definition,
( sQ648_spl
<=> v3_struct_0(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ648_spl])],[split_symbol_definition]) ).
fof(f5988,plain,
( ~ sQ648_spl
| v3_struct_0(sK30_skl) ),
inference(component_clause,[status(thm)],[f5987]) ).
fof(f5990,definition,
( sQ649_spl
<=> v3_lattice3(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition]) ).
fof(f5992,plain,
( sQ649_spl
| ~ v3_lattice3(sK30_skl) ),
inference(component_clause,[status(thm)],[f5990]) ).
fof(f5994,definition,
( sQ650_spl
<=> v1_lattice3(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition]) ).
fof(f5996,plain,
( sQ650_spl
| ~ v1_lattice3(sK30_skl) ),
inference(component_clause,[status(thm)],[f5994]) ).
fof(f6142,definition,
( sQ679_spl
<=> v2_lattice3(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition]) ).
fof(f6144,plain,
( sQ679_spl
| ~ v2_lattice3(sK30_skl) ),
inference(component_clause,[status(thm)],[f6142]) ).
fof(f6153,plain,
( sQ649_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5992,f1095]) ).
fof(f6154,plain,
sQ649_spl,
inference(contradiction_clause,[status(thm)],[f6153]) ).
fof(f6155,plain,
( ~ sQ648_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5988,f1088]) ).
fof(f6156,plain,
~ sQ648_spl,
inference(contradiction_clause,[status(thm)],[f6155]) ).
fof(f6160,definition,
( sQ681_spl
<=> v3_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition]) ).
fof(f6162,plain,
( sQ681_spl
| ~ v3_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f6160]) ).
fof(f6169,definition,
( sQ682_spl
<=> v4_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ682_spl])],[split_symbol_definition]) ).
fof(f6171,plain,
( sQ682_spl
| ~ v4_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f6169]) ).
fof(f6232,definition,
( sQ690_spl
<=> v3_lattice3(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ690_spl])],[split_symbol_definition]) ).
fof(f6234,plain,
( sQ690_spl
| ~ v3_lattice3(sK29_skl) ),
inference(component_clause,[status(thm)],[f6232]) ).
fof(f6269,plain,
( sQ690_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6234,f1078]) ).
fof(f6270,plain,
sQ690_spl,
inference(contradiction_clause,[status(thm)],[f6269]) ).
fof(f6432,definition,
( sQ722_spl
<=> v2_orders_2(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f6434,plain,
( sQ722_spl
| ~ v2_orders_2(sK27_skl) ),
inference(component_clause,[status(thm)],[f6432]) ).
fof(f6477,definition,
( sQ727_spl
<=> v3_struct_0(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ727_spl])],[split_symbol_definition]) ).
fof(f6478,plain,
( ~ sQ727_spl
| v3_struct_0(sK27_skl) ),
inference(component_clause,[status(thm)],[f6477]) ).
fof(f6480,definition,
( sQ728_spl
<=> v3_lattice3(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition]) ).
fof(f6482,plain,
( sQ728_spl
| ~ v3_lattice3(sK27_skl) ),
inference(component_clause,[status(thm)],[f6480]) ).
fof(f6484,definition,
( sQ729_spl
<=> v1_lattice3(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ729_spl])],[split_symbol_definition]) ).
fof(f6486,plain,
( sQ729_spl
| ~ v1_lattice3(sK27_skl) ),
inference(component_clause,[status(thm)],[f6484]) ).
fof(f6512,definition,
( sQ734_spl
<=> v2_lattice3(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f6514,plain,
( sQ734_spl
| ~ v2_lattice3(sK27_skl) ),
inference(component_clause,[status(thm)],[f6512]) ).
fof(f6523,plain,
( sQ728_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6482,f1054]) ).
fof(f6524,plain,
sQ728_spl,
inference(contradiction_clause,[status(thm)],[f6523]) ).
fof(f6525,plain,
( ~ sQ727_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6478,f1047]) ).
fof(f6526,plain,
~ sQ727_spl,
inference(contradiction_clause,[status(thm)],[f6525]) ).
fof(f6660,definition,
( sQ766_spl
<=> v3_orders_2(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ766_spl])],[split_symbol_definition]) ).
fof(f6662,plain,
( sQ766_spl
| ~ v3_orders_2(sK27_skl) ),
inference(component_clause,[status(thm)],[f6660]) ).
fof(f6669,definition,
( sQ767_spl
<=> v4_orders_2(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ767_spl])],[split_symbol_definition]) ).
fof(f6671,plain,
( sQ767_spl
| ~ v4_orders_2(sK27_skl) ),
inference(component_clause,[status(thm)],[f6669]) ).
fof(f6912,definition,
( sQ792_spl
<=> v3_lattice3(sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ792_spl])],[split_symbol_definition]) ).
fof(f6914,plain,
( sQ792_spl
| ~ v3_lattice3(sK24_skl) ),
inference(component_clause,[status(thm)],[f6912]) ).
fof(f6949,plain,
( sQ792_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6914,f1012]) ).
fof(f6950,plain,
sQ792_spl,
inference(contradiction_clause,[status(thm)],[f6949]) ).
fof(f7014,definition,
( sQ803_spl
<=> v2_orders_2(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ803_spl])],[split_symbol_definition]) ).
fof(f7016,plain,
( sQ803_spl
| ~ v2_orders_2(sK23_skl) ),
inference(component_clause,[status(thm)],[f7014]) ).
fof(f7017,definition,
( sQ804_spl
<=> l1_orders_2(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ804_spl])],[split_symbol_definition]) ).
fof(f7019,plain,
( sQ804_spl
| ~ l1_orders_2(sK23_skl) ),
inference(component_clause,[status(thm)],[f7017]) ).
fof(f7025,plain,
( sQ804_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7019,f989]) ).
fof(f7026,plain,
sQ804_spl,
inference(contradiction_clause,[status(thm)],[f7025]) ).
fof(f7050,definition,
( sQ808_spl
<=> v3_struct_0(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ808_spl])],[split_symbol_definition]) ).
fof(f7051,plain,
( ~ sQ808_spl
| v3_struct_0(sK23_skl) ),
inference(component_clause,[status(thm)],[f7050]) ).
fof(f7053,definition,
( sQ809_spl
<=> v3_lattice3(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ809_spl])],[split_symbol_definition]) ).
fof(f7055,plain,
( sQ809_spl
| ~ v3_lattice3(sK23_skl) ),
inference(component_clause,[status(thm)],[f7053]) ).
fof(f7057,definition,
( sQ810_spl
<=> v1_lattice3(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ810_spl])],[split_symbol_definition]) ).
fof(f7059,plain,
( sQ810_spl
| ~ v1_lattice3(sK23_skl) ),
inference(component_clause,[status(thm)],[f7057]) ).
fof(f7089,definition,
( sQ815_spl
<=> v2_lattice3(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ815_spl])],[split_symbol_definition]) ).
fof(f7091,plain,
( sQ815_spl
| ~ v2_lattice3(sK23_skl) ),
inference(component_clause,[status(thm)],[f7089]) ).
fof(f7100,plain,
( sQ809_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7055,f996]) ).
fof(f7101,plain,
sQ809_spl,
inference(contradiction_clause,[status(thm)],[f7100]) ).
fof(f7102,plain,
( ~ sQ808_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7051,f990]) ).
fof(f7103,plain,
~ sQ808_spl,
inference(contradiction_clause,[status(thm)],[f7102]) ).
fof(f7107,definition,
( sQ817_spl
<=> v3_orders_2(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ817_spl])],[split_symbol_definition]) ).
fof(f7109,plain,
( sQ817_spl
| ~ v3_orders_2(sK23_skl) ),
inference(component_clause,[status(thm)],[f7107]) ).
fof(f7116,definition,
( sQ818_spl
<=> v4_orders_2(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ818_spl])],[split_symbol_definition]) ).
fof(f7118,plain,
( sQ818_spl
| ~ v4_orders_2(sK23_skl) ),
inference(component_clause,[status(thm)],[f7116]) ).
fof(f7181,definition,
( sQ823_spl
<=> v3_lattice3(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ823_spl])],[split_symbol_definition]) ).
fof(f7183,plain,
( sQ823_spl
| ~ v3_lattice3(sK22_skl) ),
inference(component_clause,[status(thm)],[f7181]) ).
fof(f7218,plain,
( sQ823_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7183,f982]) ).
fof(f7219,plain,
sQ823_spl,
inference(contradiction_clause,[status(thm)],[f7218]) ).
fof(f7222,definition,
( sQ829_spl
<=> v1_relat_1(sK33_skl) ),
introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition]) ).
fof(f7224,plain,
( sQ829_spl
| ~ v1_relat_1(sK33_skl) ),
inference(component_clause,[status(thm)],[f7222]) ).
fof(f7225,definition,
( sQ830_spl
<=> v1_funct_1(sK33_skl) ),
introduced(definition,[new_symbols(definition,[sQ830_spl])],[split_symbol_definition]) ).
fof(f7227,plain,
( sQ830_spl
| ~ v1_funct_1(sK33_skl) ),
inference(component_clause,[status(thm)],[f7225]) ).
fof(f7420,definition,
( sQ853_spl
<=> v2_orders_2(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ853_spl])],[split_symbol_definition]) ).
fof(f7422,plain,
( sQ853_spl
| ~ v2_orders_2(sK14_skl) ),
inference(component_clause,[status(thm)],[f7420]) ).
fof(f7428,plain,
( sQ853_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7422,f921]) ).
fof(f7429,plain,
sQ853_spl,
inference(contradiction_clause,[status(thm)],[f7428]) ).
fof(f7437,definition,
( sQ855_spl
<=> v3_struct_0(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ855_spl])],[split_symbol_definition]) ).
fof(f7438,plain,
( ~ sQ855_spl
| v3_struct_0(sK14_skl) ),
inference(component_clause,[status(thm)],[f7437]) ).
fof(f7440,definition,
( sQ856_spl
<=> v3_lattice3(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ856_spl])],[split_symbol_definition]) ).
fof(f7442,plain,
( sQ856_spl
| ~ v3_lattice3(sK14_skl) ),
inference(component_clause,[status(thm)],[f7440]) ).
fof(f7465,plain,
( sQ856_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7442,f924]) ).
fof(f7466,plain,
sQ856_spl,
inference(contradiction_clause,[status(thm)],[f7465]) ).
fof(f7467,plain,
( ~ sQ855_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7438,f919]) ).
fof(f7468,plain,
~ sQ855_spl,
inference(contradiction_clause,[status(thm)],[f7467]) ).
fof(f7527,definition,
( sQ868_spl
<=> v4_orders_2(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ868_spl])],[split_symbol_definition]) ).
fof(f7529,plain,
( sQ868_spl
| ~ v4_orders_2(sK14_skl) ),
inference(component_clause,[status(thm)],[f7527]) ).
fof(f7538,plain,
( sQ868_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7529,f923]) ).
fof(f7539,plain,
sQ868_spl,
inference(contradiction_clause,[status(thm)],[f7538]) ).
fof(f7542,definition,
( sQ871_spl
<=> v3_orders_2(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ871_spl])],[split_symbol_definition]) ).
fof(f7544,plain,
( sQ871_spl
| ~ v3_orders_2(sK14_skl) ),
inference(component_clause,[status(thm)],[f7542]) ).
fof(f7553,plain,
( sQ871_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7544,f922]) ).
fof(f7554,plain,
sQ871_spl,
inference(contradiction_clause,[status(thm)],[f7553]) ).
fof(f8286,definition,
( sQ938_spl
<=> v2_orders_2(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ938_spl])],[split_symbol_definition]) ).
fof(f8288,plain,
( sQ938_spl
| ~ v2_orders_2(sK11_skl) ),
inference(component_clause,[status(thm)],[f8286]) ).
fof(f8294,plain,
( sQ938_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8288,f900]) ).
fof(f8295,plain,
sQ938_spl,
inference(contradiction_clause,[status(thm)],[f8294]) ).
fof(f8329,definition,
( sQ946_spl
<=> v3_struct_0(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ946_spl])],[split_symbol_definition]) ).
fof(f8330,plain,
( ~ sQ946_spl
| v3_struct_0(sK11_skl) ),
inference(component_clause,[status(thm)],[f8329]) ).
fof(f8332,definition,
( sQ947_spl
<=> v3_lattice3(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ947_spl])],[split_symbol_definition]) ).
fof(f8334,plain,
( sQ947_spl
| ~ v3_lattice3(sK11_skl) ),
inference(component_clause,[status(thm)],[f8332]) ).
fof(f8336,definition,
( sQ948_spl
<=> v1_lattice3(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ948_spl])],[split_symbol_definition]) ).
fof(f8338,plain,
( sQ948_spl
| ~ v1_lattice3(sK11_skl) ),
inference(component_clause,[status(thm)],[f8336]) ).
fof(f8357,plain,
( sQ948_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8338,f903]) ).
fof(f8358,plain,
sQ948_spl,
inference(contradiction_clause,[status(thm)],[f8357]) ).
fof(f8359,plain,
( sQ947_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8334,f905]) ).
fof(f8360,plain,
sQ947_spl,
inference(contradiction_clause,[status(thm)],[f8359]) ).
fof(f8361,plain,
( ~ sQ946_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8330,f898]) ).
fof(f8362,plain,
~ sQ946_spl,
inference(contradiction_clause,[status(thm)],[f8361]) ).
fof(f8370,definition,
( sQ953_spl
<=> v2_lattice3(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ953_spl])],[split_symbol_definition]) ).
fof(f8372,plain,
( sQ953_spl
| ~ v2_lattice3(sK11_skl) ),
inference(component_clause,[status(thm)],[f8370]) ).
fof(f8381,plain,
( sQ953_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8372,f904]) ).
fof(f8382,plain,
sQ953_spl,
inference(contradiction_clause,[status(thm)],[f8381]) ).
fof(f8386,definition,
( sQ955_spl
<=> v3_orders_2(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ955_spl])],[split_symbol_definition]) ).
fof(f8388,plain,
( sQ955_spl
| ~ v3_orders_2(sK11_skl) ),
inference(component_clause,[status(thm)],[f8386]) ).
fof(f8392,plain,
( sQ955_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8388,f901]) ).
fof(f8393,plain,
sQ955_spl,
inference(contradiction_clause,[status(thm)],[f8392]) ).
fof(f8508,definition,
( sQ956_spl
<=> v4_orders_2(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ956_spl])],[split_symbol_definition]) ).
fof(f8510,plain,
( sQ956_spl
| ~ v4_orders_2(sK11_skl) ),
inference(component_clause,[status(thm)],[f8508]) ).
fof(f8514,plain,
( sQ956_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8510,f902]) ).
fof(f8515,plain,
sQ956_spl,
inference(contradiction_clause,[status(thm)],[f8514]) ).
fof(f8593,definition,
( sQ971_spl
<=> v2_orders_2(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ971_spl])],[split_symbol_definition]) ).
fof(f8595,plain,
( sQ971_spl
| ~ v2_orders_2(sK10_skl) ),
inference(component_clause,[status(thm)],[f8593]) ).
fof(f8596,definition,
( sQ972_spl
<=> l1_orders_2(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ972_spl])],[split_symbol_definition]) ).
fof(f8598,plain,
( sQ972_spl
| ~ l1_orders_2(sK10_skl) ),
inference(component_clause,[status(thm)],[f8596]) ).
fof(f8604,plain,
( sQ972_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8598,f890]) ).
fof(f8605,plain,
sQ972_spl,
inference(contradiction_clause,[status(thm)],[f8604]) ).
fof(f8606,plain,
( sQ971_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8595,f892]) ).
fof(f8607,plain,
sQ971_spl,
inference(contradiction_clause,[status(thm)],[f8606]) ).
fof(f8687,definition,
( sQ980_spl
<=> v3_struct_0(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ980_spl])],[split_symbol_definition]) ).
fof(f8688,plain,
( ~ sQ980_spl
| v3_struct_0(sK10_skl) ),
inference(component_clause,[status(thm)],[f8687]) ).
fof(f8715,plain,
( ~ sQ980_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8688,f891]) ).
fof(f8716,plain,
~ sQ980_spl,
inference(contradiction_clause,[status(thm)],[f8715]) ).
fof(f8725,definition,
( sQ988_spl
<=> v16_waybel_0(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ988_spl])],[split_symbol_definition]) ).
fof(f8727,plain,
( sQ988_spl
| ~ v16_waybel_0(sK10_skl) ),
inference(component_clause,[status(thm)],[f8725]) ).
fof(f8729,definition,
( sQ989_spl
<=> v4_orders_2(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ989_spl])],[split_symbol_definition]) ).
fof(f8731,plain,
( sQ989_spl
| ~ v4_orders_2(sK10_skl) ),
inference(component_clause,[status(thm)],[f8729]) ).
fof(f8740,plain,
( sQ988_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8727,f895]) ).
fof(f8741,plain,
sQ988_spl,
inference(contradiction_clause,[status(thm)],[f8740]) ).
fof(f8742,plain,
( sQ989_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8731,f894]) ).
fof(f8743,plain,
sQ989_spl,
inference(contradiction_clause,[status(thm)],[f8742]) ).
fof(f8752,definition,
( sQ993_spl
<=> v3_orders_2(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ993_spl])],[split_symbol_definition]) ).
fof(f8754,plain,
( sQ993_spl
| ~ v3_orders_2(sK10_skl) ),
inference(component_clause,[status(thm)],[f8752]) ).
fof(f8764,plain,
( sQ993_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8754,f893]) ).
fof(f8765,plain,
sQ993_spl,
inference(contradiction_clause,[status(thm)],[f8764]) ).
fof(f9862,definition,
( sQ1116_spl
<=> k7_lattice3(sK0_skl) = k7_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1116_spl])],[split_symbol_definition]) ).
fof(f9864,plain,
( sQ1116_spl
| k7_lattice3(sK0_skl) != k7_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f9862]) ).
fof(f9908,plain,
( sQ1116_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9864]) ).
fof(f9909,plain,
sQ1116_spl,
inference(contradiction_clause,[status(thm)],[f9908]) ).
fof(f10083,definition,
( sQ1141_spl
<=> l1_orders_2(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ1141_spl])],[split_symbol_definition]) ).
fof(f10085,plain,
( sQ1141_spl
| ~ l1_orders_2(sK3_skl) ),
inference(component_clause,[status(thm)],[f10083]) ).
fof(f10091,plain,
( sQ1141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10085,f630]) ).
fof(f10092,plain,
sQ1141_spl,
inference(contradiction_clause,[status(thm)],[f10091]) ).
fof(f11000,plain,
( sQ830_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7227,f1122]) ).
fof(f11001,plain,
sQ830_spl,
inference(contradiction_clause,[status(thm)],[f11000]) ).
fof(f11002,plain,
( sQ829_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7224,f1121]) ).
fof(f11003,plain,
sQ829_spl,
inference(contradiction_clause,[status(thm)],[f11002]) ).
fof(f11004,plain,
( sQ818_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7118,f993]) ).
fof(f11005,plain,
sQ818_spl,
inference(contradiction_clause,[status(thm)],[f11004]) ).
fof(f11006,plain,
( sQ817_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7109,f992]) ).
fof(f11007,plain,
sQ817_spl,
inference(contradiction_clause,[status(thm)],[f11006]) ).
fof(f11008,plain,
( sQ815_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7091,f995]) ).
fof(f11009,plain,
sQ815_spl,
inference(contradiction_clause,[status(thm)],[f11008]) ).
fof(f11010,plain,
( sQ810_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7059,f994]) ).
fof(f11011,plain,
sQ810_spl,
inference(contradiction_clause,[status(thm)],[f11010]) ).
fof(f11012,plain,
( sQ803_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7016,f991]) ).
fof(f11013,plain,
sQ803_spl,
inference(contradiction_clause,[status(thm)],[f11012]) ).
fof(f11014,plain,
( sQ767_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6671,f1051]) ).
fof(f11015,plain,
sQ767_spl,
inference(contradiction_clause,[status(thm)],[f11014]) ).
fof(f11016,plain,
( sQ766_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6662,f1050]) ).
fof(f11017,plain,
sQ766_spl,
inference(contradiction_clause,[status(thm)],[f11016]) ).
fof(f11018,plain,
( sQ734_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6514,f1053]) ).
fof(f11019,plain,
sQ734_spl,
inference(contradiction_clause,[status(thm)],[f11018]) ).
fof(f11020,plain,
( sQ729_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6486,f1052]) ).
fof(f11021,plain,
sQ729_spl,
inference(contradiction_clause,[status(thm)],[f11020]) ).
fof(f11022,plain,
( sQ722_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6434,f1049]) ).
fof(f11023,plain,
sQ722_spl,
inference(contradiction_clause,[status(thm)],[f11022]) ).
fof(f11024,plain,
( sQ682_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6171,f1092]) ).
fof(f11025,plain,
sQ682_spl,
inference(contradiction_clause,[status(thm)],[f11024]) ).
fof(f11026,plain,
( sQ681_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6162,f1091]) ).
fof(f11027,plain,
sQ681_spl,
inference(contradiction_clause,[status(thm)],[f11026]) ).
fof(f11028,plain,
( sQ679_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6144,f1094]) ).
fof(f11029,plain,
sQ679_spl,
inference(contradiction_clause,[status(thm)],[f11028]) ).
fof(f11030,plain,
( sQ650_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5996,f1093]) ).
fof(f11031,plain,
sQ650_spl,
inference(contradiction_clause,[status(thm)],[f11030]) ).
fof(f11032,plain,
( sQ644_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5926,f1090]) ).
fof(f11033,plain,
sQ644_spl,
inference(contradiction_clause,[status(thm)],[f11032]) ).
fof(f11454,definition,
( sQ1323_spl
<=> k7_lattice3(sK1_skl) = k7_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1323_spl])],[split_symbol_definition]) ).
fof(f11456,plain,
( sQ1323_spl
| k7_lattice3(sK1_skl) != k7_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f11454]) ).
fof(f11776,plain,
( sQ1323_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11456]) ).
fof(f11777,plain,
sQ1323_spl,
inference(contradiction_clause,[status(thm)],[f11776]) ).
fof(f12647,definition,
( sQ1534_spl
<=> v2_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1534_spl])],[split_symbol_definition]) ).
fof(f12649,plain,
( sQ1534_spl
| ~ v2_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f12647]) ).
fof(f12655,plain,
( sQ1534_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12649,f1178]) ).
fof(f12656,plain,
sQ1534_spl,
inference(contradiction_clause,[status(thm)],[f12655]) ).
fof(f12674,definition,
( sQ1536_spl
<=> v3_struct_0(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1536_spl])],[split_symbol_definition]) ).
fof(f12675,plain,
( ~ sQ1536_spl
| v3_struct_0(sK40_skl) ),
inference(component_clause,[status(thm)],[f12674]) ).
fof(f12681,definition,
( sQ1538_spl
<=> v1_lattice3(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1538_spl])],[split_symbol_definition]) ).
fof(f12683,plain,
( sQ1538_spl
| ~ v1_lattice3(sK40_skl) ),
inference(component_clause,[status(thm)],[f12681]) ).
fof(f12702,plain,
( sQ1538_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12683,f1181]) ).
fof(f12703,plain,
sQ1538_spl,
inference(contradiction_clause,[status(thm)],[f12702]) ).
fof(f12704,plain,
( ~ sQ1536_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12675,f1176]) ).
fof(f12705,plain,
~ sQ1536_spl,
inference(contradiction_clause,[status(thm)],[f12704]) ).
fof(f12714,definition,
( sQ1544_spl
<=> v3_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1544_spl])],[split_symbol_definition]) ).
fof(f12716,plain,
( sQ1544_spl
| ~ v3_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f12714]) ).
fof(f12717,definition,
( sQ1545_spl
<=> v4_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1545_spl])],[split_symbol_definition]) ).
fof(f12719,plain,
( sQ1545_spl
| ~ v4_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f12717]) ).
fof(f12730,definition,
( sQ1549_spl
<=> v2_yellow_0(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1549_spl])],[split_symbol_definition]) ).
fof(f12732,plain,
( sQ1549_spl
| ~ v2_yellow_0(sK40_skl) ),
inference(component_clause,[status(thm)],[f12730]) ).
fof(f12738,plain,
( sQ1545_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12719,f1180]) ).
fof(f12739,plain,
sQ1545_spl,
inference(contradiction_clause,[status(thm)],[f12738]) ).
fof(f12740,plain,
( sQ1544_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12716,f1179]) ).
fof(f12741,plain,
sQ1544_spl,
inference(contradiction_clause,[status(thm)],[f12740]) ).
fof(f12742,plain,
( sQ1549_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12732,f1183]) ).
fof(f12743,plain,
sQ1549_spl,
inference(contradiction_clause,[status(thm)],[f12742]) ).
fof(f12748,definition,
( sQ1551_spl
<=> v2_lattice3(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ1551_spl])],[split_symbol_definition]) ).
fof(f12750,plain,
( sQ1551_spl
| ~ v2_lattice3(sK40_skl) ),
inference(component_clause,[status(thm)],[f12748]) ).
fof(f12761,plain,
( sQ1551_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12750,f1182]) ).
fof(f12762,plain,
sQ1551_spl,
inference(contradiction_clause,[status(thm)],[f12761]) ).
fof(f13209,definition,
( sQ1567_spl
<=> v16_waybel_0(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ1567_spl])],[split_symbol_definition]) ).
fof(f13211,plain,
( sQ1567_spl
| ~ v16_waybel_0(sK29_skl) ),
inference(component_clause,[status(thm)],[f13209]) ).
fof(f13214,plain,
( sQ1567_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13211,f1072]) ).
fof(f13215,plain,
sQ1567_spl,
inference(contradiction_clause,[status(thm)],[f13214]) ).
fof(f13217,plain,
! [X0,X1,X2,X3] :
( X2 = k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3)
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_1(X3)
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| ~ v3_orders_2(k7_lattice3(X1))
| ~ v2_orders_2(k7_lattice3(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(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)],[f1225,f589]) ).
fof(f13220,plain,
! [X0,X1,X2,X3] :
( X2 = k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3)
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| ~ v3_orders_2(k7_lattice3(X1))
| ~ v2_orders_2(k7_lattice3(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(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)],[f13217]) ).
fof(f13221,plain,
! [X0,X1,X2,X3] :
( X2 = k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3)
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| ~ v3_orders_2(k7_lattice3(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(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(forward_subsumption_resolution,[status(thm)],[f13220,f740]) ).
fof(f13247,plain,
! [X0,X1,X2,X3] :
( X2 = k1_waybel34(k7_lattice3(X1),k7_lattice3(X0),X3)
| ~ v17_waybel_0(X3,k7_lattice3(X1),k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_lattice3(k7_lattice3(X0))
| ~ v1_lattice3(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| ~ v3_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(k7_lattice3(X1))
| ~ v2_lattice3(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(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(forward_subsumption_resolution,[status(thm)],[f13221,f767]) ).
fof(f13251,plain,
! [X0] :
( ~ sQ44_spl
| ~ sQ3_spl
| X0 = k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl)
| ~ v3_lattice3(k7_lattice3(sK1_skl))
| ~ v3_lattice3(k7_lattice3(sK0_skl))
| ~ l1_orders_2(k7_lattice3(sK1_skl))
| ~ v2_lattice3(k7_lattice3(sK1_skl))
| ~ v1_lattice3(k7_lattice3(sK1_skl))
| ~ v4_orders_2(k7_lattice3(sK1_skl))
| ~ v3_orders_2(k7_lattice3(sK1_skl))
| ~ v2_orders_2(k7_lattice3(sK1_skl))
| ~ l1_orders_2(k7_lattice3(sK0_skl))
| ~ v2_lattice3(k7_lattice3(sK0_skl))
| ~ v1_lattice3(k7_lattice3(sK0_skl))
| ~ v4_orders_2(k7_lattice3(sK0_skl))
| ~ v3_waybel_1(k1_waybel_1(sK1_skl,sK0_skl,X0,sK2_skl),sK1_skl,sK0_skl)
| ~ m2_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl)))
| ~ v1_funct_2(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl)))
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_skl)
| ~ m2_relset_1(X0,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(X0,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| v3_struct_0(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) ),
inference(resolution,[status(thm)],[f13247,f1492]) ).
fof(f13261,definition,
! [X0] :
( sQ1570_spl
<=> ( X0 = k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl)
| ~ v3_waybel_1(k1_waybel_1(sK1_skl,sK0_skl,X0,sK2_skl),sK1_skl,sK0_skl)
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m2_relset_1(X0,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(X0,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1570_spl])],[split_symbol_definition]) ).
fof(f13262,plain,
! [X0] :
( ~ sQ1570_spl
| X0 = k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl)
| ~ v3_waybel_1(k1_waybel_1(sK1_skl,sK0_skl,X0,sK2_skl),sK1_skl,sK0_skl)
| ~ m2_relset_1(X0,u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ v1_funct_2(X0,u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m2_relset_1(X0,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(X0,u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(component_clause,[status(thm)],[f13261]) ).
fof(f13264,plain,
( ~ sQ44_spl
| ~ sQ3_spl
| ~ sQ56_spl
| ~ sQ50_spl
| ~ sQ13_spl
| ~ sQ55_spl
| ~ sQ54_spl
| ~ sQ53_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ12_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ47_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ4_spl
| sQ1570_spl
| ~ sQ0_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| sQ67_spl
| ~ sQ1_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f13251,f1541,f1422,f1425,f1428,f1234,f1636,f1404,f1407,f1410,f1231,f13261,f1248,f1251,f1237,f1257,f1270,f1501,f1504,f1507,f1299,f1513,f1516,f1519,f1522,f1525,f1302,f1510,f1528,f1240,f1464]) ).
fof(f13280,plain,
( ~ sQ1570_spl
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl))
| ~ v18_waybel_0(sK2_skl,sK0_skl,sK1_skl)
| ~ v3_lattice3(sK0_skl)
| ~ v3_lattice3(sK1_skl)
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_funct_1(sK2_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)
| k2_waybel34(sK1_skl,sK0_skl,sK2_skl) = k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl)
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m2_relset_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k2_waybel34(sK1_skl,sK0_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k2_waybel34(sK1_skl,sK0_skl,sK2_skl)) ),
inference(resolution,[status(thm)],[f13262,f1223]) ).
fof(f13282,definition,
( sQ1573_spl
<=> k2_waybel34(sK1_skl,sK0_skl,sK2_skl) = k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ1573_spl])],[split_symbol_definition]) ).
fof(f13283,plain,
( ~ sQ1573_spl
| k2_waybel34(sK1_skl,sK0_skl,sK2_skl) = k1_waybel34(k7_lattice3(sK0_skl),k7_lattice3(sK1_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f13282]) ).
fof(f13285,plain,
( ~ sQ1570_spl
| ~ sQ154_spl
| ~ sQ33_spl
| ~ sQ39_spl
| ~ sQ2_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ0_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ34_spl
| sQ1573_spl
| ~ sQ169_spl
| ~ sQ161_spl
| ~ sQ167_spl
| ~ sQ166_spl
| ~ sQ165_spl ),
inference(split_clause,[status(thm)],[f13280,f2191,f2194,f2197,f2176,f2205,f13282,f1422,f1425,f1428,f1431,f1434,f1234,f1404,f1407,f1410,f1413,f1416,f1231,f1248,f1251,f1237,f1437,f1419,f2153,f13261]) ).
fof(f13291,plain,
( ~ sQ1573_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13283,f1290]) ).
fof(f13292,plain,
( ~ sQ1573_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f13291]) ).
fof(f13293,plain,
$false,
inference(sat_refutation,[status(thm)],[f1243,f1260,f1262,f1264,f1266,f1273,f1285,f1287,f1289,f1326,f1328,f1467,f1469,f1471,f1473,f1475,f1477,f1479,f1481,f1483,f1485,f1487,f1489,f1491,f1544,f1554,f1566,f1580,f1599,f1601,f1616,f1626,f1639,f1649,f1718,f1763,f1781,f1793,f2208,f2209,f2211,f2251,f2273,f2413,f2415,f2536,f2694,f2705,f2811,f3121,f3185,f3471,f3580,f3582,f3584,f3617,f3685,f3689,f3691,f3693,f3695,f3697,f3837,f3952,f3958,f4054,f4056,f4111,f4574,f5515,f5620,f5622,f5789,f5791,f5793,f5795,f5797,f5905,f6154,f6156,f6270,f6524,f6526,f6950,f7026,f7101,f7103,f7219,f7429,f7466,f7468,f7539,f7554,f8295,f8358,f8360,f8362,f8382,f8393,f8515,f8605,f8607,f8716,f8741,f8743,f8765,f9909,f10092,f11001,f11003,f11005,f11007,f11009,f11011,f11013,f11015,f11017,f11019,f11021,f11023,f11025,f11027,f11029,f11031,f11033,f11777,f12656,f12703,f12705,f12739,f12741,f12743,f12762,f13215,f13264,f13285,f13292]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT355+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n015.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Sun Sep 20 23:51:05 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.47 % Drodi V4.1.1
% 70.45/9.46 % Refutation found
% 70.45/9.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 70.45/9.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 57.75/9.54 % Elapsed time: 9.091327 seconds
% 57.75/9.54 % CPU time: 71.372910 seconds
% 57.75/9.54 % Total memory used: 420.282 MB
% 57.75/9.54 % Net memory used: 410.886 MB
%------------------------------------------------------------------------------