%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT354+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 : n018.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 114.23s 15.08s
% Output : CNFRefutation 114.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 138
% Syntax : Number of formulae : 603 ( 132 unt; 97 def)
% Number of atoms : 2746 ( 43 equ)
% Maximal formula atoms : 41 ( 4 avg)
% Number of connectives : 3548 (1405 ~;1418 |; 572 &)
% ( 104 <=>; 49 =>; 0 <=; 0 <~>)
% Maximal formula depth : 46 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 144 ( 142 usr; 98 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 20 con; 0-4 aty)
% Number of variables : 277 ( 257 !; 20 ?)
% 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))
& v17_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> k1_waybel34(A,B,C) = k2_waybel34(k7_lattice3(B),k7_lattice3(A),k3_waybel34(A,B,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))
& v17_waybel_0(C,A,B)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> k1_waybel34(A,B,C) = k2_waybel34(k7_lattice3(B),k7_lattice3(A),k3_waybel34(A,B,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(f25,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
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(f41,axiom,
! [A,B] :
( ( 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) )
=> ! [C] :
( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
=> ( ( v5_waybel_1(C,B,A)
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_1(C) )
=> ( v22_waybel_0(C,A,B)
& v20_waybel_0(C,A,B)
& v18_waybel_0(C,A,B)
& v1_partfun1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& ~ v1_xboole_0(C)
& v1_funct_1(C) ) ) ) ),
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(f79,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)
& 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(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(k1_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(f87,axiom,
! [A] :
( v1_relat_1(A)
=> v1_relat_1(k4_relat_1(A)) ),
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(f96,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [A] :
( l1_orders_2(A)
=> m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(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(f130,axiom,
! [A,B,C] :
( ( m1_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v17_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))
& v5_waybel_1(k3_waybel34(A,B,C),k7_lattice3(B),k7_lattice3(A))
& v22_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v20_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v18_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(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(f138,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> ( v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A) )
=> ( v2_lattice3(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) ) ),
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(f158,axiom,
? [A] :
( v1_funct_1(A)
& v1_relat_1(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(f171,axiom,
? [A] :
( v1_funct_1(A)
& v1_xboole_0(A)
& v1_relat_1(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(f179,axiom,
? [A] :
( ~ v3_struct_0(A)
& l1_struct_0(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(A,B,C) != k2_waybel34(k7_lattice3(B),k7_lattice3(A),k3_waybel34(A,B,C))
& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))
& v17_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(sK0_skl,sK1_skl,sK2_skl) != k2_waybel34(k7_lattice3(sK1_skl),k7_lattice3(sK0_skl),k3_waybel34(sK0_skl,sK1_skl,sK2_skl))
& m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
& v17_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(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(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,
v17_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(sK0_skl,sK1_skl,sK2_skl) != k2_waybel34(k7_lattice3(sK1_skl),k7_lattice3(sK0_skl),k3_waybel34(sK0_skl,sK1_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(f313,plain,
! [A,B,C] :
( v1_relat_1(C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f314,plain,
! [C] :
( v1_relat_1(C)
| ! [A,B] : ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
inference(miniscoping,[status(thm)],[f313]) ).
fof(f315,plain,
! [X0,X1,X2] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
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(f356,plain,
! [X0] :
( v1_lattice3(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f354]) ).
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(f389,plain,
! [A,B] :
( ! [C] :
( ( v22_waybel_0(C,A,B)
& v20_waybel_0(C,A,B)
& v18_waybel_0(C,A,B)
& v1_partfun1(C,u1_struct_0(A),u1_struct_0(B))
& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
& ~ v1_xboole_0(C)
& v1_funct_1(C) )
| ~ v5_waybel_1(C,B,A)
| ~ v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
| ~ v1_funct_1(C)
| ~ m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
| ~ 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)],[f41]) ).
fof(f394,plain,
! [X0,X1,X2] :
( v18_waybel_0(X2,X0,X1)
| ~ v5_waybel_1(X2,X1,X0)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f389]) ).
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(f588,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(f593,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(f602,plain,
! [A,B,C] :
( ( m2_relset_1(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_2(k1_waybel34(A,B,C),u1_struct_0(B),u1_struct_0(A))
& v1_funct_1(k1_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)
| ~ 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)],[f79]) ).
fof(f603,plain,
! [X0,X1,X2] :
( v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ 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)],[f602]) ).
fof(f604,plain,
! [X0,X1,X2] :
( v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ 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)
| ~ 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)],[f602]) ).
fof(f605,plain,
! [X0,X1,X2] :
( m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ 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)
| ~ 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)],[f602]) ).
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(f616,plain,
! [A] :
( v1_relat_1(k4_relat_1(A))
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f617,plain,
! [X0] :
( v1_relat_1(k4_relat_1(X0))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f616]) ).
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(f625,plain,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| ~ m2_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f96]) ).
fof(f626,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f625]) ).
fof(f627,plain,
! [A] :
( m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f628,plain,
! [X0] :
( m2_relset_1(u1_orders_2(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[status(thm)],[f627]) ).
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(f774,plain,
! [A,B,C] :
( ( v5_orders_3(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v5_waybel_1(k3_waybel34(A,B,C),k7_lattice3(B),k7_lattice3(A))
& v22_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v20_waybel_0(k3_waybel34(A,B,C),k7_lattice3(A),k7_lattice3(B))
& v18_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))
| ~ v17_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)],[f130]) ).
fof(f783,plain,
! [X0,X1,X2] :
( v5_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X1),k7_lattice3(X0))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_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)],[f774]) ).
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(f819,plain,
! [A] :
( ( v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f820,plain,
! [X0] :
( ~ v3_struct_0(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f819]) ).
fof(f831,plain,
! [A] :
( ( v2_lattice3(k7_lattice3(A))
& v1_orders_2(k7_lattice3(A))
& ~ v3_struct_0(k7_lattice3(A)) )
| ~ l1_orders_2(A)
| ~ v1_lattice3(A) ),
inference(pre_NNF_transformation,[status(thm)],[f141]) ).
fof(f834,plain,
! [X0] :
( v2_lattice3(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0) ),
inference(cnf_transformation,[status(thm)],[f831]) ).
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(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(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(f914,plain,
( v1_funct_1(sK13_skl)
& v1_relat_1(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f158]) ).
fof(f915,plain,
v1_relat_1(sK13_skl),
inference(cnf_transformation,[status(thm)],[f914]) ).
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(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(f973,plain,
v1_yellow_0(sK22_skl),
inference(cnf_transformation,[status(thm)],[f966]) ).
fof(f975,plain,
v3_yellow_0(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(f997,plain,
v1_yellow_0(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(f1013,plain,
v1_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(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(f1041,plain,
( v1_funct_1(sK26_skl)
& v1_xboole_0(sK26_skl)
& v1_relat_1(sK26_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f171]) ).
fof(f1042,plain,
v1_relat_1(sK26_skl),
inference(cnf_transformation,[status(thm)],[f1041]) ).
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(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(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(f1069,plain,
v1_yellow_0(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(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(f1097,plain,
v2_yellow_0(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1099,plain,
v24_waybel_0(sK30_skl),
inference(cnf_transformation,[status(thm)],[f1086]) ).
fof(f1100,plain,
v25_waybel_0(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(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(f1124,plain,
( ~ v3_struct_0(sK34_skl)
& l1_struct_0(sK34_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(A,sK34_skl)],[f179]) ).
fof(f1126,plain,
~ v3_struct_0(sK34_skl),
inference(cnf_transformation,[status(thm)],[f1124]) ).
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(f1147,plain,
v2_orders_2(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1148,plain,
v3_orders_2(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1149,plain,
v4_orders_2(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1150,plain,
v1_lattice3(sK37_skl),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f1153,plain,
v2_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(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(f1180,plain,
v4_orders_2(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(f1193,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(f1234,plain,
! [X0,X1,X2] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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(destructive_equality_resolution,[status(thm)],[f588]) ).
fof(f1237,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(f1238,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)],[f1237]) ).
fof(f1242,plain,
! [X0] :
( ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| v1_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f356,f384]) ).
fof(f1255,plain,
! [X0,X1,X2] :
( v5_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X1),k7_lattice3(X0))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_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)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f783,f1282]) ).
fof(f1278,plain,
! [X0,X1,X2,X3] :
( ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 = k2_waybel34(X0,X1,X2)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f593,f1282]) ).
fof(f1281,plain,
! [X0,X1,X2] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1234,f1282]) ).
fof(f1282,plain,
! [X0] :
( ~ v2_lattice3(X0)
| v1_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1242]) ).
fof(f1294,plain,
! [X0,X1,X2] :
( v5_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X1),k7_lattice3(X0))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v17_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)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1255,f1282]) ).
fof(f1317,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)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1278,f1282]) ).
fof(f1320,plain,
! [X0,X1,X2] :
( v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ m2_relset_1(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1281,f1282]) ).
fof(f1322,plain,
! [X0] :
( ~ v1_lattice3(X0)
| ~ l1_orders_2(X0)
| v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f357,f310]) ).
fof(f1323,plain,
! [X0] :
( ~ v1_lattice3(X0)
| v2_lattice3(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1322]) ).
fof(f1334,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(f1335,plain,
! [X0,X1] :
( v1_funct_1(k1_waybel34(X0,X1,sK2_skl))
| ~ m1_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)
| ~ 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)],[f603,f215]) ).
fof(f1352,plain,
( k3_waybel34(sK0_skl,sK1_skl,sK2_skl) = sK2_skl
| ~ v1_funct_2(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)],[f1334,f218]) ).
fof(f1353,definition,
( sQ4_spl
<=> l1_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1355,plain,
( sQ4_spl
| ~ l1_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1353]) ).
fof(f1356,definition,
( sQ5_spl
<=> l1_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1358,plain,
( sQ5_spl
| ~ l1_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1356]) ).
fof(f1359,definition,
( sQ6_spl
<=> v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1361,plain,
( sQ6_spl
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1359]) ).
fof(f1362,definition,
( sQ7_spl
<=> k3_waybel34(sK0_skl,sK1_skl,sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1363,plain,
( ~ sQ7_spl
| k3_waybel34(sK0_skl,sK1_skl,sK2_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f1362]) ).
fof(f1365,plain,
( sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1352,f1353,f1356,f1359,f1362]) ).
fof(f1368,plain,
( ~ sQ7_spl
| k1_waybel34(sK0_skl,sK1_skl,sK2_skl) != k2_waybel34(k7_lattice3(sK1_skl),k7_lattice3(sK0_skl),sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f1363,f219]) ).
fof(f1369,plain,
( ~ v2_lattice3(sK1_skl)
| v1_lattice3(sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1282,f213]) ).
fof(f1370,plain,
( ~ v2_lattice3(sK0_skl)
| v1_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1282,f206]) ).
fof(f1371,definition,
( sQ8_spl
<=> v1_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1374,definition,
( sQ9_spl
<=> v2_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1376,plain,
( sQ9_spl
| ~ v2_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f1374]) ).
fof(f1377,plain,
( ~ sQ9_spl
| sQ8_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1369,f1356,f1371,f1374]) ).
fof(f1378,definition,
( sQ10_spl
<=> v1_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1381,definition,
( sQ11_spl
<=> v2_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1383,plain,
( sQ11_spl
| ~ v2_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1381]) ).
fof(f1384,plain,
( ~ sQ11_spl
| sQ10_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1370,f1353,f1378,f1381]) ).
fof(f1385,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1355,f207]) ).
fof(f1386,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1385]) ).
fof(f1387,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1358,f214]) ).
fof(f1388,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1387]) ).
fof(f1389,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1361,f216]) ).
fof(f1390,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1389]) ).
fof(f1417,plain,
! [X0,X1] :
( ~ m2_relset_1(sK2_skl,u1_struct_0(X0),u1_struct_0(X1))
| v1_funct_1(k1_waybel34(X0,X1,sK2_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(X0),u1_struct_0(X1))
| ~ 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)],[f1335,f1192]) ).
fof(f1418,plain,
( v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v1_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(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)],[f1417,f218]) ).
fof(f1419,definition,
( sQ17_spl
<=> v2_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1421,plain,
( sQ17_spl
| ~ v2_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1419]) ).
fof(f1422,definition,
( sQ18_spl
<=> v3_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1424,plain,
( sQ18_spl
| ~ v3_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1422]) ).
fof(f1425,definition,
( sQ19_spl
<=> v4_orders_2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1427,plain,
( sQ19_spl
| ~ v4_orders_2(sK0_skl) ),
inference(component_clause,[status(thm)],[f1425]) ).
fof(f1428,definition,
( sQ20_spl
<=> v2_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1430,plain,
( sQ20_spl
| ~ v2_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1431,definition,
( sQ21_spl
<=> v3_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1433,plain,
( sQ21_spl
| ~ v3_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1431]) ).
fof(f1434,definition,
( sQ22_spl
<=> v4_orders_2(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( sQ22_spl
| ~ v4_orders_2(sK1_skl) ),
inference(component_clause,[status(thm)],[f1434]) ).
fof(f1437,definition,
( sQ23_spl
<=> v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1438,plain,
( ~ sQ23_spl
| v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f1437]) ).
fof(f1440,plain,
( sQ23_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ4_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1418,f1419,f1422,f1425,f1378,f1381,f1353,f1428,f1431,f1434,f1371,f1374,f1356,f1359,f1437]) ).
fof(f1441,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1383,f205]) ).
fof(f1442,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1441]) ).
fof(f1443,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1376,f212]) ).
fof(f1444,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1443]) ).
fof(f1446,plain,
! [X0,X1] :
( ~ sQ23_spl
| k3_waybel34(X0,X1,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) = k1_waybel34(sK0_skl,sK1_skl,sK2_skl)
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0) ),
inference(resolution,[status(thm)],[f1438,f595]) ).
fof(f1456,plain,
( ~ sQ23_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(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)
| ~ v2_lattice3(sK0_skl)
| ~ v1_lattice3(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| k3_waybel34(sK1_skl,sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) = k1_waybel34(sK0_skl,sK1_skl,sK2_skl)
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ l1_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1446,f605]) ).
fof(f1457,definition,
( sQ24_spl
<=> v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f1458,plain,
( ~ sQ24_spl
| v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1457]) ).
fof(f1459,plain,
( sQ24_spl
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1457]) ).
fof(f1460,definition,
( sQ25_spl
<=> k3_waybel34(sK1_skl,sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) = k1_waybel34(sK0_skl,sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1461,plain,
( ~ sQ25_spl
| k3_waybel34(sK1_skl,sK0_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)) = k1_waybel34(sK0_skl,sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f1460]) ).
fof(f1463,definition,
( sQ26_spl
<=> v1_funct_1(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1465,plain,
( sQ26_spl
| ~ v1_funct_1(sK2_skl) ),
inference(component_clause,[status(thm)],[f1463]) ).
fof(f1466,definition,
( sQ27_spl
<=> m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1468,plain,
( sQ27_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1466]) ).
fof(f1469,plain,
( ~ sQ23_spl
| ~ sQ27_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ25_spl
| ~ sQ24_spl
| ~ sQ4_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1456,f1356,f1353,f1457,f1460,f1419,f1422,f1425,f1378,f1381,f1428,f1431,f1434,f1371,f1374,f1463,f1359,f1466,f1437]) ).
fof(f1470,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1436,f210]) ).
fof(f1471,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1470]) ).
fof(f1472,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1433,f209]) ).
fof(f1473,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1472]) ).
fof(f1474,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1430,f208]) ).
fof(f1475,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1474]) ).
fof(f1476,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1427,f203]) ).
fof(f1477,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1476]) ).
fof(f1478,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1424,f202]) ).
fof(f1479,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1478]) ).
fof(f1480,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1421,f201]) ).
fof(f1481,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f1480]) ).
fof(f1485,plain,
( sQ27_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(resolution,[status(thm)],[f1468,f1192]) ).
fof(f1486,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1485,f218]) ).
fof(f1487,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1486]) ).
fof(f1488,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1465,f215]) ).
fof(f1489,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1488]) ).
fof(f1507,plain,
( sQ24_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(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)
| ~ 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)],[f1459,f604]) ).
fof(f1508,plain,
( sQ24_spl
| ~ sQ27_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ4_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1507,f1419,f1422,f1425,f1378,f1381,f1353,f1428,f1431,f1434,f1371,f1374,f1356,f1463,f1359,f1466,f1457]) ).
fof(f1519,plain,
( ~ sQ7_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)],[f1363,f614]) ).
fof(f1520,definition,
( sQ30_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,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1523,plain,
( ~ sQ7_spl
| sQ30_spl
| ~ sQ27_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1519,f1353,f1356,f1463,f1359,f1466,f1520,f1362]) ).
fof(f1524,plain,
( ~ sQ7_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)],[f1363,f615]) ).
fof(f1525,definition,
( sQ31_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,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1526,plain,
( ~ sQ31_spl
| m2_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl))) ),
inference(component_clause,[status(thm)],[f1525]) ).
fof(f1528,plain,
( ~ sQ7_spl
| sQ31_spl
| ~ sQ27_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1524,f1353,f1356,f1463,f1359,f1466,f1525,f1362]) ).
fof(f1558,definition,
( sQ37_spl
<=> v2_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1560,plain,
( sQ37_spl
| ~ v2_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1558]) ).
fof(f1561,definition,
( sQ38_spl
<=> v3_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1563,plain,
( sQ38_spl
| ~ v3_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1561]) ).
fof(f1564,definition,
( sQ39_spl
<=> v4_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1566,plain,
( sQ39_spl
| ~ v4_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1564]) ).
fof(f1570,definition,
( sQ41_spl
<=> v2_lattice3(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1572,plain,
( sQ41_spl
| ~ v2_lattice3(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1570]) ).
fof(f1573,definition,
( sQ42_spl
<=> l1_orders_2(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1575,plain,
( sQ42_spl
| ~ l1_orders_2(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1573]) ).
fof(f1576,definition,
( sQ43_spl
<=> v2_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1578,plain,
( sQ43_spl
| ~ v2_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1576]) ).
fof(f1579,definition,
( sQ44_spl
<=> v3_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1581,plain,
( sQ44_spl
| ~ v3_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1579]) ).
fof(f1582,definition,
( sQ45_spl
<=> v4_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1584,plain,
( sQ45_spl
| ~ v4_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1582]) ).
fof(f1588,definition,
( sQ47_spl
<=> v2_lattice3(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1590,plain,
( sQ47_spl
| ~ v2_lattice3(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1588]) ).
fof(f1591,definition,
( sQ48_spl
<=> l1_orders_2(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1593,plain,
( sQ48_spl
| ~ l1_orders_2(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1591]) ).
fof(f1602,plain,
( sQ48_spl
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1593,f622]) ).
fof(f1603,plain,
( sQ48_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1602,f1356,f1591]) ).
fof(f1604,plain,
( sQ42_spl
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1575,f622]) ).
fof(f1605,plain,
( sQ42_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1604,f1353,f1573]) ).
fof(f1637,definition,
( sQ55_spl
<=> m1_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1639,plain,
( sQ55_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl))) ),
inference(component_clause,[status(thm)],[f1637]) ).
fof(f1652,plain,
( sQ55_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl))) ),
inference(resolution,[status(thm)],[f1639,f1192]) ).
fof(f1653,plain,
( sQ55_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1652,f1526]) ).
fof(f1654,plain,
( sQ55_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1653]) ).
fof(f1670,plain,
( sQ41_spl
| ~ l1_orders_2(sK0_skl)
| ~ v1_lattice3(sK0_skl) ),
inference(resolution,[status(thm)],[f1572,f834]) ).
fof(f1671,definition,
( sQ60_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1672,plain,
( ~ sQ60_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1671]) ).
fof(f1674,definition,
( sQ61_spl
<=> v3_lattice3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1676,plain,
( sQ61_spl
| ~ v3_lattice3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1674]) ).
fof(f1678,plain,
( sQ41_spl
| ~ sQ4_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1670,f1378,f1353,f1570]) ).
fof(f1694,plain,
( sQ39_spl
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1566,f787]) ).
fof(f1695,plain,
( sQ39_spl
| ~ sQ4_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1694,f1425,f1353,f1564]) ).
fof(f1696,plain,
( sQ38_spl
| ~ l1_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1563,f767]) ).
fof(f1697,plain,
( sQ38_spl
| ~ sQ4_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1696,f1422,f1353,f1561]) ).
fof(f1698,plain,
( sQ37_spl
| ~ l1_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1560,f740]) ).
fof(f1699,plain,
( sQ37_spl
| ~ sQ4_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1698,f1419,f1353,f1558]) ).
fof(f1742,plain,
( sQ47_spl
| ~ l1_orders_2(sK1_skl)
| ~ v1_lattice3(sK1_skl) ),
inference(resolution,[status(thm)],[f1590,f834]) ).
fof(f1743,definition,
( sQ72_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1744,plain,
( ~ sQ72_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f1743]) ).
fof(f1746,definition,
( sQ73_spl
<=> v3_lattice3(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1748,plain,
( sQ73_spl
| ~ v3_lattice3(sK1_skl) ),
inference(component_clause,[status(thm)],[f1746]) ).
fof(f1750,plain,
( sQ47_spl
| ~ sQ5_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1742,f1371,f1356,f1588]) ).
fof(f1755,plain,
( sQ45_spl
| ~ l1_orders_2(sK1_skl)
| ~ v4_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1584,f787]) ).
fof(f1756,plain,
( sQ45_spl
| ~ sQ5_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1755,f1434,f1356,f1582]) ).
fof(f1778,plain,
( sQ44_spl
| ~ l1_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1581,f767]) ).
fof(f1779,plain,
( sQ44_spl
| ~ sQ5_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f1778,f1431,f1356,f1579]) ).
fof(f1780,plain,
( sQ43_spl
| ~ l1_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1578,f740]) ).
fof(f1781,plain,
( sQ43_spl
| ~ sQ5_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1780,f1428,f1356,f1576]) ).
fof(f1791,definition,
( sQ77_spl
<=> v3_yellow_0(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1793,plain,
( sQ77_spl
| ~ v3_yellow_0(sK22_skl) ),
inference(component_clause,[status(thm)],[f1791]) ).
fof(f1807,plain,
( sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1748,f213]) ).
fof(f1808,plain,
sQ73_spl,
inference(contradiction_clause,[status(thm)],[f1807]) ).
fof(f1811,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1676,f206]) ).
fof(f1812,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1811]) ).
fof(f1817,plain,
( ~ sQ72_spl
| ~ v1_lattice3(sK1_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(resolution,[status(thm)],[f1744,f310]) ).
fof(f1819,plain,
( ~ sQ72_spl
| ~ sQ8_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1817,f1356,f1371,f1743]) ).
fof(f1821,plain,
( ~ sQ60_spl
| ~ v1_lattice3(sK0_skl)
| ~ l1_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1672,f310]) ).
fof(f1823,plain,
( ~ sQ60_spl
| ~ sQ10_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1821,f1353,f1378,f1671]) ).
fof(f1919,plain,
( ~ sQ25_spl
| m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ l1_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(paramodulation,[status(thm)],[f1461,f615]) ).
fof(f1920,plain,
( ~ sQ25_spl
| v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ l1_orders_2(sK0_skl)
| ~ l1_orders_2(sK1_skl) ),
inference(paramodulation,[status(thm)],[f1461,f614]) ).
fof(f1921,definition,
( sQ99_spl
<=> m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1922,plain,
( ~ sQ99_spl
| m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1921]) ).
fof(f1923,plain,
( sQ99_spl
| ~ m1_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1921]) ).
fof(f1924,definition,
( sQ100_spl
<=> m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1927,plain,
( ~ sQ25_spl
| sQ100_spl
| ~ sQ99_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ4_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1919,f1356,f1353,f1437,f1457,f1921,f1924,f1460]) ).
fof(f1928,definition,
( sQ101_spl
<=> v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1931,plain,
( ~ sQ25_spl
| sQ101_spl
| ~ sQ99_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ4_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1920,f1356,f1353,f1437,f1457,f1921,f1928,f1460]) ).
fof(f1936,definition,
( sQ102_spl
<=> v3_struct_0(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1937,plain,
( ~ sQ102_spl
| v3_struct_0(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1936]) ).
fof(f1939,definition,
( sQ103_spl
<=> v3_lattice3(k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1941,plain,
( sQ103_spl
| ~ v3_lattice3(k7_lattice3(sK1_skl)) ),
inference(component_clause,[status(thm)],[f1939]) ).
fof(f1944,plain,
( sQ103_spl
| ~ l1_orders_2(sK1_skl)
| ~ v3_lattice3(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1941,f845]) ).
fof(f1945,plain,
( sQ103_spl
| ~ sQ5_spl
| ~ sQ73_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1944,f1743,f1746,f1356,f1939]) ).
fof(f1947,plain,
( ~ sQ102_spl
| ~ l1_orders_2(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1937,f820]) ).
fof(f1952,plain,
( ~ sQ102_spl
| ~ sQ5_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1947,f1743,f1356,f1936]) ).
fof(f2028,plain,
( v5_waybel_1(k3_waybel34(sK0_skl,sK1_skl,sK2_skl),k7_lattice3(sK1_skl),k7_lattice3(sK0_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)
| ~ 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)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f1294,f217]) ).
fof(f2029,definition,
( sQ111_spl
<=> v5_waybel_1(k3_waybel34(sK0_skl,sK1_skl,sK2_skl),k7_lattice3(sK1_skl),k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f2030,plain,
( ~ sQ111_spl
| v5_waybel_1(k3_waybel34(sK0_skl,sK1_skl,sK2_skl),k7_lattice3(sK1_skl),k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2029]) ).
fof(f2032,plain,
( sQ111_spl
| ~ sQ27_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ73_spl
| ~ sQ9_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ4_spl
| ~ sQ61_spl
| ~ sQ11_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f2028,f1419,f1422,f1425,f1381,f1674,f1353,f1428,f1431,f1434,f1374,f1746,f1356,f1463,f1359,f1466,f2029]) ).
fof(f2033,plain,
( ~ sQ111_spl
| ~ sQ7_spl
| v5_waybel_1(sK2_skl,k7_lattice3(sK1_skl),k7_lattice3(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1363,f2030]) ).
fof(f2064,definition,
( sQ117_spl
<=> v3_struct_0(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2065,plain,
( ~ sQ117_spl
| v3_struct_0(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2064]) ).
fof(f2067,definition,
( sQ118_spl
<=> v3_lattice3(k7_lattice3(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( sQ118_spl
| ~ v3_lattice3(k7_lattice3(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2067]) ).
fof(f2072,plain,
( sQ118_spl
| ~ l1_orders_2(sK0_skl)
| ~ v3_lattice3(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f2069,f845]) ).
fof(f2073,plain,
( sQ118_spl
| ~ sQ4_spl
| ~ sQ61_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2072,f1671,f1674,f1353,f2067]) ).
fof(f2075,plain,
( ~ sQ117_spl
| ~ l1_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f2065,f820]) ).
fof(f2080,plain,
( ~ sQ117_spl
| ~ sQ4_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f2075,f1671,f1353,f2064]) ).
fof(f2535,plain,
( sQ99_spl
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1923,f1192]) ).
fof(f2536,plain,
( sQ99_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(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)
| ~ 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)],[f2535,f605]) ).
fof(f2537,plain,
( sQ99_spl
| ~ sQ27_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ4_spl
| ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f2536,f1419,f1422,f1425,f1378,f1381,f1353,f1428,f1431,f1434,f1371,f1374,f1356,f1463,f1359,f1466,f1921]) ).
fof(f2541,plain,
( ~ sQ99_spl
| m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1922,f1193]) ).
fof(f3038,plain,
! [X0,X1,X2] :
( ~ 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)
| ~ 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)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(resolution,[status(thm)],[f1320,f605]) ).
fof(f3039,definition,
( sQ256_spl
<=> m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f3041,plain,
( sQ256_spl
| ~ m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)) ),
inference(component_clause,[status(thm)],[f3039]) ).
fof(f3042,definition,
( sQ257_spl
<=> v17_waybel_0(sK2_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f3044,plain,
( sQ257_spl
| ~ v17_waybel_0(sK2_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f3042]) ).
fof(f3045,definition,
( sQ258_spl
<=> v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f3046,plain,
( ~ sQ258_spl
| v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f3045]) ).
fof(f3049,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3038]) ).
fof(f3050,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| v3_waybel_1(k1_waybel_1(X0,X1,X2,k1_waybel34(X0,X1,X2)),X0,X1)
| ~ v1_funct_2(k1_waybel34(X0,X1,X2),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k1_waybel34(X0,X1,X2))
| ~ 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)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3049,f1323]) ).
fof(f3051,plain,
( sQ257_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3044,f217]) ).
fof(f3052,plain,
sQ257_spl,
inference(contradiction_clause,[status(thm)],[f3051]) ).
fof(f3053,plain,
( sQ256_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3041,f218]) ).
fof(f3054,plain,
sQ256_spl,
inference(contradiction_clause,[status(thm)],[f3053]) ).
fof(f3065,definition,
( sQ259_spl
<=> m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f3067,plain,
( sQ259_spl
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3065]) ).
fof(f3077,plain,
( sQ259_spl
| ~ sQ99_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3067,f2541]) ).
fof(f3078,plain,
( sQ259_spl
| ~ sQ99_spl ),
inference(contradiction_clause,[status(thm)],[f3077]) ).
fof(f3087,plain,
( ~ sQ111_spl
| ~ sQ7_spl
| v18_waybel_0(sK2_skl,k7_lattice3(sK0_skl),k7_lattice3(sK1_skl))
| ~ v1_funct_2(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl)))
| ~ v1_funct_1(sK2_skl)
| ~ m1_relset_1(sK2_skl,u1_struct_0(k7_lattice3(sK0_skl)),u1_struct_0(k7_lattice3(sK1_skl)))
| ~ l1_orders_2(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))
| v3_struct_0(k7_lattice3(sK1_skl))
| ~ l1_orders_2(k7_lattice3(sK0_skl))
| ~ v4_orders_2(k7_lattice3(sK0_skl))
| ~ v3_orders_2(k7_lattice3(sK0_skl))
| ~ v2_orders_2(k7_lattice3(sK0_skl))
| v3_struct_0(k7_lattice3(sK0_skl)) ),
inference(resolution,[status(thm)],[f394,f2033]) ).
fof(f3099,definition,
( sQ264_spl
<=> v18_waybel_0(sK2_skl,k7_lattice3(sK0_skl),k7_lattice3(sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f3102,plain,
( ~ sQ111_spl
| ~ sQ7_spl
| sQ264_spl
| ~ sQ30_spl
| ~ sQ26_spl
| ~ sQ55_spl
| ~ sQ48_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| sQ102_spl
| ~ sQ42_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f3087,f2064,f1558,f1561,f1564,f1573,f1936,f1576,f1579,f1582,f1591,f1637,f1463,f1520,f3099,f1362,f2029]) ).
fof(f3199,definition,
( sQ278_spl
<=> v2_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f3201,plain,
( sQ278_spl
| ~ v2_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f3199]) ).
fof(f3202,definition,
( sQ279_spl
<=> v3_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f3204,plain,
( sQ279_spl
| ~ v3_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f3202]) ).
fof(f3205,definition,
( sQ280_spl
<=> v4_orders_2(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f3207,plain,
( sQ280_spl
| ~ v4_orders_2(sK30_skl) ),
inference(component_clause,[status(thm)],[f3205]) ).
fof(f3208,definition,
( sQ281_spl
<=> v24_waybel_0(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition]) ).
fof(f3210,plain,
( sQ281_spl
| ~ v24_waybel_0(sK30_skl) ),
inference(component_clause,[status(thm)],[f3208]) ).
fof(f3213,plain,
( sQ281_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3210,f1099]) ).
fof(f3214,plain,
sQ281_spl,
inference(contradiction_clause,[status(thm)],[f3213]) ).
fof(f3215,plain,
( sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3207,f1092]) ).
fof(f3216,plain,
sQ280_spl,
inference(contradiction_clause,[status(thm)],[f3215]) ).
fof(f3217,plain,
( sQ279_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3204,f1091]) ).
fof(f3218,plain,
sQ279_spl,
inference(contradiction_clause,[status(thm)],[f3217]) ).
fof(f3219,plain,
( sQ278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3201,f1090]) ).
fof(f3220,plain,
sQ278_spl,
inference(contradiction_clause,[status(thm)],[f3219]) ).
fof(f3222,definition,
( sQ282_spl
<=> v3_struct_0(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f3223,plain,
( ~ sQ282_spl
| v3_struct_0(sK30_skl) ),
inference(component_clause,[status(thm)],[f3222]) ).
fof(f3225,definition,
( sQ283_spl
<=> v25_waybel_0(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f3227,plain,
( sQ283_spl
| ~ v25_waybel_0(sK30_skl) ),
inference(component_clause,[status(thm)],[f3225]) ).
fof(f3229,plain,
( sQ283_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3227,f1100]) ).
fof(f3230,plain,
sQ283_spl,
inference(contradiction_clause,[status(thm)],[f3229]) ).
fof(f3231,plain,
( ~ sQ282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3223,f1088]) ).
fof(f3232,plain,
~ sQ282_spl,
inference(contradiction_clause,[status(thm)],[f3231]) ).
fof(f3235,definition,
( sQ284_spl
<=> v2_yellow_0(sK30_skl) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f3237,plain,
( sQ284_spl
| ~ v2_yellow_0(sK30_skl) ),
inference(component_clause,[status(thm)],[f3235]) ).
fof(f3240,plain,
( sQ284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3237,f1097]) ).
fof(f3241,plain,
sQ284_spl,
inference(contradiction_clause,[status(thm)],[f3240]) ).
fof(f3355,definition,
( sQ302_spl
<=> l1_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f3357,plain,
( sQ302_spl
| ~ l1_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f3355]) ).
fof(f3358,definition,
( sQ303_spl
<=> v3_lattice3(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition]) ).
fof(f3360,plain,
( sQ303_spl
| ~ v3_lattice3(sK31_skl) ),
inference(component_clause,[status(thm)],[f3358]) ).
fof(f3369,plain,
( sQ303_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3360,f1111]) ).
fof(f3370,plain,
sQ303_spl,
inference(contradiction_clause,[status(thm)],[f3369]) ).
fof(f3371,plain,
( sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3357,f1104]) ).
fof(f3372,plain,
sQ302_spl,
inference(contradiction_clause,[status(thm)],[f3371]) ).
fof(f3378,definition,
( sQ306_spl
<=> v3_struct_0(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition]) ).
fof(f3379,plain,
( ~ sQ306_spl
| v3_struct_0(sK25_skl) ),
inference(component_clause,[status(thm)],[f3378]) ).
fof(f3381,definition,
( sQ307_spl
<=> v2_orders_2(sK25_skl) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f3383,plain,
( sQ307_spl
| ~ v2_orders_2(sK25_skl) ),
inference(component_clause,[status(thm)],[f3381]) ).
fof(f3390,plain,
( sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1793,f975]) ).
fof(f3391,plain,
sQ77_spl,
inference(contradiction_clause,[status(thm)],[f3390]) ).
fof(f3400,definition,
( sQ309_spl
<=> v1_yellow_0(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f3402,plain,
( sQ309_spl
| ~ v1_yellow_0(sK29_skl) ),
inference(component_clause,[status(thm)],[f3400]) ).
fof(f3404,definition,
( sQ310_spl
<=> v1_yellow_0(sK24_skl) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f3406,plain,
( sQ310_spl
| ~ v1_yellow_0(sK24_skl) ),
inference(component_clause,[status(thm)],[f3404]) ).
fof(f3408,definition,
( sQ311_spl
<=> v1_yellow_0(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition]) ).
fof(f3410,plain,
( sQ311_spl
| ~ v1_yellow_0(sK23_skl) ),
inference(component_clause,[status(thm)],[f3408]) ).
fof(f3412,definition,
( sQ312_spl
<=> v1_yellow_0(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition]) ).
fof(f3414,plain,
( sQ312_spl
| ~ v1_yellow_0(sK22_skl) ),
inference(component_clause,[status(thm)],[f3412]) ).
fof(f3416,definition,
( sQ313_spl
<=> v3_orders_2(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ313_spl])],[split_symbol_definition]) ).
fof(f3418,plain,
( sQ313_spl
| ~ v3_orders_2(sK10_skl) ),
inference(component_clause,[status(thm)],[f3416]) ).
fof(f3419,definition,
( sQ314_spl
<=> v4_orders_2(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f3421,plain,
( sQ314_spl
| ~ v4_orders_2(sK10_skl) ),
inference(component_clause,[status(thm)],[f3419]) ).
fof(f3429,plain,
( sQ314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3421,f894]) ).
fof(f3430,plain,
sQ314_spl,
inference(contradiction_clause,[status(thm)],[f3429]) ).
fof(f3431,plain,
( sQ313_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3418,f893]) ).
fof(f3432,plain,
sQ313_spl,
inference(contradiction_clause,[status(thm)],[f3431]) ).
fof(f3433,plain,
( sQ312_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3414,f973]) ).
fof(f3434,plain,
sQ312_spl,
inference(contradiction_clause,[status(thm)],[f3433]) ).
fof(f3435,plain,
( sQ311_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3410,f997]) ).
fof(f3436,plain,
sQ311_spl,
inference(contradiction_clause,[status(thm)],[f3435]) ).
fof(f3437,plain,
( sQ310_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3406,f1013]) ).
fof(f3438,plain,
sQ310_spl,
inference(contradiction_clause,[status(thm)],[f3437]) ).
fof(f3439,plain,
( sQ309_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3402,f1069]) ).
fof(f3440,plain,
sQ309_spl,
inference(contradiction_clause,[status(thm)],[f3439]) ).
fof(f3525,definition,
( sQ323_spl
<=> v2_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f3527,plain,
( sQ323_spl
| ~ v2_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f3525]) ).
fof(f3528,definition,
( sQ324_spl
<=> v3_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f3530,plain,
( sQ324_spl
| ~ v3_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f3528]) ).
fof(f3531,definition,
( sQ325_spl
<=> v4_orders_2(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f3533,plain,
( sQ325_spl
| ~ v4_orders_2(sK31_skl) ),
inference(component_clause,[status(thm)],[f3531]) ).
fof(f3539,plain,
( sQ325_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3533,f1108]) ).
fof(f3540,plain,
sQ325_spl,
inference(contradiction_clause,[status(thm)],[f3539]) ).
fof(f3541,plain,
( sQ324_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3530,f1107]) ).
fof(f3542,plain,
sQ324_spl,
inference(contradiction_clause,[status(thm)],[f3541]) ).
fof(f3543,plain,
( sQ323_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3527,f1106]) ).
fof(f3544,plain,
sQ323_spl,
inference(contradiction_clause,[status(thm)],[f3543]) ).
fof(f3546,definition,
( sQ327_spl
<=> v3_struct_0(sK31_skl) ),
introduced(definition,[new_symbols(definition,[sQ327_spl])],[split_symbol_definition]) ).
fof(f3547,plain,
( ~ sQ327_spl
| v3_struct_0(sK31_skl) ),
inference(component_clause,[status(thm)],[f3546]) ).
fof(f3553,plain,
( ~ sQ327_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3547,f1105]) ).
fof(f3554,plain,
~ sQ327_spl,
inference(contradiction_clause,[status(thm)],[f3553]) ).
fof(f3653,plain,
( ~ sQ24_spl
| ~ m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))
| ~ v1_lattice3(sK1_skl)
| ~ v1_lattice3(sK0_skl)
| v3_waybel_1(k1_waybel_1(sK0_skl,sK1_skl,sK2_skl,k1_waybel34(sK0_skl,sK1_skl,sK2_skl)),sK0_skl,sK1_skl)
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl))
| ~ v17_waybel_0(sK2_skl,sK0_skl,sK1_skl)
| ~ v3_lattice3(sK1_skl)
| ~ v3_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)
| ~ l1_orders_2(sK1_skl)
| ~ v2_lattice3(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl) ),
inference(resolution,[status(thm)],[f3050,f1458]) ).
fof(f3655,plain,
( ~ sQ24_spl
| ~ sQ27_spl
| ~ sQ8_spl
| ~ sQ10_spl
| sQ258_spl
| ~ sQ23_spl
| ~ sQ257_spl
| ~ sQ73_spl
| ~ sQ61_spl
| ~ sQ256_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ9_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ4_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f3653,f1419,f1422,f1425,f1353,f1428,f1431,f1434,f1374,f1356,f1463,f1359,f3039,f1674,f1746,f3042,f1437,f3045,f1378,f1371,f1466,f1457]) ).
fof(f3689,plain,
( sQ307_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3383,f1034]) ).
fof(f3690,plain,
sQ307_spl,
inference(contradiction_clause,[status(thm)],[f3689]) ).
fof(f3691,plain,
( ~ sQ306_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3379,f1032]) ).
fof(f3692,plain,
~ sQ306_spl,
inference(contradiction_clause,[status(thm)],[f3691]) ).
fof(f3781,definition,
( sQ360_spl
<=> l1_orders_2(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition]) ).
fof(f3783,plain,
( sQ360_spl
| ~ l1_orders_2(sK37_skl) ),
inference(component_clause,[status(thm)],[f3781]) ).
fof(f3791,definition,
( sQ363_spl
<=> v1_lattice3(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f3793,plain,
( sQ363_spl
| ~ v1_lattice3(sK37_skl) ),
inference(component_clause,[status(thm)],[f3791]) ).
fof(f3795,plain,
( sQ360_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3783,f1144]) ).
fof(f3796,plain,
sQ360_spl,
inference(contradiction_clause,[status(thm)],[f3795]) ).
fof(f3939,definition,
( sQ390_spl
<=> v2_orders_2(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f3941,plain,
( sQ390_spl
| ~ v2_orders_2(sK37_skl) ),
inference(component_clause,[status(thm)],[f3939]) ).
fof(f3942,definition,
( sQ391_spl
<=> v3_orders_2(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition]) ).
fof(f3944,plain,
( sQ391_spl
| ~ v3_orders_2(sK37_skl) ),
inference(component_clause,[status(thm)],[f3942]) ).
fof(f3945,definition,
( sQ392_spl
<=> v4_orders_2(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f3947,plain,
( sQ392_spl
| ~ v4_orders_2(sK37_skl) ),
inference(component_clause,[status(thm)],[f3945]) ).
fof(f3953,plain,
( sQ392_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3947,f1149]) ).
fof(f3954,plain,
sQ392_spl,
inference(contradiction_clause,[status(thm)],[f3953]) ).
fof(f3955,plain,
( sQ391_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3944,f1148]) ).
fof(f3956,plain,
sQ391_spl,
inference(contradiction_clause,[status(thm)],[f3955]) ).
fof(f3957,plain,
( sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3941,f1147]) ).
fof(f3958,plain,
sQ390_spl,
inference(contradiction_clause,[status(thm)],[f3957]) ).
fof(f3960,definition,
( sQ394_spl
<=> v3_struct_0(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition]) ).
fof(f3961,plain,
( ~ sQ394_spl
| v3_struct_0(sK37_skl) ),
inference(component_clause,[status(thm)],[f3960]) ).
fof(f4021,plain,
( ~ sQ394_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3961,f1145]) ).
fof(f4022,plain,
~ sQ394_spl,
inference(contradiction_clause,[status(thm)],[f4021]) ).
fof(f4046,definition,
( sQ407_spl
<=> v3_yellow_0(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ407_spl])],[split_symbol_definition]) ).
fof(f4048,plain,
( sQ407_spl
| ~ v3_yellow_0(sK37_skl) ),
inference(component_clause,[status(thm)],[f4046]) ).
fof(f4056,plain,
( sQ363_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3793,f1150]) ).
fof(f4057,plain,
sQ363_spl,
inference(contradiction_clause,[status(thm)],[f4056]) ).
fof(f4070,definition,
( sQ410_spl
<=> l1_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition]) ).
fof(f4072,plain,
( sQ410_spl
| ~ l1_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f4070]) ).
fof(f4084,plain,
( sQ410_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4072,f1175]) ).
fof(f4085,plain,
sQ410_spl,
inference(contradiction_clause,[status(thm)],[f4084]) ).
fof(f4180,definition,
( sQ428_spl
<=> v3_struct_0(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition]) ).
fof(f4181,plain,
( ~ sQ428_spl
| v3_struct_0(sK40_skl) ),
inference(component_clause,[status(thm)],[f4180]) ).
fof(f4183,definition,
( sQ429_spl
<=> v2_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f4185,plain,
( sQ429_spl
| ~ v2_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f4183]) ).
fof(f4186,definition,
( sQ430_spl
<=> v4_orders_2(sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f4188,plain,
( sQ430_spl
| ~ v4_orders_2(sK40_skl) ),
inference(component_clause,[status(thm)],[f4186]) ).
fof(f4193,plain,
( sQ430_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4188,f1180]) ).
fof(f4194,plain,
sQ430_spl,
inference(contradiction_clause,[status(thm)],[f4193]) ).
fof(f4195,plain,
( sQ429_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4185,f1178]) ).
fof(f4196,plain,
sQ429_spl,
inference(contradiction_clause,[status(thm)],[f4195]) ).
fof(f4197,plain,
( ~ sQ428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4181,f1176]) ).
fof(f4198,plain,
~ sQ428_spl,
inference(contradiction_clause,[status(thm)],[f4197]) ).
fof(f4424,definition,
( sQ456_spl
<=> v2_yellow_0(sK37_skl) ),
introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition]) ).
fof(f4426,plain,
( sQ456_spl
| ~ v2_yellow_0(sK37_skl) ),
inference(component_clause,[status(thm)],[f4424]) ).
fof(f4429,plain,
( sQ456_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4426,f1153]) ).
fof(f4430,plain,
sQ456_spl,
inference(contradiction_clause,[status(thm)],[f4429]) ).
fof(f5240,plain,
( sQ407_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4048,f1154]) ).
fof(f5241,plain,
sQ407_spl,
inference(contradiction_clause,[status(thm)],[f5240]) ).
fof(f5588,plain,
! [X0] :
( ~ l1_orders_2(X0)
| m1_subset_1(u1_orders_2(X0),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))) ),
inference(resolution,[status(thm)],[f626,f628]) ).
fof(f5932,plain,
m1_subset_1(u1_orders_2(sK1_skl),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK1_skl),u1_struct_0(sK1_skl)))),
inference(resolution,[status(thm)],[f5588,f214]) ).
fof(f6060,definition,
( sQ620_spl
<=> v1_relat_1(k4_relat_1(sK33_skl)) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f6062,plain,
( sQ620_spl
| ~ v1_relat_1(k4_relat_1(sK33_skl)) ),
inference(component_clause,[status(thm)],[f6060]) ).
fof(f6122,plain,
( sQ620_spl
| ~ v1_relat_1(sK33_skl) ),
inference(resolution,[status(thm)],[f6062,f617]) ).
fof(f6123,plain,
( sQ620_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6122,f1121]) ).
fof(f6124,plain,
sQ620_spl,
inference(contradiction_clause,[status(thm)],[f6123]) ).
fof(f6128,definition,
( sQ624_spl
<=> v1_relat_1(k4_relat_1(sK26_skl)) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f6130,plain,
( sQ624_spl
| ~ v1_relat_1(k4_relat_1(sK26_skl)) ),
inference(component_clause,[status(thm)],[f6128]) ).
fof(f6135,plain,
( sQ624_spl
| ~ v1_relat_1(sK26_skl) ),
inference(resolution,[status(thm)],[f6130,f617]) ).
fof(f6136,plain,
( sQ624_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6135,f1042]) ).
fof(f6137,plain,
sQ624_spl,
inference(contradiction_clause,[status(thm)],[f6136]) ).
fof(f6209,definition,
( sQ638_spl
<=> v1_relat_1(k4_relat_1(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f6211,plain,
( sQ638_spl
| ~ v1_relat_1(k4_relat_1(sK13_skl)) ),
inference(component_clause,[status(thm)],[f6209]) ).
fof(f6216,plain,
( sQ638_spl
| ~ v1_relat_1(sK13_skl) ),
inference(resolution,[status(thm)],[f6211,f617]) ).
fof(f6217,plain,
( sQ638_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6216,f915]) ).
fof(f6218,plain,
sQ638_spl,
inference(contradiction_clause,[status(thm)],[f6217]) ).
fof(f6371,plain,
v1_relat_1(u1_orders_2(sK1_skl)),
inference(resolution,[status(thm)],[f5932,f315]) ).
fof(f7002,definition,
( sQ710_spl
<=> v1_funct_1(sK33_skl) ),
introduced(definition,[new_symbols(definition,[sQ710_spl])],[split_symbol_definition]) ).
fof(f7004,plain,
( sQ710_spl
| ~ v1_funct_1(sK33_skl) ),
inference(component_clause,[status(thm)],[f7002]) ).
fof(f7011,plain,
( sQ710_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7004,f1122]) ).
fof(f7012,plain,
sQ710_spl,
inference(contradiction_clause,[status(thm)],[f7011]) ).
fof(f7061,definition,
( sQ716_spl
<=> v3_struct_0(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ716_spl])],[split_symbol_definition]) ).
fof(f7062,plain,
( ~ sQ716_spl
| v3_struct_0(sK27_skl) ),
inference(component_clause,[status(thm)],[f7061]) ).
fof(f7084,definition,
( sQ722_spl
<=> v3_struct_0(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f7085,plain,
( ~ sQ722_spl
| v3_struct_0(sK14_skl) ),
inference(component_clause,[status(thm)],[f7084]) ).
fof(f7162,plain,
( ~ sQ722_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7085,f919]) ).
fof(f7163,plain,
~ sQ722_spl,
inference(contradiction_clause,[status(thm)],[f7162]) ).
fof(f7164,plain,
( ~ sQ716_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7062,f1047]) ).
fof(f7165,plain,
~ sQ716_spl,
inference(contradiction_clause,[status(thm)],[f7164]) ).
fof(f7421,definition,
( sQ774_spl
<=> l1_orders_2(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ774_spl])],[split_symbol_definition]) ).
fof(f7423,plain,
( sQ774_spl
| ~ l1_orders_2(sK3_skl) ),
inference(component_clause,[status(thm)],[f7421]) ).
fof(f7432,plain,
( sQ774_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7423,f630]) ).
fof(f7433,plain,
sQ774_spl,
inference(contradiction_clause,[status(thm)],[f7432]) ).
fof(f9179,definition,
( sQ1013_spl
<=> v2_orders_2(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ1013_spl])],[split_symbol_definition]) ).
fof(f9181,plain,
( sQ1013_spl
| ~ v2_orders_2(sK27_skl) ),
inference(component_clause,[status(thm)],[f9179]) ).
fof(f9202,definition,
( sQ1019_spl
<=> v2_orders_2(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ1019_spl])],[split_symbol_definition]) ).
fof(f9204,plain,
( sQ1019_spl
| ~ v2_orders_2(sK14_skl) ),
inference(component_clause,[status(thm)],[f9202]) ).
fof(f9258,plain,
( sQ1019_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9204,f921]) ).
fof(f9259,plain,
sQ1019_spl,
inference(contradiction_clause,[status(thm)],[f9258]) ).
fof(f9260,plain,
( sQ1013_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9181,f1049]) ).
fof(f9261,plain,
sQ1013_spl,
inference(contradiction_clause,[status(thm)],[f9260]) ).
fof(f9263,definition,
( sQ1033_spl
<=> v1_relat_1(k4_relat_1(u1_orders_2(sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1033_spl])],[split_symbol_definition]) ).
fof(f9265,plain,
( sQ1033_spl
| ~ v1_relat_1(k4_relat_1(u1_orders_2(sK1_skl))) ),
inference(component_clause,[status(thm)],[f9263]) ).
fof(f9441,plain,
( sQ1033_spl
| ~ v1_relat_1(u1_orders_2(sK1_skl)) ),
inference(resolution,[status(thm)],[f9265,f617]) ).
fof(f9442,plain,
( sQ1033_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9441,f6371]) ).
fof(f9443,plain,
sQ1033_spl,
inference(contradiction_clause,[status(thm)],[f9442]) ).
fof(f10918,definition,
( sQ1221_spl
<=> v3_orders_2(sK27_skl) ),
introduced(definition,[new_symbols(definition,[sQ1221_spl])],[split_symbol_definition]) ).
fof(f10920,plain,
( sQ1221_spl
| ~ v3_orders_2(sK27_skl) ),
inference(component_clause,[status(thm)],[f10918]) ).
fof(f10925,definition,
( sQ1223_spl
<=> v3_orders_2(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ1223_spl])],[split_symbol_definition]) ).
fof(f10927,plain,
( sQ1223_spl
| ~ v3_orders_2(sK14_skl) ),
inference(component_clause,[status(thm)],[f10925]) ).
fof(f10942,plain,
( sQ1223_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10927,f922]) ).
fof(f10943,plain,
sQ1223_spl,
inference(contradiction_clause,[status(thm)],[f10942]) ).
fof(f10944,plain,
( sQ1221_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10920,f1050]) ).
fof(f10945,plain,
sQ1221_spl,
inference(contradiction_clause,[status(thm)],[f10944]) ).
fof(f13109,definition,
( sQ1423_spl
<=> v3_struct_0(sK34_skl) ),
introduced(definition,[new_symbols(definition,[sQ1423_spl])],[split_symbol_definition]) ).
fof(f13110,plain,
( ~ sQ1423_spl
| v3_struct_0(sK34_skl) ),
inference(component_clause,[status(thm)],[f13109]) ).
fof(f13123,plain,
( ~ sQ1423_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13110,f1126]) ).
fof(f13124,plain,
~ sQ1423_spl,
inference(contradiction_clause,[status(thm)],[f13123]) ).
fof(f13346,plain,
! [X0,X1,X2,X3] :
( X3 = k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),X2)
| ~ 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)
| ~ v18_waybel_0(X2,k7_lattice3(X0),k7_lattice3(X1))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ 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)
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_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))
| ~ 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)],[f1238,f1317]) ).
fof(f13349,plain,
! [X0,X1,X2,X3] :
( X3 = k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),X2)
| ~ v18_waybel_0(X2,k7_lattice3(X0),k7_lattice3(X1))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_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))
| ~ 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)],[f13346]) ).
fof(f13350,plain,
! [X0,X1,X2,X3] :
( X3 = k2_waybel34(k7_lattice3(X1),k7_lattice3(X0),X2)
| ~ v18_waybel_0(X2,k7_lattice3(X0),k7_lattice3(X1))
| ~ v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(k7_lattice3(X0))
| ~ v2_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))
| ~ 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)],[f13349,f740]) ).
fof(f15753,plain,
( ~ sQ258_spl
| k1_waybel34(sK0_skl,sK1_skl,sK2_skl) = k2_waybel34(k7_lattice3(sK1_skl),k7_lattice3(sK0_skl),sK2_skl)
| ~ v18_waybel_0(sK2_skl,k7_lattice3(sK0_skl),k7_lattice3(sK1_skl))
| ~ v3_lattice3(k7_lattice3(sK0_skl))
| ~ v3_lattice3(k7_lattice3(sK1_skl))
| ~ l1_orders_2(k7_lattice3(sK0_skl))
| ~ v2_lattice3(k7_lattice3(sK0_skl))
| ~ v4_orders_2(k7_lattice3(sK0_skl))
| ~ v3_orders_2(k7_lattice3(sK0_skl))
| ~ v2_orders_2(k7_lattice3(sK0_skl))
| ~ l1_orders_2(k7_lattice3(sK1_skl))
| ~ v2_lattice3(k7_lattice3(sK1_skl))
| ~ v4_orders_2(k7_lattice3(sK1_skl))
| ~ v3_orders_2(k7_lattice3(sK1_skl))
| ~ m2_relset_1(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(sK0_skl)))
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k7_lattice3(sK1_skl)),u1_struct_0(k7_lattice3(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(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_2(k1_waybel34(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))
| ~ v1_funct_1(k1_waybel34(sK0_skl,sK1_skl,sK2_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(sK1_skl)
| ~ v4_orders_2(sK1_skl)
| ~ v3_orders_2(sK1_skl)
| ~ v2_orders_2(sK1_skl)
| v3_struct_0(sK1_skl)
| ~ l1_orders_2(sK0_skl)
| ~ v4_orders_2(sK0_skl)
| ~ v3_orders_2(sK0_skl)
| ~ v2_orders_2(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f13350,f3046]) ).
fof(f15758,definition,
( sQ1681_spl
<=> k1_waybel34(sK0_skl,sK1_skl,sK2_skl) = k2_waybel34(k7_lattice3(sK1_skl),k7_lattice3(sK0_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ1681_spl])],[split_symbol_definition]) ).
fof(f15759,plain,
( ~ sQ1681_spl
| k1_waybel34(sK0_skl,sK1_skl,sK2_skl) = k2_waybel34(k7_lattice3(sK1_skl),k7_lattice3(sK0_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f15758]) ).
fof(f15761,plain,
( ~ sQ258_spl
| sQ1681_spl
| ~ sQ264_spl
| ~ sQ118_spl
| ~ sQ103_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ37_spl
| ~ sQ48_spl
| ~ sQ47_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ100_spl
| ~ sQ101_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ259_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ256_spl
| ~ sQ6_spl
| ~ sQ26_spl
| ~ sQ5_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| sQ72_spl
| ~ sQ4_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f15753,f1671,f1419,f1422,f1425,f1353,f1743,f1428,f1431,f1434,f1356,f1463,f1359,f3039,f1437,f1457,f3065,f1520,f1525,f1928,f1924,f1579,f1582,f1588,f1591,f1558,f1561,f1564,f1570,f1573,f1939,f2067,f3099,f15758,f3045]) ).
fof(f15766,plain,
( ~ sQ1681_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15759,f1368]) ).
fof(f15767,plain,
( ~ sQ1681_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f15766]) ).
fof(f15768,plain,
$false,
inference(sat_refutation,[status(thm)],[f1365,f1377,f1384,f1386,f1388,f1390,f1440,f1442,f1444,f1469,f1471,f1473,f1475,f1477,f1479,f1481,f1487,f1489,f1508,f1523,f1528,f1603,f1605,f1654,f1678,f1695,f1697,f1699,f1750,f1756,f1779,f1781,f1808,f1812,f1819,f1823,f1927,f1931,f1945,f1952,f2032,f2073,f2080,f2537,f3052,f3054,f3078,f3102,f3214,f3216,f3218,f3220,f3230,f3232,f3241,f3370,f3372,f3391,f3430,f3432,f3434,f3436,f3438,f3440,f3540,f3542,f3544,f3554,f3655,f3690,f3692,f3796,f3954,f3956,f3958,f4022,f4057,f4085,f4194,f4196,f4198,f4430,f5241,f6124,f6137,f6218,f7012,f7163,f7165,f7433,f9259,f9261,f9443,f10943,f10945,f13124,f15761,f15767]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT354+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n018.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Sun Sep 20 23:49:28 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 114.23/15.08 % Refutation found
% 114.23/15.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 114.23/15.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.90/15.19 % Elapsed time: 14.734478 seconds
% 3.90/15.19 % CPU time: 116.030455 seconds
% 3.90/15.19 % Total memory used: 498.328 MB
% 3.90/15.19 % Net memory used: 486.594 MB
%------------------------------------------------------------------------------