%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU410+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 : n013.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 02:57:23 PM UTC 2026
% Result : Theorem 222.40s 40.07s
% Output : CNFRefutation 150.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 29
% Syntax : Number of formulae : 433 ( 140 unt; 8 def)
% Number of atoms : 2774 ( 117 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 3186 (1409 ~;1488 |; 216 &)
% ( 14 <=>; 59 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 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 : 26 ( 24 usr; 9 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-4 aty)
% Number of variables : 629 ( 0 sgn 610 !; 19 ?; 248 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X3 = X5
& X2 = X4
& r1_latsum_1(X0,X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1) )
=> k13_lattice3(X0,X2,X3) = k13_lattice3(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_latsum_1) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( X3 = X5
& X2 = X4
& r1_latsum_1(X0,X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1) )
=> k13_lattice3(X0,X2,X3) = k13_lattice3(X1,X4,X5) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f6,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X0))
& m1_subset_1(X1,u1_struct_0(X0))
& l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0) )
=> k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k13_lattice3) ).
fof(f7,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f8,axiom,
! [X0,X1,X2] :
( X2 = k3_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X1)
& r2_hidden(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X0))
& m1_subset_1(X1,u1_struct_0(X0))
& l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0) )
=> m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k13_lattice3) ).
fof(f17,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f27,axiom,
! [X0] :
? [X1] : m1_subset_1(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f30,axiom,
! [X0] :
( ( l1_struct_0(X0)
& ~ v3_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f44,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X0))
& m1_subset_1(X1,u1_struct_0(X0))
& l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ( r3_orders_2(X0,X1,X2)
<=> r1_orders_2(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r3_orders_2) ).
fof(f46,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X0))
& m1_subset_1(X1,u1_struct_0(X0))
& l1_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> r3_orders_2(X0,X1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r3_orders_2) ).
fof(f47,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( r2_hidden(X2,u1_struct_0(X0))
=> m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_latsum_1) ).
fof(f48,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( r2_hidden(X2,k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))
=> m1_subset_1(X2,u1_struct_0(X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_latsum_1) ).
fof(f49,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
=> ( ( v3_orders_2(X1)
& v3_orders_2(X0)
& r1_latsum_1(X0,X1)
& X3 = X5
& X2 = X4 )
=> ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(X1,X4,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_latsum_1) ).
fof(f50,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
& v12_waybel_0(X1,X0)
& v1_waybel_0(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X3,X1)
& r2_hidden(X2,X1) )
=> r2_hidden(k13_lattice3(X0,X2,X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_latsum_1) ).
fof(f51,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( l1_orders_2(X1)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k1_latsum_1(X0,X1)))
=> ( ( r2_hidden(X2,u1_struct_0(X1))
& r1_orders_2(k1_latsum_1(X0,X1),X2,X3)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0) )
=> r2_hidden(X3,u1_struct_0(X1)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_latsum_1) ).
fof(f52,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f53,axiom,
! [X0] :
( ( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( X3 = k13_lattice3(X0,X1,X2)
<=> ( ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ( ( r1_orders_2(X0,X2,X4)
& r1_orders_2(X0,X1,X4) )
=> r1_orders_2(X0,X3,X4) ) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_yellow_0) ).
fof(f55,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( r2_hidden(X0,X1)
| v1_xboole_0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f57,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X2))
& r2_hidden(X0,X1) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f60,axiom,
! [X0,X1] :
~ ( v1_xboole_0(X1)
& r2_hidden(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f62,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
=> ( ( v3_orders_2(X0)
& r1_latsum_1(X0,X1)
& X3 = X5
& X2 = X4 )
=> ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(k1_latsum_1(X0,X1),X4,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_latsum_1) ).
fof(f68,plain,
? [X0] :
( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_orders_2(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
& ? [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
& X3 = X5
& X2 = X4
& r1_latsum_1(X0,X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& k13_lattice3(X0,X2,X3) != k13_lattice3(X1,X4,X5) ) ) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f69,plain,
? [X0] :
( l1_orders_2(X0)
& v1_lattice3(X0)
& v4_orders_2(X0)
& v3_orders_2(X0)
& v2_orders_2(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_orders_2(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& ? [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
& ? [X5] :
( m1_subset_1(X5,u1_struct_0(X1))
& X3 = X5
& X2 = X4
& r1_latsum_1(X0,X1)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
& m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& v1_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X1)
& k13_lattice3(X0,X2,X3) != k13_lattice3(X1,X4,X5) ) ) ) ) ) ),
inference(flattening,[],[f68]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1) ),
inference(flattening,[],[f73]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
inference(flattening,[],[f78]) ).
fof(f82,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f87,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f30]) ).
fof(f88,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(flattening,[],[f87]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( r3_orders_2(X0,X1,X2)
<=> r1_orders_2(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f44]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( r3_orders_2(X0,X1,X2)
<=> r1_orders_2(X0,X1,X2) ) ),
inference(flattening,[],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| r3_orders_2(X0,X1,X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f104,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| r3_orders_2(X0,X1,X1) ),
inference(flattening,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ r2_hidden(X2,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1))) ) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f106,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ r2_hidden(X2,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1))) ) ) ),
inference(flattening,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ r2_hidden(X2,k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))
| m1_subset_1(X2,u1_struct_0(X1)) ) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f108,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ r2_hidden(X2,k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))
| m1_subset_1(X2,u1_struct_0(X1)) ) ) ),
inference(flattening,[],[f107]) ).
fof(f109,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X1))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(X1,X4,X5) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f110,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X1))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(X1,X4,X5) ) ) ) ) ) ) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v12_waybel_0(X1,X0)
| ~ v1_waybel_0(X1,X0)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k13_lattice3(X0,X2,X3),X1) ) ) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f112,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v12_waybel_0(X1,X0)
| ~ v1_waybel_0(X1,X0)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k13_lattice3(X0,X2,X3),X1) ) ) ) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ r2_hidden(X2,u1_struct_0(X1))
| ~ r1_orders_2(k1_latsum_1(X0,X1),X2,X3)
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
| r2_hidden(X3,u1_struct_0(X1)) ) ) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f114,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ r2_hidden(X2,u1_struct_0(X1))
| ~ r1_orders_2(k1_latsum_1(X0,X1),X2,X3)
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
| r2_hidden(X3,u1_struct_0(X1)) ) ) ) ),
inference(flattening,[],[f113]) ).
fof(f115,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f52]) ).
fof(f116,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ( X3 = k13_lattice3(X0,X1,X2)
<=> ( ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X4)
| ~ r1_orders_2(X0,X1,X4)
| r1_orders_2(X0,X3,X4) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) ) ) ) ) ),
inference(ennf_transformation,[],[f53]) ).
fof(f117,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ( X3 = k13_lattice3(X0,X1,X2)
<=> ( ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X4)
| ~ r1_orders_2(X0,X1,X4)
| r1_orders_2(X0,X3,X4) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) ) ) ) ) ),
inference(flattening,[],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f55]) ).
fof(f119,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(flattening,[],[f118]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(ennf_transformation,[],[f57]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(flattening,[],[f121]) ).
fof(f125,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f127,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(k1_latsum_1(X0,X1),X4,X5) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f62]) ).
fof(f128,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ( r1_orders_2(X0,X2,X3)
<=> r1_orders_2(k1_latsum_1(X0,X1),X4,X5) ) ) ) ) ) ) ),
inference(flattening,[],[f127]) ).
fof(f131,plain,
( l1_orders_2(sK0)
& v1_lattice3(sK0)
& v4_orders_2(sK0)
& v3_orders_2(sK0)
& v2_orders_2(sK0)
& ~ v3_struct_0(sK0)
& l1_orders_2(sK1)
& v1_lattice3(sK1)
& v4_orders_2(sK1)
& v3_orders_2(sK1)
& v2_orders_2(sK1)
& ~ v3_struct_0(sK1)
& m1_subset_1(sK2,u1_struct_0(sK0))
& m1_subset_1(sK3,u1_struct_0(sK0))
& m1_subset_1(sK4,u1_struct_0(sK1))
& m1_subset_1(sK5,u1_struct_0(sK1))
& sK3 = sK5
& sK2 = sK4
& r1_latsum_1(sK0,sK1)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK0)))
& v13_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK0)
& m1_subset_1(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK1)
& v1_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK1)
& k13_lattice3(sK0,sK2,sK3) != k13_lattice3(sK1,sK4,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5)],[f69]) ).
fof(f132,plain,
! [X0,X1,X2] :
( ( k3_xboole_0(X0,X1) != X2
| ! [X3] :
( ( ~ r2_hidden(X3,X2)
| ( r2_hidden(X3,X1)
& r2_hidden(X3,X0) ) )
& ( ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X2) ) ) )
& ( ? [X3] :
( ( r2_hidden(X3,X2)
| ( r2_hidden(X3,X1)
& r2_hidden(X3,X0) ) )
& ( ~ r2_hidden(X3,X2)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) ) )
| X2 = k3_xboole_0(X0,X1) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f133,plain,
! [X0,X1,X2] :
( ( k3_xboole_0(X0,X1) != X2
| ! [X3] :
( ( ~ r2_hidden(X3,X2)
| ( r2_hidden(X3,X1)
& r2_hidden(X3,X0) ) )
& ( ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X2) ) ) )
& ( ? [X3] :
( ( r2_hidden(X3,X2)
| ( r2_hidden(X3,X1)
& r2_hidden(X3,X0) ) )
& ( ~ r2_hidden(X3,X2)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) ) )
| X2 = k3_xboole_0(X0,X1) ) ),
inference(flattening,[],[f132]) ).
fof(f134,plain,
! [X0,X1,X2] :
( ( k3_xboole_0(X0,X1) != X2
| ! [X4] :
( ( ~ r2_hidden(X4,X2)
| ( r2_hidden(X4,X1)
& r2_hidden(X4,X0) ) )
& ( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X2) ) ) )
& ( ? [X3] :
( ( r2_hidden(X3,X2)
| ( r2_hidden(X3,X1)
& r2_hidden(X3,X0) ) )
& ( ~ r2_hidden(X3,X2)
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0) ) )
| X2 = k3_xboole_0(X0,X1) ) ),
inference(rectify,[],[f133]) ).
fof(f135,plain,
! [X0,X1,X2] :
( ( k3_xboole_0(X0,X1) != X2
| ! [X4] :
( ( ~ r2_hidden(X4,X2)
| ( r2_hidden(X4,X1)
& r2_hidden(X4,X0) ) )
& ( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X2) ) ) )
& ( ( ( r2_hidden(sK6(X0,X1,X2),X2)
| ( r2_hidden(sK6(X0,X1,X2),X1)
& r2_hidden(sK6(X0,X1,X2),X0) ) )
& ( ~ r2_hidden(sK6(X0,X1,X2),X2)
| ~ r2_hidden(sK6(X0,X1,X2),X1)
| ~ r2_hidden(sK6(X0,X1,X2),X0) ) )
| X2 = k3_xboole_0(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X3,sK6(X0,X1,X2))],[f134]) ).
fof(f139,plain,
! [X0] : m1_subset_1(sK10(X0),X0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X1,sK10(X0))],[f27]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ( ( ~ r3_orders_2(X0,X1,X2)
| r1_orders_2(X0,X1,X2) )
& ( ~ r1_orders_2(X0,X1,X2)
| r3_orders_2(X0,X1,X2) ) ) ),
inference(nnf_transformation,[],[f102]) ).
fof(f150,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X1))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ( ( ~ r1_orders_2(X0,X2,X3)
| r1_orders_2(X1,X4,X5) )
& ( ~ r1_orders_2(X1,X4,X5)
| r1_orders_2(X0,X2,X3) ) ) ) ) ) ) ) ),
inference(nnf_transformation,[],[f110]) ).
fof(f151,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ( ( k13_lattice3(X0,X1,X2) != X3
| ( ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X4)
| ~ r1_orders_2(X0,X1,X4)
| r1_orders_2(X0,X3,X4) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) )
& ( ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& r1_orders_2(X0,X2,X4)
& r1_orders_2(X0,X1,X4)
& ~ r1_orders_2(X0,X3,X4) )
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| X3 = k13_lattice3(X0,X1,X2) ) ) ) ) ) ),
inference(nnf_transformation,[],[f117]) ).
fof(f152,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ( ( k13_lattice3(X0,X1,X2) != X3
| ( ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X4)
| ~ r1_orders_2(X0,X1,X4)
| r1_orders_2(X0,X3,X4) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) )
& ( ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& r1_orders_2(X0,X2,X4)
& r1_orders_2(X0,X1,X4)
& ~ r1_orders_2(X0,X3,X4) )
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| X3 = k13_lattice3(X0,X1,X2) ) ) ) ) ) ),
inference(flattening,[],[f151]) ).
fof(f153,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ( ( k13_lattice3(X0,X1,X2) != X3
| ( ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X5)
| ~ r1_orders_2(X0,X1,X5)
| r1_orders_2(X0,X3,X5) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) )
& ( ? [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
& r1_orders_2(X0,X2,X4)
& r1_orders_2(X0,X1,X4)
& ~ r1_orders_2(X0,X3,X4) )
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| X3 = k13_lattice3(X0,X1,X2) ) ) ) ) ) ),
inference(rectify,[],[f152]) ).
fof(f154,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ( ( k13_lattice3(X0,X1,X2) != X3
| ( ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X5)
| ~ r1_orders_2(X0,X1,X5)
| r1_orders_2(X0,X3,X5) )
& r1_orders_2(X0,X2,X3)
& r1_orders_2(X0,X1,X3) ) )
& ( ( m1_subset_1(sK19(X0,X1,X2,X3),u1_struct_0(X0))
& r1_orders_2(X0,X2,sK19(X0,X1,X2,X3))
& r1_orders_2(X0,X1,sK19(X0,X1,X2,X3))
& ~ r1_orders_2(X0,X3,sK19(X0,X1,X2,X3)) )
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| X3 = k13_lattice3(X0,X1,X2) ) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X4,sK19(X0,X1,X2,X3))],[f153]) ).
fof(f155,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(X0))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ( ( ~ r1_orders_2(X0,X2,X3)
| r1_orders_2(k1_latsum_1(X0,X1),X4,X5) )
& ( ~ r1_orders_2(k1_latsum_1(X0,X1),X4,X5)
| r1_orders_2(X0,X2,X3) ) ) ) ) ) ) ) ),
inference(nnf_transformation,[],[f128]) ).
fof(f156,plain,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f157,plain,
v1_lattice3(sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f158,plain,
v4_orders_2(sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f159,plain,
v3_orders_2(sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f160,plain,
v2_orders_2(sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f161,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f162,plain,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f163,plain,
v1_lattice3(sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f164,plain,
v4_orders_2(sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f165,plain,
v3_orders_2(sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f166,plain,
v2_orders_2(sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f167,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f168,plain,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f131]) ).
fof(f169,plain,
m1_subset_1(sK3,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f131]) ).
fof(f170,plain,
m1_subset_1(sK4,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f131]) ).
fof(f171,plain,
m1_subset_1(sK5,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f131]) ).
fof(f172,plain,
sK3 = sK5,
inference(cnf_transformation,[],[f131]) ).
fof(f173,plain,
sK2 = sK4,
inference(cnf_transformation,[],[f131]) ).
fof(f174,plain,
r1_latsum_1(sK0,sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f175,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(cnf_transformation,[],[f131]) ).
fof(f176,plain,
v13_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK0),
inference(cnf_transformation,[],[f131]) ).
fof(f177,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(cnf_transformation,[],[f131]) ).
fof(f178,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f179,plain,
v1_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK1),
inference(cnf_transformation,[],[f131]) ).
fof(f180,plain,
k13_lattice3(sK0,sK2,sK3) != k13_lattice3(sK1,sK4,sK5),
inference(cnf_transformation,[],[f131]) ).
fof(f183,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| k13_lattice3(X0,X1,X2) = k13_lattice3(X0,X2,X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f184,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f7]) ).
fof(f186,plain,
! [X2,X0,X1,X4] :
( k3_xboole_0(X0,X1) != X2
| ~ r2_hidden(X4,X2)
| r2_hidden(X4,X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f187,plain,
! [X2,X0,X1,X4] :
( k3_xboole_0(X0,X1) != X2
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X2) ),
inference(cnf_transformation,[],[f135]) ).
fof(f194,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f197,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f203,plain,
! [X0] : m1_subset_1(sK10(X0),X0),
inference(cnf_transformation,[],[f139]) ).
fof(f207,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f88]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ r3_orders_2(X0,X1,X2)
| r1_orders_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f149]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| r3_orders_2(X0,X1,X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f238,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| v3_struct_0(X1)
| ~ r2_hidden(X2,u1_struct_0(X0))
| m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1))) ),
inference(cnf_transformation,[],[f106]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ r2_hidden(X2,k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))
| m1_subset_1(X2,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f108]) ).
fof(f240,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ~ r1_orders_2(X0,X2,X3)
| r1_orders_2(X1,X4,X5) ),
inference(cnf_transformation,[],[f150]) ).
fof(f241,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ~ r1_orders_2(X1,X4,X5)
| r1_orders_2(X0,X2,X3) ),
inference(cnf_transformation,[],[f150]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v12_waybel_0(X1,X0)
| ~ v1_waybel_0(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r2_hidden(X3,X1)
| ~ r2_hidden(X2,X1)
| r2_hidden(k13_lattice3(X0,X2,X3),X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f243,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ l1_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ m1_subset_1(X3,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ r2_hidden(X2,u1_struct_0(X1))
| ~ r1_orders_2(k1_latsum_1(X0,X1),X2,X3)
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
| r2_hidden(X3,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f244,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f245,plain,
! [X2,X3,X0,X1,X5] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| k13_lattice3(X0,X1,X2) != X3
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X5)
| ~ r1_orders_2(X0,X1,X5)
| r1_orders_2(X0,X3,X5) ),
inference(cnf_transformation,[],[f154]) ).
fof(f246,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| k13_lattice3(X0,X1,X2) != X3
| r1_orders_2(X0,X2,X3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f247,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| k13_lattice3(X0,X1,X2) != X3
| r1_orders_2(X0,X1,X3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f249,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| r1_orders_2(X0,X2,sK19(X0,X1,X2,X3))
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| k13_lattice3(X0,X1,X2) = X3 ),
inference(cnf_transformation,[],[f154]) ).
fof(f250,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| r1_orders_2(X0,X1,sK19(X0,X1,X2,X3))
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| k13_lattice3(X0,X1,X2) = X3 ),
inference(cnf_transformation,[],[f154]) ).
fof(f251,plain,
! [X2,X3,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ r1_orders_2(X0,X3,sK19(X0,X1,X2,X3))
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| k13_lattice3(X0,X1,X2) = X3 ),
inference(cnf_transformation,[],[f154]) ).
fof(f253,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f255,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f122]) ).
fof(f258,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f260,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| X2 != X4
| ~ r1_orders_2(X0,X2,X3)
| r1_orders_2(k1_latsum_1(X0,X1),X4,X5) ),
inference(cnf_transformation,[],[f155]) ).
fof(f263,plain,
k13_lattice3(sK1,sK4,sK5) != k13_lattice3(sK0,sK4,sK5),
inference(definition_unfolding,[],[f180,f173,f172]) ).
fof(f264,plain,
m1_subset_1(sK5,u1_struct_0(sK0)),
inference(definition_unfolding,[],[f169,f172]) ).
fof(f265,plain,
m1_subset_1(sK4,u1_struct_0(sK0)),
inference(definition_unfolding,[],[f168,f173]) ).
fof(f266,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,k3_xboole_0(X0,X1)) ),
inference(equality_resolution,[],[f187]) ).
fof(f267,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,k3_xboole_0(X0,X1))
| r2_hidden(X4,X0) ),
inference(equality_resolution,[],[f186]) ).
fof(f269,plain,
! [X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| ~ r1_orders_2(X1,X4,X5)
| r1_orders_2(X0,X4,X3) ),
inference(equality_resolution,[],[f241]) ).
fof(f270,plain,
! [X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| ~ r1_orders_2(X1,X4,X5)
| r1_orders_2(X0,X4,X5) ),
inference(equality_resolution,[],[f269]) ).
fof(f271,plain,
! [X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| ~ r1_orders_2(X0,X4,X3)
| r1_orders_2(X1,X4,X5) ),
inference(equality_resolution,[],[f240]) ).
fof(f272,plain,
! [X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| ~ r1_orders_2(X0,X4,X5)
| r1_orders_2(X1,X4,X5) ),
inference(equality_resolution,[],[f271]) ).
fof(f273,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| r1_orders_2(X0,X1,k13_lattice3(X0,X1,X2)) ),
inference(equality_resolution,[],[f247]) ).
fof(f274,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| r1_orders_2(X0,X2,k13_lattice3(X0,X1,X2)) ),
inference(equality_resolution,[],[f246]) ).
fof(f275,plain,
! [X2,X0,X1,X5] :
( ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X5)
| ~ r1_orders_2(X0,X1,X5)
| r1_orders_2(X0,k13_lattice3(X0,X1,X2),X5) ),
inference(equality_resolution,[],[f245]) ).
fof(f278,plain,
! [X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| X3 != X5
| ~ r1_orders_2(X0,X4,X3)
| r1_orders_2(k1_latsum_1(X0,X1),X4,X5) ),
inference(equality_resolution,[],[f260]) ).
fof(f279,plain,
! [X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ m1_subset_1(X5,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X1)
| ~ r1_orders_2(X0,X4,X5)
| r1_orders_2(k1_latsum_1(X0,X1),X4,X5) ),
inference(equality_resolution,[],[f278]) ).
tcf(c_49,negated_conjecture,
k13_lattice3(sK1,sK4,sK5) != k13_lattice3(sK0,sK4,sK5),
inference(cnf_transformation,[],[f263]) ).
tcf(c_50,negated_conjecture,
v1_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK1),
inference(cnf_transformation,[],[f179]) ).
tcf(c_51,negated_conjecture,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK1),
inference(cnf_transformation,[],[f178]) ).
tcf(c_52,negated_conjecture,
m1_subset_1(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(cnf_transformation,[],[f177]) ).
tcf(c_53,negated_conjecture,
v13_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),sK0),
inference(cnf_transformation,[],[f176]) ).
tcf(c_54,negated_conjecture,
m1_subset_1(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(sK1)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(cnf_transformation,[],[f175]) ).
tcf(c_55,negated_conjecture,
r1_latsum_1(sK0,sK1),
inference(cnf_transformation,[],[f174]) ).
tcf(c_56,negated_conjecture,
m1_subset_1(sK5,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f171]) ).
tcf(c_57,negated_conjecture,
m1_subset_1(sK4,u1_struct_0(sK1)),
inference(cnf_transformation,[],[f170]) ).
tcf(c_58,negated_conjecture,
m1_subset_1(sK5,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f264]) ).
tcf(c_59,negated_conjecture,
m1_subset_1(sK4,u1_struct_0(sK0)),
inference(cnf_transformation,[],[f265]) ).
tcf(c_60,negated_conjecture,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f167]) ).
tcf(c_61,negated_conjecture,
v2_orders_2(sK1),
inference(cnf_transformation,[],[f166]) ).
tcf(c_62,negated_conjecture,
v3_orders_2(sK1),
inference(cnf_transformation,[],[f165]) ).
tcf(c_63,negated_conjecture,
v4_orders_2(sK1),
inference(cnf_transformation,[],[f164]) ).
tcf(c_64,negated_conjecture,
v1_lattice3(sK1),
inference(cnf_transformation,[],[f163]) ).
tcf(c_65,negated_conjecture,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f162]) ).
tcf(c_66,negated_conjecture,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f161]) ).
tcf(c_67,negated_conjecture,
v2_orders_2(sK0),
inference(cnf_transformation,[],[f160]) ).
tcf(c_68,negated_conjecture,
v3_orders_2(sK0),
inference(cnf_transformation,[],[f159]) ).
tcf(c_69,negated_conjecture,
v4_orders_2(sK0),
inference(cnf_transformation,[],[f158]) ).
tcf(c_70,negated_conjecture,
v1_lattice3(sK0),
inference(cnf_transformation,[],[f157]) ).
tcf(c_71,negated_conjecture,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f156]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k13_lattice3(X1,X0,X2) = k13_lattice3(X1,X2,X0) )
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f184]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(X0,k3_xboole_0(X1,X2))
| ~ r2_hidden(X0,X2)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(X0,X1)
| ~ r2_hidden(X0,k3_xboole_0(X1,X2)) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k13_lattice3(X1,X0,X2),u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_88,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_94,plain,
! [X0: $i] : m1_subset_1(sK10(X0),X0),
inference(cnf_transformation,[],[f203]) ).
tcf(c_98,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_orders_2(X0,X1,X2)
| ~ l1_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r3_orders_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| r3_orders_2(X1,X0,X0)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| m1_subset_1(X0,u1_struct_0(k1_latsum_1(X1,X2)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(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)
| ~ r2_hidden(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| m1_subset_1(X0,u1_struct_0(X2))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(X1),u1_struct_0(X2))) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X3)
| v3_struct_0(X0)
| r1_orders_2(X3,X1,X2)
| ~ l1_orders_2(X3)
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X3)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X3))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X3)
| v3_struct_0(X0)
| r1_orders_2(X3,X1,X2)
| ~ l1_orders_2(X3)
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X3)
| ~ v3_orders_2(X0)
| ~ r1_latsum_1(X0,X3)
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X3))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| r2_hidden(k13_lattice3(X1,X2,X3),X0)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X2,X0)
| ~ v12_waybel_0(X0,X1)
| ~ v1_waybel_0(X0,X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r2_hidden(X3,u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ r2_hidden(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(X0,X1)))
| ~ r1_orders_2(k1_latsum_1(X0,X1),X2,X3)
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),X0)
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k13_lattice3(X0,X2,X3) = X1 )
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X3,X1)
| ~ r1_orders_2(X0,X2,X1)
| ~ r1_orders_2(X0,X1,sK19(X0,X2,X3,X1)) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_orders_2(X0,X1,sK19(X0,X1,X3,X2))
| ( k13_lattice3(X0,X1,X3) = X2 )
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X3,X2)
| ~ r1_orders_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_orders_2(X0,X3,sK19(X0,X1,X3,X2))
| ( k13_lattice3(X0,X1,X3) = X2 )
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X3,X2)
| ~ r1_orders_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_orders_2(X0,X1,k13_lattice3(X0,X1,X2))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_orders_2(X0,X2,k13_lattice3(X0,X1,X2))
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X2),X3)
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X3)
| ~ r1_orders_2(X0,X1,X3)
| ~ m1_subset_1(k13_lattice3(X0,X1,X2),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X2,X1)
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| r1_orders_2(k1_latsum_1(X1,X2),X0,X3)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ r1_latsum_1(X1,X2)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ r1_orders_2(X1,X0,X3)
| ~ m1_subset_1(X3,u1_struct_0(k1_latsum_1(X1,X2)))
| ~ m1_subset_1(X0,u1_struct_0(k1_latsum_1(X1,X2))) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_219,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(prop_impl_just,[status(thm)],[c_88]) ).
tcf(c_673,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| r2_hidden(k13_lattice3(X1,X3,X2),X0)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X2,X0)
| ~ v12_waybel_0(X0,X1)
| ~ v1_waybel_0(X0,X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_133,c_146]) ).
tcf(c_824,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_orders_2(X1,X2,k13_lattice3(X1,X0,X2))
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_141,c_85]) ).
tcf(c_825,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_orders_2(X1,X0,k13_lattice3(X1,X0,X2))
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_140,c_85]) ).
tcf(c_826,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_orders_2(X0,k13_lattice3(X0,X1,X3),X2)
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X3,X2)
| ~ r1_orders_2(X0,X1,X2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_142,c_85]) ).
tcf(c_1156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| r2_hidden(k13_lattice3(X1,X3,X2),X0)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X2,X0)
| ~ v12_waybel_0(X0,X1)
| ~ v1_waybel_0(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_673,c_146]) ).
tcf(c_1247,plain,
v1_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK1),
inference(demodulation,[status(thm)],[c_50,c_75]) ).
tcf(c_1248,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK1),
inference(demodulation,[status(thm)],[c_51,c_75]) ).
tcf(c_1249,plain,
v13_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK0),
inference(demodulation,[status(thm)],[c_53,c_75]) ).
tcf(c_1318,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(demodulation,[status(thm)],[c_54,c_75]) ).
tcf(c_1319,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK1))),
inference(demodulation,[status(thm)],[c_52,c_75]) ).
tcf(c_2019,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ l1_orders_2(X0)
| ~ v1_xboole_0(u1_struct_0(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_219,c_98]) ).
tcf(c_2020,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(unflattening,[status(thm)],[c_2019]) ).
tcf(c_2127,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| r2_hidden(k13_lattice3(X1,X3,X2),X0)
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ r2_hidden(X3,X0)
| ~ r2_hidden(X2,X0)
| ~ v12_waybel_0(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ( X1 != sK1 )
| ( k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_1156,c_1247]) ).
tcf(c_2128,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| r2_hidden(k13_lattice3(sK1,X1,X0),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),sK1)
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ m1_subset_1(k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)),k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(unflattening,[status(thm)],[c_2127]) ).
tcf(c_2130,plain,
! [X0: $i,X1: $i] :
( ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| r2_hidden(k13_lattice3(sK1,X1,X0),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))) ),
inference(global_subsumption_just,[status(thm)],[c_2128,c_65,c_64,c_63,c_62,c_61,c_60,c_1248,c_1319,c_2128]) ).
tcf(c_2131,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k13_lattice3(sK1,X1,X0),k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(X1,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0)))
| ~ r2_hidden(X0,k3_xboole_0(u1_struct_0(sK1),u1_struct_0(sK0))) ),
inference(renaming,[status(thm)],[c_2130]) ).
tcf(c_2429,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r1_orders_2(X1,X2,X3)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X3)
| ( X1 != sK0 )
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_131]) ).
tcf(c_2430,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(sK1)
| r1_orders_2(sK0,X0,X1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v3_orders_2(sK0)
| ~ v3_orders_2(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ r1_orders_2(sK1,X0,X1) ),
inference(unflattening,[status(thm)],[c_2429]) ).
tcf(c_2432,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ r1_orders_2(sK1,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2430,c_71,c_68,c_65,c_62,c_66,c_60,c_2430]) ).
tcf(c_2453,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r1_orders_2(X0,X2,X3)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ v3_orders_2(X0)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r1_orders_2(X1,X2,X3)
| ( X1 != sK0 )
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_132]) ).
tcf(c_2454,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(sK1)
| r1_orders_2(sK1,X0,X1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v3_orders_2(sK0)
| ~ v3_orders_2(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ r1_orders_2(sK0,X0,X1) ),
inference(unflattening,[status(thm)],[c_2453]) ).
tcf(c_2456,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ r1_orders_2(sK0,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2454,c_71,c_68,c_65,c_62,c_66,c_60,c_2454]) ).
tcf(c_2477,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r1_orders_2(k1_latsum_1(X1,X0),X2,X3)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v3_orders_2(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r1_orders_2(X1,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(k1_latsum_1(X1,X0)))
| ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(X1,X0)))
| ( X1 != sK0 )
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_152]) ).
tcf(c_2478,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(sK1)
| r1_orders_2(k1_latsum_1(sK0,sK1),X0,X1)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v3_orders_2(sK0)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ r1_orders_2(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,sK1)))
| ~ m1_subset_1(X0,u1_struct_0(k1_latsum_1(sK0,sK1))) ),
inference(unflattening,[status(thm)],[c_2477]) ).
tcf(c_2480,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(k1_latsum_1(sK0,sK1),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k1_latsum_1(sK0,sK1)))
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,sK1)))
| ~ r1_orders_2(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(global_subsumption_just,[status(thm)],[c_2478,c_71,c_68,c_65,c_66,c_60,c_2478]) ).
tcf(c_2481,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(k1_latsum_1(sK0,sK1),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ r1_orders_2(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,sK1)))
| ~ m1_subset_1(X0,u1_struct_0(k1_latsum_1(sK0,sK1))) ),
inference(renaming,[status(thm)],[c_2480]) ).
tcf(c_4034,definition,
iPr_def_10 = k1_latsum_1(sK0,sK1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_4035,definition,
iPr_def_11 = u1_struct_0(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_4036,definition,
iPr_def_12 = u1_struct_0(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_4037,definition,
iPr_def_13 = u1_struct_0(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_4038,definition,
iPr_def_14 = k3_xboole_0(iPr_def_13,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_4040,definition,
iPr_def_16 = k1_zfmisc_1(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_4041,definition,
iPr_def_17 = k13_lattice3(sK1,sK4,sK5),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_4042,definition,
iPr_def_18 = k13_lattice3(sK0,sK4,sK5),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_4043,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(iPr_def_10,X0,X1)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X1,iPr_def_11)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_11)
| ~ r1_orders_2(sK0,X0,X1) ),
inference(demodulation,[status(thm)],[c_2481,c_4036,c_4034,c_4035]) ).
tcf(c_4044,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK1,X0,X1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r1_orders_2(sK0,X0,X1) ),
inference(demodulation,[status(thm)],[c_2456,c_4037]) ).
tcf(c_4045,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,X1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r1_orders_2(sK1,X0,X1) ),
inference(demodulation,[status(thm)],[c_2432]) ).
tcf(c_4047,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k13_lattice3(sK1,X1,X0),iPr_def_14)
| ~ r2_hidden(X1,iPr_def_14)
| ~ r2_hidden(X0,iPr_def_14) ),
inference(demodulation,[status(thm)],[c_2131,c_4038]) ).
tcf(c_4049,plain,
m1_subset_1(iPr_def_14,iPr_def_16),
inference(demodulation,[status(thm)],[c_1318,c_4040]) ).
tcf(c_4050,plain,
v13_waybel_0(iPr_def_14,sK0),
inference(demodulation,[status(thm)],[c_1249]) ).
tcf(c_4051,negated_conjecture,
l1_orders_2(sK0),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_4052,negated_conjecture,
v1_lattice3(sK0),
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_4053,negated_conjecture,
v4_orders_2(sK0),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_4054,negated_conjecture,
v3_orders_2(sK0),
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_4055,negated_conjecture,
v2_orders_2(sK0),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_4056,negated_conjecture,
~ v3_struct_0(sK0),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_4057,negated_conjecture,
l1_orders_2(sK1),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_4058,negated_conjecture,
v1_lattice3(sK1),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_4059,negated_conjecture,
v4_orders_2(sK1),
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_4060,negated_conjecture,
v3_orders_2(sK1),
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_4061,negated_conjecture,
v2_orders_2(sK1),
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_4062,negated_conjecture,
~ v3_struct_0(sK1),
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_4063,negated_conjecture,
m1_subset_1(sK4,iPr_def_12),
inference(demodulation,[status(thm)],[c_59]) ).
tcf(c_4064,negated_conjecture,
m1_subset_1(sK5,iPr_def_12),
inference(demodulation,[status(thm)],[c_58]) ).
tcf(c_4065,negated_conjecture,
m1_subset_1(sK4,iPr_def_13),
inference(demodulation,[status(thm)],[c_57]) ).
tcf(c_4066,negated_conjecture,
m1_subset_1(sK5,iPr_def_13),
inference(demodulation,[status(thm)],[c_56]) ).
tcf(c_4067,negated_conjecture,
iPr_def_17 != iPr_def_18,
inference(demodulation,[status(thm)],[c_49,c_4042,c_4041]) ).
tcf(c_5787,plain,
k3_xboole_0(iPr_def_12,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_4038,c_75]) ).
tcf(c_5867,plain,
! [X0: $i] :
( r2_hidden(X0,iPr_def_12)
| ~ r2_hidden(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_5787,c_80]) ).
tcf(c_5900,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k13_lattice3(sK1,X1,X0),iPr_def_12)
| ~ r2_hidden(X1,iPr_def_14)
| ~ r2_hidden(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_4047,c_5867]) ).
tcf(c_5923,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k13_lattice3(sK1,X1,X0),iPr_def_12)
| ~ r2_hidden(X1,iPr_def_14)
| ~ r2_hidden(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_5900,c_135]) ).
tcf(c_6075,plain,
( m1_subset_1(iPr_def_17,iPr_def_12)
| ~ r2_hidden(sK5,iPr_def_14)
| ~ r2_hidden(sK4,iPr_def_14) ),
inference(superposition,[status(thm)],[c_4041,c_5923]) ).
tcf(c_6119,plain,
( v1_xboole_0(iPr_def_12)
| r2_hidden(sK4,iPr_def_12) ),
inference(superposition,[status(thm)],[c_4063,c_144]) ).
tcf(c_6120,plain,
( v1_xboole_0(iPr_def_12)
| r2_hidden(sK5,iPr_def_12) ),
inference(superposition,[status(thm)],[c_4064,c_144]) ).
tcf(c_6121,plain,
( v1_xboole_0(iPr_def_13)
| r2_hidden(sK4,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4065,c_144]) ).
tcf(c_6122,plain,
( v1_xboole_0(iPr_def_13)
| r2_hidden(sK5,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4066,c_144]) ).
tcf(c_6548,plain,
! [X0: $i] :
( r2_hidden(X0,iPr_def_14)
| ~ r2_hidden(X0,iPr_def_13)
| ~ r2_hidden(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_5787,c_79]) ).
tcf(c_7705,plain,
( m1_subset_1(iPr_def_17,u1_struct_0(sK1))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_85]) ).
tcf(c_7706,plain,
( m1_subset_1(iPr_def_18,u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_85]) ).
tcf(c_7708,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4037,c_85]) ).
tcf(c_7712,plain,
( m1_subset_1(iPr_def_18,iPr_def_12)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_7706,c_4036]) ).
tcf(c_7713,plain,
m1_subset_1(iPr_def_18,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_7712,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_7714,plain,
( m1_subset_1(iPr_def_17,iPr_def_13)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_7705,c_4037]) ).
tcf(c_7715,plain,
m1_subset_1(iPr_def_17,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_7714,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_7723,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_7708,c_4037]) ).
tcf(c_7724,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7723,c_4057,c_4058,c_4059]) ).
tcf(c_7770,plain,
( r1_orders_2(sK1,sK5,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_824]) ).
tcf(c_7771,plain,
( r1_orders_2(sK0,sK5,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_824]) ).
tcf(c_7774,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X1,k13_lattice3(sK1,X0,X1))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_824,c_4045]) ).
tcf(c_7776,plain,
( r1_orders_2(sK0,sK5,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_7771,c_4036]) ).
tcf(c_7777,plain,
r1_orders_2(sK0,sK5,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_7776,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_7778,plain,
( r1_orders_2(sK1,sK5,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_7770,c_4037]) ).
tcf(c_7779,plain,
r1_orders_2(sK1,sK5,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_7778,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_7790,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X1,k13_lattice3(sK1,X0,X1))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_7774,c_4037]) ).
tcf(c_7791,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X1,k13_lattice3(sK1,X0,X1))
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7790,c_4057,c_4058,c_4059]) ).
tcf(c_7838,plain,
( r1_orders_2(sK1,sK4,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_825]) ).
tcf(c_7839,plain,
( r1_orders_2(sK0,sK4,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_825]) ).
tcf(c_7842,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,k13_lattice3(sK1,X0,X1))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_825,c_4045]) ).
tcf(c_7844,plain,
( r1_orders_2(sK0,sK4,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_7839,c_4036]) ).
tcf(c_7845,plain,
r1_orders_2(sK0,sK4,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_7844,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_7846,plain,
( r1_orders_2(sK1,sK4,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_7838,c_4037]) ).
tcf(c_7847,plain,
r1_orders_2(sK1,sK4,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_7846,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_7858,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,k13_lattice3(sK1,X0,X1))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_7842,c_4037]) ).
tcf(c_7859,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,k13_lattice3(sK1,X0,X1))
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7858,c_4057,c_4058,c_4059]) ).
tcf(c_7905,plain,
( v1_xboole_0(iPr_def_12)
| r2_hidden(iPr_def_18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7713,c_144]) ).
tcf(c_7908,plain,
( v1_xboole_0(iPr_def_13)
| r2_hidden(iPr_def_17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_7715,c_144]) ).
tcf(c_7911,plain,
( r1_orders_2(sK1,sK5,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK5,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7777,c_4044]) ).
tcf(c_7917,plain,
( r1_orders_2(sK1,sK5,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7911,c_7713,c_4066,c_4064]) ).
tcf(c_7924,plain,
( r1_orders_2(sK1,sK4,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7845,c_4044]) ).
tcf(c_7925,plain,
( r1_orders_2(iPr_def_10,sK4,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(iPr_def_18,iPr_def_11)
| ~ m1_subset_1(sK4,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_11) ),
inference(superposition,[status(thm)],[c_7845,c_4043]) ).
tcf(c_7926,plain,
( r1_orders_2(iPr_def_10,sK4,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_11)
| ~ m1_subset_1(sK4,iPr_def_11) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7925,c_7713,c_4063]) ).
tcf(c_7930,plain,
( r1_orders_2(sK1,sK4,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7924,c_7713,c_4065,c_4063]) ).
tcf(c_7933,plain,
( r1_orders_2(sK0,sK4,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_13)
| ~ m1_subset_1(iPr_def_17,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(superposition,[status(thm)],[c_7847,c_4045]) ).
tcf(c_7934,plain,
( r1_orders_2(sK0,sK4,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7933,c_7715,c_4065,c_4063]) ).
tcf(c_8192,plain,
! [X0: $i,X1: $i] :
( ( k13_lattice3(sK1,X0,X1) = k13_lattice3(sK1,X1,X0) )
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4037,c_74]) ).
tcf(c_8201,plain,
! [X0: $i,X1: $i] :
( ( k13_lattice3(sK1,X0,X1) = k13_lattice3(sK1,X1,X0) )
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_8192,c_4037]) ).
tcf(c_8202,plain,
! [X0: $i,X1: $i] :
( ( k13_lattice3(sK1,X0,X1) = k13_lattice3(sK1,X1,X0) )
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8201,c_4057,c_4058,c_4059]) ).
tcf(c_8817,plain,
! [X0: $i] :
( r1_orders_2(sK1,iPr_def_17,X0)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| ~ r1_orders_2(sK1,sK5,X0)
| ~ r1_orders_2(sK1,sK4,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_826]) ).
tcf(c_8818,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,X0)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| ~ r1_orders_2(sK0,sK5,X0)
| ~ r1_orders_2(sK0,sK4,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_826]) ).
tcf(c_8823,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,X0)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r1_orders_2(sK0,sK5,X0)
| ~ r1_orders_2(sK0,sK4,X0) ),
inference(light_normalisation,[status(thm)],[c_8818,c_4036]) ).
tcf(c_8824,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,X0)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r1_orders_2(sK0,sK5,X0)
| ~ r1_orders_2(sK0,sK4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8823,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_8829,plain,
! [X0: $i] :
( r1_orders_2(sK1,iPr_def_17,X0)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ r1_orders_2(sK1,sK5,X0)
| ~ r1_orders_2(sK1,sK4,X0) ),
inference(light_normalisation,[status(thm)],[c_8817,c_4037]) ).
tcf(c_8830,plain,
! [X0: $i] :
( r1_orders_2(sK1,iPr_def_17,X0)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ r1_orders_2(sK1,sK5,X0)
| ~ r1_orders_2(sK1,sK4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8829,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_8946,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_struct_0(sK1)
| m1_subset_1(X0,u1_struct_0(iPr_def_10))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK0)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK0)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK0)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ r2_hidden(X0,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4034,c_129]) ).
tcf(c_8954,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_struct_0(sK1)
| m1_subset_1(X0,iPr_def_11)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK0)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK0)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK0)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK0)
| ~ v2_orders_2(sK1)
| ~ r2_hidden(X0,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_8946,c_4035,c_4036]) ).
tcf(c_8955,plain,
! [X0: $i] :
( m1_subset_1(X0,iPr_def_11)
| ~ r2_hidden(X0,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8954,c_4056,c_4062,c_4051,c_4057,c_4052,c_4058,c_4053,c_4059,c_4054,c_4060,c_4055,c_4061]) ).
tcf(c_9200,plain,
( v1_xboole_0(iPr_def_12)
| m1_subset_1(sK4,iPr_def_11) ),
inference(superposition,[status(thm)],[c_6119,c_8955]) ).
tcf(c_9203,plain,
( v1_xboole_0(iPr_def_12)
| m1_subset_1(iPr_def_18,iPr_def_11) ),
inference(superposition,[status(thm)],[c_7905,c_8955]) ).
tcf(c_10342,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(X2,u1_struct_0(X0))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(X0)
| ~ r2_hidden(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(sK0,X0)))
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,X0)))
| ~ r1_orders_2(k1_latsum_1(sK0,X0),X1,X2)
| ~ v13_waybel_0(k3_xboole_0(u1_struct_0(sK0),u1_struct_0(X0)),sK0)
| ~ m1_subset_1(k3_xboole_0(iPr_def_12,u1_struct_0(X0)),k1_zfmisc_1(iPr_def_12)) ),
inference(superposition,[status(thm)],[c_4036,c_134]) ).
tcf(c_10373,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(X2,u1_struct_0(X0))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(X0)
| ~ r2_hidden(X1,u1_struct_0(X0))
| ~ v13_waybel_0(k3_xboole_0(iPr_def_12,u1_struct_0(X0)),sK0)
| ~ m1_subset_1(k3_xboole_0(iPr_def_12,u1_struct_0(X0)),iPr_def_16)
| ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(sK0,X0)))
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,X0)))
| ~ r1_orders_2(k1_latsum_1(sK0,X0),X1,X2) ),
inference(light_normalisation,[status(thm)],[c_10342,c_4036,c_4040]) ).
tcf(c_10374,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(X2,u1_struct_0(X0))
| ~ l1_orders_2(X0)
| ~ r2_hidden(X1,u1_struct_0(X0))
| ~ v13_waybel_0(k3_xboole_0(iPr_def_12,u1_struct_0(X0)),sK0)
| ~ m1_subset_1(k3_xboole_0(iPr_def_12,u1_struct_0(X0)),iPr_def_16)
| ~ m1_subset_1(X2,u1_struct_0(k1_latsum_1(sK0,X0)))
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,X0)))
| ~ r1_orders_2(k1_latsum_1(sK0,X0),X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10373,c_4051]) ).
tcf(c_10598,plain,
! [X0: $i] :
( ( k13_lattice3(sK1,X0,sK4) = k13_lattice3(sK1,sK4,X0) )
| ~ m1_subset_1(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4065,c_8202]) ).
tcf(c_10722,plain,
k13_lattice3(sK1,sK4,sK5) = k13_lattice3(sK1,sK5,sK4),
inference(superposition,[status(thm)],[c_4066,c_10598]) ).
tcf(c_10728,plain,
k13_lattice3(sK1,sK5,sK4) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_10722,c_4041]) ).
tcf(c_11901,plain,
( r1_orders_2(sK1,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_13)
| ~ r1_orders_2(sK1,sK5,iPr_def_17) ),
inference(superposition,[status(thm)],[c_7847,c_8830]) ).
tcf(c_11906,plain,
r1_orders_2(sK1,iPr_def_17,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_11901,c_7715,c_7779]) ).
tcf(c_12133,plain,
( r1_orders_2(sK0,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_13)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_11906,c_4045]) ).
tcf(c_12134,plain,
( r1_orders_2(sK0,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12133,c_7715]) ).
tcf(c_13394,plain,
( ~ v1_xboole_0(iPr_def_12)
| ~ r2_hidden(sK4,iPr_def_12) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_13523,plain,
( ~ v1_xboole_0(iPr_def_13)
| ~ r2_hidden(sK4,iPr_def_13) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_13639,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X1,k13_lattice3(sK1,X0,X1))
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7791,c_7724,c_7791]) ).
tcf(c_13657,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,k13_lattice3(sK1,X0,sK4))
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,sK4),iPr_def_12)
| ~ r1_orders_2(sK0,sK5,k13_lattice3(sK1,X0,sK4)) ),
inference(superposition,[status(thm)],[c_13639,c_8824]) ).
tcf(c_13673,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,k13_lattice3(sK1,X0,sK4))
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,X0,sK4),iPr_def_12)
| ~ r1_orders_2(sK0,sK5,k13_lattice3(sK1,X0,sK4)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13657,c_4065,c_4063]) ).
tcf(c_13832,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,k13_lattice3(sK1,X0,X1))
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(k13_lattice3(sK1,X0,X1),iPr_def_12) ),
inference(global_subsumption_just,[status(thm)],[c_7859,c_7724,c_7859]) ).
tcf(c_13850,plain,
( r1_orders_2(sK0,iPr_def_18,k13_lattice3(sK1,sK5,sK4))
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(k13_lattice3(sK1,sK5,sK4),iPr_def_12) ),
inference(superposition,[status(thm)],[c_13832,c_13673]) ).
tcf(c_13855,plain,
( r1_orders_2(sK0,iPr_def_18,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_13850,c_10728]) ).
tcf(c_13856,plain,
( r1_orders_2(sK0,iPr_def_18,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13855,c_4066,c_4064,c_4065]) ).
tcf(c_14567,plain,
( v3_struct_0(sK0)
| ~ v1_xboole_0(iPr_def_12)
| ~ l1_orders_2(sK0) ),
inference(superposition,[status(thm)],[c_4036,c_2020]) ).
tcf(c_14568,plain,
( v3_struct_0(sK1)
| ~ v1_xboole_0(iPr_def_13)
| ~ l1_orders_2(sK1) ),
inference(superposition,[status(thm)],[c_4037,c_2020]) ).
tcf(c_14570,plain,
~ v1_xboole_0(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_14568,c_4062,c_4057]) ).
tcf(c_14571,plain,
~ v1_xboole_0(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_14567,c_4056,c_4051]) ).
tcf(c_14578,plain,
r2_hidden(sK5,iPr_def_13),
inference(backward_subsumption_resolution,[status(thm)],[c_6122,c_14570]) ).
tcf(c_14579,plain,
r2_hidden(sK4,iPr_def_13),
inference(backward_subsumption_resolution,[status(thm)],[c_6121,c_14570]) ).
tcf(c_14590,plain,
m1_subset_1(iPr_def_18,iPr_def_11),
inference(backward_subsumption_resolution,[status(thm)],[c_9203,c_14571]) ).
tcf(c_14592,plain,
m1_subset_1(sK4,iPr_def_11),
inference(backward_subsumption_resolution,[status(thm)],[c_9200,c_14571]) ).
tcf(c_14595,plain,
r2_hidden(iPr_def_18,iPr_def_12),
inference(backward_subsumption_resolution,[status(thm)],[c_7905,c_14571]) ).
tcf(c_14598,plain,
r2_hidden(sK5,iPr_def_12),
inference(backward_subsumption_resolution,[status(thm)],[c_6120,c_14571]) ).
tcf(c_14599,plain,
r2_hidden(sK4,iPr_def_12),
inference(backward_subsumption_resolution,[status(thm)],[c_6119,c_14571]) ).
tcf(c_14601,plain,
( r1_orders_2(iPr_def_10,sK4,iPr_def_18)
| ~ m1_subset_1(sK4,iPr_def_11) ),
inference(backward_subsumption_resolution,[status(thm)],[c_7926,c_14590]) ).
tcf(c_14612,plain,
r1_orders_2(iPr_def_10,sK4,iPr_def_18),
inference(backward_subsumption_resolution,[status(thm)],[c_14601,c_14592]) ).
tcf(c_28270,plain,
! [X0: $i,X1: $i] :
( r2_hidden(X1,u1_struct_0(sK1))
| ~ l1_orders_2(sK1)
| ~ r2_hidden(X0,u1_struct_0(sK1))
| ~ r1_orders_2(iPr_def_10,X0,X1)
| ~ v13_waybel_0(k3_xboole_0(iPr_def_12,u1_struct_0(sK1)),sK0)
| ~ m1_subset_1(k3_xboole_0(iPr_def_12,u1_struct_0(sK1)),iPr_def_16)
| ~ m1_subset_1(X1,u1_struct_0(k1_latsum_1(sK0,sK1)))
| ~ m1_subset_1(X0,u1_struct_0(k1_latsum_1(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_4034,c_10374]) ).
tcf(c_28271,plain,
! [X0: $i,X1: $i] :
( r2_hidden(X1,iPr_def_13)
| ~ l1_orders_2(sK1)
| ~ v13_waybel_0(iPr_def_14,sK0)
| ~ m1_subset_1(iPr_def_14,iPr_def_16)
| ~ r2_hidden(X0,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_11)
| ~ m1_subset_1(X0,iPr_def_11)
| ~ r1_orders_2(iPr_def_10,X0,X1) ),
inference(light_normalisation,[status(thm)],[c_28270,c_4034,c_4035,c_4037,c_5787]) ).
tcf(c_28272,plain,
! [X0: $i,X1: $i] :
( r2_hidden(X1,iPr_def_13)
| ~ r2_hidden(X0,iPr_def_13)
| ~ m1_subset_1(X1,iPr_def_11)
| ~ m1_subset_1(X0,iPr_def_11)
| ~ r1_orders_2(iPr_def_10,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_28271,c_4057,c_4050,c_4049]) ).
tcf(c_28405,plain,
( r2_hidden(iPr_def_18,iPr_def_13)
| ~ r2_hidden(sK4,iPr_def_13)
| ~ m1_subset_1(iPr_def_18,iPr_def_11)
| ~ m1_subset_1(sK4,iPr_def_11) ),
inference(superposition,[status(thm)],[c_14612,c_28272]) ).
tcf(c_28430,plain,
r2_hidden(iPr_def_18,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_28405,c_14579,c_14590,c_14592]) ).
tcf(c_28949,plain,
m1_subset_1(iPr_def_18,iPr_def_13),
inference(superposition,[status(thm)],[c_28430,c_135]) ).
tcf(c_34470,plain,
( r2_hidden(sK4,iPr_def_14)
| ~ r2_hidden(sK4,iPr_def_13) ),
inference(superposition,[status(thm)],[c_14599,c_6548]) ).
tcf(c_34471,plain,
( r2_hidden(sK5,iPr_def_14)
| ~ r2_hidden(sK5,iPr_def_13) ),
inference(superposition,[status(thm)],[c_14598,c_6548]) ).
tcf(c_34479,plain,
( r2_hidden(iPr_def_18,iPr_def_14)
| ~ r2_hidden(iPr_def_18,iPr_def_13) ),
inference(superposition,[status(thm)],[c_14595,c_6548]) ).
tcf(c_34491,plain,
r2_hidden(iPr_def_18,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_34479,c_28430]) ).
tcf(c_34492,plain,
r2_hidden(sK5,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_34471,c_14578]) ).
tcf(c_34493,plain,
r2_hidden(sK4,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_34470,c_14579]) ).
tcf(c_34554,plain,
( m1_subset_1(iPr_def_17,iPr_def_12)
| ~ r2_hidden(sK4,iPr_def_14) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6075,c_34492]) ).
tcf(c_34559,plain,
m1_subset_1(iPr_def_17,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_34554,c_34493]) ).
tcf(c_277575,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r3_orders_2(X1,X0,X0)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(resolution,[status(thm)],[c_128,c_94]) ).
tcf(c_465969,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r3_orders_2(X1,X0,X0)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_128,c_277575]) ).
tcf(c_465982,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| r3_orders_2(X1,k13_lattice3(X1,X0,X2),k13_lattice3(X1,X0,X2))
| ~ l1_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(superposition,[status(thm)],[c_85,c_465969]) ).
tcf(c_466293,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k13_lattice3(X0,X1,X2) = X1 )
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X1)
| ~ r1_orders_2(X0,X1,X1) ),
inference(superposition,[status(thm)],[c_137,c_136]) ).
tcf(c_466322,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k13_lattice3(X0,X1,X2) = X2 )
| ~ l1_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_orders_2(X0,X2,X2)
| ~ r1_orders_2(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_138,c_136]) ).
tcf(c_466445,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| r1_orders_2(sK0,X0,X1)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ r3_orders_2(sK0,X0,X1) ),
inference(superposition,[status(thm)],[c_4036,c_126]) ).
tcf(c_466451,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(X1)
| m1_subset_1(X0,u1_struct_0(X1))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(X1)
| ~ r2_hidden(X0,k3_xboole_0(iPr_def_12,u1_struct_0(X1))) ),
inference(superposition,[status(thm)],[c_4036,c_130]) ).
tcf(c_466478,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m1_subset_1(X0,u1_struct_0(X1))
| ~ l1_orders_2(X1)
| ~ r2_hidden(X0,k3_xboole_0(iPr_def_12,u1_struct_0(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_466451,c_4056,c_4051]) ).
tcf(c_466494,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| r1_orders_2(sK0,X0,X1)
| ~ l1_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r3_orders_2(sK0,X0,X1) ),
inference(light_normalisation,[status(thm)],[c_466445,c_4036]) ).
tcf(c_466495,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK0,X0,X1)
| ~ m1_subset_1(X1,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r3_orders_2(sK0,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_466494,c_4056,c_4051,c_4055]) ).
tcf(c_466860,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| r1_orders_2(sK1,X0,X1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ r3_orders_2(sK1,X0,X1) ),
inference(superposition,[status(thm)],[c_4037,c_126]) ).
tcf(c_466909,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| r1_orders_2(sK1,X0,X1)
| ~ l1_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ r3_orders_2(sK1,X0,X1) ),
inference(light_normalisation,[status(thm)],[c_466860,c_4037]) ).
tcf(c_466910,plain,
! [X0: $i,X1: $i] :
( r1_orders_2(sK1,X0,X1)
| ~ m1_subset_1(X1,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ r3_orders_2(sK1,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_466909,c_4062,c_4057,c_4061]) ).
tcf(c_467036,plain,
k3_xboole_0(iPr_def_12,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_4038,c_75]) ).
tcf(c_467039,plain,
! [X0: $i] :
( r2_hidden(X0,iPr_def_14)
| ~ r2_hidden(X0,iPr_def_13)
| ~ r2_hidden(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_467036,c_79]) ).
tcf(c_467067,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,iPr_def_12)
| ~ m1_subset_1(X1,iPr_def_16)
| ~ r2_hidden(X0,X1) ),
inference(superposition,[status(thm)],[c_4040,c_146]) ).
tcf(c_467077,plain,
( r1_orders_2(sK1,sK4,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_825]) ).
tcf(c_467079,plain,
( m1_subset_1(iPr_def_17,u1_struct_0(sK1))
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_85]) ).
tcf(c_467080,plain,
! [X0: $i] :
( r1_orders_2(sK1,iPr_def_17,X0)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1))
| ~ r1_orders_2(sK1,sK5,X0)
| ~ r1_orders_2(sK1,sK4,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_826]) ).
tcf(c_467082,plain,
( m1_subset_1(iPr_def_17,iPr_def_13)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_467079,c_4037]) ).
tcf(c_467083,plain,
m1_subset_1(iPr_def_17,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_467082,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_467086,plain,
( r1_orders_2(sK1,sK4,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_467077,c_4037]) ).
tcf(c_467087,plain,
r1_orders_2(sK1,sK4,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_467086,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_467088,plain,
! [X0: $i] :
( r1_orders_2(sK1,iPr_def_17,X0)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ r1_orders_2(sK1,sK5,X0)
| ~ r1_orders_2(sK1,sK4,X0) ),
inference(light_normalisation,[status(thm)],[c_467080,c_4037]) ).
tcf(c_467089,plain,
! [X0: $i] :
( r1_orders_2(sK1,iPr_def_17,X0)
| ~ m1_subset_1(X0,iPr_def_13)
| ~ r1_orders_2(sK1,sK5,X0)
| ~ r1_orders_2(sK1,sK4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_467088,c_4057,c_4058,c_4059,c_4066,c_4065]) ).
tcf(c_467107,plain,
( r1_orders_2(sK0,sK4,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_825]) ).
tcf(c_467108,plain,
( r1_orders_2(sK0,sK5,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_824]) ).
tcf(c_467109,plain,
( m1_subset_1(iPr_def_18,u1_struct_0(sK0))
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_85]) ).
tcf(c_467110,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,X0)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0))
| ~ r1_orders_2(sK0,sK5,X0)
| ~ r1_orders_2(sK0,sK4,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_826]) ).
tcf(c_467112,plain,
( m1_subset_1(iPr_def_18,iPr_def_12)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_467109,c_4036]) ).
tcf(c_467113,plain,
m1_subset_1(iPr_def_18,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_467112,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_467114,plain,
( r1_orders_2(sK0,sK5,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_467108,c_4036]) ).
tcf(c_467115,plain,
r1_orders_2(sK0,sK5,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_467114,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_467116,plain,
( r1_orders_2(sK0,sK4,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_467107,c_4036]) ).
tcf(c_467117,plain,
r1_orders_2(sK0,sK4,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_467116,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_467118,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,X0)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r1_orders_2(sK0,sK5,X0)
| ~ r1_orders_2(sK0,sK4,X0) ),
inference(light_normalisation,[status(thm)],[c_467110,c_4036]) ).
tcf(c_467119,plain,
! [X0: $i] :
( r1_orders_2(sK0,iPr_def_18,X0)
| ~ m1_subset_1(X0,iPr_def_12)
| ~ r1_orders_2(sK0,sK5,X0)
| ~ r1_orders_2(sK0,sK4,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_467118,c_4051,c_4052,c_4053,c_4064,c_4063]) ).
tcf(c_467184,plain,
( v1_xboole_0(iPr_def_13)
| r2_hidden(iPr_def_17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_467083,c_144]) ).
tcf(c_467230,plain,
( v1_xboole_0(iPr_def_12)
| r2_hidden(iPr_def_18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_467113,c_144]) ).
tcf(c_467454,plain,
( r1_orders_2(sK0,sK4,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_13)
| ~ m1_subset_1(iPr_def_17,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(superposition,[status(thm)],[c_467087,c_4045]) ).
tcf(c_467455,plain,
( r1_orders_2(sK0,sK4,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_467454,c_467083,c_4065,c_4063]) ).
tcf(c_467517,plain,
( r1_orders_2(sK1,sK5,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK5,iPr_def_12) ),
inference(superposition,[status(thm)],[c_467115,c_4044]) ).
tcf(c_467518,plain,
( r1_orders_2(sK1,sK5,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_467517,c_467113,c_4066,c_4064]) ).
tcf(c_467521,plain,
( r1_orders_2(sK1,sK4,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(superposition,[status(thm)],[c_467117,c_4044]) ).
tcf(c_467522,plain,
( r1_orders_2(sK1,sK4,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_467521,c_467113,c_4065,c_4063]) ).
tcf(c_469734,plain,
r2_hidden(iPr_def_17,iPr_def_13),
inference(global_subsumption_just,[status(thm)],[c_467184,c_7908,c_13523,c_14579]) ).
tcf(c_469988,plain,
r2_hidden(iPr_def_18,iPr_def_12),
inference(global_subsumption_just,[status(thm)],[c_467230,c_7905,c_13394,c_14599]) ).
tcf(c_470278,plain,
( v3_struct_0(sK1)
| r3_orders_2(sK1,iPr_def_17,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ m1_subset_1(sK5,u1_struct_0(sK1))
| ~ m1_subset_1(sK4,u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4041,c_465982]) ).
tcf(c_470279,plain,
( v3_struct_0(sK0)
| r3_orders_2(sK0,iPr_def_18,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m1_subset_1(sK5,u1_struct_0(sK0))
| ~ m1_subset_1(sK4,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_4042,c_465982]) ).
tcf(c_470281,plain,
( v3_struct_0(sK0)
| r3_orders_2(sK0,iPr_def_18,iPr_def_18)
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_470279,c_4036]) ).
tcf(c_470282,plain,
r3_orders_2(sK0,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_470281,c_4056,c_4051,c_4052,c_4053,c_4055,c_4064,c_4063]) ).
tcf(c_470283,plain,
( v3_struct_0(sK1)
| r3_orders_2(sK1,iPr_def_17,iPr_def_17)
| ~ l1_orders_2(sK1)
| ~ v1_lattice3(sK1)
| ~ v4_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ m1_subset_1(sK5,iPr_def_13)
| ~ m1_subset_1(sK4,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_470278,c_4037]) ).
tcf(c_470284,plain,
r3_orders_2(sK1,iPr_def_17,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_470283,c_4062,c_4057,c_4058,c_4059,c_4061,c_4066,c_4065]) ).
tcf(c_476902,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| m1_subset_1(X0,u1_struct_0(sK1))
| ~ l1_orders_2(sK1)
| ~ r2_hidden(X0,k3_xboole_0(iPr_def_12,iPr_def_13)) ),
inference(superposition,[status(thm)],[c_4037,c_466478]) ).
tcf(c_476908,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| m1_subset_1(X0,iPr_def_13)
| ~ l1_orders_2(sK1)
| ~ r2_hidden(X0,iPr_def_14) ),
inference(light_normalisation,[status(thm)],[c_476902,c_4037,c_467036]) ).
tcf(c_476909,plain,
! [X0: $i] :
( m1_subset_1(X0,iPr_def_13)
| ~ r2_hidden(X0,iPr_def_14) ),
inference(forward_subsumption_resolution,[status(thm)],[c_476908,c_4062,c_4057]) ).
tcf(c_477329,plain,
( r1_orders_2(sK0,iPr_def_18,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_470282,c_466495]) ).
tcf(c_477331,plain,
r1_orders_2(sK0,iPr_def_18,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_477329,c_467113]) ).
tcf(c_483128,plain,
( r1_orders_2(sK1,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_470284,c_466910]) ).
tcf(c_483130,plain,
r1_orders_2(sK1,iPr_def_17,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_483128,c_467083]) ).
tcf(c_483283,plain,
( r1_orders_2(sK0,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_13)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_483130,c_4045]) ).
tcf(c_483284,plain,
( r1_orders_2(sK0,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_483283,c_467083]) ).
tcf(c_484010,plain,
( r2_hidden(iPr_def_18,iPr_def_14)
| ~ r2_hidden(iPr_def_18,iPr_def_13) ),
inference(superposition,[status(thm)],[c_469988,c_467039]) ).
tcf(c_484878,plain,
( m1_subset_1(iPr_def_17,iPr_def_12)
| ~ m1_subset_1(iPr_def_13,iPr_def_16) ),
inference(superposition,[status(thm)],[c_469734,c_467067]) ).
tcf(c_492034,plain,
r2_hidden(iPr_def_18,iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_484010,c_34491]) ).
tcf(c_492041,plain,
m1_subset_1(iPr_def_18,iPr_def_13),
inference(superposition,[status(thm)],[c_492034,c_476909]) ).
tcf(c_495609,plain,
m1_subset_1(iPr_def_17,iPr_def_12),
inference(global_subsumption_just,[status(thm)],[c_484878,c_34559]) ).
tcf(c_504335,plain,
r1_orders_2(sK0,sK4,iPr_def_17),
inference(global_subsumption_just,[status(thm)],[c_467455,c_7934,c_34559]) ).
tcf(c_504343,plain,
( r1_orders_2(sK0,iPr_def_18,iPr_def_17)
| ~ m1_subset_1(iPr_def_17,iPr_def_12)
| ~ r1_orders_2(sK0,sK5,iPr_def_17) ),
inference(superposition,[status(thm)],[c_504335,c_467119]) ).
tcf(c_504345,plain,
( r1_orders_2(sK0,iPr_def_18,iPr_def_17)
| ~ r1_orders_2(sK0,sK5,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_504343,c_495609]) ).
tcf(c_506111,plain,
r1_orders_2(sK1,sK5,iPr_def_18),
inference(global_subsumption_just,[status(thm)],[c_467518,c_7917,c_28949]) ).
tcf(c_506885,plain,
r1_orders_2(sK1,sK4,iPr_def_18),
inference(global_subsumption_just,[status(thm)],[c_467522,c_7930,c_28949]) ).
tcf(c_506893,plain,
( r1_orders_2(sK1,iPr_def_17,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13)
| ~ r1_orders_2(sK1,sK5,iPr_def_18) ),
inference(superposition,[status(thm)],[c_506885,c_467089]) ).
tcf(c_506895,plain,
r1_orders_2(sK1,iPr_def_17,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_506893,c_492041,c_506111]) ).
tcf(c_508291,plain,
( r1_orders_2(sK0,iPr_def_17,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,iPr_def_13)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(iPr_def_17,iPr_def_13)
| ~ m1_subset_1(iPr_def_17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_506895,c_4045]) ).
tcf(c_508292,plain,
r1_orders_2(sK0,iPr_def_17,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_508291,c_492041,c_467113,c_467083,c_495609]) ).
tcf(c_509909,plain,
( ( k13_lattice3(sK0,iPr_def_17,iPr_def_18) = iPr_def_18 )
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ r1_orders_2(sK0,iPr_def_18,iPr_def_18)
| ~ m1_subset_1(iPr_def_18,u1_struct_0(sK0))
| ~ m1_subset_1(iPr_def_17,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_508292,c_466322]) ).
tcf(c_509916,plain,
( ( k13_lattice3(sK0,iPr_def_17,iPr_def_18) = iPr_def_18 )
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(iPr_def_17,iPr_def_12)
| ~ r1_orders_2(sK0,iPr_def_18,iPr_def_18) ),
inference(light_normalisation,[status(thm)],[c_509909,c_4036]) ).
tcf(c_509917,plain,
k13_lattice3(sK0,iPr_def_17,iPr_def_18) = iPr_def_18,
inference(forward_subsumption_resolution,[status(thm)],[c_509916,c_4051,c_4052,c_4053,c_467113,c_495609,c_477331]) ).
tcf(c_540150,plain,
r1_orders_2(sK0,iPr_def_17,iPr_def_17),
inference(global_subsumption_just,[status(thm)],[c_483284,c_12134,c_34559]) ).
tcf(c_594031,plain,
r1_orders_2(sK0,iPr_def_18,iPr_def_17),
inference(global_subsumption_just,[status(thm)],[c_504345,c_13856,c_34559]) ).
tcf(c_594036,plain,
( ( k13_lattice3(sK0,iPr_def_17,iPr_def_18) = iPr_def_17 )
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ r1_orders_2(sK0,iPr_def_17,iPr_def_17)
| ~ m1_subset_1(iPr_def_18,u1_struct_0(sK0))
| ~ m1_subset_1(iPr_def_17,u1_struct_0(sK0)) ),
inference(superposition,[status(thm)],[c_594031,c_466293]) ).
tcf(c_594041,plain,
( ( iPr_def_17 = iPr_def_18 )
| ~ l1_orders_2(sK0)
| ~ v1_lattice3(sK0)
| ~ v4_orders_2(sK0)
| ~ m1_subset_1(iPr_def_18,iPr_def_12)
| ~ m1_subset_1(iPr_def_17,iPr_def_12)
| ~ r1_orders_2(sK0,iPr_def_17,iPr_def_17) ),
inference(light_normalisation,[status(thm)],[c_594036,c_4036,c_509917]) ).
tcf(c_594042,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_594041,c_4067,c_4051,c_4052,c_4053,c_467113,c_495609,c_540150]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU410+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.10/5.38 % Computer : n013.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 : Thu Sep 24 14:02:41 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.42 Running first-order theorem proving
% 0.15/5.42 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.15/5.43
% 0.15/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.43
% 0.15/5.43 % Detected problem language: tptp
% 0.15/5.44 % Proving...
% 222.40/40.07 % SZS status Started for theBenchmark.p
% 222.40/40.07 % SZS status Theorem for theBenchmark.p
% 222.40/40.07
% 222.40/40.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 222.40/40.07
% 222.40/40.07 % ------ iProver source info
% 222.40/40.07
% 222.40/40.07 % git: date: 2026-07-19 20:42:38 +0200
% 222.40/40.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 222.40/40.07 % git: non_committed_changes: false
% 222.40/40.07
% 222.40/40.07 % ------ Parsing...
% 222.40/40.07 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 222.40/40.07
% 222.40/40.07 % ------ Preprocessing... sup_sim: 5 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 222.40/40.07
% 222.40/40.07 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 222.40/40.07
% 222.40/40.07 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 222.40/40.07 % ------ Proving...
% 222.40/40.07 % ------ Problem Properties
% 222.40/40.07
% 222.40/40.07 %
% 222.40/40.07 % clauses 108
% 222.40/40.07 % conjectures 17
% 222.40/40.07 % EPR 35
% 222.40/40.07 % Horn 91
% 222.40/40.07 % unary 45
% 222.40/40.07 % binary 16
% 222.40/40.07 % lits 332
% 222.40/40.07 % lits eq 29
% 222.40/40.07 % fd_pure 0
% 222.40/40.07 % fd_pseudo 0
% 222.40/40.07 % fd_cond 1
% 222.40/40.07 % fd_pseudo_cond 10
% 222.40/40.07 % AC symbols 0
% 222.40/40.07
% 222.40/40.07 % ------ Schedule dynamic 5 is on
% 222.40/40.07
% 222.40/40.07 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 222.40/40.07
% 222.40/40.07
% 222.40/40.07 % ------
% 222.40/40.07 % Current options:
% 222.40/40.07 % ------
% 222.40/40.07
% 222.40/40.07
% 222.40/40.07 %
% 222.40/40.07
% 222.40/40.07 % ------ Proving...
% 222.40/40.07 % Proof_search_loop: time out after: 9679 full_loop iterations
% 222.40/40.07
% 222.40/40.07 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 222.40/40.07
% 222.40/40.07
% 222.40/40.07 % ------
% 222.40/40.07 % Current options:
% 222.40/40.07 % ------
% 222.40/40.07
% 222.40/40.07
% 222.40/40.07 %
% 222.40/40.07
% 222.40/40.07 % ------ Proving...
% 222.40/40.07 % Proof_search_loop: time out after: 12758 full_loop iterations
% 222.40/40.07
% 222.40/40.07 % ------ Option_1: Negative Selections Time Limit: 35.
% 222.40/40.07
% 222.40/40.07
% 222.40/40.07 % ------
% 222.40/40.07 % Current options:
% 222.40/40.07 % ------
% 222.40/40.07
% 222.40/40.07
% 222.40/40.07 %
% 222.40/40.07
% 222.40/40.07 % ------ Proving...
% 222.40/40.07 %
% 222.40/40.07
% 222.40/40.07 % SZS status Theorem for theBenchmark.p
% 222.40/40.07
% 222.40/40.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 150.43/40.08
% 150.43/40.08
%------------------------------------------------------------------------------