%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT355+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n007.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 : Fri Sep 25 01:59:36 PM UTC 2026
% Result : Theorem 126.62s 19.39s
% Output : CNFRefutation 126.62s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f1366ERROR: Could not build tree for root c_163474ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( 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) )
=> ! [X1] :
( ( 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) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) = k2_waybel34(X1,X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( 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) )
=> ! [X1] :
( ( 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) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) = k2_waybel34(X1,X0,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f23,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattice3) ).
fof(f33,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( v3_lattice3(X0)
& ~ v3_struct_0(X0) )
=> ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f38,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f72,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1) )
=> ! [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) )
=> ( ( v17_waybel_0(X2,X0,X1)
& v3_lattice3(X1)
& v3_lattice3(X0) )
=> ! [X3] :
( ( 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) )
=> ( X3 = k1_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_waybel34) ).
fof(f73,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1) )
=> ! [X2] :
( ( 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) )
=> ( ( v18_waybel_0(X2,X1,X0)
& v3_lattice3(X1)
& v3_lattice3(X0) )
=> ! [X3] :
( ( 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) )
=> ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_waybel34) ).
fof(f74,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( l1_orders_2(X1)
=> ! [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) )
=> k3_waybel34(X0,X1,X2) = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_waybel34) ).
fof(f84,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k2_waybel34(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_waybel34) ).
fof(f86,axiom,
! [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)
& l1_orders_2(X0) )
=> ( m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_1(k3_waybel34(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_waybel34) ).
fof(f90,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( l1_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_lattice3) ).
fof(f122,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0) )
=> ( v2_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_yellow_7) ).
fof(f127,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_orders_2(X0) )
=> ( v3_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_yellow_7) ).
fof(f131,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v4_orders_2(X0) )
=> ( v4_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_yellow_7) ).
fof(f132,axiom,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v3_lattice3(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v21_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_relat_1(k3_waybel34(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_waybel34) ).
fof(f141,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v1_lattice3(X0) )
=> ( v2_lattice3(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& ~ v3_struct_0(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_yellow_7) ).
fof(f144,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v3_lattice3(X0)
& ~ v3_struct_0(X0) )
=> ( v3_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& ~ v3_struct_0(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_yellow_7) ).
fof(f188,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f237,plain,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v3_lattice3(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v1_partfun1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_relat_1(k3_waybel34(X0,X1,X2)) ) ),
inference(pure_predicate_removal,[],[f132]) ).
fof(f241,plain,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v3_lattice3(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( v5_orders_3(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_relat_1(k3_waybel34(X0,X1,X2)) ) ),
inference(pure_predicate_removal,[],[f237]) ).
fof(f255,plain,
! [X0,X1,X2] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_orders_2(X1)
& v3_lattice3(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& l1_orders_2(X0)
& v3_lattice3(X0)
& v2_lattice3(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0) )
=> ( v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_relat_1(k3_waybel34(X0,X1,X2)) ) ),
inference(pure_predicate_removal,[],[f241]) ).
fof(f257,plain,
? [X0] :
( 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)
& ? [X1] :
( 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)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) != k2_waybel34(X1,X0,X2) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f258,plain,
? [X0] :
( 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)
& ? [X1] :
( 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)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v18_waybel_0(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& k1_waybel34(k7_lattice3(X0),k7_lattice3(X1),k3_waybel34(X0,X1,X2)) != k2_waybel34(X1,X0,X2) ) ) ),
inference(flattening,[],[f257]) ).
fof(f286,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f287,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f286]) ).
fof(f302,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f33]) ).
fof(f303,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f302]) ).
fof(f310,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f311,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f310]) ).
fof(f371,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [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)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ! [X3] :
( ~ 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)
| ( X3 = k1_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) ) ) ) ),
inference(ennf_transformation,[],[f72]) ).
fof(f372,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [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)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ! [X3] :
( ~ 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)
| ( X3 = k1_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ) ) ) ) ),
inference(flattening,[],[f371]) ).
fof(f373,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [X2] :
( ~ 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)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ! [X3] :
( ~ 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)
| ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ) ) ) ) ),
inference(ennf_transformation,[],[f73]) ).
fof(f374,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [X2] :
( ~ 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)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ! [X3] :
( ~ 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)
| ( X3 = k2_waybel34(X0,X1,X2)
<=> v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ) ) ) ) ),
inference(flattening,[],[f373]) ).
fof(f375,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ! [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)
| k3_waybel34(X0,X1,X2) = X2 ) ) ),
inference(ennf_transformation,[],[f74]) ).
fof(f376,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ! [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)
| k3_waybel34(X0,X1,X2) = X2 ) ) ),
inference(flattening,[],[f375]) ).
fof(f381,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k2_waybel34(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f84]) ).
fof(f382,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k2_waybel34(X0,X1,X2)) ) ),
inference(flattening,[],[f381]) ).
fof(f383,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)
| ~ l1_orders_2(X0)
| ( m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_1(k3_waybel34(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f86]) ).
fof(f384,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)
| ~ l1_orders_2(X0)
| ( m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& v1_funct_1(k3_waybel34(X0,X1,X2)) ) ),
inference(flattening,[],[f383]) ).
fof(f387,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ( l1_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(ennf_transformation,[],[f90]) ).
fof(f420,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ( v2_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(ennf_transformation,[],[f122]) ).
fof(f421,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ( v2_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(flattening,[],[f420]) ).
fof(f427,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ( v3_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(ennf_transformation,[],[f127]) ).
fof(f428,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| ( v3_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(flattening,[],[f427]) ).
fof(f435,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ( v4_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(ennf_transformation,[],[f131]) ).
fof(f436,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| ( v4_orders_2(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
inference(flattening,[],[f435]) ).
fof(f437,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_relat_1(k3_waybel34(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f255]) ).
fof(f438,plain,
! [X0,X1,X2] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ( v4_waybel_1(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v19_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1))
& v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
& ~ v1_xboole_0(k3_waybel34(X0,X1,X2))
& v1_funct_1(k3_waybel34(X0,X1,X2))
& v1_relat_1(k3_waybel34(X0,X1,X2)) ) ),
inference(flattening,[],[f437]) ).
fof(f453,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ( v2_lattice3(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& ~ v3_struct_0(k7_lattice3(X0)) ) ),
inference(ennf_transformation,[],[f141]) ).
fof(f454,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ( v2_lattice3(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& ~ v3_struct_0(k7_lattice3(X0)) ) ),
inference(flattening,[],[f453]) ).
fof(f458,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v3_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& ~ v3_struct_0(k7_lattice3(X0)) ) ),
inference(ennf_transformation,[],[f144]) ).
fof(f459,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v3_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& ~ v3_struct_0(k7_lattice3(X0)) ) ),
inference(flattening,[],[f458]) ).
fof(f533,plain,
( l1_orders_2(sK12)
& v3_lattice3(sK12)
& v2_lattice3(sK12)
& v1_lattice3(sK12)
& v4_orders_2(sK12)
& v3_orders_2(sK12)
& v2_orders_2(sK12)
& l1_orders_2(sK13)
& v3_lattice3(sK13)
& v2_lattice3(sK13)
& v1_lattice3(sK13)
& v4_orders_2(sK13)
& v3_orders_2(sK13)
& v2_orders_2(sK13)
& m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
& v18_waybel_0(sK14,sK12,sK13)
& v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
& v1_funct_1(sK14)
& k1_waybel34(k7_lattice3(sK12),k7_lattice3(sK13),k3_waybel34(sK12,sK13,sK14)) != k2_waybel34(sK13,sK12,sK14) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X0,sK12),skolemize(X1,sK13),skolemize(X2,sK14)],[f258]) ).
fof(f544,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [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)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ! [X3] :
( ~ 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)
| ( ( k1_waybel34(X0,X1,X2) != X3
| v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) )
& ( ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| X3 = k1_waybel34(X0,X1,X2) ) ) ) ) ) ),
inference(nnf_transformation,[],[f372]) ).
fof(f545,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ! [X2] :
( ~ 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)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ! [X3] :
( ~ 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)
| ( ( k2_waybel34(X0,X1,X2) != X3
| v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) )
& ( ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| X3 = k2_waybel34(X0,X1,X2) ) ) ) ) ) ),
inference(nnf_transformation,[],[f374]) ).
fof(f585,plain,
! [X0,X1,X2] :
( ( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) )
& ( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f188]) ).
fof(f587,plain,
l1_orders_2(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f588,plain,
v3_lattice3(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f589,plain,
v2_lattice3(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f590,plain,
v1_lattice3(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f591,plain,
v4_orders_2(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f592,plain,
v3_orders_2(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f593,plain,
v2_orders_2(sK12),
inference(cnf_transformation,[],[f533]) ).
fof(f594,plain,
l1_orders_2(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f595,plain,
v3_lattice3(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f596,plain,
v2_lattice3(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f597,plain,
v1_lattice3(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f598,plain,
v4_orders_2(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f599,plain,
v3_orders_2(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f600,plain,
v2_orders_2(sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f601,plain,
m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13)),
inference(cnf_transformation,[],[f533]) ).
fof(f602,plain,
v18_waybel_0(sK14,sK12,sK13),
inference(cnf_transformation,[],[f533]) ).
fof(f603,plain,
v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)),
inference(cnf_transformation,[],[f533]) ).
fof(f604,plain,
v1_funct_1(sK14),
inference(cnf_transformation,[],[f533]) ).
fof(f605,plain,
k1_waybel34(k7_lattice3(sK12),k7_lattice3(sK13),k3_waybel34(sK12,sK13,sK14)) != k2_waybel34(sK13,sK12,sK14),
inference(cnf_transformation,[],[f533]) ).
fof(f677,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f287]) ).
fof(f706,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f303]) ).
fof(f730,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f311]) ).
fof(f893,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ 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)
| ~ v17_waybel_0(X2,X0,X1)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| k1_waybel34(X0,X1,X2) = X3 ),
inference(cnf_transformation,[],[f544]) ).
fof(f894,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ 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)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ 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)
| k2_waybel34(X0,X1,X2) != X3
| v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1) ),
inference(cnf_transformation,[],[f545]) ).
fof(f896,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ 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)
| k3_waybel34(X0,X1,X2) = X2 ),
inference(cnf_transformation,[],[f376]) ).
fof(f904,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f382]) ).
fof(f905,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f382]) ).
fof(f906,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_funct_1(k2_waybel34(X0,X1,X2)) ),
inference(cnf_transformation,[],[f382]) ).
fof(f907,plain,
! [X2,X0,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)
| m2_relset_1(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) ),
inference(cnf_transformation,[],[f384]) ).
fof(f908,plain,
! [X2,X0,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)
| v1_funct_2(k3_waybel34(X0,X1,X2),u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1))) ),
inference(cnf_transformation,[],[f384]) ).
fof(f912,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f387]) ).
fof(f998,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v2_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f421]) ).
fof(f1017,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_orders_2(X0)
| v3_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f428]) ).
fof(f1030,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| v4_orders_2(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f436]) ).
fof(f1034,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v18_waybel_0(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v17_waybel_0(k3_waybel34(X0,X1,X2),k7_lattice3(X0),k7_lattice3(X1)) ),
inference(cnf_transformation,[],[f438]) ).
fof(f1064,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| v2_lattice3(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f454]) ).
fof(f1073,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v3_lattice3(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f459]) ).
fof(f1345,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f585]) ).
fof(f1360,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ 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)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1) ),
inference(equality_resolution,[],[f894]) ).
tcf(c_49,negated_conjecture,
k1_waybel34(k7_lattice3(sK12),k7_lattice3(sK13),k3_waybel34(sK12,sK13,sK14)) != k2_waybel34(sK13,sK12,sK14),
inference(cnf_transformation,[],[f605]) ).
tcf(c_50,negated_conjecture,
v1_funct_1(sK14),
inference(cnf_transformation,[],[f604]) ).
tcf(c_51,negated_conjecture,
v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)),
inference(cnf_transformation,[],[f603]) ).
tcf(c_52,negated_conjecture,
v18_waybel_0(sK14,sK12,sK13),
inference(cnf_transformation,[],[f602]) ).
tcf(c_53,negated_conjecture,
m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13)),
inference(cnf_transformation,[],[f601]) ).
tcf(c_54,negated_conjecture,
v2_orders_2(sK13),
inference(cnf_transformation,[],[f600]) ).
tcf(c_55,negated_conjecture,
v3_orders_2(sK13),
inference(cnf_transformation,[],[f599]) ).
tcf(c_56,negated_conjecture,
v4_orders_2(sK13),
inference(cnf_transformation,[],[f598]) ).
tcf(c_57,negated_conjecture,
v1_lattice3(sK13),
inference(cnf_transformation,[],[f597]) ).
tcf(c_58,negated_conjecture,
v2_lattice3(sK13),
inference(cnf_transformation,[],[f596]) ).
tcf(c_59,negated_conjecture,
v3_lattice3(sK13),
inference(cnf_transformation,[],[f595]) ).
tcf(c_60,negated_conjecture,
l1_orders_2(sK13),
inference(cnf_transformation,[],[f594]) ).
tcf(c_61,negated_conjecture,
v2_orders_2(sK12),
inference(cnf_transformation,[],[f593]) ).
tcf(c_62,negated_conjecture,
v3_orders_2(sK12),
inference(cnf_transformation,[],[f592]) ).
tcf(c_63,negated_conjecture,
v4_orders_2(sK12),
inference(cnf_transformation,[],[f591]) ).
tcf(c_64,negated_conjecture,
v1_lattice3(sK12),
inference(cnf_transformation,[],[f590]) ).
tcf(c_65,negated_conjecture,
v2_lattice3(sK12),
inference(cnf_transformation,[],[f589]) ).
tcf(c_66,negated_conjecture,
v3_lattice3(sK12),
inference(cnf_transformation,[],[f588]) ).
tcf(c_67,negated_conjecture,
l1_orders_2(sK12),
inference(cnf_transformation,[],[f587]) ).
tcf(c_128,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0) ),
inference(cnf_transformation,[],[f677]) ).
tcf(c_149,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f706]) ).
tcf(c_171,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[],[f730]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k1_waybel34(X0,X1,X2) = X3 )
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ),
inference(cnf_transformation,[],[f893]) ).
tcf(c_292,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f1360]) ).
tcf(c_293,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k3_waybel34(X1,X2,X0) = X0 )
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f896]) ).
tcf(c_300,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_funct_1(k2_waybel34(X2,X1,X0))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f906]) ).
tcf(c_301,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_funct_2(k2_waybel34(X2,X1,X0),u1_struct_0(X2),u1_struct_0(X1))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f905]) ).
tcf(c_302,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(k2_waybel34(X2,X1,X0),u1_struct_0(X2),u1_struct_0(X1))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f904]) ).
tcf(c_304,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_funct_2(k3_waybel34(X1,X2,X0),u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X2)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f908]) ).
tcf(c_305,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(k3_waybel34(X1,X2,X0),u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X2)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f907]) ).
tcf(c_309,plain,
! [X0: $i] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f912]) ).
tcf(c_395,plain,
! [X0: $i] :
( v2_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[],[f998]) ).
tcf(c_414,plain,
! [X0: $i] :
( v3_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X0) ),
inference(cnf_transformation,[],[f1017]) ).
tcf(c_427,plain,
! [X0: $i] :
( v4_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0) ),
inference(cnf_transformation,[],[f1030]) ).
tcf(c_432,plain,
! [X0: $i,X1: $i,X2: $i] :
( v17_waybel_0(k3_waybel34(X1,X2,X0),k7_lattice3(X1),k7_lattice3(X2))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v18_waybel_0(X0,X1,X2)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f1034]) ).
tcf(c_462,plain,
! [X0: $i] :
( v2_lattice3(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0) ),
inference(cnf_transformation,[],[f1064]) ).
tcf(c_470,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_lattice3(k7_lattice3(X0))
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f1073]) ).
tcf(c_742,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f1345]) ).
tcf(c_748,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v3_waybel_1(k1_waybel_1(k7_lattice3(X1),k7_lattice3(X0),X3,X2),k7_lattice3(X1),k7_lattice3(X0))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(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(X3,u1_struct_0(k7_lattice3(X1)),u1_struct_0(k7_lattice3(X0)))
| ~ v1_funct_2(X2,u1_struct_0(k7_lattice3(X0)),u1_struct_0(k7_lattice3(X1)))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ),
inference(cnf_transformation,[],[f1366]) ).
tcf(c_1207,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k1_waybel34(X0,X1,X2) = X3 )
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v17_waybel_0(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X3)
| ~ v2_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v4_orders_2(X1) ),
inference(global_subsumption_just,[status(thm)],[c_289,c_171,c_149,c_289]) ).
tcf(c_1208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k1_waybel34(X0,X1,X2) = X3 )
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ v17_waybel_0(X2,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X2,X3),X0,X1) ),
inference(renaming,[status(thm)],[c_1207]) ).
tcf(c_1209,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(X2)
| ~ v2_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v4_orders_2(X1) ),
inference(global_subsumption_just,[status(thm)],[c_292,c_171,c_149,c_292]) ).
tcf(c_1210,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_waybel_1(k1_waybel_1(X0,X1,k2_waybel34(X0,X1,X2),X2),X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X1)
| ~ v3_lattice3(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ v18_waybel_0(X2,X1,X0)
| ~ v1_funct_1(k2_waybel34(X0,X1,X2))
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m2_relset_1(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k2_waybel34(X0,X1,X2),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(renaming,[status(thm)],[c_1209]) ).
tcf(c_1332,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_1334,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1341,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( v1_funct_2(X0,X2,X4)
| ~ v1_funct_2(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1343,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m2_relset_1(X0,X2,X4)
| ~ m2_relset_1(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1425,plain,
( ~ v3_struct_0(sK13)
| ~ v1_lattice3(sK13) ),
inference(superposition,[status(thm)],[c_60,c_128]) ).
tcf(c_1426,plain,
( ~ v3_struct_0(sK12)
| ~ v1_lattice3(sK12) ),
inference(superposition,[status(thm)],[c_67,c_128]) ).
tcf(c_1468,plain,
( ( k3_waybel34(sK12,sK13,sK14) = sK14 )
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(superposition,[status(thm)],[c_51,c_293]) ).
tcf(c_1469,plain,
k3_waybel34(sK12,sK13,sK14) = sK14,
inference(global_subsumption_just,[status(thm)],[c_1468,c_67,c_60,c_50,c_53,c_1468]) ).
tcf(c_1492,plain,
( m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(instantiation,[status(thm)],[c_742]) ).
tcf(c_1523,plain,
k1_waybel34(k7_lattice3(sK12),k7_lattice3(sK13),sK14) != k2_waybel34(sK13,sK12,sK14),
inference(superposition,[status(thm)],[c_1469,c_49]) ).
tcf(c_1950,plain,
! [X0: $i,X1: $i] :
( v1_funct_2(k2_waybel34(X1,X0,sK14),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(sK14)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ m1_relset_1(sK14,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK14,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(instantiation,[status(thm)],[c_301]) ).
tcf(c_1972,plain,
! [X0: $i,X1: $i] :
( m2_relset_1(k2_waybel34(X1,X0,sK14),u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_funct_1(sK14)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X1)
| ~ v2_orders_2(X0)
| ~ m1_relset_1(sK14,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(sK14,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(instantiation,[status(thm)],[c_302]) ).
tcf(c_2220,plain,
( v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v2_lattice3(sK13)
| ~ v2_lattice3(sK12)
| ~ v1_lattice3(sK13)
| ~ v1_lattice3(sK12)
| ~ v4_orders_2(sK13)
| ~ v4_orders_2(sK12)
| ~ v3_orders_2(sK13)
| ~ v3_orders_2(sK12)
| ~ v2_orders_2(sK13)
| ~ v2_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(superposition,[status(thm)],[c_51,c_300]) ).
tcf(c_2386,plain,
! [X0: $i,X1: $i] :
( ( k2_waybel34(sK13,sK12,sK14) = X1 )
| ( X1 != X0 )
| ( k2_waybel34(sK13,sK12,sK14) != X0 ) ),
inference(instantiation,[status(thm)],[c_1334]) ).
tcf(c_2474,plain,
( v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v2_lattice3(sK13)
| ~ v2_lattice3(sK12)
| ~ v1_lattice3(sK13)
| ~ v1_lattice3(sK12)
| ~ v4_orders_2(sK13)
| ~ v4_orders_2(sK12)
| ~ v3_orders_2(sK13)
| ~ v3_orders_2(sK12)
| ~ v2_orders_2(sK13)
| ~ v2_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(instantiation,[status(thm)],[c_1950]) ).
tcf(c_2477,plain,
( m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v2_lattice3(sK13)
| ~ v2_lattice3(sK12)
| ~ v1_lattice3(sK13)
| ~ v1_lattice3(sK12)
| ~ v4_orders_2(sK13)
| ~ v4_orders_2(sK12)
| ~ v3_orders_2(sK13)
| ~ v3_orders_2(sK12)
| ~ v2_orders_2(sK13)
| ~ v2_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(instantiation,[status(thm)],[c_1972]) ).
tcf(c_3562,plain,
! [X0: $i] : u1_struct_0(X0) = u1_struct_0(X0),
inference(instantiation,[status(thm)],[c_1332]) ).
tcf(c_4872,plain,
( v1_funct_2(sK14,u1_struct_0(k7_lattice3(sK12)),u1_struct_0(k7_lattice3(sK13)))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(superposition,[status(thm)],[c_1469,c_304]) ).
tcf(c_5240,plain,
( v3_waybel_1(k1_waybel_1(sK13,sK12,k2_waybel34(sK13,sK12,sK14),sK14),sK13,sK12)
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v3_lattice3(sK13)
| ~ v3_lattice3(sK12)
| ~ v2_lattice3(sK13)
| ~ v2_lattice3(sK12)
| ~ v1_lattice3(sK12)
| ~ v4_orders_2(sK13)
| ~ v4_orders_2(sK12)
| ~ v3_orders_2(sK13)
| ~ v3_orders_2(sK12)
| ~ v2_orders_2(sK13)
| ~ v2_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ v18_waybel_0(sK14,sK12,sK13)
| ~ v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12)) ),
inference(instantiation,[status(thm)],[c_1210]) ).
tcf(c_5268,plain,
( m2_relset_1(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ m1_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12)) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_5269,plain,
( v1_funct_2(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ m1_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12)) ),
inference(instantiation,[status(thm)],[c_304]) ).
tcf(c_5275,plain,
( ( k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) = k2_waybel34(sK13,sK12,sK14) )
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12)) ),
inference(instantiation,[status(thm)],[c_293]) ).
tcf(c_5276,plain,
( m1_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12)) ),
inference(instantiation,[status(thm)],[c_742]) ).
tcf(c_5619,plain,
! [X0: $i] :
( ( k2_waybel34(sK13,sK12,sK14) = X0 )
| ( X0 != k2_waybel34(sK13,sK12,sK14) )
| ( k2_waybel34(sK13,sK12,sK14) != k2_waybel34(sK13,sK12,sK14) ) ),
inference(instantiation,[status(thm)],[c_2386]) ).
tcf(c_5620,plain,
k2_waybel34(sK13,sK12,sK14) = k2_waybel34(sK13,sK12,sK14),
inference(instantiation,[status(thm)],[c_1332]) ).
tcf(c_7112,plain,
( m2_relset_1(sK14,u1_struct_0(k7_lattice3(sK12)),u1_struct_0(k7_lattice3(sK13)))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(superposition,[status(thm)],[c_1469,c_305]) ).
tcf(c_9628,plain,
( l1_orders_2(k7_lattice3(sK13))
| ~ l1_orders_2(sK13) ),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_9700,plain,
( v3_struct_0(sK13)
| v3_struct_0(sK12)
| v3_waybel_1(k1_waybel_1(k7_lattice3(sK12),k7_lattice3(sK13),sK14,k2_waybel34(sK13,sK12,sK14)),k7_lattice3(sK12),k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v4_orders_2(sK13)
| ~ v4_orders_2(sK12)
| ~ v3_orders_2(sK13)
| ~ v3_orders_2(sK12)
| ~ v2_orders_2(sK13)
| ~ v2_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ m2_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ m2_relset_1(sK14,u1_struct_0(k7_lattice3(sK12)),u1_struct_0(k7_lattice3(sK13)))
| ~ v1_funct_2(sK14,u1_struct_0(k7_lattice3(sK12)),u1_struct_0(k7_lattice3(sK13)))
| ~ m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(sK13),u1_struct_0(sK12))
| ~ v3_waybel_1(k1_waybel_1(sK13,sK12,k2_waybel34(sK13,sK12,sK14),sK14),sK13,sK12)
| ~ m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12))) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_10112,plain,
u1_struct_0(k7_lattice3(sK13)) = u1_struct_0(k7_lattice3(sK13)),
inference(instantiation,[status(thm)],[c_3562]) ).
tcf(c_10685,plain,
( ( k2_waybel34(sK13,sK12,sK14) = k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) )
| ( k2_waybel34(sK13,sK12,sK14) != k2_waybel34(sK13,sK12,sK14) )
| ( k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) != k2_waybel34(sK13,sK12,sK14) ) ),
inference(instantiation,[status(thm)],[c_5619]) ).
tcf(c_17690,plain,
( l1_orders_2(k7_lattice3(sK12))
| ~ l1_orders_2(sK12) ),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_20502,plain,
u1_struct_0(k7_lattice3(sK12)) = u1_struct_0(k7_lattice3(sK12)),
inference(instantiation,[status(thm)],[c_3562]) ).
tcf(c_22040,plain,
( v3_struct_0(sK13)
| v3_lattice3(k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ v3_lattice3(sK13) ),
inference(instantiation,[status(thm)],[c_470]) ).
tcf(c_22096,plain,
( v2_orders_2(k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ v2_orders_2(sK13) ),
inference(instantiation,[status(thm)],[c_395]) ).
tcf(c_25747,plain,
( v2_orders_2(k7_lattice3(sK12))
| ~ l1_orders_2(sK12)
| ~ v2_orders_2(sK12) ),
inference(instantiation,[status(thm)],[c_395]) ).
tcf(c_26712,plain,
( v17_waybel_0(sK14,k7_lattice3(sK12),k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ l1_orders_2(sK12)
| ~ v3_lattice3(sK13)
| ~ v3_lattice3(sK12)
| ~ v2_lattice3(sK13)
| ~ v2_lattice3(sK12)
| ~ v1_lattice3(sK13)
| ~ v1_lattice3(sK12)
| ~ v4_orders_2(sK13)
| ~ v4_orders_2(sK12)
| ~ v3_orders_2(sK13)
| ~ v3_orders_2(sK12)
| ~ v2_orders_2(sK13)
| ~ v2_orders_2(sK12)
| ~ v1_funct_1(sK14)
| ~ v18_waybel_0(sK14,sK12,sK13)
| ~ m1_relset_1(sK14,u1_struct_0(sK12),u1_struct_0(sK13))
| ~ v1_funct_2(sK14,u1_struct_0(sK12),u1_struct_0(sK13)) ),
inference(superposition,[status(thm)],[c_1469,c_432]) ).
tcf(c_27223,plain,
( v3_struct_0(sK12)
| v3_lattice3(k7_lattice3(sK12))
| ~ l1_orders_2(sK12)
| ~ v3_lattice3(sK12) ),
inference(instantiation,[status(thm)],[c_470]) ).
tcf(c_27381,plain,
( v4_orders_2(k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ v4_orders_2(sK13) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_30173,plain,
( v4_orders_2(k7_lattice3(sK12))
| ~ l1_orders_2(sK12)
| ~ v4_orders_2(sK12) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_33259,plain,
( v3_orders_2(k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ v3_orders_2(sK13) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_40139,plain,
( v3_orders_2(k7_lattice3(sK12))
| ~ l1_orders_2(sK12)
| ~ v3_orders_2(sK12) ),
inference(instantiation,[status(thm)],[c_414]) ).
tcf(c_44383,plain,
( v2_lattice3(k7_lattice3(sK13))
| ~ l1_orders_2(sK13)
| ~ v1_lattice3(sK13) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_44503,plain,
( ~ v3_struct_0(k7_lattice3(sK13))
| ~ l1_orders_2(k7_lattice3(sK13))
| ~ v2_lattice3(k7_lattice3(sK13)) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_49941,plain,
( v2_lattice3(k7_lattice3(sK12))
| ~ l1_orders_2(sK12)
| ~ v1_lattice3(sK12) ),
inference(instantiation,[status(thm)],[c_462]) ).
tcf(c_51034,plain,
( v3_struct_0(k7_lattice3(sK13))
| v1_lattice3(k7_lattice3(sK13))
| ~ l1_orders_2(k7_lattice3(sK13))
| ~ v3_lattice3(k7_lattice3(sK13)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_92991,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(X0,X1,X2)
| ~ m2_relset_1(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( X2 != u1_struct_0(k7_lattice3(sK12)) )
| ( X1 != u1_struct_0(k7_lattice3(sK13)) )
| ( X0 != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) ) ),
inference(instantiation,[status(thm)],[c_1343]) ).
tcf(c_92992,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_funct_2(X0,X1,X2)
| ~ v1_funct_2(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( X2 != u1_struct_0(k7_lattice3(sK12)) )
| ( X1 != u1_struct_0(k7_lattice3(sK13)) )
| ( X0 != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) ) ),
inference(instantiation,[status(thm)],[c_1341]) ).
tcf(c_105713,plain,
! [X0: $i,X1: $i] :
( v1_funct_2(X0,X1,u1_struct_0(k7_lattice3(sK12)))
| ~ v1_funct_2(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( X1 != u1_struct_0(k7_lattice3(sK13)) )
| ( X0 != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) )
| ( u1_struct_0(k7_lattice3(sK12)) != u1_struct_0(k7_lattice3(sK12)) ) ),
inference(instantiation,[status(thm)],[c_92992]) ).
tcf(c_105714,plain,
! [X0: $i,X1: $i] :
( m2_relset_1(X0,X1,u1_struct_0(k7_lattice3(sK12)))
| ~ m2_relset_1(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( X1 != u1_struct_0(k7_lattice3(sK13)) )
| ( X0 != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) )
| ( u1_struct_0(k7_lattice3(sK12)) != u1_struct_0(k7_lattice3(sK12)) ) ),
inference(instantiation,[status(thm)],[c_92991]) ).
tcf(c_152993,plain,
! [X0: $i] :
( v1_funct_2(X0,u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ v1_funct_2(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( X0 != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) )
| ( u1_struct_0(k7_lattice3(sK13)) != u1_struct_0(k7_lattice3(sK13)) )
| ( u1_struct_0(k7_lattice3(sK12)) != u1_struct_0(k7_lattice3(sK12)) ) ),
inference(instantiation,[status(thm)],[c_105713]) ).
tcf(c_153016,plain,
! [X0: $i] :
( m2_relset_1(X0,u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ m2_relset_1(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( X0 != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) )
| ( u1_struct_0(k7_lattice3(sK13)) != u1_struct_0(k7_lattice3(sK13)) )
| ( u1_struct_0(k7_lattice3(sK12)) != u1_struct_0(k7_lattice3(sK12)) ) ),
inference(instantiation,[status(thm)],[c_105714]) ).
tcf(c_160518,plain,
( v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ v1_funct_2(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( u1_struct_0(k7_lattice3(sK13)) != u1_struct_0(k7_lattice3(sK13)) )
| ( u1_struct_0(k7_lattice3(sK12)) != u1_struct_0(k7_lattice3(sK12)) )
| ( k2_waybel34(sK13,sK12,sK14) != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) ) ),
inference(instantiation,[status(thm)],[c_152993]) ).
tcf(c_160540,plain,
( m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ m2_relset_1(k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ( u1_struct_0(k7_lattice3(sK13)) != u1_struct_0(k7_lattice3(sK13)) )
| ( u1_struct_0(k7_lattice3(sK12)) != u1_struct_0(k7_lattice3(sK12)) )
| ( k2_waybel34(sK13,sK12,sK14) != k3_waybel34(sK13,sK12,k2_waybel34(sK13,sK12,sK14)) ) ),
inference(instantiation,[status(thm)],[c_153016]) ).
tcf(c_163472,plain,
( ( k1_waybel34(k7_lattice3(sK12),k7_lattice3(sK13),sK14) = k2_waybel34(sK13,sK12,sK14) )
| ~ v1_funct_1(sK14)
| ~ l1_orders_2(k7_lattice3(sK13))
| ~ l1_orders_2(k7_lattice3(sK12))
| ~ v3_lattice3(k7_lattice3(sK13))
| ~ v3_lattice3(k7_lattice3(sK12))
| ~ v2_lattice3(k7_lattice3(sK13))
| ~ v2_lattice3(k7_lattice3(sK12))
| ~ v1_lattice3(k7_lattice3(sK13))
| ~ v4_orders_2(k7_lattice3(sK13))
| ~ v4_orders_2(k7_lattice3(sK12))
| ~ v3_orders_2(k7_lattice3(sK13))
| ~ v3_orders_2(k7_lattice3(sK12))
| ~ v2_orders_2(k7_lattice3(sK13))
| ~ v2_orders_2(k7_lattice3(sK12))
| ~ v1_funct_1(k2_waybel34(sK13,sK12,sK14))
| ~ v17_waybel_0(sK14,k7_lattice3(sK12),k7_lattice3(sK13))
| ~ m2_relset_1(sK14,u1_struct_0(k7_lattice3(sK12)),u1_struct_0(k7_lattice3(sK13)))
| ~ v1_funct_2(sK14,u1_struct_0(k7_lattice3(sK12)),u1_struct_0(k7_lattice3(sK13)))
| ~ m2_relset_1(k2_waybel34(sK13,sK12,sK14),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ v1_funct_2(k2_waybel34(sK13,sK12,sK14),u1_struct_0(k7_lattice3(sK13)),u1_struct_0(k7_lattice3(sK12)))
| ~ v3_waybel_1(k1_waybel_1(k7_lattice3(sK12),k7_lattice3(sK13),sK14,k2_waybel34(sK13,sK12,sK14)),k7_lattice3(sK12),k7_lattice3(sK13)) ),
inference(instantiation,[status(thm)],[c_1208]) ).
tcf(c_163474,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_163472,c_160540,c_160518,c_51034,c_49941,c_44503,c_44383,c_40139,c_33259,c_30173,c_27381,c_27223,c_26712,c_25747,c_22096,c_22040,c_20502,c_17690,c_10685,c_10112,c_9700,c_9628,c_7112,c_5620,c_5276,c_5275,c_5268,c_5269,c_5240,c_4872,c_2477,c_2474,c_2220,c_1523,c_1492,c_1425,c_1426,c_51,c_53,c_52,c_50,c_54,c_55,c_56,c_57,c_58,c_59,c_60,c_61,c_62,c_63,c_64,c_65,c_66,c_67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT355+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 21:17:07 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 126.62/19.39 % SZS status Started for theBenchmark.p
% 126.62/19.39 % SZS status Theorem for theBenchmark.p
% 126.62/19.39
% 126.62/19.39 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 126.62/19.39
% 126.62/19.39 % ------ iProver source info
% 126.62/19.39
% 126.62/19.39 % git: date: 2026-07-19 20:42:38 +0200
% 126.62/19.39 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 126.62/19.39 % git: non_committed_changes: false
% 126.62/19.39
% 126.62/19.39 % ------ Parsing...
% 126.62/19.39 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 126.62/19.39
% 126.62/19.39 % ------ Preprocessing... sf_s rm: 103 0s sf_e sf_s rm: 8 0s sf_e %
% 126.62/19.39
% 126.62/19.39 % ------ Preprocessing...%
% 126.62/19.39
% 126.62/19.39 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 126.62/19.39 % ------ Proving...
% 126.62/19.39 % ------ Problem Properties
% 126.62/19.39
% 126.62/19.39 %
% 126.62/19.39 % clauses 558
% 126.62/19.39 % conjectures 19
% 126.62/19.39 % EPR 388
% 126.62/19.39 % Horn 471
% 126.62/19.39 % unary 222
% 126.62/19.39 % binary 164
% 126.62/19.39 % lits 1920
% 126.62/19.39 % lits eq 17
% 126.62/19.39 % fd_pure 0
% 126.62/19.39 % fd_pseudo 0
% 126.62/19.39 % fd_cond 1
% 126.62/19.39 % fd_pseudo_cond 5
% 126.62/19.39 % AC symbols 0
% 126.62/19.39
% 126.62/19.39 % ------ Input Options Time Limit: Unbounded
% 126.62/19.39
% 126.62/19.39
% 126.62/19.39 % ------
% 126.62/19.39 % Current options:
% 126.62/19.39 % ------
% 126.62/19.39
% 126.62/19.39
% 126.62/19.39 %
% 126.62/19.39
% 126.62/19.39 % ------ Proving...
% 126.62/19.39 %
% 126.62/19.39
% 126.62/19.39 % SZS status Theorem for theBenchmark.p
% 126.62/19.39
% 126.62/19.39 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 126.62/19.39
% 126.62/19.39
%------------------------------------------------------------------------------