%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT356+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:59:37 PM UTC 2026
% Result : Theorem 4.83s 6.75s
% Output : CNFRefutation 4.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of formulae : 98 ( 15 unt; 1 def)
% Number of atoms : 802 ( 36 equ)
% Maximal formula atoms : 25 ( 8 avg)
% Number of connectives : 1147 ( 443 ~; 426 |; 244 &)
% ( 6 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 32 ( 30 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-4 aty)
% Number of variables : 118 ( 0 sgn 116 !; 2 ?; 36 :)
% 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) )
=> ( k2_waybel34(X0,X0,k7_grcat_1(X0)) = k7_grcat_1(X0)
& k1_waybel34(X0,X0,k7_grcat_1(X0)) = k7_grcat_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_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) )
=> ( k2_waybel34(X0,X0,k7_grcat_1(X0)) = k7_grcat_1(X0)
& k1_waybel34(X0,X0,k7_grcat_1(X0)) = k7_grcat_1(X0) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f29,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/sandbox2/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f34,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f49,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/sandbox2/benchmark/theBenchmark.p',d1_waybel34) ).
fof(f50,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/sandbox2/benchmark/theBenchmark.p',d2_waybel34) ).
fof(f61,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(k7_grcat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_grcat_1) ).
fof(f62,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f91,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v2_funct_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_waybel10) ).
fof(f93,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v21_waybel_0(k7_grcat_1(X0),X0,X0)
& v20_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v11_quantal1(k7_grcat_1(X0))
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v2_funct_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_waybel10) ).
fof(f129,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_waybel34) ).
fof(f143,plain,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v21_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v11_quantal1(k7_grcat_1(X0))
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v2_funct_1(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f93]) ).
fof(f146,plain,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v21_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v11_quantal1(k7_grcat_1(X0))
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f143]) ).
fof(f152,plain,
! [X0] :
( l1_struct_0(X0)
=> ( v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f91]) ).
fof(f155,plain,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v5_orders_3(k7_grcat_1(X0),X0,X0)
& v11_quantal1(k7_grcat_1(X0))
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f146]) ).
fof(f170,plain,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v11_quantal1(k7_grcat_1(X0))
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f155]) ).
fof(f173,plain,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v1_partfun1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f170]) ).
fof(f188,plain,
! [X0] :
( ( l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(pure_predicate_removal,[],[f173]) ).
fof(f193,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)
& ( k7_grcat_1(X0) != k2_waybel34(X0,X0,k7_grcat_1(X0))
| k7_grcat_1(X0) != k1_waybel34(X0,X0,k7_grcat_1(X0)) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f194,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)
& ( k7_grcat_1(X0) != k2_waybel34(X0,X0,k7_grcat_1(X0))
| k7_grcat_1(X0) != k1_waybel34(X0,X0,k7_grcat_1(X0)) ) ),
inference(flattening,[],[f193]) ).
fof(f232,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,[],[f29]) ).
fof(f233,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,[],[f232]) ).
fof(f240,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f241,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f240]) ).
fof(f265,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,[],[f49]) ).
fof(f266,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,[],[f265]) ).
fof(f267,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,[],[f50]) ).
fof(f268,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,[],[f267]) ).
fof(f273,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ( m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(k7_grcat_1(X0)) ) ),
inference(ennf_transformation,[],[f61]) ).
fof(f274,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f300,plain,
! [X0] :
( ~ l1_struct_0(X0)
| ( v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(ennf_transformation,[],[f152]) ).
fof(f303,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(ennf_transformation,[],[f188]) ).
fof(f304,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(flattening,[],[f303]) ).
fof(f344,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0) ),
inference(ennf_transformation,[],[f129]) ).
fof(f345,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0) ),
inference(flattening,[],[f344]) ).
fof(f356,plain,
( l1_orders_2(sK4)
& v3_lattice3(sK4)
& v2_lattice3(sK4)
& v1_lattice3(sK4)
& v4_orders_2(sK4)
& v3_orders_2(sK4)
& v2_orders_2(sK4)
& ( k7_grcat_1(sK4) != k2_waybel34(sK4,sK4,k7_grcat_1(sK4))
| k7_grcat_1(sK4) != k1_waybel34(sK4,sK4,k7_grcat_1(sK4)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X0,sK4)],[f194]) ).
fof(f359,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,[],[f266]) ).
fof(f360,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,[],[f268]) ).
fof(f389,plain,
l1_orders_2(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f390,plain,
v3_lattice3(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f391,plain,
v2_lattice3(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f392,plain,
v1_lattice3(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f393,plain,
v4_orders_2(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f394,plain,
v3_orders_2(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f395,plain,
v2_orders_2(sK4),
inference(cnf_transformation,[],[f356]) ).
fof(f396,plain,
( k7_grcat_1(sK4) != k2_waybel34(sK4,sK4,k7_grcat_1(sK4))
| k7_grcat_1(sK4) != k1_waybel34(sK4,sK4,k7_grcat_1(sK4)) ),
inference(cnf_transformation,[],[f356]) ).
fof(f475,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f233]) ).
fof(f498,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f241]) ).
fof(f534,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,[],[f359]) ).
fof(f536,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)
| ~ v3_waybel_1(k1_waybel_1(X0,X1,X3,X2),X0,X1)
| k2_waybel34(X0,X1,X2) = X3 ),
inference(cnf_transformation,[],[f360]) ).
fof(f544,plain,
! [X0] :
( ~ l1_struct_0(X0)
| m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f273]) ).
fof(f547,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f607,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v1_funct_1(k7_grcat_1(X0)) ),
inference(cnf_transformation,[],[f300]) ).
fof(f627,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f353]) ).
fof(f760,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_49,negated_conjecture,
( ( k2_waybel34(sK4,sK4,k7_grcat_1(sK4)) != k7_grcat_1(sK4) )
| ( k1_waybel34(sK4,sK4,k7_grcat_1(sK4)) != k7_grcat_1(sK4) ) ),
inference(cnf_transformation,[],[f396]) ).
tcf(c_50,negated_conjecture,
v2_orders_2(sK4),
inference(cnf_transformation,[],[f395]) ).
tcf(c_51,negated_conjecture,
v3_orders_2(sK4),
inference(cnf_transformation,[],[f394]) ).
tcf(c_52,negated_conjecture,
v4_orders_2(sK4),
inference(cnf_transformation,[],[f393]) ).
tcf(c_53,negated_conjecture,
v1_lattice3(sK4),
inference(cnf_transformation,[],[f392]) ).
tcf(c_54,negated_conjecture,
v2_lattice3(sK4),
inference(cnf_transformation,[],[f391]) ).
tcf(c_55,negated_conjecture,
v3_lattice3(sK4),
inference(cnf_transformation,[],[f390]) ).
tcf(c_56,negated_conjecture,
l1_orders_2(sK4),
inference(cnf_transformation,[],[f389]) ).
tcf(c_115,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f475]) ).
tcf(c_136,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[],[f498]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k1_waybel34(X0,X1,X2) = X3 )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ 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)
| ~ 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,[],[f534]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_waybel34(X0,X1,X3) = X2 )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ 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)
| ~ v18_waybel_0(X3,X1,X0)
| ~ 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,[],[f536]) ).
tcf(c_168,plain,
! [X0: $i] :
( m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f544]) ).
tcf(c_169,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f547]) ).
tcf(c_229,plain,
! [X0: $i] :
( v1_funct_1(k7_grcat_1(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f607]) ).
tcf(c_249,plain,
! [X0: $i] :
( sP2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0) ),
inference(cnf_transformation,[],[f627]) ).
tcf(c_382,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_waybel_1(k1_waybel_1(X0,X0,k7_grcat_1(X0),k7_grcat_1(X0)),X0,X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f760]) ).
tcf(c_394,plain,
( l1_struct_0(sK4)
| ~ l1_orders_2(sK4) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_426,plain,
( v1_funct_1(k7_grcat_1(sK4))
| ~ l1_struct_0(sK4) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_483,plain,
( ~ v3_struct_0(sK4)
| ~ l1_orders_2(sK4)
| ~ v2_lattice3(sK4) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_505,plain,
( sP2(sK4)
| v3_struct_0(sK4)
| ~ l1_orders_2(sK4)
| ~ v2_orders_2(sK4) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_526,plain,
( m2_relset_1(k7_grcat_1(sK4),u1_struct_0(sK4),u1_struct_0(sK4))
| ~ l1_struct_0(sK4) ),
inference(instantiation,[status(thm)],[c_168]) ).
tcf(c_696,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_waybel34(X0,X1,X3) = X2 )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ 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))
| ~ v18_waybel_0(X3,X1,X0)
| ~ 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_158,c_136,c_115,c_158]) ).
tcf(c_697,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_waybel34(X0,X1,X3) = X2 )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ 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)
| ~ v18_waybel_0(X3,X1,X0)
| ~ 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_696]) ).
tcf(c_698,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k1_waybel34(X0,X1,X2) = X3 )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ 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)
| ~ 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_156,c_136,c_115,c_156]) ).
tcf(c_699,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k1_waybel34(X0,X1,X2) = X3 )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X2)
| ~ 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)
| ~ 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_698]) ).
tcf(c_28938,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( k2_waybel34(X0,X0,k7_grcat_1(X0)) = k7_grcat_1(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)
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_382,c_697]) ).
tcf(c_28957,plain,
( v3_struct_0(sK4)
| ( k2_waybel34(sK4,sK4,k7_grcat_1(sK4)) = k7_grcat_1(sK4) )
| ~ l1_orders_2(sK4)
| ~ v3_lattice3(sK4)
| ~ v2_lattice3(sK4)
| ~ v1_lattice3(sK4)
| ~ v4_orders_2(sK4)
| ~ v3_orders_2(sK4)
| ~ v2_orders_2(sK4)
| ~ v1_funct_1(k7_grcat_1(sK4))
| ~ v18_waybel_0(k7_grcat_1(sK4),sK4,sK4)
| ~ m2_relset_1(k7_grcat_1(sK4),u1_struct_0(sK4),u1_struct_0(sK4))
| ~ v1_funct_2(k7_grcat_1(sK4),u1_struct_0(sK4),u1_struct_0(sK4)) ),
inference(instantiation,[status(thm)],[c_28938]) ).
tcf(c_29303,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( k1_waybel34(X0,X0,k7_grcat_1(X0)) = k7_grcat_1(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)
| ~ v1_funct_1(k7_grcat_1(X0))
| ~ v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ m2_relset_1(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_382,c_699]) ).
tcf(c_29322,plain,
( v3_struct_0(sK4)
| ( k1_waybel34(sK4,sK4,k7_grcat_1(sK4)) = k7_grcat_1(sK4) )
| ~ l1_orders_2(sK4)
| ~ v3_lattice3(sK4)
| ~ v2_lattice3(sK4)
| ~ v1_lattice3(sK4)
| ~ v4_orders_2(sK4)
| ~ v3_orders_2(sK4)
| ~ v2_orders_2(sK4)
| ~ v1_funct_1(k7_grcat_1(sK4))
| ~ v17_waybel_0(k7_grcat_1(sK4),sK4,sK4)
| ~ m2_relset_1(k7_grcat_1(sK4),u1_struct_0(sK4),u1_struct_0(sK4))
| ~ v1_funct_2(k7_grcat_1(sK4),u1_struct_0(sK4),u1_struct_0(sK4)) ),
inference(instantiation,[status(thm)],[c_29303]) ).
fof(f352,definition,
! [X0] :
( ~ sP2(X0)
| ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f353,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| sP2(X0) ),
inference(definition_folding,[],[f304,f352]) ).
fof(f366,plain,
! [X0] :
( ~ sP2(X0)
| ( v8_waybel_1(k7_grcat_1(X0),X0)
& v7_waybel_1(k7_grcat_1(X0),X0)
& v6_waybel_1(k7_grcat_1(X0),X0)
& v23_waybel_0(k7_grcat_1(X0),X0,X0)
& v22_waybel_0(k7_grcat_1(X0),X0,X0)
& v19_waybel_0(k7_grcat_1(X0),X0,X0)
& v18_waybel_0(k7_grcat_1(X0),X0,X0)
& v17_waybel_0(k7_grcat_1(X0),X0,X0)
& v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
& ~ v1_xboole_0(k7_grcat_1(X0))
& v1_funct_1(k7_grcat_1(X0))
& v1_relat_1(k7_grcat_1(X0)) ) ),
inference(nnf_transformation,[],[f352]) ).
fof(f621,plain,
! [X0] :
( ~ sP2(X0)
| v18_waybel_0(k7_grcat_1(X0),X0,X0) ),
inference(cnf_transformation,[],[f366]) ).
fof(f622,plain,
! [X0] :
( ~ sP2(X0)
| v17_waybel_0(k7_grcat_1(X0),X0,X0) ),
inference(cnf_transformation,[],[f366]) ).
fof(f623,plain,
! [X0] :
( ~ sP2(X0)
| v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f366]) ).
tcf(c_240,plain,
! [X0: $i] :
( v1_funct_2(k7_grcat_1(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f623]) ).
tcf(c_241,plain,
! [X0: $i] :
( v17_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f622]) ).
tcf(c_242,plain,
! [X0: $i] :
( v18_waybel_0(k7_grcat_1(X0),X0,X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f621]) ).
tcf(c_466,plain,
( v18_waybel_0(k7_grcat_1(sK4),sK4,sK4)
| ~ sP2(sK4) ),
inference(instantiation,[status(thm)],[c_242]) ).
tcf(c_467,plain,
( v17_waybel_0(k7_grcat_1(sK4),sK4,sK4)
| ~ sP2(sK4) ),
inference(instantiation,[status(thm)],[c_241]) ).
tcf(c_506,plain,
( v1_funct_2(k7_grcat_1(sK4),u1_struct_0(sK4),u1_struct_0(sK4))
| ~ sP2(sK4) ),
inference(instantiation,[status(thm)],[c_240]) ).
tcf(c_29323,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_29322,c_28957,c_49,c_526,c_506,c_505,c_483,c_467,c_466,c_426,c_394,c_50,c_51,c_52,c_53,c_54,c_55,c_56]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT356+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.38 % Computer : n019.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Wed Sep 23 21:19:40 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.43
% 0.14/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.43
% 0.14/5.43 % Detected problem language: tptp
% 0.14/5.45 % Proving...
% 4.83/6.75 % SZS status Started for theBenchmark.p
% 4.83/6.75 % SZS status Theorem for theBenchmark.p
% 4.83/6.75
% 4.83/6.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.83/6.75
% 4.83/6.75 % ------ iProver source info
% 4.83/6.75
% 4.83/6.75 % git: date: 2026-07-19 20:42:38 +0200
% 4.83/6.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.83/6.75 % git: non_committed_changes: false
% 4.83/6.75
% 4.83/6.75 % ------ Parsing...
% 4.83/6.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.83/6.75
% 4.83/6.75 % ------ Preprocessing... sup_sim: 1 sf_s rm: 123 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 16 0s sf_e pe_s pe_e %
% 4.83/6.75
% 4.83/6.75 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.83/6.75
% 4.83/6.75 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.83/6.75 % ------ Proving...
% 4.83/6.75 % ------ Problem Properties
% 4.83/6.75
% 4.83/6.75 %
% 4.83/6.75 % clauses 145
% 4.83/6.75 % conjectures 8
% 4.83/6.75 % EPR 46
% 4.83/6.75 % Horn 102
% 4.83/6.75 % unary 47
% 4.83/6.75 % binary 26
% 4.83/6.75 % lits 753
% 4.83/6.75 % lits eq 11
% 4.83/6.75 % fd_pure 0
% 4.83/6.75 % fd_pseudo 0
% 4.83/6.75 % fd_cond 1
% 4.83/6.75 % fd_pseudo_cond 3
% 4.83/6.75 % AC symbols 0
% 4.83/6.75
% 4.83/6.75 % ------ Schedule dynamic 5 is on
% 4.83/6.75
% 4.83/6.75 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.83/6.75
% 4.83/6.75
% 4.83/6.75 % ------
% 4.83/6.75 % Current options:
% 4.83/6.75 % ------
% 4.83/6.75
% 4.83/6.75
% 4.83/6.75 %
% 4.83/6.75
% 4.83/6.75 % ------ Proving...
% 4.83/6.75 %
% 4.83/6.75
% 4.83/6.75 % SZS status Theorem for theBenchmark.p
% 4.83/6.75
% 4.83/6.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.83/6.75
% 4.83/6.75
%------------------------------------------------------------------------------