%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : TOP042+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 : n014.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 03:55:27 PM UTC 2026
% Result : Theorem 268.36s 39.52s
% Output : CNFRefutation 268.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 18
% Syntax : Number of formulae : 208 ( 49 unt; 2 def)
% Number of atoms : 1013 ( 131 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1366 ( 561 ~; 619 |; 141 &)
% ( 14 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-4 aty)
% Number of variables : 361 ( 0 sgn 339 !; 22 ?; 133 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_tsp_1(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
=> v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_tsp_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_tsp_1(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
=> v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f50,axiom,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f52,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_tsp_1(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X3 = u1_struct_0(X1)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
=> k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_tsp_2) ).
fof(f53,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ( m2_tsp_1(X1,X0)
<=> ( ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( v4_pre_topc(X2,X1)
<=> ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_tsp_1) ).
fof(f54,axiom,
! [X0,X1] :
( ( m1_pre_topc(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1)
& l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ( m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k1_tsp_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_tsp_2) ).
fof(f60,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& l1_struct_0(X1)
& l1_struct_0(X0) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f61,axiom,
! [X0,X1] :
( ( m1_pre_topc(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1)
& l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k4_tsp_2(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f64,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f70,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f108,axiom,
! [X0,X1] :
( ( m1_pre_topc(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1)
& l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_tsp_2) ).
fof(f109,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f110,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f111,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f114,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_pre_topc(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_tsep_1) ).
fof(f117,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(f120,axiom,
! [X0] :
( ( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t62_tex_4) ).
fof(f154,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m2_tsp_1(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1)
& ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
& v4_pre_topc(X2,X0)
& ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f155,plain,
? [X0] :
( l1_pre_topc(X0)
& v2_pre_topc(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m2_tsp_1(X1,X0)
& v2_tsp_2(X1,X0)
& ~ v3_struct_0(X1)
& ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
& v4_pre_topc(X2,X0)
& ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1) ) ) ),
inference(flattening,[],[f154]) ).
fof(f219,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X3
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) ) ) ) ),
inference(ennf_transformation,[],[f52]) ).
fof(f220,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X3
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) ) ) ) ),
inference(flattening,[],[f219]) ).
fof(f221,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| ( m2_tsp_1(X1,X0)
<=> ( ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ( v4_pre_topc(X2,X1)
<=> ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
inference(ennf_transformation,[],[f53]) ).
fof(f222,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k1_tsp_2(X0,X1)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f223,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k1_tsp_2(X0,X1)) ) ),
inference(flattening,[],[f222]) ).
fof(f226,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(ennf_transformation,[],[f60]) ).
fof(f227,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(flattening,[],[f226]) ).
fof(f228,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k4_tsp_2(X0,X1)) ) ),
inference(ennf_transformation,[],[f61]) ).
fof(f229,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(k4_tsp_2(X0,X1)) ) ),
inference(flattening,[],[f228]) ).
fof(f232,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f235,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ) ),
inference(ennf_transformation,[],[f70]) ).
fof(f272,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
inference(ennf_transformation,[],[f108]) ).
fof(f273,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
inference(flattening,[],[f272]) ).
fof(f274,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
inference(ennf_transformation,[],[f109]) ).
fof(f275,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
inference(flattening,[],[f274]) ).
fof(f276,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
inference(ennf_transformation,[],[f111]) ).
fof(f278,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ m1_pre_topc(X1,X0)
| m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
inference(ennf_transformation,[],[f114]) ).
fof(f284,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1 ) ),
inference(ennf_transformation,[],[f120]) ).
fof(f285,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1 ) ),
inference(flattening,[],[f284]) ).
fof(f296,plain,
( l1_pre_topc(sK4)
& v2_pre_topc(sK4)
& ~ v3_struct_0(sK4)
& m2_tsp_1(sK5,sK4)
& v2_tsp_2(sK5,sK4)
& ~ v3_struct_0(sK5)
& m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
& v4_pre_topc(sK6,sK4)
& ~ v4_pre_topc(k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6)],[f155]) ).
fof(f299,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( k4_tsp_2(X0,X1) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X3
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = X3
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
& k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4) ) )
| X2 = k4_tsp_2(X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f220]) ).
fof(f300,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( k4_tsp_2(X0,X1) != X2
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X5
| ! [X6] :
( ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6) ) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = X3
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
& k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4) ) )
| X2 = k4_tsp_2(X0,X1) ) ) ) ) ),
inference(rectify,[],[f299]) ).
fof(f301,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ! [X2] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ( ( k4_tsp_2(X0,X1) != X2
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X5
| ! [X6] :
( ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6) ) ) )
& ( ( m1_subset_1(sK7(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK7(X0,X1,X2)
& m1_subset_1(sK8(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& k5_subset_1(u1_struct_0(X0),sK7(X0,X1,X2),k3_tex_4(X0,sK8(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK8(X0,X1,X2)) )
| X2 = k4_tsp_2(X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X3,sK7(X0,X1,X2)),skolemize(X4,sK8(X0,X1,X2))],[f300]) ).
fof(f302,plain,
! [X1,X0] :
( ~ sP2(X1,X0)
| ( ( ~ m2_tsp_1(X1,X0)
| sP1(X0,X1) )
& ( ~ sP1(X0,X1)
| m2_tsp_1(X1,X0) ) ) ),
inference(nnf_transformation,[],[f292]) ).
fof(f303,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ( ( ~ m2_tsp_1(X0,X1)
| sP1(X1,X0) )
& ( ~ sP1(X1,X0)
| m2_tsp_1(X0,X1) ) ) ),
inference(rectify,[],[f302]) ).
fof(f328,plain,
! [X0,X1,X2] :
( ( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) )
& ( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f110]) ).
fof(f329,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) )
& ( ~ m1_pre_topc(X1,X0)
| m2_tsp_1(X1,X0) ) ) ),
inference(nnf_transformation,[],[f276]) ).
fof(f330,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,[],[f117]) ).
fof(f331,plain,
l1_pre_topc(sK4),
inference(cnf_transformation,[],[f296]) ).
fof(f332,plain,
v2_pre_topc(sK4),
inference(cnf_transformation,[],[f296]) ).
fof(f333,plain,
~ v3_struct_0(sK4),
inference(cnf_transformation,[],[f296]) ).
fof(f334,plain,
m2_tsp_1(sK5,sK4),
inference(cnf_transformation,[],[f296]) ).
fof(f335,plain,
v2_tsp_2(sK5,sK4),
inference(cnf_transformation,[],[f296]) ).
fof(f336,plain,
~ v3_struct_0(sK5),
inference(cnf_transformation,[],[f296]) ).
fof(f337,plain,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4))),
inference(cnf_transformation,[],[f296]) ).
fof(f338,plain,
v4_pre_topc(sK6,sK4),
inference(cnf_transformation,[],[f296]) ).
fof(f339,plain,
~ v4_pre_topc(k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),sK5),
inference(cnf_transformation,[],[f296]) ).
fof(f440,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f50]) ).
fof(f442,plain,
! [X2,X0,X1,X6,X5] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k4_tsp_2(X0,X1) != X2
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6) ),
inference(cnf_transformation,[],[f301]) ).
fof(f447,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ~ m2_tsp_1(X0,X1)
| sP1(X1,X0) ),
inference(cnf_transformation,[],[f303]) ).
fof(f459,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| sP2(X1,X0) ),
inference(cnf_transformation,[],[f293]) ).
fof(f463,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v1_funct_1(k1_tsp_2(X0,X1)) ),
inference(cnf_transformation,[],[f223]) ).
fof(f465,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f227]) ).
fof(f466,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f229]) ).
fof(f467,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f229]) ).
fof(f468,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f229]) ).
fof(f469,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v1_funct_1(k4_tsp_2(X0,X1)) ),
inference(cnf_transformation,[],[f229]) ).
fof(f471,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f474,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f235]) ).
fof(f572,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f273]) ).
fof(f573,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
inference(cnf_transformation,[],[f275]) ).
fof(f574,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f328]) ).
fof(f576,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f329]) ).
fof(f580,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f278]) ).
fof(f583,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f330]) ).
fof(f584,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f330]) ).
fof(f587,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1 ),
inference(cnf_transformation,[],[f285]) ).
fof(f591,plain,
! [X2,X0,X1,X6] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| k4_tsp_2(X0,X1) != X2
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| k4_pre_topc(X0,X1,X2,X6) = k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6)) ),
inference(equality_resolution,[],[f442]) ).
fof(f592,plain,
! [X0,X1,X6] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| v3_struct_0(X1)
| ~ m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k4_tsp_2(X0,X1))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X6) ),
inference(equality_resolution,[],[f591]) ).
tcf(c_49,negated_conjecture,
~ v4_pre_topc(k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),sK5),
inference(cnf_transformation,[],[f339]) ).
tcf(c_50,negated_conjecture,
v4_pre_topc(sK6,sK4),
inference(cnf_transformation,[],[f338]) ).
tcf(c_51,negated_conjecture,
m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4))),
inference(cnf_transformation,[],[f337]) ).
tcf(c_52,negated_conjecture,
~ v3_struct_0(sK5),
inference(cnf_transformation,[],[f336]) ).
tcf(c_53,negated_conjecture,
v2_tsp_2(sK5,sK4),
inference(cnf_transformation,[],[f335]) ).
tcf(c_54,negated_conjecture,
m2_tsp_1(sK5,sK4),
inference(cnf_transformation,[],[f334]) ).
tcf(c_55,negated_conjecture,
~ v3_struct_0(sK4),
inference(cnf_transformation,[],[f333]) ).
tcf(c_56,negated_conjecture,
v2_pre_topc(sK4),
inference(cnf_transformation,[],[f332]) ).
tcf(c_57,negated_conjecture,
l1_pre_topc(sK4),
inference(cnf_transformation,[],[f331]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[],[f440]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X2)) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2) )
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| ~ v2_tsp_2(X1,X0)
| ~ v1_funct_1(k4_tsp_2(X0,X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f592]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] :
( sP1(X1,X0)
| ~ sP2(X0,X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f447]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] :
( sP2(X0,X1)
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f459]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_1(k1_tsp_2(X1,X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(X0,X1)
| ~ v2_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f463]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k4_pre_topc(X1,X2,X0,X3),k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f465]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_1(k4_tsp_2(X1,X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(X0,X1)
| ~ v2_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f469]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_2(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(X0,X1)
| ~ v2_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f468]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(X1,X0),X1,X0)
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(X0,X1)
| ~ v2_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f467]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m2_relset_1(k4_tsp_2(X1,X0),u1_struct_0(X1),u1_struct_0(X0))
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(X0,X1)
| ~ v2_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f466]) ).
tcf(c_157,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f471]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f474]) ).
tcf(c_258,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k4_tsp_2(X1,X0) = k1_tsp_2(X1,X0) )
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m1_pre_topc(X0,X1)
| ~ v2_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f572]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_subset_1(X1,X0,X2) = k3_xboole_0(X0,X2) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X1))
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f573]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f574]) ).
tcf(c_263,plain,
! [X0: $i,X1: $i] :
( m1_pre_topc(X0,X1)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f576]) ).
tcf(c_266,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1)
| ~ m1_pre_topc(X0,X1) ),
inference(cnf_transformation,[],[f580]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f584]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f583]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ( k3_tex_4(X1,X0) = X0 )
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ v4_pre_topc(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f587]) ).
tcf(c_424,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_269]) ).
tcf(c_426,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m2_relset_1(X0,X1,X2)
| m1_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_261]) ).
tcf(c_427,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(renaming,[status(thm)],[c_426]) ).
tcf(c_1004,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_subset_1(X1,X2,X0) = k3_xboole_0(X2,X0) )
| ~ r1_tarski(X2,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(bin_hyper_res,[status(thm)],[c_259,c_424]) ).
tcf(c_2340,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1(X3,X1)
| ~ l1_pre_topc(X2)
| ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_145,c_134]) ).
tcf(c_2341,plain,
! [X0: $i,X1: $i] :
( sP1(X1,X0)
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X0,X1) ),
inference(unflattening,[status(thm)],[c_2340]) ).
tcf(c_2343,plain,
! [X0: $i,X1: $i] :
( sP1(X1,X0)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2341,c_160,c_2341]) ).
tcf(c_3056,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) )
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_258]) ).
tcf(c_3057,plain,
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| ( k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) )
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(unflattening,[status(thm)],[c_3056]) ).
tcf(c_3058,plain,
( ( k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5) )
| ~ m1_pre_topc(sK5,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3057,c_57,c_56,c_55,c_52,c_3057]) ).
tcf(c_3066,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_155]) ).
tcf(c_3067,plain,
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(unflattening,[status(thm)],[c_3066]) ).
tcf(c_3068,plain,
( m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_pre_topc(sK5,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3067,c_57,c_56,c_55,c_52,c_3067]) ).
tcf(c_3076,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_154]) ).
tcf(c_3077,plain,
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| v5_pre_topc(k4_tsp_2(sK4,sK5),sK4,sK5)
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(unflattening,[status(thm)],[c_3076]) ).
tcf(c_3078,plain,
( v5_pre_topc(k4_tsp_2(sK4,sK5),sK4,sK5)
| ~ m1_pre_topc(sK5,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3077,c_57,c_56,c_55,c_52,c_3077]) ).
tcf(c_3086,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_153]) ).
tcf(c_3087,plain,
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(unflattening,[status(thm)],[c_3086]) ).
tcf(c_3088,plain,
( v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_pre_topc(sK5,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3087,c_57,c_56,c_55,c_52,c_3087]) ).
tcf(c_3096,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_1(k4_tsp_2(X0,X1))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_152]) ).
tcf(c_3097,plain,
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| v1_funct_1(k4_tsp_2(sK4,sK5))
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(unflattening,[status(thm)],[c_3096]) ).
tcf(c_3098,plain,
( v1_funct_1(k4_tsp_2(sK4,sK5))
| ~ m1_pre_topc(sK5,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3097,c_57,c_56,c_55,c_52,c_3097]) ).
tcf(c_3136,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_1(k1_tsp_2(X0,X1))
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m1_pre_topc(X1,X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_146]) ).
tcf(c_3137,plain,
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| v1_funct_1(k1_tsp_2(sK4,sK5))
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m1_pre_topc(sK5,sK4) ),
inference(unflattening,[status(thm)],[c_3136]) ).
tcf(c_3138,plain,
( v1_funct_1(k1_tsp_2(sK4,sK5))
| ~ m1_pre_topc(sK5,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3137,c_57,c_56,c_55,c_52,c_3137]) ).
tcf(c_3146,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X2)) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2) )
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| ~ v1_funct_1(k4_tsp_2(X0,X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_132]) ).
tcf(c_3147,plain,
! [X0: $i] :
( v3_struct_0(sK5)
| v3_struct_0(sK4)
| ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ m2_tsp_1(sK5,sK4)
| ~ v1_funct_1(k4_tsp_2(sK4,sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v5_pre_topc(k4_tsp_2(sK4,sK5),sK4,sK5)
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(unflattening,[status(thm)],[c_3146]) ).
tcf(c_3149,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v5_pre_topc(k4_tsp_2(sK4,sK5),sK4,sK5)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v1_funct_1(k4_tsp_2(sK4,sK5)) ),
inference(global_subsumption_just,[status(thm)],[c_3147,c_57,c_56,c_55,c_54,c_52,c_3147]) ).
tcf(c_3150,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ v1_funct_1(k4_tsp_2(sK4,sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v5_pre_topc(k4_tsp_2(sK4,sK5),sK4,sK5)
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(renaming,[status(thm)],[c_3149]) ).
tcf(c_3334,plain,
! [X0: $i,X1: $i] :
( sP1(X0,X1)
| ~ l1_pre_topc(X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_2343]) ).
tcf(c_3335,plain,
( sP1(sK4,sK5)
| ~ l1_pre_topc(sK4) ),
inference(unflattening,[status(thm)],[c_3334]) ).
tcf(c_3336,plain,
sP1(sK4,sK5),
inference(global_subsumption_just,[status(thm)],[c_3335,c_57,c_3335]) ).
tcf(c_3341,plain,
! [X0: $i,X1: $i] :
( m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_263]) ).
tcf(c_3342,plain,
( m1_pre_topc(sK5,sK4)
| ~ l1_pre_topc(sK4) ),
inference(unflattening,[status(thm)],[c_3341]) ).
tcf(c_3343,plain,
m1_pre_topc(sK5,sK4),
inference(global_subsumption_just,[status(thm)],[c_3342,c_57,c_3342]) ).
tcf(c_3348,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ( X1 != sK5 )
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_160]) ).
tcf(c_3349,plain,
( l1_pre_topc(sK5)
| ~ l1_pre_topc(sK4) ),
inference(unflattening,[status(thm)],[c_3348]) ).
tcf(c_3350,plain,
l1_pre_topc(sK5),
inference(global_subsumption_just,[status(thm)],[c_3349,c_57,c_3349]) ).
tcf(c_3407,plain,
v1_funct_1(k1_tsp_2(sK4,sK5)),
inference(backward_subsumption_resolution,[status(thm)],[c_3138,c_3343]) ).
tcf(c_3409,plain,
k4_tsp_2(sK4,sK5) = k1_tsp_2(sK4,sK5),
inference(backward_subsumption_resolution,[status(thm)],[c_3058,c_3343]) ).
tcf(c_3410,plain,
v5_pre_topc(k4_tsp_2(sK4,sK5),sK4,sK5),
inference(backward_subsumption_resolution,[status(thm)],[c_3078,c_3343]) ).
tcf(c_3412,plain,
m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)),
inference(backward_subsumption_resolution,[status(thm)],[c_3068,c_3343]) ).
tcf(c_3414,plain,
v1_funct_1(k4_tsp_2(sK4,sK5)),
inference(backward_subsumption_resolution,[status(thm)],[c_3098,c_3343]) ).
tcf(c_3426,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ v1_funct_1(k4_tsp_2(sK4,sK5))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m2_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(resolution,[status(thm)],[c_3410,c_3150]) ).
tcf(c_3428,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(global_subsumption_just,[status(thm)],[c_3426,c_57,c_3068,c_3078,c_3088,c_3098,c_3150,c_3342]) ).
tcf(c_3429,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(renaming,[status(thm)],[c_3428]) ).
tcf(c_3470,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ( u1_struct_0(sK5) != X2 )
| ( u1_struct_0(sK4) != X1 )
| ( k4_tsp_2(sK4,sK5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_427,c_3412]) ).
tcf(c_3471,plain,
m1_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)),
inference(unflattening,[status(thm)],[c_3470]) ).
tcf(c_3501,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k4_pre_topc(X1,X2,X0,X3),k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ( k4_tsp_2(sK4,sK5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_151,c_3414]) ).
tcf(c_3502,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k4_pre_topc(X0,X1,k4_tsp_2(sK4,sK5),X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(unflattening,[status(thm)],[c_3501]) ).
tcf(c_3537,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k4_pre_topc(X1,X2,X0,X3),k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ( k1_tsp_2(sK4,sK5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_151,c_3407]) ).
tcf(c_3538,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k4_pre_topc(X0,X1,k1_tsp_2(sK4,sK5),X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k1_tsp_2(sK4,sK5),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k1_tsp_2(sK4,sK5),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(unflattening,[status(thm)],[c_3537]) ).
tcf(c_3816,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_pre_topc(X1)
| ( X1 != sK4 )
| ( X0 != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_266,c_3343]) ).
tcf(c_3817,plain,
( m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4)))
| ~ l1_pre_topc(sK4) ),
inference(unflattening,[status(thm)],[c_3816]) ).
tcf(c_3818,plain,
m1_subset_1(u1_struct_0(sK5),k1_zfmisc_1(u1_struct_0(sK4))),
inference(global_subsumption_just,[status(thm)],[c_3817,c_57,c_3817]) ).
tcf(c_4350,plain,
! [X0: $i,X1: $i] :
( ( k3_tex_4(X0,X1) = X1 )
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ( X0 != sK4 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_273]) ).
tcf(c_4351,plain,
! [X0: $i] :
( ( k3_tex_4(sK4,X0) = X0 )
| ~ l1_pre_topc(sK4)
| ~ v2_pre_topc(sK4)
| ~ v4_pre_topc(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(unflattening,[status(thm)],[c_4350]) ).
tcf(c_4353,plain,
! [X0: $i] :
( ( k3_tex_4(sK4,X0) = X0 )
| ~ v4_pre_topc(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(global_subsumption_just,[status(thm)],[c_4351,c_57,c_56,c_4351]) ).
tcf(c_6209,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_269]) ).
tcf(c_6498,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_subset_1(X1,X2,X0) = k3_xboole_0(X2,X0) )
| ~ r1_tarski(X2,X1)
| ~ r1_tarski(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_1004,c_6209]) ).
tcf(c_8544,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,X0)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),X0) )
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4))) ),
inference(prop_impl_just,[status(thm)],[c_57,c_3429,c_3817]) ).
tcf(c_12801,plain,
l1_struct_0(sK4),
inference(superposition,[status(thm)],[c_57,c_157]) ).
tcf(c_12803,plain,
l1_struct_0(sK5),
inference(superposition,[status(thm)],[c_3350,c_157]) ).
tcf(c_12869,plain,
( ( k3_tex_4(sK4,sK6) = sK6 )
| ~ v4_pre_topc(sK6,sK4) ),
inference(superposition,[status(thm)],[c_51,c_4353]) ).
tcf(c_12875,plain,
k3_tex_4(sK4,sK6) = sK6,
inference(global_subsumption_just,[status(thm)],[c_12869,c_50,c_12869]) ).
tcf(c_12910,plain,
k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,sK6)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),
inference(superposition,[status(thm)],[c_51,c_8544]) ).
tcf(c_12928,plain,
k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6) = k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6),
inference(superposition,[status(thm)],[c_12875,c_12910]) ).
tcf(c_13141,plain,
( m1_subset_1(k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6),k1_zfmisc_1(u1_struct_0(sK5)))
| ~ l1_struct_0(sK5)
| ~ l1_struct_0(sK4)
| ~ m1_relset_1(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v1_funct_2(k4_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(superposition,[status(thm)],[c_12928,c_3502]) ).
tcf(c_144606,plain,
( ( k3_tex_4(sK4,sK6) = sK6 )
| ~ v4_pre_topc(sK6,sK4) ),
inference(superposition,[status(thm)],[c_51,c_4353]) ).
tcf(c_144609,plain,
k3_tex_4(sK4,sK6) = sK6,
inference(global_subsumption_just,[status(thm)],[c_144606,c_50,c_12869]) ).
tcf(c_144623,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k4_pre_topc(X0,X1,k4_tsp_2(sK4,sK5),X2),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k1_tsp_2(sK4,sK5),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k1_tsp_2(sK4,sK5),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(superposition,[status(thm)],[c_3409,c_3538]) ).
tcf(c_144636,plain,
r1_tarski(sK6,u1_struct_0(sK4)),
inference(superposition,[status(thm)],[c_51,c_270]) ).
tcf(c_144639,plain,
r1_tarski(u1_struct_0(sK5),u1_struct_0(sK4)),
inference(superposition,[status(thm)],[c_3818,c_270]) ).
tcf(c_144717,plain,
k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),k3_tex_4(sK4,sK6)) = k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6),
inference(superposition,[status(thm)],[c_51,c_8544]) ).
tcf(c_144808,plain,
k4_pre_topc(sK4,sK5,k4_tsp_2(sK4,sK5),sK6) = k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6),
inference(superposition,[status(thm)],[c_144609,c_144717]) ).
tcf(c_144821,plain,
~ v4_pre_topc(k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6),sK5),
inference(superposition,[status(thm)],[c_144808,c_49]) ).
tcf(c_144822,plain,
( m1_subset_1(k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6),k1_zfmisc_1(u1_struct_0(sK5)))
| ~ l1_struct_0(sK5)
| ~ l1_struct_0(sK4)
| ~ m1_relset_1(k1_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5))
| ~ v1_funct_2(k1_tsp_2(sK4,sK5),u1_struct_0(sK4),u1_struct_0(sK5)) ),
inference(superposition,[status(thm)],[c_144808,c_144623]) ).
tcf(c_144944,plain,
! [X0: $i] :
( ( k5_subset_1(u1_struct_0(sK4),X0,sK6) = k3_xboole_0(X0,sK6) )
| ~ r1_tarski(X0,u1_struct_0(sK4)) ),
inference(superposition,[status(thm)],[c_144636,c_6498]) ).
tcf(c_145100,plain,
k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6) = k3_xboole_0(u1_struct_0(sK5),sK6),
inference(superposition,[status(thm)],[c_144639,c_144944]) ).
tcf(c_145211,plain,
~ v4_pre_topc(k3_xboole_0(u1_struct_0(sK5),sK6),sK5),
inference(superposition,[status(thm)],[c_145100,c_144821]) ).
tcf(c_145222,plain,
~ v4_pre_topc(k3_xboole_0(sK6,u1_struct_0(sK5)),sK5),
inference(superposition,[status(thm)],[c_126,c_145211]) ).
tcf(c_154050,plain,
m1_subset_1(k5_subset_1(u1_struct_0(sK4),u1_struct_0(sK5),sK6),k1_zfmisc_1(u1_struct_0(sK5))),
inference(global_subsumption_just,[status(thm)],[c_144822,c_57,c_3088,c_3342,c_3471,c_12803,c_12801,c_13141]) ).
tcf(c_154053,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK5),sK6),k1_zfmisc_1(u1_struct_0(sK5))),
inference(superposition,[status(thm)],[c_145100,c_154050]) ).
tcf(c_154180,plain,
m1_subset_1(k3_xboole_0(sK6,u1_struct_0(sK5)),k1_zfmisc_1(u1_struct_0(sK5))),
inference(superposition,[status(thm)],[c_126,c_154053]) ).
fof(f291,definition,
! [X0,X1] :
( sP1(X0,X1)
<=> ( ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ( v4_pre_topc(X2,X1)
<=> ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f292,definition,
! [X1,X0] :
( ~ sP2(X1,X0)
| ( m2_tsp_1(X1,X0)
<=> sP1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f293,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ l1_pre_topc(X1)
| sP2(X1,X0) ) ),
inference(definition_folding,[],[f221,f292,f291]) ).
fof(f304,plain,
! [X0,X1] :
( ( ~ sP1(X0,X1)
| ( ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ( ( ~ v4_pre_topc(X2,X1)
| ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( k3_xboole_0(X3,u1_struct_0(X1)) != X2
| ~ v4_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| v4_pre_topc(X2,X1) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ( v4_pre_topc(X2,X1)
| ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ~ v4_pre_topc(X2,X1)
| ! [X3] :
( k3_xboole_0(X3,u1_struct_0(X1)) != X2
| ~ v4_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| sP1(X0,X1) ) ),
inference(nnf_transformation,[],[f291]) ).
fof(f305,plain,
! [X0,X1] :
( ( ~ sP1(X0,X1)
| ( ! [X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ( ( ~ v4_pre_topc(X2,X1)
| ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( k3_xboole_0(X3,u1_struct_0(X1)) != X2
| ~ v4_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| v4_pre_topc(X2,X1) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ( v4_pre_topc(X2,X1)
| ? [X3] :
( X2 = k3_xboole_0(X3,u1_struct_0(X1))
& v4_pre_topc(X3,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ~ v4_pre_topc(X2,X1)
| ! [X3] :
( k3_xboole_0(X3,u1_struct_0(X1)) != X2
| ~ v4_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| sP1(X0,X1) ) ),
inference(flattening,[],[f304]) ).
fof(f306,plain,
! [X0,X1] :
( ( ~ sP1(X0,X1)
| ( ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
| ( ( ~ v4_pre_topc(X5,X1)
| ? [X7] :
( k3_xboole_0(X7,u1_struct_0(X1)) = X5
& v4_pre_topc(X7,X0)
& m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X6] :
( k3_xboole_0(X6,u1_struct_0(X1)) != X5
| ~ v4_pre_topc(X6,X0)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| v4_pre_topc(X5,X1) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ( v4_pre_topc(X2,X1)
| ? [X4] :
( k3_xboole_0(X4,u1_struct_0(X1)) = X2
& v4_pre_topc(X4,X0)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ~ v4_pre_topc(X2,X1)
| ! [X3] :
( k3_xboole_0(X3,u1_struct_0(X1)) != X2
| ~ v4_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| sP1(X0,X1) ) ),
inference(rectify,[],[f305]) ).
fof(f307,plain,
! [X0,X1] :
( ( ~ sP1(X0,X1)
| ( ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
| ( ( ~ v4_pre_topc(X5,X1)
| ( k3_xboole_0(sK11(X0,X1,X5),u1_struct_0(X1)) = X5
& v4_pre_topc(sK11(X0,X1,X5),X0)
& m1_subset_1(sK11(X0,X1,X5),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X6] :
( k3_xboole_0(X6,u1_struct_0(X1)) != X5
| ~ v4_pre_topc(X6,X0)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| v4_pre_topc(X5,X1) ) ) )
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( ( m1_subset_1(sK9(X0,X1),k1_zfmisc_1(u1_struct_0(X1)))
& ( v4_pre_topc(sK9(X0,X1),X1)
| ( sK9(X0,X1) = k3_xboole_0(sK10(X0,X1),u1_struct_0(X1))
& v4_pre_topc(sK10(X0,X1),X0)
& m1_subset_1(sK10(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ~ v4_pre_topc(sK9(X0,X1),X1)
| ! [X3] :
( k3_xboole_0(X3,u1_struct_0(X1)) != sK9(X0,X1)
| ~ v4_pre_topc(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| sP1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X2,sK9(X0,X1)),skolemize(X4,sK10(X0,X1)),skolemize(X7,sK11(X0,X1,X5))],[f306]) ).
fof(f452,plain,
! [X0,X1,X6,X5] :
( ~ sP1(X0,X1)
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
| k3_xboole_0(X6,u1_struct_0(X1)) != X5
| ~ v4_pre_topc(X6,X0)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| v4_pre_topc(X5,X1) ),
inference(cnf_transformation,[],[f307]) ).
fof(f593,plain,
! [X0,X1,X6] :
( ~ sP1(X0,X1)
| ~ m1_subset_1(k3_xboole_0(X6,u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X6,X0)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| v4_pre_topc(k3_xboole_0(X6,u1_struct_0(X1)),X1) ),
inference(equality_resolution,[],[f452]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i] :
( v4_pre_topc(k3_xboole_0(X0,u1_struct_0(X1)),X1)
| ~ sP1(X2,X1)
| ~ v4_pre_topc(X0,X2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X2)))
| ~ m1_subset_1(k3_xboole_0(X0,u1_struct_0(X1)),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f593]) ).
tcf(c_5849,plain,
! [X0: $i,X1: $i,X2: $i] :
( v4_pre_topc(k3_xboole_0(X2,u1_struct_0(X0)),X0)
| ~ v4_pre_topc(X2,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(k3_xboole_0(X2,u1_struct_0(X0)),k1_zfmisc_1(u1_struct_0(X0)))
| ( X1 != sK4 )
| ( X0 != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_141,c_3336]) ).
tcf(c_5850,plain,
! [X0: $i] :
( v4_pre_topc(k3_xboole_0(X0,u1_struct_0(sK5)),sK5)
| ~ v4_pre_topc(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(k3_xboole_0(X0,u1_struct_0(sK5)),k1_zfmisc_1(u1_struct_0(sK5))) ),
inference(unflattening,[status(thm)],[c_5849]) ).
tcf(c_266692,plain,
! [X0: $i] :
( v4_pre_topc(k3_xboole_0(X0,u1_struct_0(sK5)),sK5)
| ~ sP1(sK4,sK5)
| ~ v4_pre_topc(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(k3_xboole_0(X0,u1_struct_0(sK5)),k1_zfmisc_1(u1_struct_0(sK5))) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_266874,plain,
! [X0: $i] :
( v4_pre_topc(k3_xboole_0(X0,u1_struct_0(sK5)),sK5)
| ~ m1_subset_1(k3_xboole_0(X0,u1_struct_0(sK5)),k1_zfmisc_1(u1_struct_0(sK5)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v4_pre_topc(X0,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_266692,c_5850]) ).
tcf(c_266875,plain,
! [X0: $i] :
( v4_pre_topc(k3_xboole_0(X0,u1_struct_0(sK5)),sK5)
| ~ v4_pre_topc(X0,sK4)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(k3_xboole_0(X0,u1_struct_0(sK5)),k1_zfmisc_1(u1_struct_0(sK5))) ),
inference(renaming,[status(thm)],[c_266874]) ).
tcf(c_266876,plain,
( v4_pre_topc(k3_xboole_0(sK6,u1_struct_0(sK5)),sK5)
| ~ v4_pre_topc(sK6,sK4)
| ~ m1_subset_1(sK6,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ m1_subset_1(k3_xboole_0(sK6,u1_struct_0(sK5)),k1_zfmisc_1(u1_struct_0(sK5))) ),
inference(instantiation,[status(thm)],[c_266875]) ).
tcf(c_266877,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_266876,c_154180,c_145222,c_51,c_50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP042+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.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 04:17:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 268.36/39.52 % SZS status Started for theBenchmark.p
% 268.36/39.52 % SZS status Theorem for theBenchmark.p
% 268.36/39.52
% 268.36/39.52 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 268.36/39.52
% 268.36/39.52 % ------ iProver source info
% 268.36/39.52
% 268.36/39.52 % git: date: 2026-07-19 20:42:38 +0200
% 268.36/39.52 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 268.36/39.52 % git: non_committed_changes: false
% 268.36/39.52
% 268.36/39.52 % ------ Parsing...
% 268.36/39.52 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 268.36/39.52
% 268.36/39.52 % ------ Preprocessing... sup_sim: 0 sf_s rm: 96 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 16 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 16 0s sf_e pe_s pe_e %
% 268.36/39.52
% 268.36/39.52 % ------ Preprocessing... gs_s sp: 1 0s gs_e snvd_s sp: 0 0s snvd_e %
% 268.36/39.52
% 268.36/39.52 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 268.36/39.52 % ------ Proving...
% 268.36/39.52 % ------ Problem Properties
% 268.36/39.52
% 268.36/39.52 %
% 268.36/39.52 % clauses 118
% 268.36/39.52 % conjectures 5
% 268.36/39.52 % EPR 23
% 268.36/39.52 % Horn 111
% 268.36/39.52 % unary 44
% 268.36/39.52 % binary 29
% 268.36/39.52 % lits 261
% 268.36/39.52 % lits eq 18
% 268.36/39.52 % fd_pure 0
% 268.36/39.52 % fd_pseudo 0
% 268.36/39.52 % fd_cond 1
% 268.36/39.52 % fd_pseudo_cond 1
% 268.36/39.52 % AC symbols 0
% 268.36/39.52
% 268.36/39.52 % ------ Input Options Time Limit: Unbounded
% 268.36/39.52
% 268.36/39.52
% 268.36/39.52 % ------
% 268.36/39.52 % Current options:
% 268.36/39.52 % ------
% 268.36/39.52
% 268.36/39.52
% 268.36/39.52 %
% 268.36/39.52
% 268.36/39.52 % ------ Proving...
% 268.36/39.52 %
% 268.36/39.52
% 268.36/39.52 % ------ Proving...
% 268.36/39.52 %
% 268.36/39.52
% 268.36/39.52 % ------ Proving...
% 268.36/39.52 %
% 268.36/39.52
% 268.36/39.52 % ------ Proving...
% 268.36/39.52 %
% 268.36/39.52
% 268.36/39.52 % ------ Proving...
% 268.36/39.52 %
% 268.36/39.52
% 268.36/39.52 % SZS status Theorem for theBenchmark.p
% 268.36/39.52
% 268.36/39.52 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 268.36/39.53
% 268.36/39.53
%------------------------------------------------------------------------------