%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT374+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:59:42 PM UTC 2026
% Result : Theorem 18.67s 3.32s
% Output : CNFRefutation 18.67s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f344ERROR: Could not build tree for root c_24156ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<=> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t49_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<=> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f29,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( v3_lattice3(X0)
& ~ v3_struct_0(X0) )
=> ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f35,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v2_lattice3(X0)
=> ~ v3_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_lattice3) ).
fof(f37,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f50,axiom,
! [X0] :
( l2_altcat_1(X0)
=> ! [X1] :
( l2_altcat_1(X1)
=> ( m1_altcat_2(X1,X0)
<=> ( r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0))
& r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_altcat_2) ).
fof(f65,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( l2_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f67,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& ~ v3_struct_0(k9_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_waybel34) ).
fof(f68,axiom,
! [X0] :
( l1_altcat_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_altcat_1) ).
fof(f71,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f72,axiom,
! [X0] :
( l2_altcat_1(X0)
=> ! [X1] :
( m1_altcat_2(X1,X0)
=> l2_altcat_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_altcat_2) ).
fof(f96,axiom,
! [X0] :
( ( l1_struct_0(X0)
& ~ v3_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f116,axiom,
? [X0] : ~ v2_setfam_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_setfam_1) ).
fof(f131,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ! [X1] :
( ( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1) )
=> ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_waybel34) ).
fof(f133,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( r2_hidden(X0,X1)
| v1_xboole_0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f134,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f135,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X2))
& r2_hidden(X0,X1) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f180,plain,
? [X0] :
( ~ v2_setfam_1(X0)
& ? [X1] :
( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<~> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f181,plain,
? [X0] :
( ~ v2_setfam_1(X0)
& ? [X1] :
( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
<~> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
inference(flattening,[],[f180]) ).
fof(f214,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f29]) ).
fof(f215,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ( v2_lattice3(X0)
& v1_lattice3(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f214]) ).
fof(f224,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f225,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(flattening,[],[f224]) ).
fof(f227,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f250,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ( m1_altcat_2(X1,X0)
<=> ( r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0))
& r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f265,plain,
! [X0] :
( v1_xboole_0(X0)
| ( l2_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& ~ v3_struct_0(k5_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f65]) ).
fof(f268,plain,
! [X0] :
( v2_setfam_1(X0)
| ( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
& v6_altcat_1(k9_waybel34(X0))
& v2_altcat_1(k9_waybel34(X0))
& ~ v3_struct_0(k9_waybel34(X0)) ) ),
inference(ennf_transformation,[],[f67]) ).
fof(f269,plain,
! [X0] :
( ~ l1_altcat_1(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f271,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f272,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,X0)
| l2_altcat_1(X1) ) ),
inference(ennf_transformation,[],[f72]) ).
fof(f291,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f96]) ).
fof(f292,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(flattening,[],[f291]) ).
fof(f324,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
inference(ennf_transformation,[],[f131]) ).
fof(f325,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
<=> ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) ) ) ),
inference(flattening,[],[f324]) ).
fof(f327,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f133]) ).
fof(f328,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(flattening,[],[f327]) ).
fof(f329,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(ennf_transformation,[],[f135]) ).
fof(f330,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(flattening,[],[f329]) ).
fof(f347,plain,
? [X0] :
( ~ v2_setfam_1(X0)
& ? [X1] :
( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
| ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) )
& ( ~ m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1) ) ) ),
inference(nnf_transformation,[],[f181]) ).
fof(f348,plain,
? [X0] :
( ~ v2_setfam_1(X0)
& ? [X1] :
( l1_orders_2(X1)
& v2_lattice3(X1)
& v1_lattice3(X1)
& v4_orders_2(X1)
& v3_orders_2(X1)
& v2_orders_2(X1)
& ( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
| ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) )
& ( ~ m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1) ) ) ),
inference(flattening,[],[f347]) ).
fof(f349,plain,
( ~ v2_setfam_1(sK6)
& l1_orders_2(sK7)
& v2_lattice3(sK7)
& v1_lattice3(sK7)
& v4_orders_2(sK7)
& v3_orders_2(sK7)
& v2_orders_2(sK7)
& ( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| ( r2_hidden(u1_struct_0(sK7),sK6)
& v3_lattice3(sK7)
& v1_orders_2(sK7) ) )
& ( ~ m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ r2_hidden(u1_struct_0(sK7),sK6)
| ~ v3_lattice3(sK7)
| ~ v1_orders_2(sK7) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f348]) ).
fof(f356,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ( ( ~ m1_altcat_2(X1,X0)
| ( r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0))
& r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( ~ r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0))
| ~ r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| m1_altcat_2(X1,X0) ) ) ) ),
inference(nnf_transformation,[],[f250]) ).
fof(f357,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| ! [X1] :
( ~ l2_altcat_1(X1)
| ( ( ~ m1_altcat_2(X1,X0)
| ( r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0))
& r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( ~ r2_altcat_2(k3_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1)),k3_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0)),u2_altcat_1(X1),u2_altcat_1(X0))
| ~ r2_altcat_2(k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_altcat_1(X1),u1_altcat_1(X0))
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| m1_altcat_2(X1,X0) ) ) ) ),
inference(flattening,[],[f356]) ).
fof(f362,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ v6_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ( ( k9_waybel34(X0) != X1
| ( ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
| sP4(X4,X3,X0,X1) ) )
& ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(X1)) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
& ~ sP4(X4,X3,X0,X1) ) )
| ? [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
& ~ m1_subset_1(X2,u1_struct_0(X1)) )
| X1 = k9_waybel34(X0) ) ) ) ),
inference(nnf_transformation,[],[f344]) ).
fof(f363,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ v6_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ( ( k9_waybel34(X0) != X1
| ( ! [X3] :
( ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
| ! [X4] :
( ~ m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
| sP4(X4,X3,X0,X1) ) )
& ! [X2] :
( ~ m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X2,u1_struct_0(X1)) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
& ~ sP4(X4,X3,X0,X1) ) )
| ? [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
& ~ m1_subset_1(X2,u1_struct_0(X1)) )
| X1 = k9_waybel34(X0) ) ) ) ),
inference(flattening,[],[f362]) ).
fof(f364,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ v6_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ( ( k9_waybel34(X0) != X1
| ( ! [X6] :
( ~ m1_subset_1(X6,u1_struct_0(k5_waybel34(X0)))
| ! [X7] :
( ~ m1_subset_1(X7,u1_struct_0(k5_waybel34(X0)))
| sP4(X7,X6,X0,X1) ) )
& ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X5,u1_struct_0(X1)) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
& ? [X4] :
( m1_subset_1(X4,u1_struct_0(k5_waybel34(X0)))
& ~ sP4(X4,X3,X0,X1) ) )
| ? [X2] :
( m1_subset_1(X2,u1_struct_0(k5_waybel34(X0)))
& ~ m1_subset_1(X2,u1_struct_0(X1)) )
| X1 = k9_waybel34(X0) ) ) ) ),
inference(rectify,[],[f363]) ).
fof(f365,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ m1_altcat_2(X1,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ v6_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| ( ( k9_waybel34(X0) != X1
| ( ! [X6] :
( ~ m1_subset_1(X6,u1_struct_0(k5_waybel34(X0)))
| ! [X7] :
( ~ m1_subset_1(X7,u1_struct_0(k5_waybel34(X0)))
| sP4(X7,X6,X0,X1) ) )
& ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X5,u1_struct_0(X1)) ) ) )
& ( ( m1_subset_1(sK12(X0,X1),u1_struct_0(k5_waybel34(X0)))
& m1_subset_1(sK13(X0,X1),u1_struct_0(k5_waybel34(X0)))
& ~ sP4(sK13(X0,X1),sK12(X0,X1),X0,X1) )
| ( m1_subset_1(sK11(X0,X1),u1_struct_0(k5_waybel34(X0)))
& ~ m1_subset_1(sK11(X0,X1),u1_struct_0(X1)) )
| X1 = k9_waybel34(X0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X2,sK11(X0,X1)),skolemize(X3,sK12(X0,X1)),skolemize(X4,sK13(X0,X1))],[f364]) ).
fof(f386,plain,
~ v2_setfam_1(sK33),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X0,sK33)],[f116]) ).
fof(f397,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ( ( ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) )
& ( ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1)
| m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ) ) ) ),
inference(nnf_transformation,[],[f325]) ).
fof(f398,plain,
! [X0] :
( v2_setfam_1(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ( ( ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ( r2_hidden(u1_struct_0(X1),X0)
& v3_lattice3(X1)
& v1_orders_2(X1) ) )
& ( ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1)
| m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ) ) ) ),
inference(flattening,[],[f397]) ).
fof(f399,plain,
! [X0,X1] :
( ( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) )
& ( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f134]) ).
fof(f400,plain,
~ v2_setfam_1(sK6),
inference(cnf_transformation,[],[f349]) ).
fof(f401,plain,
l1_orders_2(sK7),
inference(cnf_transformation,[],[f349]) ).
fof(f402,plain,
v2_lattice3(sK7),
inference(cnf_transformation,[],[f349]) ).
fof(f403,plain,
v1_lattice3(sK7),
inference(cnf_transformation,[],[f349]) ).
fof(f404,plain,
v4_orders_2(sK7),
inference(cnf_transformation,[],[f349]) ).
fof(f405,plain,
v3_orders_2(sK7),
inference(cnf_transformation,[],[f349]) ).
fof(f406,plain,
v2_orders_2(sK7),
inference(cnf_transformation,[],[f349]) ).
fof(f407,plain,
( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| r2_hidden(u1_struct_0(sK7),sK6) ),
inference(cnf_transformation,[],[f349]) ).
fof(f408,plain,
( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| v3_lattice3(sK7) ),
inference(cnf_transformation,[],[f349]) ).
fof(f409,plain,
( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| v1_orders_2(sK7) ),
inference(cnf_transformation,[],[f349]) ).
fof(f410,plain,
( ~ m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ r2_hidden(u1_struct_0(sK7),sK6)
| ~ v3_lattice3(sK7)
| ~ v1_orders_2(sK7) ),
inference(cnf_transformation,[],[f349]) ).
fof(f482,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f215]) ).
fof(f506,plain,
! [X0] :
( ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v3_struct_0(X0) ),
inference(cnf_transformation,[],[f225]) ).
fof(f508,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f227]) ).
fof(f563,plain,
! [X0,X1] :
( ~ l2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| ~ m1_altcat_2(X1,X0)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f357]) ).
fof(f576,plain,
! [X0,X1,X5] :
( v2_setfam_1(X0)
| ~ m1_altcat_2(X1,k5_waybel34(X0))
| ~ v3_altcat_2(X1,k5_waybel34(X0))
| ~ v6_altcat_1(X1)
| ~ v2_altcat_1(X1)
| v3_struct_0(X1)
| k9_waybel34(X0) != X1
| ~ m1_subset_1(X5,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X5,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f365]) ).
fof(f600,plain,
! [X0] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f265]) ).
fof(f610,plain,
! [X0] :
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f268]) ).
fof(f611,plain,
! [X0] :
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f268]) ).
fof(f612,plain,
! [X0] :
( v2_setfam_1(X0)
| v6_altcat_1(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f268]) ).
fof(f613,plain,
! [X0] :
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f268]) ).
fof(f614,plain,
! [X0] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f268]) ).
fof(f615,plain,
! [X0] :
( ~ l1_altcat_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f617,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f271]) ).
fof(f618,plain,
! [X0,X1] :
( ~ l2_altcat_1(X0)
| ~ m1_altcat_2(X1,X0)
| l2_altcat_1(X1) ),
inference(cnf_transformation,[],[f272]) ).
fof(f643,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f292]) ).
fof(f741,plain,
~ v2_setfam_1(sK33),
inference(cnf_transformation,[],[f386]) ).
fof(f777,plain,
! [X0,X1] :
( v2_setfam_1(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| r2_hidden(u1_struct_0(X1),X0) ),
inference(cnf_transformation,[],[f398]) ).
fof(f778,plain,
! [X0,X1] :
( v2_setfam_1(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| v3_lattice3(X1) ),
inference(cnf_transformation,[],[f398]) ).
fof(f779,plain,
! [X0,X1] :
( v2_setfam_1(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| v1_orders_2(X1) ),
inference(cnf_transformation,[],[f398]) ).
fof(f780,plain,
! [X0,X1] :
( v2_setfam_1(X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1)
| m1_subset_1(X1,u1_struct_0(k5_waybel34(X0))) ),
inference(cnf_transformation,[],[f398]) ).
fof(f782,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f328]) ).
fof(f784,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f399]) ).
fof(f785,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f330]) ).
fof(f794,plain,
! [X0,X5] :
( v2_setfam_1(X0)
| ~ m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ~ v6_altcat_1(k9_waybel34(X0))
| ~ v2_altcat_1(k9_waybel34(X0))
| v3_struct_0(k9_waybel34(X0))
| ~ m1_subset_1(X5,u1_struct_0(k5_waybel34(X0)))
| m1_subset_1(X5,u1_struct_0(k9_waybel34(X0))) ),
inference(equality_resolution,[],[f576]) ).
tcf(c_49,negated_conjecture,
( ~ v3_lattice3(sK7)
| ~ v1_orders_2(sK7)
| ~ r2_hidden(u1_struct_0(sK7),sK6)
| ~ m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(cnf_transformation,[],[f410]) ).
tcf(c_50,negated_conjecture,
( v1_orders_2(sK7)
| m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(cnf_transformation,[],[f409]) ).
tcf(c_51,negated_conjecture,
( v3_lattice3(sK7)
| m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(cnf_transformation,[],[f408]) ).
tcf(c_52,negated_conjecture,
( r2_hidden(u1_struct_0(sK7),sK6)
| m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(cnf_transformation,[],[f407]) ).
tcf(c_53,negated_conjecture,
v2_orders_2(sK7),
inference(cnf_transformation,[],[f406]) ).
tcf(c_54,negated_conjecture,
v3_orders_2(sK7),
inference(cnf_transformation,[],[f405]) ).
tcf(c_55,negated_conjecture,
v4_orders_2(sK7),
inference(cnf_transformation,[],[f404]) ).
tcf(c_56,negated_conjecture,
v1_lattice3(sK7),
inference(cnf_transformation,[],[f403]) ).
tcf(c_57,negated_conjecture,
v2_lattice3(sK7),
inference(cnf_transformation,[],[f402]) ).
tcf(c_58,negated_conjecture,
l1_orders_2(sK7),
inference(cnf_transformation,[],[f401]) ).
tcf(c_59,negated_conjecture,
~ v2_setfam_1(sK6),
inference(cnf_transformation,[],[f400]) ).
tcf(c_113,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v3_lattice3(X0) ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_134,plain,
! [X0: $i] :
( ~ v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0) ),
inference(cnf_transformation,[],[f506]) ).
tcf(c_136,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f508]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l2_altcat_1(X1)
| ~ l2_altcat_1(X0)
| ~ m1_altcat_2(X0,X1) ),
inference(cnf_transformation,[],[f563]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| v3_struct_0(k9_waybel34(X1))
| m1_subset_1(X0,u1_struct_0(k9_waybel34(X1)))
| ~ v2_altcat_1(k9_waybel34(X1))
| ~ v6_altcat_1(k9_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(cnf_transformation,[],[f794]) ).
tcf(c_216,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| l2_altcat_1(k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f600]) ).
tcf(c_220,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f614]) ).
tcf(c_221,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f613]) ).
tcf(c_222,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v6_altcat_1(k9_waybel34(X0)) ),
inference(cnf_transformation,[],[f612]) ).
tcf(c_223,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f611]) ).
tcf(c_224,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(cnf_transformation,[],[f610]) ).
tcf(c_225,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f615]) ).
tcf(c_227,plain,
! [X0: $i] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(cnf_transformation,[],[f617]) ).
tcf(c_228,plain,
! [X0: $i,X1: $i] :
( l2_altcat_1(X0)
| ~ l2_altcat_1(X1)
| ~ m1_altcat_2(X0,X1) ),
inference(cnf_transformation,[],[f618]) ).
tcf(c_253,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f643]) ).
tcf(c_351,plain,
~ v2_setfam_1(sK33),
inference(cnf_transformation,[],[f741]) ).
tcf(c_387,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| m1_subset_1(X0,u1_struct_0(k5_waybel34(X1)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),X1) ),
inference(cnf_transformation,[],[f780]) ).
tcf(c_388,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| v1_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(cnf_transformation,[],[f779]) ).
tcf(c_389,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(cnf_transformation,[],[f778]) ).
tcf(c_390,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| r2_hidden(u1_struct_0(X0),X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(cnf_transformation,[],[f777]) ).
tcf(c_392,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f782]) ).
tcf(c_393,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f784]) ).
tcf(c_395,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,[],[f785]) ).
tcf(c_615,plain,
! [X0: $i,X1: $i] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l2_altcat_1(X1)
| ~ m1_altcat_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_172,c_228,c_172]) ).
tcf(c_632,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| m1_subset_1(X0,u1_struct_0(k5_waybel34(X1)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),X1)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_387,c_134,c_113,c_387]) ).
tcf(c_633,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| m1_subset_1(X0,u1_struct_0(k5_waybel34(X1)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),X1) ),
inference(renaming,[status(thm)],[c_632]) ).
tcf(c_640,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_393]) ).
tcf(c_648,plain,
( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| v3_lattice3(sK7) ),
inference(prop_impl_just,[status(thm)],[c_51]) ).
tcf(c_649,plain,
( v3_lattice3(sK7)
| m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(renaming,[status(thm)],[c_648]) ).
tcf(c_662,plain,
! [X0: $i] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_227]) ).
tcf(c_790,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v1_xboole_0(X0) ),
inference(prop_impl_just,[status(thm)],[c_136]) ).
tcf(c_930,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| ~ v3_struct_0(k9_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_220]) ).
tcf(c_932,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v2_altcat_1(k9_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_221]) ).
tcf(c_934,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v6_altcat_1(k9_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_222]) ).
tcf(c_936,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_223]) ).
tcf(c_938,plain,
! [X0: $i] :
( v2_setfam_1(X0)
| m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)) ),
inference(prop_impl_just,[status(thm)],[c_224]) ).
tcf(c_950,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_225]) ).
tcf(c_1525,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,X2)
| ~ r1_tarski(X1,X2)
| ~ r2_hidden(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_395,c_640]) ).
tcf(c_1900,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| v3_struct_0(k9_waybel34(X1))
| m1_subset_1(X0,u1_struct_0(k9_waybel34(X1)))
| ~ v6_altcat_1(k9_waybel34(X1))
| ~ m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_191,c_932]) ).
tcf(c_1909,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| v3_struct_0(k9_waybel34(X1))
| m1_subset_1(X0,u1_struct_0(k9_waybel34(X1)))
| ~ m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1900,c_934]) ).
tcf(c_2013,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| m1_subset_1(X0,u1_struct_0(k9_waybel34(X1)))
| ~ m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1909,c_930]) ).
tcf(c_2121,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| m1_subset_1(X0,u1_struct_0(k9_waybel34(X1)))
| ~ m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2013,c_936]) ).
tcf(c_2129,plain,
! [X0: $i,X1: $i] :
( v2_setfam_1(X1)
| m1_subset_1(X0,u1_struct_0(k9_waybel34(X1)))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2121,c_938]) ).
tcf(c_3792,plain,
! [X0: $i,X1: $i] :
( l1_struct_0(X1)
| ~ l2_altcat_1(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_662,c_950]) ).
tcf(c_3793,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l2_altcat_1(X0) ),
inference(unflattening,[status(thm)],[c_3792]) ).
tcf(c_7154,plain,
! [X0: $i] :
( m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_938]) ).
tcf(c_7155,plain,
m1_altcat_2(k9_waybel34(sK6),k5_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_7154]) ).
tcf(c_7174,plain,
! [X0: $i] :
( ~ v3_struct_0(k9_waybel34(X0))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_930]) ).
tcf(c_7175,plain,
~ v3_struct_0(k9_waybel34(sK6)),
inference(unflattening,[status(thm)],[c_7174]) ).
tcf(c_7287,plain,
! [X0: $i] :
( ~ v1_xboole_0(X0)
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_790]) ).
tcf(c_7288,plain,
~ v1_xboole_0(sK6),
inference(unflattening,[status(thm)],[c_7287]) ).
tcf(c_7313,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X1,u1_struct_0(k9_waybel34(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_2129]) ).
tcf(c_7314,plain,
! [X0: $i] :
( m1_subset_1(X0,u1_struct_0(k9_waybel34(sK6)))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6))) ),
inference(unflattening,[status(thm)],[c_7313]) ).
tcf(c_7315,plain,
( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_7314]) ).
tcf(c_7334,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_633]) ).
tcf(c_7335,plain,
! [X0: $i] :
( m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK6) ),
inference(unflattening,[status(thm)],[c_7334]) ).
tcf(c_7336,plain,
( m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6)))
| ~ l1_orders_2(sK7)
| ~ v2_lattice3(sK7)
| ~ v4_orders_2(sK7)
| ~ v3_orders_2(sK7)
| ~ v2_orders_2(sK7)
| ~ v3_lattice3(sK7)
| ~ v1_orders_2(sK7)
| ~ r2_hidden(u1_struct_0(sK7),sK6) ),
inference(instantiation,[status(thm)],[c_7335]) ).
tcf(c_7364,plain,
! [X0: $i,X1: $i] :
( r2_hidden(u1_struct_0(X1),X0)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_390]) ).
tcf(c_7365,plain,
! [X0: $i] :
( r2_hidden(u1_struct_0(X0),sK6)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6))) ),
inference(unflattening,[status(thm)],[c_7364]) ).
tcf(c_7366,plain,
( r2_hidden(u1_struct_0(sK7),sK6)
| ~ l1_orders_2(sK7)
| ~ v2_lattice3(sK7)
| ~ v1_lattice3(sK7)
| ~ v4_orders_2(sK7)
| ~ v3_orders_2(sK7)
| ~ v2_orders_2(sK7)
| ~ m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_7365]) ).
tcf(c_7391,plain,
! [X0: $i,X1: $i] :
( v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_389]) ).
tcf(c_7392,plain,
! [X0: $i] :
( v3_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6))) ),
inference(unflattening,[status(thm)],[c_7391]) ).
tcf(c_7418,plain,
! [X0: $i,X1: $i] :
( v1_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ( X0 != sK6 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_388]) ).
tcf(c_7419,plain,
! [X0: $i] :
( v1_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6))) ),
inference(unflattening,[status(thm)],[c_7418]) ).
tcf(c_7420,plain,
( v1_orders_2(sK7)
| ~ l1_orders_2(sK7)
| ~ v2_lattice3(sK7)
| ~ v1_lattice3(sK7)
| ~ v4_orders_2(sK7)
| ~ v3_orders_2(sK7)
| ~ v2_orders_2(sK7)
| ~ m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_7419]) ).
tcf(c_7739,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X1,u1_struct_0(k5_waybel34(X0)))
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v1_orders_2(X1)
| ~ r2_hidden(u1_struct_0(X1),X0)
| ( X0 != sK33 ) ),
inference(resolution_lifted,[status(thm)],[c_633,c_351]) ).
tcf(c_7740,plain,
! [X0: $i] :
( m1_subset_1(X0,u1_struct_0(k5_waybel34(sK33)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK33) ),
inference(unflattening,[status(thm)],[c_7739]) ).
tcf(c_9125,plain,
! [X0: $i] :
( m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| m1_subset_1(X0,u1_struct_0(k5_waybel34(sK33)))
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ v1_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK33)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_649,c_7740]) ).
tcf(c_9126,plain,
( m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK33)))
| m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ l1_orders_2(sK7)
| ~ v2_lattice3(sK7)
| ~ v4_orders_2(sK7)
| ~ v3_orders_2(sK7)
| ~ v2_orders_2(sK7)
| ~ v1_orders_2(sK7)
| ~ r2_hidden(u1_struct_0(sK7),sK33) ),
inference(unflattening,[status(thm)],[c_9125]) ).
tcf(c_9127,plain,
m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))),
inference(global_subsumption_just,[status(thm)],[c_9126,c_58,c_57,c_55,c_54,c_53,c_51,c_50,c_52,c_7315,c_7336]) ).
tcf(c_9150,plain,
! [X0: $i] :
( ~ v1_orders_2(sK7)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(sK7),sK6)
| ~ m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6)))
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_7392]) ).
tcf(c_9151,plain,
( ~ l1_orders_2(sK7)
| ~ v2_lattice3(sK7)
| ~ v1_lattice3(sK7)
| ~ v4_orders_2(sK7)
| ~ v3_orders_2(sK7)
| ~ v2_orders_2(sK7)
| ~ v1_orders_2(sK7)
| ~ r2_hidden(u1_struct_0(sK7),sK6)
| ~ m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6)))
| ~ m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(unflattening,[status(thm)],[c_9150]) ).
tcf(c_9152,plain,
~ m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6))),
inference(global_subsumption_just,[status(thm)],[c_9151,c_58,c_57,c_56,c_55,c_54,c_53,c_7366,c_7420,c_9127,c_9151]) ).
tcf(c_19357,plain,
( v3_struct_0(k9_waybel34(sK6))
| ~ l1_struct_0(k9_waybel34(sK6))
| ~ v1_xboole_0(u1_struct_0(k9_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_253]) ).
tcf(c_19404,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X1,u1_struct_0(k5_waybel34(sK6)))
| ~ r2_hidden(X1,X0)
| ~ r1_tarski(X0,u1_struct_0(k5_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_1525]) ).
tcf(c_19443,plain,
( v1_xboole_0(sK6)
| l2_altcat_1(k5_waybel34(sK6)) ),
inference(instantiation,[status(thm)],[c_216]) ).
tcf(c_19600,plain,
( l1_struct_0(k9_waybel34(sK6))
| ~ l2_altcat_1(k9_waybel34(sK6)) ),
inference(instantiation,[status(thm)],[c_3793]) ).
tcf(c_20422,plain,
( l2_altcat_1(k9_waybel34(sK6))
| ~ l2_altcat_1(k5_waybel34(sK6))
| ~ m1_altcat_2(k9_waybel34(sK6),k5_waybel34(sK6)) ),
inference(instantiation,[status(thm)],[c_228]) ).
tcf(c_20679,plain,
! [X0: $i] :
( v1_xboole_0(u1_struct_0(k9_waybel34(sK6)))
| r2_hidden(X0,u1_struct_0(k9_waybel34(sK6)))
| ~ m1_subset_1(X0,u1_struct_0(k9_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_392]) ).
tcf(c_20680,plain,
( v1_xboole_0(u1_struct_0(k9_waybel34(sK6)))
| r2_hidden(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ m1_subset_1(sK7,u1_struct_0(k9_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_20679]) ).
tcf(c_22872,plain,
! [X0: $i] :
( m1_subset_1(X0,u1_struct_0(k5_waybel34(sK6)))
| ~ r2_hidden(X0,u1_struct_0(k9_waybel34(sK6)))
| ~ r1_tarski(u1_struct_0(k9_waybel34(sK6)),u1_struct_0(k5_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_19404]) ).
tcf(c_22873,plain,
( m1_subset_1(sK7,u1_struct_0(k5_waybel34(sK6)))
| ~ r2_hidden(sK7,u1_struct_0(k9_waybel34(sK6)))
| ~ r1_tarski(u1_struct_0(k9_waybel34(sK6)),u1_struct_0(k5_waybel34(sK6))) ),
inference(instantiation,[status(thm)],[c_22872]) ).
tcf(c_24155,plain,
( r1_tarski(u1_struct_0(k9_waybel34(sK6)),u1_struct_0(k5_waybel34(sK6)))
| ~ l2_altcat_1(k5_waybel34(sK6))
| ~ m1_altcat_2(k9_waybel34(sK6),k5_waybel34(sK6)) ),
inference(instantiation,[status(thm)],[c_615]) ).
tcf(c_24156,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_24155,c_22873,c_20680,c_20422,c_19600,c_19443,c_19357,c_9152,c_9127,c_7288,c_7175,c_7155]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT374+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 21:28:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.43 Running first-order theorem proving
% 0.14/0.43 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.44
% 0.14/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.44
% 0.14/0.45 % Detected problem language: tptp
% 0.14/0.46 % Proving...
% 18.67/3.32 % SZS status Started for theBenchmark.p
% 18.67/3.32 % SZS status Theorem for theBenchmark.p
% 18.67/3.32
% 18.67/3.32 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 18.67/3.32
% 18.67/3.32 % ------ iProver source info
% 18.67/3.32
% 18.67/3.32 % git: date: 2026-07-19 20:42:38 +0200
% 18.67/3.32 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 18.67/3.32 % git: non_committed_changes: false
% 18.67/3.32
% 18.67/3.32 % ------ Parsing...
% 18.67/3.32 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 18.67/3.32
% 18.67/3.32 % ------ Preprocessing... sup_sim: 0 sf_s rm: 48 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e %
% 18.67/3.32
% 18.67/3.32 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 18.67/3.32
% 18.67/3.32 % ------ Preprocessing... sf_s rm: 11 0s sf_e sf_s rm: 0 0s sf_e
% 18.67/3.32 % ------ Proving...
% 18.67/3.32 % ------ Problem Properties
% 18.67/3.32
% 18.67/3.32 %
% 18.67/3.32 % clauses 301
% 18.67/3.32 % conjectures 6
% 18.67/3.32 % EPR 136
% 18.67/3.32 % Horn 231
% 18.67/3.32 % unary 115
% 18.67/3.32 % binary 72
% 18.67/3.32 % lits 965
% 18.67/3.32 % lits eq 37
% 18.67/3.32 % fd_pure 0
% 18.67/3.32 % fd_pseudo 0
% 18.67/3.32 % fd_cond 13
% 18.67/3.32 % fd_pseudo_cond 6
% 18.67/3.32 % AC symbols 0
% 18.67/3.32
% 18.67/3.32 % ------ Input Options Time Limit: Unbounded
% 18.67/3.32
% 18.67/3.32
% 18.67/3.32 % ------
% 18.67/3.32 % Current options:
% 18.67/3.32 % ------
% 18.67/3.32
% 18.67/3.32
% 18.67/3.32 %
% 18.67/3.32
% 18.67/3.32 % ------ Proving...
% 18.67/3.32 %
% 18.67/3.32
% 18.67/3.32 % SZS status Theorem for theBenchmark.p
% 18.67/3.32
% 18.67/3.32 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.67/3.32
% 18.67/3.32
%------------------------------------------------------------------------------