%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : TOP037+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n020.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:26 PM UTC 2026
% Result : Theorem 8.36s 1.90s
% Output : CNFRefutation 8.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 30
% Syntax : Number of formulae : 245 ( 60 unt; 10 def)
% Number of atoms : 1011 ( 210 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 1126 ( 470 ~; 521 |; 100 &)
% ( 4 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 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 : 33 ( 31 usr; 11 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-4 aty)
% Number of variables : 389 ( 0 sgn 383 !; 6 ?; 194 :)
% 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)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k3_tex_4(X0,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_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)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2) = k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k3_tex_4(X0,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f21,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f51,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/sandbox/benchmark/theBenchmark.p',dt_k1_tsp_2) ).
fof(f59,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/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f62,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f67,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f68,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f77,axiom,
! [X0] :
( ( l1_struct_0(X0)
& ~ v3_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f80,axiom,
( v5_membered(k1_xboole_0)
& v4_membered(k1_xboole_0)
& v3_membered(k1_xboole_0)
& v2_membered(k1_xboole_0)
& v1_membered(k1_xboole_0)
& v1_xboole_0(k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_membered) ).
fof(f93,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,X0,X1)
& v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f94,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) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f95,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/sandbox/benchmark/theBenchmark.p',redefinition_k4_tsp_2) ).
fof(f96,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) )
=> k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_pre_topc) ).
fof(f97,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f98,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f100,axiom,
! [X0,X1] :
( ( v1_funct_1(X1)
& v1_relat_1(X1) )
=> ( r1_tarski(X0,k2_relat_1(X1))
=> k9_relat_1(X1,k10_relat_1(X1,X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t147_funct_1) ).
fof(f101,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f103,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] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> k5_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2)) = k3_tex_4(X0,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_tsp_2) ).
fof(f105,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f106,axiom,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
& v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> ( ( X1 = k1_xboole_0
=> X0 = k1_xboole_0 )
=> k2_funct_2(X0,X1,X2,X0) = k2_relat_1(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_funct_2) ).
fof(f113,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))
& 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(pure_predicate_removal,[],[f51]) ).
fof(f114,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))
& 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(pure_predicate_removal,[],[f59]) ).
fof(f142,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)))
& k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2) != k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k3_tex_4(X0,X2)) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f143,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)))
& k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2) != k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k3_tex_4(X0,X2)) ) ) ),
inference(flattening,[],[f142]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(ennf_transformation,[],[f21]) ).
fof(f206,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))
& 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,[],[f113]) ).
fof(f207,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))
& 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,[],[f206]) ).
fof(f214,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))
& 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,[],[f114]) ).
fof(f215,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))
& 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,[],[f214]) ).
fof(f218,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f220,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f67]) ).
fof(f221,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ) ),
inference(ennf_transformation,[],[f68]) ).
fof(f224,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f77]) ).
fof(f225,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(flattening,[],[f224]) ).
fof(f244,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f93]) ).
fof(f245,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(flattening,[],[f244]) ).
fof(f246,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)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f94]) ).
fof(f247,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)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(flattening,[],[f246]) ).
fof(f248,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,[],[f95]) ).
fof(f249,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,[],[f248]) ).
fof(f250,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)
| k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f96]) ).
fof(f251,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)
| k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
inference(flattening,[],[f250]) ).
fof(f252,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
inference(ennf_transformation,[],[f98]) ).
fof(f253,plain,
! [X0,X1] :
( ~ v1_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ r1_tarski(X0,k2_relat_1(X1))
| k9_relat_1(X1,k10_relat_1(X1,X0)) = X0 ),
inference(ennf_transformation,[],[f100]) ).
fof(f254,plain,
! [X0,X1] :
( ~ v1_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ r1_tarski(X0,k2_relat_1(X1))
| k9_relat_1(X1,k10_relat_1(X1,X0)) = X0 ),
inference(flattening,[],[f253]) ).
fof(f255,plain,
! [X0,X1,X2] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(ennf_transformation,[],[f101]) ).
fof(f256,plain,
! [X0,X1,X2] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(flattening,[],[f255]) ).
fof(f258,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)))
| k5_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2)) = k3_tex_4(X0,X2) ) ) ),
inference(ennf_transformation,[],[f103]) ).
fof(f259,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)))
| k5_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2)) = k3_tex_4(X0,X2) ) ) ),
inference(flattening,[],[f258]) ).
fof(f262,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ( X1 = k1_xboole_0
& k1_xboole_0 != X0 )
| k2_funct_2(X0,X1,X2,X0) = k2_relat_1(X2) ),
inference(ennf_transformation,[],[f106]) ).
fof(f263,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ( X1 = k1_xboole_0
& k1_xboole_0 != X0 )
| k2_funct_2(X0,X1,X2,X0) = k2_relat_1(X2) ),
inference(flattening,[],[f262]) ).
fof(f274,plain,
( l1_pre_topc(sK2)
& v2_pre_topc(sK2)
& ~ v3_struct_0(sK2)
& m2_tsp_1(sK3,sK2)
& v2_tsp_2(sK3,sK2)
& ~ v3_struct_0(sK3)
& m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2)))
& k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4) != k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k3_tex_4(sK2,sK4)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f143]) ).
fof(f297,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,[],[f97]) ).
fof(f298,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,[],[f252]) ).
fof(f299,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,[],[f105]) ).
fof(f300,plain,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f274]) ).
fof(f301,plain,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f274]) ).
fof(f302,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f274]) ).
fof(f303,plain,
m2_tsp_1(sK3,sK2),
inference(cnf_transformation,[],[f274]) ).
fof(f304,plain,
v2_tsp_2(sK3,sK2),
inference(cnf_transformation,[],[f274]) ).
fof(f305,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f274]) ).
fof(f306,plain,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf_transformation,[],[f274]) ).
fof(f307,plain,
k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4) != k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k3_tex_4(sK2,sK4)),
inference(cnf_transformation,[],[f274]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f163]) ).
fof(f409,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)) ),
inference(cnf_transformation,[],[f207]) ).
fof(f410,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(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f207]) ).
fof(f411,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,[],[f207]) ).
fof(f416,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,[],[f215]) ).
fof(f417,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,[],[f215]) ).
fof(f419,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f218]) ).
fof(f421,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f220]) ).
fof(f422,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f221]) ).
fof(f430,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f225]) ).
fof(f438,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f80]) ).
fof(f487,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f245]) ).
fof(f488,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)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f247]) ).
fof(f489,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,[],[f249]) ).
fof(f490,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)
| k5_pre_topc(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f251]) ).
fof(f491,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f297]) ).
fof(f492,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f297]) ).
fof(f493,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f298]) ).
fof(f496,plain,
! [X0,X1] :
( ~ v1_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ r1_tarski(X0,k2_relat_1(X1))
| k9_relat_1(X1,k10_relat_1(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f254]) ).
fof(f497,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(cnf_transformation,[],[f256]) ).
fof(f499,plain,
! [X2,X0,X1] :
( ~ 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)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| k3_tex_4(X0,X2) = k5_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2)) ),
inference(cnf_transformation,[],[f259]) ).
fof(f501,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f299]) ).
fof(f503,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k1_xboole_0 = X1
| k2_funct_2(X0,X1,X2,X0) = k2_relat_1(X2) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_49,negated_conjecture,
k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k3_tex_4(sK2,sK4)) != k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),sK4),
inference(cnf_transformation,[],[f307]) ).
tcf(c_50,negated_conjecture,
m1_subset_1(sK4,k1_zfmisc_1(u1_struct_0(sK2))),
inference(cnf_transformation,[],[f306]) ).
tcf(c_51,negated_conjecture,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f305]) ).
tcf(c_52,negated_conjecture,
v2_tsp_2(sK3,sK2),
inference(cnf_transformation,[],[f304]) ).
tcf(c_53,negated_conjecture,
m2_tsp_1(sK3,sK2),
inference(cnf_transformation,[],[f303]) ).
tcf(c_54,negated_conjecture,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f302]) ).
tcf(c_55,negated_conjecture,
v2_pre_topc(sK2),
inference(cnf_transformation,[],[f301]) ).
tcf(c_56,negated_conjecture,
l1_pre_topc(sK2),
inference(cnf_transformation,[],[f300]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_126,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,[],[f411]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_2(k1_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,[],[f410]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m2_relset_1(k1_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,[],[f409]) ).
tcf(c_132,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,[],[f417]) ).
tcf(c_133,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,[],[f416]) ).
tcf(c_136,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f419]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f421]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X0)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f422]) ).
tcf(c_147,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f430]) ).
tcf(c_150,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f438]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f487]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k4_pre_topc(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ 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,[],[f488]) ).
tcf(c_206,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,[],[f489]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k5_pre_topc(X1,X2,X0,X3) = k10_relat_1(X0,X3) )
| ~ 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,[],[f490]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(X0,X1,X2)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f492]) ).
tcf(c_209,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f491]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i] :
( m1_pre_topc(X0,X1)
| ~ l1_pre_topc(X1)
| ~ m2_tsp_1(X0,X1) ),
inference(cnf_transformation,[],[f493]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i] :
( ( k9_relat_1(X1,k10_relat_1(X1,X0)) = X0 )
| ~ v1_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ r1_tarski(X0,k2_relat_1(X1)) ),
inference(cnf_transformation,[],[f496]) ).
tcf(c_214,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f497]) ).
tcf(c_216,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| ( k5_pre_topc(X1,X2,k4_tsp_2(X1,X2),k4_pre_topc(X1,X2,k4_tsp_2(X1,X2),X0)) = k3_tex_4(X1,X0) )
| ~ l1_pre_topc(X1)
| ~ v2_pre_topc(X1)
| ~ m2_tsp_1(X2,X1)
| ~ v2_tsp_2(X2,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f499]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f501]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = k1_xboole_0 )
| ( k2_funct_2(X1,X2,X0,X1) = k2_relat_1(X0) )
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f503]) ).
tcf(c_342,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_209]) ).
tcf(c_343,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(renaming,[status(thm)],[c_342]) ).
tcf(c_344,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_208]) ).
tcf(c_410,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m1_relset_1(X0,X1,X2)
| m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(prop_impl_just,[status(thm)],[c_208,c_138]) ).
tcf(c_411,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_relset_1(X0,X1,X2) ),
inference(renaming,[status(thm)],[c_410]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = k1_xboole_0 )
| ( k2_funct_2(X1,X2,X0,X1) = k2_relat_1(X0) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(bin_hyper_res,[status(thm)],[c_221,c_344]) ).
tcf(c_3273,plain,
! [X0: $i,X1: $i] :
( m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0)
| ( X1 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_211]) ).
tcf(c_3274,plain,
( m1_pre_topc(sK3,sK2)
| ~ l1_pre_topc(sK2) ),
inference(unflattening,[status(thm)],[c_3273]) ).
tcf(c_3280,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ( X1 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_139]) ).
tcf(c_3281,plain,
( l1_pre_topc(sK3)
| ~ l1_pre_topc(sK2) ),
inference(unflattening,[status(thm)],[c_3280]) ).
tcf(c_3287,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k5_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2)) = k3_tex_4(X0,X2) )
| ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| ~ v2_tsp_2(X1,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ( X1 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_216]) ).
tcf(c_3288,plain,
! [X0: $i] :
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| ( k5_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),X0)) = k3_tex_4(sK2,X0) )
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ v2_tsp_2(sK3,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(unflattening,[status(thm)],[c_3287]) ).
tcf(c_3290,plain,
! [X0: $i] :
( ( k5_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),X0)) = k3_tex_4(sK2,X0) )
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(global_subsumption_just,[status(thm)],[c_3288,c_56,c_55,c_54,c_52,c_51,c_3288]) ).
tcf(c_3582,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 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_206]) ).
tcf(c_3583,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| ( k4_tsp_2(sK2,sK3) = k1_tsp_2(sK2,sK3) )
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(unflattening,[status(thm)],[c_3582]) ).
tcf(c_3584,plain,
k4_tsp_2(sK2,sK3) = k1_tsp_2(sK2,sK3),
inference(global_subsumption_just,[status(thm)],[c_3583,c_56,c_55,c_54,c_51,c_3274,c_3583]) ).
tcf(c_3596,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 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_133]) ).
tcf(c_3597,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(unflattening,[status(thm)],[c_3596]) ).
tcf(c_3598,plain,
v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)),
inference(global_subsumption_just,[status(thm)],[c_3597,c_56,c_55,c_54,c_51,c_3274,c_3597]) ).
tcf(c_3603,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 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_132]) ).
tcf(c_3604,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| v1_funct_1(k4_tsp_2(sK2,sK3))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(unflattening,[status(thm)],[c_3603]) ).
tcf(c_3605,plain,
v1_funct_1(k4_tsp_2(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_3604,c_56,c_55,c_54,c_51,c_3274,c_3604]) ).
tcf(c_3610,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m2_relset_1(k1_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 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_128]) ).
tcf(c_3611,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| m2_relset_1(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(unflattening,[status(thm)],[c_3610]) ).
tcf(c_3612,plain,
m2_relset_1(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)),
inference(global_subsumption_just,[status(thm)],[c_3611,c_56,c_55,c_54,c_51,c_3274,c_3611]) ).
tcf(c_3617,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v1_funct_2(k1_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 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_127]) ).
tcf(c_3618,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| v1_funct_2(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(unflattening,[status(thm)],[c_3617]) ).
tcf(c_3619,plain,
v1_funct_2(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)),
inference(global_subsumption_just,[status(thm)],[c_3618,c_56,c_55,c_54,c_51,c_3274,c_3618]) ).
tcf(c_3624,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 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_126]) ).
tcf(c_3625,plain,
( v3_struct_0(sK3)
| v3_struct_0(sK2)
| v1_funct_1(k1_tsp_2(sK2,sK3))
| ~ l1_pre_topc(sK2)
| ~ v2_pre_topc(sK2)
| ~ m1_pre_topc(sK3,sK2) ),
inference(unflattening,[status(thm)],[c_3624]) ).
tcf(c_3626,plain,
v1_funct_1(k1_tsp_2(sK2,sK3)),
inference(global_subsumption_just,[status(thm)],[c_3625,c_56,c_55,c_54,c_51,c_3274,c_3625]) ).
tcf(c_3661,plain,
! [X0: $i,X1: $i] :
( l1_pre_topc(X1)
| ~ l1_pre_topc(X0)
| ( X1 != sK3 )
| ( X0 != sK2 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_139]) ).
tcf(c_3662,plain,
( l1_pre_topc(sK3)
| ~ l1_pre_topc(sK2) ),
inference(unflattening,[status(thm)],[c_3661]) ).
tcf(c_3663,plain,
l1_pre_topc(sK3),
inference(global_subsumption_just,[status(thm)],[c_3662,c_56,c_3281]) ).
tcf(c_3716,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ( u1_struct_0(sK3) != X2 )
| ( u1_struct_0(sK2) != X1 )
| ( k1_tsp_2(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_343,c_3612]) ).
tcf(c_3717,plain,
m1_relset_1(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3)),
inference(unflattening,[status(thm)],[c_3716]) ).
tcf(c_3883,plain,
! [X0: $i] :
( ~ l1_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0))
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_51,c_147]) ).
tcf(c_3884,plain,
( ~ l1_struct_0(sK3)
| ~ v1_xboole_0(u1_struct_0(sK3)) ),
inference(unflattening,[status(thm)],[c_3883]) ).
tcf(c_4100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k5_pre_topc(X1,X2,X0,X3) = k10_relat_1(X0,X3) )
| ~ 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(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_207,c_3605]) ).
tcf(c_4101,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k10_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(unflattening,[status(thm)],[c_4100]) ).
tcf(c_4118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k4_pre_topc(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ 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(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_205,c_3605]) ).
tcf(c_4119,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k9_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1)) ),
inference(unflattening,[status(thm)],[c_4118]) ).
tcf(c_4208,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = k1_xboole_0 )
| ( k2_funct_2(X1,X2,X0,X1) = k2_relat_1(X0) )
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2)
| ( k1_tsp_2(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_746,c_3626]) ).
tcf(c_4209,plain,
! [X0: $i,X1: $i] :
( ( X1 = k1_xboole_0 )
| ( k2_funct_2(X0,X1,k1_tsp_2(sK2,sK3),X0) = k2_relat_1(k1_tsp_2(sK2,sK3)) )
| ~ m1_relset_1(k1_tsp_2(sK2,sK3),X0,X1)
| ~ v1_funct_2(k1_tsp_2(sK2,sK3),X0,X1) ),
inference(unflattening,[status(thm)],[c_4208]) ).
tcf(c_4258,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2)
| ( k1_tsp_2(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_204,c_3626]) ).
tcf(c_4259,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k2_funct_2(X0,X1,k1_tsp_2(sK2,sK3),X2) = k9_relat_1(k1_tsp_2(sK2,sK3),X2) )
| ~ m1_relset_1(k1_tsp_2(sK2,sK3),X0,X1)
| ~ v1_funct_2(k1_tsp_2(sK2,sK3),X0,X1) ),
inference(unflattening,[status(thm)],[c_4258]) ).
tcf(c_4330,plain,
! [X0: $i,X1: $i] :
( ( k9_relat_1(X0,k10_relat_1(X0,X1)) = X1 )
| ~ v1_relat_1(X0)
| ~ r1_tarski(X1,k2_relat_1(X0))
| ( k1_tsp_2(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_213,c_3626]) ).
tcf(c_4331,plain,
! [X0: $i] :
( ( k9_relat_1(k1_tsp_2(sK2,sK3),k10_relat_1(k1_tsp_2(sK2,sK3),X0)) = X0 )
| ~ v1_relat_1(k1_tsp_2(sK2,sK3))
| ~ r1_tarski(X0,k2_relat_1(k1_tsp_2(sK2,sK3))) ),
inference(unflattening,[status(thm)],[c_4330]) ).
tcf(c_4702,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k2_funct_2(X0,X1,k1_tsp_2(sK2,sK3),X2) = k9_relat_1(k1_tsp_2(sK2,sK3),X2) )
| ~ m1_relset_1(k1_tsp_2(sK2,sK3),X0,X1)
| ( u1_struct_0(sK3) != X1 )
| ( u1_struct_0(sK2) != X0 )
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(resolution_lifted,[status(thm)],[c_3598,c_4259]) ).
tcf(c_4703,plain,
! [X0: $i] :
( ( k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k1_tsp_2(sK2,sK3),X0) = k9_relat_1(k1_tsp_2(sK2,sK3),X0) )
| ~ m1_relset_1(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(unflattening,[status(thm)],[c_4702]) ).
tcf(c_4705,plain,
! [X0: $i] : k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k1_tsp_2(sK2,sK3),X0) = k9_relat_1(k1_tsp_2(sK2,sK3),X0),
inference(global_subsumption_just,[status(thm)],[c_4703,c_56,c_55,c_54,c_51,c_3274,c_3583,c_3717,c_4703]) ).
tcf(c_4711,plain,
! [X0: $i,X1: $i] :
( ( X1 = k1_xboole_0 )
| ( k2_funct_2(X0,X1,k1_tsp_2(sK2,sK3),X0) = k2_relat_1(k1_tsp_2(sK2,sK3)) )
| ~ m1_relset_1(k1_tsp_2(sK2,sK3),X0,X1)
| ( u1_struct_0(sK3) != X1 )
| ( u1_struct_0(sK2) != X0 )
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(resolution_lifted,[status(thm)],[c_3598,c_4209]) ).
tcf(c_4712,plain,
( ( u1_struct_0(sK3) = k1_xboole_0 )
| ( k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k1_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k1_tsp_2(sK2,sK3)) )
| ~ m1_relset_1(k1_tsp_2(sK2,sK3),u1_struct_0(sK2),u1_struct_0(sK3))
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(unflattening,[status(thm)],[c_4711]) ).
tcf(c_4713,plain,
( ( u1_struct_0(sK3) = k1_xboole_0 )
| ( k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k1_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k1_tsp_2(sK2,sK3)) ) ),
inference(global_subsumption_just,[status(thm)],[c_4712,c_56,c_55,c_54,c_51,c_3274,c_3583,c_3717,c_4712]) ).
tcf(c_4880,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k9_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1))
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) )
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(resolution_lifted,[status(thm)],[c_3619,c_4119]) ).
tcf(c_4882,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k9_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1))
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_4880,c_56,c_55,c_54,c_51,c_3274,c_3583,c_4880]) ).
tcf(c_4903,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k10_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1))
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) )
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(resolution_lifted,[status(thm)],[c_3619,c_4101]) ).
tcf(c_4905,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k10_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ~ m1_relset_1(k4_tsp_2(sK2,sK3),u1_struct_0(X0),u1_struct_0(X1))
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_4903,c_56,c_55,c_54,c_51,c_3274,c_3583,c_4903]) ).
tcf(c_5029,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ( u1_struct_0(sK3) != X2 )
| ( u1_struct_0(sK2) != X1 )
| ( k1_tsp_2(sK2,sK3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_411,c_3717]) ).
tcf(c_5030,plain,
m1_subset_1(k1_tsp_2(sK2,sK3),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK3)))),
inference(unflattening,[status(thm)],[c_5029]) ).
tcf(c_5576,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k10_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) )
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(resolution_lifted,[status(thm)],[c_3717,c_4905]) ).
tcf(c_5578,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k10_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_5576,c_56,c_55,c_54,c_51,c_3274,c_3583,c_5576]) ).
tcf(c_5596,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k9_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) )
| ( k4_tsp_2(sK2,sK3) != k1_tsp_2(sK2,sK3) ) ),
inference(resolution_lifted,[status(thm)],[c_3717,c_4882]) ).
tcf(c_5598,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_pre_topc(X0,X1,k4_tsp_2(sK2,sK3),X2) = k9_relat_1(k4_tsp_2(sK2,sK3),X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X1) != u1_struct_0(sK3) )
| ( u1_struct_0(X0) != u1_struct_0(sK2) ) ),
inference(global_subsumption_just,[status(thm)],[c_5596,c_56,c_55,c_54,c_51,c_3274,c_3583,c_5596]) ).
tcf(c_5820,plain,
( ( k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k1_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k1_tsp_2(sK2,sK3)) )
| ( u1_struct_0(sK3) = k1_xboole_0 ) ),
inference(prop_impl_just,[status(thm)],[c_4713]) ).
tcf(c_5821,plain,
( ( u1_struct_0(sK3) = k1_xboole_0 )
| ( k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k1_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k1_tsp_2(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_5820]) ).
tcf(c_6451,plain,
m1_subset_1(k4_tsp_2(sK2,sK3),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK3)))),
inference(light_normalisation,[status(thm)],[c_5030,c_3584]) ).
tcf(c_6533,plain,
! [X0: $i] : k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k4_tsp_2(sK2,sK3),X0) = k9_relat_1(k4_tsp_2(sK2,sK3),X0),
inference(light_normalisation,[status(thm)],[c_4705,c_3584]) ).
tcf(c_6548,plain,
( ( u1_struct_0(sK3) = k1_xboole_0 )
| ( k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),k4_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k4_tsp_2(sK2,sK3)) ) ),
inference(light_normalisation,[status(thm)],[c_5821,c_3584]) ).
tcf(c_6549,plain,
( ( u1_struct_0(sK3) = k1_xboole_0 )
| ( k9_relat_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k4_tsp_2(sK2,sK3)) ) ),
inference(demodulation,[status(thm)],[c_6548,c_6533]) ).
tcf(c_6556,plain,
! [X0: $i] :
( ( k9_relat_1(k4_tsp_2(sK2,sK3),k10_relat_1(k4_tsp_2(sK2,sK3),X0)) = X0 )
| ~ v1_relat_1(k4_tsp_2(sK2,sK3))
| ~ r1_tarski(X0,k2_relat_1(k4_tsp_2(sK2,sK3))) ),
inference(light_normalisation,[status(thm)],[c_4331,c_3584]) ).
tcf(c_6727,plain,
! [X0: $i] :
( ( k5_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),k4_pre_topc(sK2,sK3,k4_tsp_2(sK2,sK3),X0)) = k3_tex_4(sK2,X0) )
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(prop_impl_just,[status(thm)],[c_3290]) ).
tcf(c_6751,plain,
( ~ v1_xboole_0(u1_struct_0(sK3))
| ~ l1_struct_0(sK3) ),
inference(prop_impl_just,[status(thm)],[c_3884]) ).
tcf(c_6752,plain,
( ~ l1_struct_0(sK3)
| ~ v1_xboole_0(u1_struct_0(sK3)) ),
inference(renaming,[status(thm)],[c_6751]) ).
tcf(c_6771,plain,
( ( k9_relat_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k4_tsp_2(sK2,sK3)) )
| ( u1_struct_0(sK3) = k1_xboole_0 ) ),
inference(prop_impl_just,[status(thm)],[c_6549]) ).
tcf(c_6772,plain,
( ( u1_struct_0(sK3) = k1_xboole_0 )
| ( k9_relat_1(k4_tsp_2(sK2,sK3),u1_struct_0(sK2)) = k2_relat_1(k4_tsp_2(sK2,sK3)) ) ),
inference(renaming,[status(thm)],[c_6771]) ).
tcf(c_7525,definition,
iPr_def_10 = k4_tsp_2(sK2,sK3),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_7526,definition,
iPr_def_11 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_7528,definition,
iPr_def_13 = u1_struct_0(sK2),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_7529,definition,
iPr_def_14 = k2_zfmisc_1(iPr_def_13,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_7530,definition,
iPr_def_15 = k1_zfmisc_1(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_7534,definition,
iPr_def_19 = k2_relat_1(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_7536,definition,
iPr_def_21 = k1_zfmisc_1(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_7541,definition,
iPr_def_26 = k3_tex_4(sK2,sK4),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_7542,definition,
iPr_def_27 = k4_pre_topc(sK2,sK3,iPr_def_10,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_7543,definition,
iPr_def_28 = k4_pre_topc(sK2,sK3,iPr_def_10,sK4),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_7547,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k4_pre_topc(X0,X1,iPr_def_10,X2) = k9_relat_1(iPr_def_10,X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X1) != iPr_def_11 )
| ( u1_struct_0(X0) != iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_5598]) ).
tcf(c_7548,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k5_pre_topc(X0,X1,iPr_def_10,X2) = k10_relat_1(iPr_def_10,X2) )
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X1) != iPr_def_11 )
| ( u1_struct_0(X0) != iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_5578]) ).
tcf(c_7549,plain,
m1_subset_1(iPr_def_10,iPr_def_15),
inference(demodulation,[status(thm)],[c_6451,c_7529,c_7530]) ).
tcf(c_7552,plain,
! [X0: $i] :
( ( k9_relat_1(iPr_def_10,k10_relat_1(iPr_def_10,X0)) = X0 )
| ~ v1_relat_1(iPr_def_10)
| ~ r1_tarski(X0,iPr_def_19) ),
inference(demodulation,[status(thm)],[c_6556,c_7534]) ).
tcf(c_7563,plain,
l1_pre_topc(sK3),
inference(demodulation,[status(thm)],[c_3663]) ).
tcf(c_7564,negated_conjecture,
l1_pre_topc(sK2),
inference(demodulation,[status(thm)],[c_56]) ).
tcf(c_7566,negated_conjecture,
m1_subset_1(sK4,iPr_def_21),
inference(demodulation,[status(thm)],[c_50]) ).
tcf(c_7567,negated_conjecture,
iPr_def_27 != iPr_def_28,
inference(demodulation,[status(thm)],[c_49,c_7543,c_7541,c_7542]) ).
tcf(c_9223,plain,
( ( k1_xboole_0 = iPr_def_11 )
| ( k9_relat_1(iPr_def_10,iPr_def_13) = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_6772,c_7525,c_7526,c_7528,c_7534]) ).
tcf(c_9234,plain,
l1_struct_0(sK2),
inference(superposition,[status(thm)],[c_7564,c_136]) ).
tcf(c_9236,plain,
l1_struct_0(sK3),
inference(superposition,[status(thm)],[c_7563,c_136]) ).
tcf(c_9330,plain,
! [X0: $i,X1: $i] :
( ( k5_pre_topc(sK2,X0,iPr_def_10,X1) = k10_relat_1(iPr_def_10,X1) )
| ~ l1_struct_0(sK2)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X0) != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_7528,c_7548]) ).
tcf(c_9331,plain,
! [X0: $i,X1: $i] :
( ( k4_pre_topc(sK2,X0,iPr_def_10,X1) = k9_relat_1(iPr_def_10,X1) )
| ~ l1_struct_0(sK2)
| ~ l1_struct_0(X0)
| ( u1_struct_0(X0) != iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_7528,c_7547]) ).
tcf(c_9343,plain,
! [X0: $i,X1: $i] :
( ( k4_pre_topc(sK2,X0,iPr_def_10,X1) = k9_relat_1(iPr_def_10,X1) )
| ~ l1_struct_0(X0)
| ( u1_struct_0(X0) != iPr_def_11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9331,c_9234]) ).
tcf(c_9347,plain,
! [X0: $i,X1: $i] :
( ( k5_pre_topc(sK2,X0,iPr_def_10,X1) = k10_relat_1(iPr_def_10,X1) )
| ~ l1_struct_0(X0)
| ( u1_struct_0(X0) != iPr_def_11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9330,c_9234]) ).
tcf(c_9402,plain,
! [X0: $i] :
( ( k4_pre_topc(sK2,sK3,iPr_def_10,X0) = k9_relat_1(iPr_def_10,X0) )
| ~ l1_struct_0(sK3) ),
inference(superposition,[status(thm)],[c_7526,c_9343]) ).
tcf(c_9403,plain,
! [X0: $i] : k4_pre_topc(sK2,sK3,iPr_def_10,X0) = k9_relat_1(iPr_def_10,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_9402,c_9236]) ).
tcf(c_9420,plain,
! [X0: $i] :
( ( k5_pre_topc(sK2,sK3,iPr_def_10,X0) = k10_relat_1(iPr_def_10,X0) )
| ~ l1_struct_0(sK3) ),
inference(superposition,[status(thm)],[c_7526,c_9347]) ).
tcf(c_9421,plain,
! [X0: $i] : k5_pre_topc(sK2,sK3,iPr_def_10,X0) = k10_relat_1(iPr_def_10,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_9420,c_9236]) ).
tcf(c_9633,plain,
k9_relat_1(iPr_def_10,iPr_def_26) = iPr_def_27,
inference(demodulation,[status(thm)],[c_7542,c_9403]) ).
tcf(c_9665,plain,
! [X0: $i] :
( r1_tarski(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_21) ),
inference(superposition,[status(thm)],[c_7536,c_219]) ).
tcf(c_9709,plain,
~ v1_xboole_0(u1_struct_0(sK3)),
inference(global_subsumption_just,[status(thm)],[c_6752,c_3884,c_9236]) ).
tcf(c_9711,plain,
~ v1_xboole_0(iPr_def_11),
inference(light_normalisation,[status(thm)],[c_9709,c_7526]) ).
tcf(c_9713,plain,
k9_relat_1(iPr_def_10,sK4) = iPr_def_28,
inference(demodulation,[status(thm)],[c_7543,c_9403]) ).
tcf(c_9723,plain,
! [X0: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(iPr_def_14)) ),
inference(superposition,[status(thm)],[c_7529,c_83]) ).
tcf(c_9724,plain,
! [X0: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,iPr_def_15) ),
inference(light_normalisation,[status(thm)],[c_9723,c_7530]) ).
tcf(c_9768,plain,
v1_relat_1(iPr_def_10),
inference(superposition,[status(thm)],[c_7549,c_9724]) ).
tcf(c_9777,plain,
! [X0: $i] :
( ( k9_relat_1(iPr_def_10,k10_relat_1(iPr_def_10,X0)) = X0 )
| ~ r1_tarski(X0,iPr_def_19) ),
inference(backward_subsumption_resolution,[status(thm)],[c_7552,c_9768]) ).
tcf(c_10092,plain,
! [X0: $i] :
( r1_tarski(k9_relat_1(iPr_def_10,X0),iPr_def_19)
| ( k1_xboole_0 = iPr_def_11 )
| ~ v1_relat_1(iPr_def_10)
| ~ r1_tarski(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_9223,c_214]) ).
tcf(c_10118,plain,
! [X0: $i] :
( r1_tarski(k9_relat_1(iPr_def_10,X0),iPr_def_19)
| ( k1_xboole_0 = iPr_def_11 )
| ~ r1_tarski(X0,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10092,c_9768]) ).
tcf(c_10148,plain,
! [X0: $i] :
( ( k5_pre_topc(sK2,sK3,iPr_def_10,k9_relat_1(iPr_def_10,X0)) = k3_tex_4(sK2,X0) )
| ~ m1_subset_1(X0,iPr_def_21) ),
inference(light_normalisation,[status(thm)],[c_6727,c_7525,c_7528,c_7536,c_9403]) ).
tcf(c_10149,plain,
! [X0: $i] :
( ( k10_relat_1(iPr_def_10,k9_relat_1(iPr_def_10,X0)) = k3_tex_4(sK2,X0) )
| ~ m1_subset_1(X0,iPr_def_21) ),
inference(demodulation,[status(thm)],[c_10148,c_9421]) ).
tcf(c_10159,plain,
k10_relat_1(iPr_def_10,k9_relat_1(iPr_def_10,sK4)) = k3_tex_4(sK2,sK4),
inference(superposition,[status(thm)],[c_7566,c_10149]) ).
tcf(c_10171,plain,
k10_relat_1(iPr_def_10,iPr_def_28) = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_10159,c_7541,c_9713]) ).
tcf(c_10730,plain,
! [X0: $i] :
( ( k1_xboole_0 = iPr_def_11 )
| ( k9_relat_1(iPr_def_10,k10_relat_1(iPr_def_10,k9_relat_1(iPr_def_10,X0))) = k9_relat_1(iPr_def_10,X0) )
| ~ r1_tarski(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_10118,c_9777]) ).
tcf(c_11266,plain,
r1_tarski(sK4,iPr_def_13),
inference(superposition,[status(thm)],[c_7566,c_9665]) ).
tcf(c_11388,plain,
( ( k1_xboole_0 = iPr_def_11 )
| ( k9_relat_1(iPr_def_10,k10_relat_1(iPr_def_10,k9_relat_1(iPr_def_10,sK4))) = k9_relat_1(iPr_def_10,sK4) ) ),
inference(superposition,[status(thm)],[c_11266,c_10730]) ).
tcf(c_11389,plain,
( ( iPr_def_27 = iPr_def_28 )
| ( k1_xboole_0 = iPr_def_11 ) ),
inference(light_normalisation,[status(thm)],[c_11388,c_9633,c_9713,c_10171]) ).
tcf(c_11390,plain,
k1_xboole_0 = iPr_def_11,
inference(forward_subsumption_resolution,[status(thm)],[c_11389,c_7567]) ).
tcf(c_11421,plain,
v1_xboole_0(iPr_def_11),
inference(demodulation,[status(thm)],[c_150,c_11390]) ).
tcf(c_11425,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_11421,c_9711]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP037+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.54 % Computer : n020.cluster.edu
% 0.08/0.54 % Model : x86_64 x86_64
% 0.08/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.54 % Memory : 8046.5625MB
% 0.08/0.54 % OS : Linux 6.8.0-71-generic
% 0.08/0.54 % CPULimit : 300
% 0.08/0.54 % WCLimit : 300
% 0.08/0.54 % DateTime : Fri Sep 25 04:16:20 UTC 2026
% 0.08/0.54 % CPUTime :
% 0.08/0.54 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.58 Running first-order theorem proving
% 0.13/0.58 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.59
% 0.13/0.59 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.59
% 0.13/0.59 % Detected problem language: tptp
% 0.13/0.60 % Proving...
% 8.36/1.90 % SZS status Started for theBenchmark.p
% 8.36/1.90 % SZS status Theorem for theBenchmark.p
% 8.36/1.90
% 8.36/1.90 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.36/1.90
% 8.36/1.90 % ------ iProver source info
% 8.36/1.90
% 8.36/1.90 % git: date: 2026-07-19 20:42:38 +0200
% 8.36/1.90 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.36/1.90 % git: non_committed_changes: false
% 8.36/1.90
% 8.36/1.90 % ------ Parsing...
% 8.36/1.90 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.36/1.90
% 8.36/1.90 % ------ Preprocessing... sup_sim: 0 sf_s rm: 66 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 19 sf_s rm: 18 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 18 0s sf_e pe_s pe_e %
% 8.36/1.90
% 8.36/1.90 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.36/1.90
% 8.36/1.90 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.36/1.90 % ------ Proving...
% 8.36/1.90 % ------ Problem Properties
% 8.36/1.90
% 8.36/1.90 %
% 8.36/1.90 % clauses 101
% 8.36/1.90 % conjectures 4
% 8.36/1.90 % EPR 32
% 8.36/1.90 % Horn 97
% 8.36/1.90 % unary 52
% 8.36/1.90 % binary 25
% 8.36/1.90 % lits 182
% 8.36/1.90 % lits eq 43
% 8.36/1.90 % fd_pure 0
% 8.36/1.90 % fd_pseudo 0
% 8.36/1.90 % fd_cond 1
% 8.36/1.90 % fd_pseudo_cond 1
% 8.36/1.90 % AC symbols 0
% 8.36/1.90
% 8.36/1.90 % ------ Schedule dynamic 5 is on
% 8.36/1.90
% 8.36/1.90 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.36/1.90
% 8.36/1.90
% 8.36/1.90 % ------
% 8.36/1.90 % Current options:
% 8.36/1.90 % ------
% 8.36/1.90
% 8.36/1.90
% 8.36/1.90 %
% 8.36/1.90
% 8.36/1.90 % ------ Proving...
% 8.36/1.90 %
% 8.36/1.90
% 8.36/1.90 % SZS status Theorem for theBenchmark.p
% 8.36/1.90
% 8.36/1.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.36/1.91
% 8.36/1.91
%------------------------------------------------------------------------------