%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP042+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:34:04 PM UTC 2026
% Result : Theorem 30.56s 5.83s
% Output : Refutation 32.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 17
% Syntax : Number of formulae : 202 ( 51 unt; 0 def)
% Number of atoms : 934 ( 154 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 1249 ( 517 ~; 577 |; 112 &)
% ( 8 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 3 con; 0-4 aty)
% Number of variables : 286 ( 268 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21,axiom,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f572,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k5_subset_1) ).
fof(f574,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f602,axiom,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_setfam_1) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6850,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f13332,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(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/sandbox/benchmark/theBenchmark.p',t62_tex_4) ).
fof(f13426,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( v4_pre_topc(X2,X0)
& ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ~ ( v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_tsp_1) ).
fof(f13459,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(f13461,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(f13469,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& 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)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f13470,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_tsp_2) ).
fof(f13489,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f13507,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_tsp_2) ).
fof(f13527,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( 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/sandbox/benchmark/theBenchmark.p',d12_tsp_2) ).
fof(f13534,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [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/sandbox/benchmark/theBenchmark.p',t35_tsp_2) ).
fof(f13535,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [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)],[f13534]) ).
fof(f13617,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& 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)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f13469]) ).
fof(f13618,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& 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)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f13617]) ).
fof(f13619,plain,
! [X0,X1] :
( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f13470]) ).
fof(f13620,plain,
! [X0,X1] :
( k4_tsp_2(X0,X1) = k1_tsp_2(X0,X1)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f13619]) ).
fof(f13657,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13489]) ).
fof(f13658,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13657]) ).
fof(f13693,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v4_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13507]) ).
fof(f13694,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v4_pre_topc(X2,X0)
<=> ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13693]) ).
fof(f13733,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13527]) ).
fof(f13734,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13733]) ).
fof(f13747,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v4_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13535]) ).
fof(f13748,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ v4_pre_topc(k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),X1)
& v4_pre_topc(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f13747]) ).
fof(f13869,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f574]) ).
fof(f13870,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f13869]) ).
fof(f13873,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f572]) ).
fof(f13874,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k5_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f13873]) ).
fof(f13998,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13332]) ).
fof(f13999,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13998]) ).
fof(f14256,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13461]) ).
fof(f14258,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13459]) ).
fof(f14259,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ v4_pre_topc(X2,X0)
| ? [X3] :
( v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13426]) ).
fof(f14260,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ v4_pre_topc(X2,X0)
| ? [X3] :
( v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f14259]) ).
fof(f14894,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6850]) ).
fof(f15096,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f20703,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f13694]) ).
fof(f20704,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X3,X1)
& X3 = k3_xboole_0(X2,u1_struct_0(X1)) ) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f20703]) ).
fof(f20705,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& ? [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(X4,X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = X4 ) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f20704]) ).
fof(f20706,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v4_pre_topc(X2,X0)
| k3_tex_4(X0,X2) != X2
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v4_pre_topc(X3,X1)
| k3_xboole_0(X2,u1_struct_0(X1)) != X3 ) )
& ( ( X2 = k3_tex_4(X0,X2)
& m1_subset_1(sK64(X1,X2),k1_zfmisc_1(u1_struct_0(X1)))
& v4_pre_topc(sK64(X1,X2),X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = sK64(X1,X2) )
| ~ v4_pre_topc(X2,X0) ) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64]),skolemize(X4,sK64(X1,X2))],[f20705]) ).
fof(f20719,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ? [X3] :
( ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
& u1_struct_0(X1) = X3
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f13734]) ).
fof(f20720,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ? [X3] :
( ? [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) != k4_pre_topc(X0,X1,X2,X4)
& m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
& u1_struct_0(X1) = X3
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X5] :
( ! [X6] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f20719]) ).
fof(f20721,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK73(X0,X1,X2),k3_tex_4(X0,sK74(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK74(X0,X1,X2))
& m1_subset_1(sK74(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK73(X0,X1,X2)
& m1_subset_1(sK73(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ! [X5] :
( ! [X6] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
| k4_tsp_2(X0,X1) != X2 ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73,sK74]),skolemize(X3,sK73(X0,X1,X2)),skolemize(X4,sK74(X0,X1,X2))],[f20720]) ).
fof(f20722,plain,
( ~ v4_pre_topc(k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),sK77),sK76)
& v4_pre_topc(sK77,sK75)
& m1_subset_1(sK77,k1_zfmisc_1(u1_struct_0(sK75)))
& ~ v3_struct_0(sK76)
& v2_tsp_2(sK76,sK75)
& m2_tsp_1(sK76,sK75)
& ~ v3_struct_0(sK75)
& v2_pre_topc(sK75)
& l1_pre_topc(sK75) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75,sK76,sK77]),skolemize(X0,sK75),skolemize(X1,sK76),skolemize(X2,sK77)],[f13748]) ).
fof(f20897,plain,
! [X0] :
( ! [X1] :
( ( m2_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f14256]) ).
fof(f20899,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ~ v4_pre_topc(X2,X0)
| ( v4_pre_topc(sK171(X1,X2),X1)
& k3_xboole_0(X2,u1_struct_0(X1)) = sK171(X1,X2)
& m1_subset_1(sK171(X1,X2),k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK171]),skolemize(X3,sK171(X1,X2))],[f14260]) ).
fof(f22977,plain,
! [X0,X1] :
( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f13618]) ).
fof(f22978,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f13618]) ).
fof(f22979,plain,
! [X0,X1] :
( v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f13618]) ).
fof(f22980,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| v1_funct_1(k4_tsp_2(X0,X1)) ),
inference(cnf_transformation,[],[f13618]) ).
fof(f22981,plain,
! [X0,X1] :
( ~ m1_pre_topc(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| k1_tsp_2(X0,X1) = k4_tsp_2(X0,X1) ),
inference(cnf_transformation,[],[f13620]) ).
fof(f23033,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13658]) ).
fof(f23088,plain,
! [X2,X0,X1] :
( k3_xboole_0(X2,u1_struct_0(X1)) = sK64(X1,X2)
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20706]) ).
fof(f23139,plain,
! [X2,X0,X1,X6,X5] :
( k5_subset_1(u1_struct_0(X0),X5,k3_tex_4(X0,X6)) = k4_pre_topc(X0,X1,X2,X6)
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X1) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
| k4_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20721]) ).
fof(f23152,plain,
l1_pre_topc(sK75),
inference(cnf_transformation,[],[f20722]) ).
fof(f23153,plain,
v2_pre_topc(sK75),
inference(cnf_transformation,[],[f20722]) ).
fof(f23154,plain,
~ v3_struct_0(sK75),
inference(cnf_transformation,[],[f20722]) ).
fof(f23155,plain,
m2_tsp_1(sK76,sK75),
inference(cnf_transformation,[],[f20722]) ).
fof(f23156,plain,
v2_tsp_2(sK76,sK75),
inference(cnf_transformation,[],[f20722]) ).
fof(f23157,plain,
~ v3_struct_0(sK76),
inference(cnf_transformation,[],[f20722]) ).
fof(f23158,plain,
m1_subset_1(sK77,k1_zfmisc_1(u1_struct_0(sK75))),
inference(cnf_transformation,[],[f20722]) ).
fof(f23159,plain,
v4_pre_topc(sK77,sK75),
inference(cnf_transformation,[],[f20722]) ).
fof(f23160,plain,
~ v4_pre_topc(k4_pre_topc(sK75,sK76,k4_tsp_2(sK75,sK76),sK77),sK76),
inference(cnf_transformation,[],[f20722]) ).
fof(f23387,plain,
! [X2,X0,X1] :
( k3_xboole_0(X1,X2) = k5_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f13870]) ).
fof(f23389,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) = k5_subset_1(X0,X2,X1) ),
inference(cnf_transformation,[],[f13874]) ).
fof(f23514,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| k3_tex_4(X0,X1) = X1
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13999]) ).
fof(f23854,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| m1_pre_topc(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20897]) ).
fof(f23857,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1) ),
inference(cnf_transformation,[],[f14258]) ).
fof(f23859,plain,
! [X2,X0,X1] :
( ~ v4_pre_topc(X2,X0)
| k3_xboole_0(X2,u1_struct_0(X1)) = sK171(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20899]) ).
fof(f23860,plain,
! [X2,X0,X1] :
( ~ m2_tsp_1(X1,X0)
| v4_pre_topc(sK171(X1,X2),X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_pre_topc(X2,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f20899]) ).
fof(f24963,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14894]) ).
fof(f25059,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f25259,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f15096]) ).
fof(f26351,plain,
! [X0,X1] : k2_tarski(X0,X1) = k2_tarski(X1,X0),
inference(cnf_transformation,[],[f21]) ).
fof(f26722,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f602]) ).
fof(f33002,plain,
! [X2,X0,X1] :
( sK64(X1,X2) = k4_xboole_0(X2,k4_xboole_0(X2,u1_struct_0(X1)))
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f23088,f25059]) ).
fof(f33008,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k4_xboole_0(X1,k4_xboole_0(X1,X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(definition_unfolding,[],[f23387,f25059]) ).
fof(f33022,plain,
! [X2,X0,X1] :
( ~ v4_pre_topc(X2,X0)
| sK171(X1,X2) = k4_xboole_0(X2,k4_xboole_0(X2,u1_struct_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(definition_unfolding,[],[f23859,f25059]) ).
fof(f33699,plain,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k1_setfam_1(k2_tarski(X0,X1)),
inference(definition_unfolding,[],[f26722,f25059]) ).
fof(f35116,plain,
! [X2,X0,X1,X6] :
( k4_pre_topc(X0,X1,X2,X6) = k5_subset_1(u1_struct_0(X0),u1_struct_0(X1),k3_tex_4(X0,X6))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| k4_tsp_2(X0,X1) != X2
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f23139]) ).
fof(f35117,plain,
! [X0,X1,X6] :
( ~ v1_funct_1(k4_tsp_2(X0,X1))
| ~ m1_subset_1(X6,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(u1_struct_0(X1),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)
| ~ v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ 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))
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f35116]) ).
fof(f36676,plain,
! [X2,X0,X1] :
( ~ m2_tsp_1(X1,X0)
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| sK171(X1,X2) = k1_setfam_1(k2_tarski(X2,u1_struct_0(X1)))
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f33022,f33699]) ).
fof(f36718,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) = k1_setfam_1(k2_tarski(X1,X2)) ),
inference(forward_demodulation,[],[f33008,f33699]) ).
fof(f36734,plain,
! [X2,X0,X1] :
( ~ v2_pre_topc(X0)
| ~ v4_pre_topc(X2,X0)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0)
| v3_struct_0(X0)
| sK64(X1,X2) = k1_setfam_1(k2_tarski(X2,u1_struct_0(X1)))
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f33002,f33699]) ).
fof(f37122,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK75)
| l1_pre_topc(X0) ),
inference(resolution,[],[f23857,f23152]) ).
fof(f37123,plain,
l1_pre_topc(sK76),
inference(resolution,[],[f37122,f23155]) ).
fof(f37127,plain,
( m1_pre_topc(sK76,sK75)
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23854,f23155]) ).
fof(f37128,plain,
m1_pre_topc(sK76,sK75),
inference(forward_subsumption_resolution,[],[f37127,f23152]) ).
fof(f37129,plain,
( v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_1(k4_tsp_2(sK75,sK76)) ),
inference(resolution,[],[f37128,f22980]) ).
fof(f37130,plain,
( v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(resolution,[],[f37128,f22981]) ).
fof(f37131,plain,
( ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37130,f23154]) ).
fof(f37132,plain,
( ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_1(k4_tsp_2(sK75,sK76)) ),
inference(forward_subsumption_resolution,[],[f37129,f23154]) ).
fof(f37133,plain,
( ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37131,f23153]) ).
fof(f37134,plain,
( ~ l1_pre_topc(sK75)
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_1(k4_tsp_2(sK75,sK76)) ),
inference(forward_subsumption_resolution,[],[f37132,f23153]) ).
fof(f37135,plain,
( v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37133,f23152]) ).
fof(f37136,plain,
( v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| v1_funct_1(k4_tsp_2(sK75,sK76)) ),
inference(forward_subsumption_resolution,[],[f37134,f23152]) ).
fof(f37137,plain,
( ~ v2_tsp_2(sK76,sK75)
| k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76) ),
inference(forward_subsumption_resolution,[],[f37135,f23157]) ).
fof(f37138,plain,
( ~ v2_tsp_2(sK76,sK75)
| v1_funct_1(k4_tsp_2(sK75,sK76)) ),
inference(forward_subsumption_resolution,[],[f37136,f23157]) ).
fof(f37139,plain,
k4_tsp_2(sK75,sK76) = k1_tsp_2(sK75,sK76),
inference(forward_subsumption_resolution,[],[f37137,f23156]) ).
fof(f37140,plain,
v1_funct_1(k4_tsp_2(sK75,sK76)),
inference(forward_subsumption_resolution,[],[f37138,f23156]) ).
fof(f37141,plain,
v1_funct_1(k1_tsp_2(sK75,sK76)),
inference(forward_demodulation,[],[f37140,f37139]) ).
fof(f37142,plain,
~ v4_pre_topc(k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),sK77),sK76),
inference(superposition,[],[f23160,f37139]) ).
fof(f37143,plain,
! [X0] :
( ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ m1_subset_1(u1_struct_0(sK76),k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f35117,f37139]) ).
fof(f37147,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f25259,f24963]) ).
fof(f37148,plain,
u1_struct_0(sK75) = k2_pre_topc(sK75),
inference(resolution,[],[f37147,f23152]) ).
fof(f37149,plain,
u1_struct_0(sK76) = k2_pre_topc(sK76),
inference(resolution,[],[f37147,f37123]) ).
fof(f37150,plain,
m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75))),
inference(superposition,[],[f23158,f37148]) ).
fof(f37151,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(superposition,[],[f22977,f37148]) ).
fof(f37153,plain,
! [X0] :
( v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(superposition,[],[f22979,f37148]) ).
fof(f37155,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(X0,sK75)
| v3_struct_0(sK75)
| ~ l1_pre_topc(sK75) ),
inference(superposition,[],[f23033,f37148]) ).
fof(f37185,plain,
! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(X0,sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37155,f23154]) ).
fof(f37187,plain,
! [X0] :
( v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37153,f23154]) ).
fof(f37189,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37151,f23154]) ).
fof(f37192,plain,
! [X0] :
( ~ m2_tsp_1(X0,sK75)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_subsumption_resolution,[],[f37185,f23152]) ).
fof(f37193,plain,
! [X0] :
( v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37187,f23153]) ).
fof(f37194,plain,
! [X0] :
( m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37189,f23153]) ).
fof(f37197,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| v1_funct_2(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37193,f23152]) ).
fof(f37198,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| m2_relset_1(k4_tsp_2(sK75,X0),k2_pre_topc(sK75),u1_struct_0(X0))
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37194,f23152]) ).
fof(f37255,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| v3_struct_0(sK75)
| k3_tex_4(sK75,X0) = X0
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23514,f23153]) ).
fof(f37256,plain,
! [X0] :
( v3_struct_0(sK75)
| v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(resolution,[],[f22978,f23153]) ).
fof(f37257,plain,
! [X0] :
( v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ l1_pre_topc(sK75)
| v3_struct_0(X0)
| ~ v2_tsp_2(X0,sK75)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37256,f23154]) ).
fof(f37258,plain,
! [X0] :
( ~ v2_tsp_2(X0,sK75)
| v3_struct_0(X0)
| v5_pre_topc(k4_tsp_2(sK75,X0),sK75,X0)
| ~ m1_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37257,f23152]) ).
fof(f37259,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| v3_struct_0(sK75)
| sK64(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f36734,f23153]) ).
fof(f37281,plain,
( v3_struct_0(sK76)
| v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m1_pre_topc(sK76,sK75) ),
inference(resolution,[],[f37258,f23156]) ).
fof(f37282,plain,
( v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76)
| ~ m1_pre_topc(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37281,f23157]) ).
fof(f37283,plain,
v5_pre_topc(k4_tsp_2(sK75,sK76),sK75,sK76),
inference(forward_subsumption_resolution,[],[f37282,f37128]) ).
fof(f37284,plain,
v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76),
inference(forward_demodulation,[],[f37283,f37139]) ).
fof(f37302,plain,
( v3_struct_0(sK76)
| v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m1_pre_topc(sK76,sK75) ),
inference(resolution,[],[f37197,f23156]) ).
fof(f37303,plain,
( v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m1_pre_topc(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37302,f23157]) ).
fof(f37304,plain,
v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)),
inference(forward_subsumption_resolution,[],[f37303,f37128]) ).
fof(f37305,plain,
v1_funct_2(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37304,f37149]) ).
fof(f37306,plain,
v1_funct_2(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37305,f37139]) ).
fof(f37307,plain,
( v3_struct_0(sK76)
| m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m1_pre_topc(sK76,sK75) ),
inference(resolution,[],[f37198,f23156]) ).
fof(f37308,plain,
( m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76))
| ~ m1_pre_topc(sK76,sK75) ),
inference(forward_subsumption_resolution,[],[f37307,f23157]) ).
fof(f37309,plain,
m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),u1_struct_0(sK76)),
inference(forward_subsumption_resolution,[],[f37308,f37128]) ).
fof(f37310,plain,
m2_relset_1(k4_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37309,f37149]) ).
fof(f37311,plain,
m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f37310,f37139]) ).
fof(f37331,plain,
m1_subset_1(u1_struct_0(sK76),k1_zfmisc_1(k2_pre_topc(sK75))),
inference(resolution,[],[f37192,f23155]) ).
fof(f37332,plain,
m1_subset_1(k2_pre_topc(sK76),k1_zfmisc_1(k2_pre_topc(sK75))),
inference(forward_demodulation,[],[f37331,f37149]) ).
fof(f37345,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k3_tex_4(sK75,X0) = X0
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37255,f23154]) ).
fof(f37346,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| sK64(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1)))
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37259,f23154]) ).
fof(f37351,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k3_tex_4(sK75,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f37345,f23152]) ).
fof(f37352,plain,
! [X0,X1] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v2_tsp_2(X1,sK75)
| ~ m2_tsp_1(X1,sK75)
| sK64(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1))) ),
inference(forward_subsumption_resolution,[],[f37346,f23152]) ).
fof(f37357,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v4_pre_topc(X0,sK75)
| k3_tex_4(sK75,X0) = X0 ),
inference(forward_demodulation,[],[f37351,f37148]) ).
fof(f37358,plain,
! [X0,X1] :
( ~ v2_tsp_2(X1,sK75)
| ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(X1,sK75)
| sK64(X1,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(X1))) ),
inference(forward_demodulation,[],[f37352,f37148]) ).
fof(f37363,plain,
( ~ v4_pre_topc(sK77,sK75)
| sK77 = k3_tex_4(sK75,sK77) ),
inference(resolution,[],[f37357,f37150]) ).
fof(f37372,plain,
sK77 = k3_tex_4(sK75,sK77),
inference(forward_subsumption_resolution,[],[f37363,f23159]) ).
fof(f37380,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_tsp_1(sK76,sK75)
| sK64(sK76,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) ),
inference(resolution,[],[f37358,f23156]) ).
fof(f37381,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| sK64(sK76,X0) = k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) ),
inference(forward_subsumption_resolution,[],[f37380,f23155]) ).
fof(f37382,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v4_pre_topc(X0,sK75)
| sK64(sK76,X0) = k1_setfam_1(k2_tarski(X0,k2_pre_topc(sK76))) ),
inference(forward_demodulation,[],[f37381,f37149]) ).
fof(f37383,plain,
( ~ v4_pre_topc(sK77,sK75)
| sK64(sK76,sK77) = k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) ),
inference(resolution,[],[f37382,f37150]) ).
fof(f37385,plain,
sK64(sK76,sK77) = k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))),
inference(forward_subsumption_resolution,[],[f37383,f23159]) ).
fof(f37479,plain,
! [X0] :
( v4_pre_topc(sK171(sK76,X0),sK76)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v4_pre_topc(X0,sK75)
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f23860,f23155]) ).
fof(f37480,plain,
! [X0] :
( v4_pre_topc(sK171(sK76,X0),sK76)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| ~ v4_pre_topc(X0,sK75) ),
inference(forward_subsumption_resolution,[],[f37479,f23152]) ).
fof(f37481,plain,
! [X0] :
( v4_pre_topc(sK171(sK76,X0),sK76)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v4_pre_topc(X0,sK75) ),
inference(forward_demodulation,[],[f37480,f37148]) ).
fof(f37528,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k5_subset_1(k2_pre_topc(sK75),X0,sK77) = k5_subset_1(k2_pre_topc(sK75),sK77,X0) ),
inference(resolution,[],[f23389,f37150]) ).
fof(f37534,plain,
k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77) = k5_subset_1(k2_pre_topc(sK75),sK77,k2_pre_topc(sK76)),
inference(resolution,[],[f37528,f37332]) ).
fof(f37842,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k5_subset_1(k2_pre_topc(sK75),X0,sK77) = k1_setfam_1(k2_tarski(X0,sK77)) ),
inference(resolution,[],[f36718,f37150]) ).
fof(f37848,plain,
k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77) = k1_setfam_1(k2_tarski(k2_pre_topc(sK76),sK77)),
inference(resolution,[],[f37842,f37332]) ).
fof(f37851,plain,
k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77),
inference(forward_demodulation,[],[f37848,f26351]) ).
fof(f37853,plain,
sK64(sK76,sK77) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77),
inference(forward_demodulation,[],[f37851,f37385]) ).
fof(f37855,plain,
sK64(sK76,sK77) = k5_subset_1(k2_pre_topc(sK75),sK77,k2_pre_topc(sK76)),
inference(superposition,[],[f37534,f37853]) ).
fof(f38614,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) = sK171(sK76,X0)
| ~ l1_pre_topc(sK75) ),
inference(resolution,[],[f36676,f23155]) ).
fof(f38615,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) = sK171(sK76,X0) ),
inference(forward_subsumption_resolution,[],[f38614,f23152]) ).
fof(f38616,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v4_pre_topc(X0,sK75)
| k1_setfam_1(k2_tarski(X0,u1_struct_0(sK76))) = sK171(sK76,X0) ),
inference(forward_demodulation,[],[f38615,f37148]) ).
fof(f38617,plain,
! [X0] :
( ~ v4_pre_topc(X0,sK75)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k1_setfam_1(k2_tarski(X0,k2_pre_topc(sK76))) = sK171(sK76,X0) ),
inference(forward_demodulation,[],[f38616,f37149]) ).
fof(f38622,plain,
( ~ m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75)))
| k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) = sK171(sK76,sK77) ),
inference(resolution,[],[f38617,f23159]) ).
fof(f38623,plain,
k1_setfam_1(k2_tarski(sK77,k2_pre_topc(sK76))) = sK171(sK76,sK77),
inference(forward_subsumption_resolution,[],[f38622,f37150]) ).
fof(f38626,plain,
sK64(sK76,sK77) = sK171(sK76,sK77),
inference(forward_demodulation,[],[f38623,f37385]) ).
fof(f38633,plain,
( v4_pre_topc(sK64(sK76,sK77),sK76)
| ~ m1_subset_1(sK77,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v4_pre_topc(sK77,sK75) ),
inference(superposition,[],[f37481,f38626]) ).
fof(f38634,plain,
( v4_pre_topc(sK64(sK76,sK77),sK76)
| ~ v4_pre_topc(sK77,sK75) ),
inference(forward_subsumption_resolution,[],[f38633,f37150]) ).
fof(f38635,plain,
v4_pre_topc(sK64(sK76,sK77),sK76),
inference(forward_subsumption_resolution,[],[f38634,f23159]) ).
fof(f38698,plain,
! [X0] :
( ~ v1_funct_1(k1_tsp_2(sK75,sK76))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f37143,f23033]) ).
fof(f38702,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ v5_pre_topc(k1_tsp_2(sK75,sK76),sK75,sK76)
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38698,f37141]) ).
fof(f38705,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| v3_struct_0(sK76)
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38702,f37284]) ).
fof(f38708,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ v2_tsp_2(sK76,sK75)
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38705,f23157]) ).
fof(f38711,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_tsp_1(sK76,sK75)
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38708,f23156]) ).
fof(f38713,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| v3_struct_0(sK75)
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38711,f23155]) ).
fof(f38715,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ v2_pre_topc(sK75)
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38713,f23154]) ).
fof(f38717,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ l1_pre_topc(sK75) ),
inference(forward_subsumption_resolution,[],[f38715,f23153]) ).
fof(f38718,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f38717,f23152]) ).
fof(f38719,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k5_subset_1(u1_struct_0(sK75),u1_struct_0(sK76),k3_tex_4(sK75,X0)) = k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0)
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f38718,f37148]) ).
fof(f38720,plain,
! [X0] :
( k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(u1_struct_0(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f38719,f37149]) ).
fof(f38721,plain,
! [X0] :
( k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f38720,f37148]) ).
fof(f38722,plain,
! [X0] :
( ~ v1_funct_2(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),k2_pre_topc(sK76))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f38721,f37149]) ).
fof(f38723,plain,
! [X0] :
( ~ v1_funct_2(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_demodulation,[],[f38722,f37148]) ).
fof(f38724,plain,
! [X0] :
( k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),u1_struct_0(sK76)) ),
inference(forward_subsumption_resolution,[],[f38723,f37306]) ).
fof(f38725,plain,
! [X0] :
( ~ m2_relset_1(k1_tsp_2(sK75,sK76),u1_struct_0(sK75),k2_pre_topc(sK76))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_demodulation,[],[f38724,f37149]) ).
fof(f38726,plain,
! [X0] :
( ~ m2_relset_1(k1_tsp_2(sK75,sK76),k2_pre_topc(sK75),k2_pre_topc(sK76))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75))) ),
inference(forward_demodulation,[],[f38725,f37148]) ).
fof(f38727,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK75)))
| k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),X0) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,X0)) ),
inference(forward_subsumption_resolution,[],[f38726,f37311]) ).
fof(f38731,plain,
k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),sK77) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),k3_tex_4(sK75,sK77)),
inference(resolution,[],[f38727,f37150]) ).
fof(f38735,plain,
k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),sK77) = k5_subset_1(k2_pre_topc(sK75),k2_pre_topc(sK76),sK77),
inference(forward_demodulation,[],[f38731,f37372]) ).
fof(f38738,plain,
k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),sK77) = k5_subset_1(k2_pre_topc(sK75),sK77,k2_pre_topc(sK76)),
inference(forward_demodulation,[],[f38735,f37534]) ).
fof(f38739,plain,
k4_pre_topc(sK75,sK76,k1_tsp_2(sK75,sK76),sK77) = sK64(sK76,sK77),
inference(forward_demodulation,[],[f38738,f37855]) ).
fof(f38741,plain,
~ v4_pre_topc(sK64(sK76,sK77),sK76),
inference(superposition,[],[f37142,f38739]) ).
fof(f38745,plain,
$false,
inference(forward_subsumption_resolution,[],[f38741,f38635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP042+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n019.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:03:06 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.75/3.18 % (121893)Detected formulas, will run a generic FOF schedule.
% 13.75/3.18 % (121902)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2612751328:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 13.75/3.18 % (121900)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1510095252:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 13.75/3.18 % (121901)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=488364026:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 13.75/3.18 % (121898)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2629131279:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 13.75/3.18 % (121903)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=248081309:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 13.75/3.18 % (121899)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3457278626:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 13.75/3.18 % (121904)dis-21_1_sil=8000:lcm=predicate:random_seed=429817928:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 13.75/3.18 % (121902)Instruction limit reached!
% 13.75/3.18 % (121902)------------------------------
% 13.75/3.18 % (121902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.75/3.18 % (121902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/3.18 % (121902)CaDiCaL version: 2.1.3
% 13.75/3.18 % (121902)Termination reason: Instruction limit
% 13.75/3.18 % (121902)Termination phase: Preprocessing 3
% 13.75/3.18 % (121902)Time elapsed: 0.058 s
% 13.75/3.18 % (121902)Peak memory usage: 106 MB
% 13.75/3.18 % (121902)Instructions burned: 119 (million)
% 13.75/3.18 % (121903)Instruction limit reached!
% 13.75/3.18 % (121903)------------------------------
% 13.75/3.18 % (121903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.75/3.18 % (121903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/3.18 % (121903)CaDiCaL version: 2.1.3
% 13.75/3.18 % (121903)Termination reason: Instruction limit
% 13.75/3.18 % (121903)Termination phase: Property scanning
% 13.75/3.18 % (121903)Time elapsed: 0.059 s
% 13.75/3.18 % (121903)Peak memory usage: 102 MB
% 13.75/3.18 % (121903)Instructions burned: 141 (million)
% 13.75/3.18 % (121901)Instruction limit reached!
% 13.75/3.18 % (121901)------------------------------
% 13.75/3.18 % (121901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.75/3.18 % (121901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/3.18 % (121901)CaDiCaL version: 2.1.3
% 13.75/3.18 % (121901)Termination reason: Instruction limit
% 13.75/3.18 % (121901)Termination phase: Saturation
% 13.75/3.18 % (121901)Time elapsed: 0.083 s
% 13.75/3.18 % (121901)Peak memory usage: 106 MB
% 13.75/3.18 % (121901)Instructions burned: 109 (million)
% 13.75/3.18 % (121904)Instruction limit reached!
% 13.75/3.18 % (121904)------------------------------
% 13.75/3.18 % (121904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.75/3.18 % (121904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.75/3.18 % (121904)CaDiCaL version: 2.1.3
% 13.75/3.18 % (121904)Termination reason: Instruction limit
% 13.75/3.18 % (121904)Termination phase: Preprocessing 1
% 13.75/3.18 % (121904)Time elapsed: 0.094 s
% 13.75/3.18 % (121904)Peak memory usage: 103 MB
% 13.75/3.18 % (121904)Instructions burned: 129 (million)
% 13.75/3.18 % (121912)lrs+10_1_sil=8000:sp=occurrence:random_seed=294279334:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 13.75/3.18 % (121913)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1329221219:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 13.75/3.18 % (121914)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2292494936:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 13.75/3.18 % (121912)Instruction limit reached!
% 13.75/3.18 % (121912)------------------------------
% 13.75/3.18 % (121912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.75/3.18 % (121912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.99 % (121912)CaDiCaL version: 2.1.3
% 18.87/3.99 % (121912)Termination reason: Instruction limit
% 18.87/3.99 % (121912)Termination phase: Saturation
% 18.87/3.99 % (121912)Time elapsed: 0.107 s
% 18.87/3.99 % (121912)Peak memory usage: 110 MB
% 18.87/3.99 % (121912)Instructions burned: 285 (million)
% 18.87/3.99 % (121915)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3504267065:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 18.87/3.99 % (121913)Instruction limit reached!
% 18.87/3.99 % (121913)------------------------------
% 18.87/3.99 % (121913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.99 % (121913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.99 % (121913)CaDiCaL version: 2.1.3
% 18.87/3.99 % (121913)Termination reason: Instruction limit
% 18.87/3.99 % (121913)Termination phase: Property scanning
% 18.87/3.99 % (121913)Time elapsed: 0.069 s
% 18.87/3.99 % (121913)Peak memory usage: 102 MB
% 18.87/3.99 % (121913)Instructions burned: 159 (million)
% 18.87/3.99 % (121920)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3262692646:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 18.87/3.99 % (121915)Instruction limit reached!
% 18.87/3.99 % (121915)------------------------------
% 18.87/3.99 % (121915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.99 % (121915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.99 % (121915)CaDiCaL version: 2.1.3
% 18.87/3.99 % (121915)Termination reason: Instruction limit
% 18.87/3.99 % (121915)Termination phase: SInE selection
% 18.87/3.99 % (121915)Time elapsed: 0.129 s
% 18.87/3.99 % (121915)Peak memory usage: 103 MB
% 18.87/3.99 % (121915)Instructions burned: 249 (million)
% 18.87/3.99 % (121914)Instruction limit reached!
% 18.87/3.99 % (121914)------------------------------
% 18.87/3.99 % (121914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.99 % (121914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.99 % (121914)CaDiCaL version: 2.1.3
% 18.87/3.99 % (121914)Termination reason: Instruction limit
% 18.87/3.99 % (121914)Termination phase: Saturation
% 18.87/3.99 % (121914)Time elapsed: 0.164 s
% 18.87/3.99 % (121914)Peak memory usage: 107 MB
% 18.87/3.99 % (121914)Instructions burned: 326 (million)
% 18.87/3.99 % (121921)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2907067214:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 18.87/3.99 % (121920)Instruction limit reached!
% 18.87/3.99 % (121920)------------------------------
% 18.87/3.99 % (121920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.99 % (121920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.99 % (121920)CaDiCaL version: 2.1.3
% 18.87/3.99 % (121920)Termination reason: Instruction limit
% 18.87/3.99 % (121920)Termination phase: Saturation
% 18.87/3.99 % (121920)Time elapsed: 0.106 s
% 18.87/3.99 % (121920)Peak memory usage: 110 MB
% 18.87/3.99 % (121920)Instructions burned: 295 (million)
% 18.87/3.99 % (121923)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4171026431:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 18.87/3.99 % (121924)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3315327813:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 18.87/3.99 % (121926)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1992535670:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 18.87/3.99 % (121923)Instruction limit reached!
% 18.87/3.99 % (121923)------------------------------
% 18.87/3.99 % (121923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.99 % (121923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.87/3.99 % (121923)CaDiCaL version: 2.1.3
% 18.87/3.99 % (121923)Termination reason: Instruction limit
% 18.87/3.99 % (121923)Termination phase: Preprocessing 2
% 18.87/3.99 % (121923)Time elapsed: 0.097 s
% 18.87/3.99 % (121923)Peak memory usage: 105 MB
% 18.87/3.99 % (121923)Instructions burned: 113 (million)
% 18.87/3.99 % (121926)Instruction limit reached!
% 18.87/3.99 % (121926)------------------------------
% 18.87/3.99 % (121926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.87/3.99 % (121926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121926)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121926)Termination reason: Instruction limit
% 30.56/5.83 % (121926)Termination phase: Property scanning
% 30.56/5.83 % (121926)Time elapsed: 0.027 s
% 30.56/5.83 % (121926)Peak memory usage: 102 MB
% 30.56/5.83 % (121926)Instructions burned: 116 (million)
% 30.56/5.83 % (121924)Instruction limit reached!
% 30.56/5.83 % (121924)------------------------------
% 30.56/5.83 % (121924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121924)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121924)Termination reason: Instruction limit
% 30.56/5.83 % (121924)Termination phase: Preprocessing 2
% 30.56/5.83 % (121924)Time elapsed: 0.104 s
% 30.56/5.83 % (121924)Peak memory usage: 106 MB
% 30.56/5.83 % (121924)Instructions burned: 127 (million)
% 30.56/5.83 % (121931)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1827650840:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 30.56/5.83 % (121930)lrs+10_1_sil=8000:sp=occurrence:random_seed=710984104:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 30.56/5.83 % (121932)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2767438466:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 30.56/5.83 % (121931)Instruction limit reached!
% 30.56/5.83 % (121931)------------------------------
% 30.56/5.83 % (121931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121931)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121931)Termination reason: Instruction limit
% 30.56/5.83 % (121931)Termination phase: Saturation
% 30.56/5.83 % (121931)Time elapsed: 0.148 s
% 30.56/5.83 % (121931)Peak memory usage: 111 MB
% 30.56/5.83 % (121931)Instructions burned: 438 (million)
% 30.56/5.83 % (121936)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4157192806:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 30.56/5.83 % (121936)Instruction limit reached!
% 30.56/5.83 % (121936)------------------------------
% 30.56/5.83 % (121936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121936)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121936)Termination reason: Instruction limit
% 30.56/5.83 % (121936)Termination phase: Property scanning
% 30.56/5.83 % (121936)Time elapsed: 0.108 s
% 30.56/5.83 % (121936)Peak memory usage: 106 MB
% 30.56/5.83 % (121936)Instructions burned: 136 (million)
% 30.56/5.83 % (121930)Instruction limit reached!
% 30.56/5.83 % (121930)------------------------------
% 30.56/5.83 % (121930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121930)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121930)Termination reason: Instruction limit
% 30.56/5.83 % (121930)Termination phase: Saturation
% 30.56/5.83 % (121930)Time elapsed: 0.524 s
% 30.56/5.83 % (121930)Peak memory usage: 121 MB
% 30.56/5.83 % (121930)Instructions burned: 908 (million)
% 30.56/5.83 % (121938)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3021413715:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 30.56/5.83 % (121921)Instruction limit reached!
% 30.56/5.83 % (121921)------------------------------
% 30.56/5.83 % (121921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121921)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121921)Termination reason: Instruction limit
% 30.56/5.83 % (121921)Termination phase: Saturation
% 30.56/5.83 % (121921)Time elapsed: 1.040 s
% 30.56/5.83 % (121921)Peak memory usage: 239 MB
% 30.56/5.83 % (121921)Instructions burned: 2352 (million)
% 30.56/5.83 % (121939)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3820929328:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 30.56/5.83 % (121942)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2007118296:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 30.56/5.83 % (121942)Instruction limit reached!
% 30.56/5.83 % (121942)------------------------------
% 30.56/5.83 % (121942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121942)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121942)Termination reason: Instruction limit
% 30.56/5.83 % (121942)Termination phase: Property scanning
% 30.56/5.83 % (121942)Time elapsed: 0.029 s
% 30.56/5.83 % (121942)Peak memory usage: 102 MB
% 30.56/5.83 % (121942)Instructions burned: 126 (million)
% 30.56/5.83 % (121938)Instruction limit reached!
% 30.56/5.83 % (121938)------------------------------
% 30.56/5.83 % (121938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121938)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121938)Termination reason: Instruction limit
% 30.56/5.83 % (121938)Termination phase: Property scanning
% 30.56/5.83 % (121938)Time elapsed: 0.399 s
% 30.56/5.83 % (121938)Peak memory usage: 121 MB
% 30.56/5.83 % (121938)Instructions burned: 594 (million)
% 30.56/5.83 % (121944)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3207282923:i=134:gtgl=5:slsql=off:gtg=exists_sym_2974 on theBenchmark for (2974ds/134Mi)
% 30.56/5.83 % (121944)Instruction limit reached!
% 30.56/5.83 % (121944)------------------------------
% 30.56/5.83 % (121944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121944)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121944)Termination reason: Instruction limit
% 30.56/5.83 % (121944)Termination phase: Property scanning
% 30.56/5.83 % (121944)Time elapsed: 0.032 s
% 30.56/5.83 % (121944)Peak memory usage: 102 MB
% 30.56/5.83 % (121944)Instructions burned: 138 (million)
% 30.56/5.83 % (121945)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3808982543:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 30.56/5.83 % (121947)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1134887304:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 30.56/5.83 % (121945)Instruction limit reached!
% 30.56/5.83 % (121945)------------------------------
% 30.56/5.83 % (121945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121945)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121945)Termination reason: Instruction limit
% 30.56/5.83 % (121945)Termination phase: Saturation
% 30.56/5.83 % (121945)Time elapsed: 0.105 s
% 30.56/5.83 % (121945)Peak memory usage: 108 MB
% 30.56/5.83 % (121945)Instructions burned: 141 (million)
% 30.56/5.83 % (121947)Instruction limit reached!
% 30.56/5.83 % (121947)------------------------------
% 30.56/5.83 % (121947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121947)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121947)Termination reason: Instruction limit
% 30.56/5.83 % (121947)Termination phase: Saturation
% 30.56/5.83 % (121947)Time elapsed: 0.159 s
% 30.56/5.83 % (121947)Peak memory usage: 111 MB
% 30.56/5.83 % (121947)Instructions burned: 435 (million)
% 30.56/5.83 % (121950)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4029670635:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 30.56/5.83 % (121951)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2920993402:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 30.56/5.83 % (121951)Instruction limit reached!
% 30.56/5.83 % (121951)------------------------------
% 30.56/5.83 % (121951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.56/5.83 % (121951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.56/5.83 % (121951)CaDiCaL version: 2.1.3
% 30.56/5.83 % (121951)Termination reason: Instruction limit
% 30.56/5.83 % (121951)Termination phase: Preprocessing 1
% 30.56/5.83 % (121951)Time elapsed: 0.066 s
% 30.56/5.83 % (121951)Peak memory usage: 103 MB
% 30.56/5.83 % (121951)Instructions burned: 152 (million)
% 30.56/5.83 % (121954)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=695750585:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 30.56/5.83 % (121899)First to succeed.
% 30.56/5.83 % (121899)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-121893"
% 30.56/5.83 % (121899)Refutation found. Thanks to Tanya!
% 30.56/5.83 % SZS status Theorem for theBenchmark
% 30.56/5.83 % SZS output start Proof for theBenchmark
% See solution above
% 32.61/5.93 % (121899)------------------------------
% 32.61/5.93 % (121899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.61/5.93 % (121899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.61/5.93 % (121899)CaDiCaL version: 2.1.3
% 32.61/5.93 % (121899)Termination reason: Refutation
% 32.61/5.93 % (121899)Time elapsed: 3.890 s
% 32.61/5.93 % (121899)Peak memory usage: 285 MB
% 32.61/5.93 % (121899)Instructions burned: 6381 (million)
% 32.61/5.93 % (121899)------------------------------
% 32.61/5.93 % (121899)------------------------------
% 32.61/5.93 % (121893)Success in time 5.164 s
% 32.61/5.93 % Vampire exiting
%------------------------------------------------------------------------------