%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP037+4 : 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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:34:00 PM UTC 2026
% Result : Theorem 15.49s 6.51s
% Output : Refutation 28.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 15
% Syntax : Number of formulae : 130 ( 24 unt; 8 def)
% Number of atoms : 678 ( 65 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 918 ( 370 ~; 449 |; 67 &)
% ( 13 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 9 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-4 aty)
% Number of variables : 123 ( 0 sgn 113 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34215,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k3_tex_4(X0,X1) = k3_tex_4(X0,k3_tex_4(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_tex_4) ).
fof(f34273,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_tex_4) ).
fof(f34366,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(f34374,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(f34394,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(f34432,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(f34434,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)))
=> 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(f34435,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)))
=> 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)],[f34434]) ).
fof(f34517,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,[],[f34374]) ).
fof(f34518,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,[],[f34517]) ).
fof(f34557,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,[],[f34394]) ).
fof(f34558,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,[],[f34557]) ).
fof(f34633,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,[],[f34432]) ).
fof(f34634,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,[],[f34633]) ).
fof(f34637,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( 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))
& 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,[],[f34435]) ).
fof(f34638,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( 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))
& 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,[],[f34637]) ).
fof(f34867,plain,
! [X0,X1] :
( m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f34273]) ).
fof(f34868,plain,
! [X0,X1] :
( m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f34867]) ).
fof(f34899,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = k3_tex_4(X0,k3_tex_4(X0,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34215]) ).
fof(f34900,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = k3_tex_4(X0,k3_tex_4(X0,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34899]) ).
fof(f35161,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f35461,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,[],[f34634]) ).
fof(f35462,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,[],[f35461]) ).
fof(f35463,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k4_tsp_2(X0,X1)
| ( k5_subset_1(u1_struct_0(X0),sK25(X0,X1,X2),k3_tex_4(X0,sK26(X0,X1,X2))) != k4_pre_topc(X0,X1,X2,sK26(X0,X1,X2))
& m1_subset_1(sK26(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& u1_struct_0(X1) = sK25(X0,X1,X2)
& m1_subset_1(sK25(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,[sK25,sK26]),skolemize(X3,sK25(X0,X1,X2)),skolemize(X4,sK26(X0,X1,X2))],[f35462]) ).
fof(f35464,plain,
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),sK29) != k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,sK29))
& m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
& ~ v3_struct_0(sK28)
& v2_tsp_2(sK28,sK27)
& m2_tsp_1(sK28,sK27)
& ~ v3_struct_0(sK27)
& v2_pre_topc(sK27)
& l1_pre_topc(sK27) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29)],[f34638]) ).
fof(f35639,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,[],[f35161]) ).
fof(f35779,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,[],[f34518]) ).
fof(f35780,plain,
! [X0,X1] :
( v5_pre_topc(k4_tsp_2(X0,X1),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(cnf_transformation,[],[f34518]) ).
fof(f35781,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,[],[f34518]) ).
fof(f35782,plain,
! [X0,X1] :
( v1_funct_1(k4_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(cnf_transformation,[],[f34518]) ).
fof(f35835,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,[],[f34558]) ).
fof(f35941,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,[],[f35463]) ).
fof(f35947,plain,
l1_pre_topc(sK27),
inference(cnf_transformation,[],[f35464]) ).
fof(f35948,plain,
v2_pre_topc(sK27),
inference(cnf_transformation,[],[f35464]) ).
fof(f35949,plain,
~ v3_struct_0(sK27),
inference(cnf_transformation,[],[f35464]) ).
fof(f35950,plain,
m2_tsp_1(sK28,sK27),
inference(cnf_transformation,[],[f35464]) ).
fof(f35951,plain,
v2_tsp_2(sK28,sK27),
inference(cnf_transformation,[],[f35464]) ).
fof(f35952,plain,
~ v3_struct_0(sK28),
inference(cnf_transformation,[],[f35464]) ).
fof(f35953,plain,
m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27))),
inference(cnf_transformation,[],[f35464]) ).
fof(f35954,plain,
k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),sK29) != k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,sK29)),
inference(cnf_transformation,[],[f35464]) ).
fof(f36300,plain,
! [X0,X1] :
( m1_subset_1(k3_tex_4(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f34868]) ).
fof(f36320,plain,
! [X0,X1] :
( k3_tex_4(X0,X1) = k3_tex_4(X0,k3_tex_4(X0,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34900]) ).
fof(f36624,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f35639]) ).
fof(f37216,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,[],[f35941]) ).
fof(f37217,plain,
! [X0,X1,X6] :
( 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)
| ~ 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)))
| ~ 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(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,[],[f37216]) ).
fof(f37385,definition,
( spl244_1
<=> m2_tsp_1(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl244_1])],[avatar_definition]) ).
fof(f37387,plain,
( m2_tsp_1(sK28,sK27)
| ~ spl244_1 ),
inference(avatar_component_clause,[],[f37385]) ).
fof(f37388,plain,
spl244_1,
inference(avatar_split_clause,[],[f35950,f37385]) ).
fof(f37392,plain,
( m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ l1_pre_topc(sK27)
| ~ spl244_1 ),
inference(resolution,[],[f37387,f35835]) ).
fof(f37436,plain,
( m1_pre_topc(sK28,sK27)
| ~ l1_pre_topc(sK27)
| ~ spl244_1 ),
inference(resolution,[],[f37387,f36624]) ).
fof(f37530,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v2_tsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_1 ),
inference(resolution,[],[f37387,f37217]) ).
fof(f37541,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v2_tsp_2(sK28,sK27)
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37530,f35952]) ).
fof(f37632,plain,
( m1_pre_topc(sK28,sK27)
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37436,f35947]) ).
fof(f37671,plain,
( m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ l1_pre_topc(sK27)
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37392,f35949]) ).
fof(f37676,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37541,f35951]) ).
fof(f37788,plain,
( m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37671,f35947]) ).
fof(f37793,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37676,f35949]) ).
fof(f37871,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37793,f37788]) ).
fof(f37943,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ l1_pre_topc(sK27) )
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37871,f35948]) ).
fof(f37989,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28)) )
| ~ spl244_1 ),
inference(forward_subsumption_resolution,[],[f37943,f35947]) ).
fof(f38049,definition,
( spl244_2
<=> v3_struct_0(sK27) ),
introduced(definition,[new_symbols(definition,[spl244_2])],[avatar_definition]) ).
fof(f38051,plain,
( ~ v3_struct_0(sK27)
| spl244_2 ),
inference(avatar_component_clause,[],[f38049]) ).
fof(f38052,plain,
~ spl244_2,
inference(avatar_split_clause,[],[f35949,f38049]) ).
fof(f38054,definition,
( spl244_3
<=> v3_struct_0(sK28) ),
introduced(definition,[new_symbols(definition,[spl244_3])],[avatar_definition]) ).
fof(f38056,plain,
( ~ v3_struct_0(sK28)
| spl244_3 ),
inference(avatar_component_clause,[],[f38054]) ).
fof(f38057,plain,
~ spl244_3,
inference(avatar_split_clause,[],[f35952,f38054]) ).
fof(f38059,definition,
( spl244_4
<=> k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),sK29) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,sK29)) ),
introduced(definition,[new_symbols(definition,[spl244_4])],[avatar_definition]) ).
fof(f38061,plain,
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),sK29) != k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,sK29))
| spl244_4 ),
inference(avatar_component_clause,[],[f38059]) ).
fof(f38062,plain,
~ spl244_4,
inference(avatar_split_clause,[],[f35954,f38059]) ).
fof(f38064,definition,
( spl244_5
<=> m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27))) ),
introduced(definition,[new_symbols(definition,[spl244_5])],[avatar_definition]) ).
fof(f38066,plain,
( m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ spl244_5 ),
inference(avatar_component_clause,[],[f38064]) ).
fof(f38067,plain,
spl244_5,
inference(avatar_split_clause,[],[f35953,f38064]) ).
fof(f40128,definition,
( spl244_6
<=> v2_tsp_2(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl244_6])],[avatar_definition]) ).
fof(f40130,plain,
( v2_tsp_2(sK28,sK27)
| ~ spl244_6 ),
inference(avatar_component_clause,[],[f40128]) ).
fof(f40131,plain,
spl244_6,
inference(avatar_split_clause,[],[f35951,f40128]) ).
fof(f40146,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| ~ spl244_6 ),
inference(resolution,[],[f40130,f35779]) ).
fof(f40147,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| ~ spl244_6 ),
inference(resolution,[],[f40130,f35780]) ).
fof(f40148,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| ~ spl244_6 ),
inference(resolution,[],[f40130,f35781]) ).
fof(f40149,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| v3_struct_0(sK27)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| ~ spl244_6 ),
inference(resolution,[],[f40130,f35782]) ).
fof(f40249,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40149,f38051]) ).
fof(f40250,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40148,f38051]) ).
fof(f40251,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40147,f38051]) ).
fof(f40252,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v2_pre_topc(sK27)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40146,f38051]) ).
fof(f40280,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40249,f35948]) ).
fof(f40281,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40250,f35948]) ).
fof(f40282,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40251,f35948]) ).
fof(f40283,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40252,f35948]) ).
fof(f40311,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40280,f35947]) ).
fof(f40312,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40281,f35947]) ).
fof(f40313,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40282,f35947]) ).
fof(f40314,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40283,f35947]) ).
fof(f40342,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40311,f38056]) ).
fof(f40343,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40312,f38056]) ).
fof(f40344,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40313,f38056]) ).
fof(f40345,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ m1_pre_topc(sK28,sK27)
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40314,f38056]) ).
fof(f40365,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40342,f37632]) ).
fof(f40366,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40343,f37632]) ).
fof(f40367,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40344,f37632]) ).
fof(f40368,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40345,f37632]) ).
fof(f40385,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28)) )
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(backward_subsumption_resolution,[],[f37989,f40365]) ).
fof(f40396,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28)) )
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40385,f40366]) ).
fof(f40399,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28)) )
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40396,f40367]) ).
fof(f40402,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27))) )
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(forward_subsumption_resolution,[],[f40399,f40368]) ).
fof(f40408,definition,
( spl244_7
<=> ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27))) ) ),
introduced(definition,[new_symbols(definition,[spl244_7])],[avatar_definition]) ).
fof(f40409,plain,
( ! [X0] :
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),X0) = k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27))) )
| ~ spl244_7 ),
inference(avatar_component_clause,[],[f40408]) ).
fof(f40410,plain,
( spl244_7
| ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6 ),
inference(avatar_split_clause,[],[f40402,f40128,f38054,f38049,f37385,f40408]) ).
fof(f40432,plain,
( ! [X0] :
( k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0)) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(k3_tex_4(sK27,X0),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_7 ),
inference(superposition,[],[f40409,f36320]) ).
fof(f40493,plain,
( ! [X0] :
( k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0)) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ l1_pre_topc(sK27) )
| ~ spl244_7 ),
inference(forward_subsumption_resolution,[],[f40432,f36300]) ).
fof(f40529,plain,
( ! [X0] :
( k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0)) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ l1_pre_topc(sK27) )
| spl244_2
| ~ spl244_7 ),
inference(forward_subsumption_resolution,[],[f40493,f38051]) ).
fof(f40560,plain,
( ! [X0] :
( k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0)) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27))) )
| spl244_2
| ~ spl244_7 ),
inference(forward_subsumption_resolution,[],[f40529,f35947]) ).
fof(f54815,definition,
( spl244_38
<=> ! [X0] :
( k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0)) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27))) ) ),
introduced(definition,[new_symbols(definition,[spl244_38])],[avatar_definition]) ).
fof(f54816,plain,
( ! [X0] :
( k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,X0)) = k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),k3_tex_4(sK27,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK27))) )
| ~ spl244_38 ),
inference(avatar_component_clause,[],[f54815]) ).
fof(f54817,plain,
( spl244_38
| spl244_2
| ~ spl244_7 ),
inference(avatar_split_clause,[],[f40560,f40408,f38049,f54815]) ).
fof(f54836,plain,
( k4_pre_topc(sK27,sK28,k4_tsp_2(sK27,sK28),sK29) != k5_subset_1(u1_struct_0(sK27),u1_struct_0(sK28),k3_tex_4(sK27,sK29))
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| spl244_4
| ~ spl244_38 ),
inference(superposition,[],[f38061,f54816]) ).
fof(f54853,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| spl244_4
| ~ spl244_7
| ~ spl244_38 ),
inference(forward_subsumption_resolution,[],[f54836,f40409]) ).
fof(f54868,plain,
( $false
| spl244_4
| ~ spl244_5
| ~ spl244_7
| ~ spl244_38 ),
inference(forward_subsumption_resolution,[],[f54853,f38066]) ).
fof(f54869,plain,
( spl244_4
| ~ spl244_5
| ~ spl244_7
| ~ spl244_38 ),
inference(avatar_contradiction_clause,[],[f54868]) ).
cnf(s1,plain,
spl244_1,
inference(sat_conversion,[],[f37388]) ).
cnf(s2,plain,
~ spl244_2,
inference(sat_conversion,[],[f38052]) ).
cnf(s3,plain,
~ spl244_3,
inference(sat_conversion,[],[f38057]) ).
cnf(s4,plain,
~ spl244_4,
inference(sat_conversion,[],[f38062]) ).
cnf(s5,plain,
spl244_5,
inference(sat_conversion,[],[f38067]) ).
cnf(s6,plain,
spl244_6,
inference(sat_conversion,[],[f40131]) ).
cnf(s7,plain,
( ~ spl244_1
| spl244_2
| spl244_3
| ~ spl244_6
| spl244_7 ),
inference(sat_conversion,[],[f40410]) ).
cnf(s38,plain,
( spl244_2
| ~ spl244_7
| spl244_38 ),
inference(sat_conversion,[],[f54817]) ).
cnf(s39,plain,
( spl244_4
| ~ spl244_5
| ~ spl244_7
| ~ spl244_38 ),
inference(sat_conversion,[],[f54869]) ).
cnf(s63,plain,
spl244_7,
inference(rat,[],[s7,s2,s6,s3,s1]) ).
cnf(s69,plain,
spl244_38,
inference(rat,[],[s38,s2,s63]) ).
cnf(s70,plain,
$false,
inference(rat,[],[s39,s4,s5,s69,s63]) ).
fof(f54918,plain,
$false,
inference(avatar_sat_refutation,[],[s70]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP037+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.17 % Computer : n013.cluster.edu
% 0.13/0.17 % Model : x86_64 x86_64
% 0.13/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.17 % Memory : 8046.5625MB
% 0.13/0.17 % OS : Linux 6.8.0-71-generic
% 0.13/0.17 % CPULimit : 300
% 0.13/0.17 % WCLimit : 300
% 0.13/0.17 % DateTime : Mon Sep 28 18:59:44 UTC 2026
% 0.13/0.17 % CPUTime :
% 0.13/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.21 Running first-order theorem proving
% 0.13/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
% 19.07/5.14 % (1449331)Detected formulas, will run a generic FOF schedule.
% 19.07/5.14 % (1449336)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=2329903273:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 19.07/5.14 % (1449337)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=509797646:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 19.07/5.14 % (1449338)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=3597902461:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 19.07/5.14 % (1449339)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=621966133:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 19.07/5.14 % (1449340)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1326499573:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 19.07/5.14 % (1449341)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3495947737:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 19.07/5.14 % (1449342)dis-21_1_sil=8000:lcm=predicate:random_seed=2456702235:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 19.07/5.14 % (1449341)Instruction limit reached!
% 19.07/5.14 % (1449341)------------------------------
% 19.07/5.14 % (1449341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/5.14 % (1449341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/5.14 % (1449341)CaDiCaL version: 2.1.3
% 19.07/5.14 % (1449341)Termination reason: Instruction limit
% 19.07/5.14 % (1449341)Termination phase: Property scanning
% 19.07/5.14 % (1449341)Time elapsed: 0.061 s
% 19.07/5.14 % (1449341)Peak memory usage: 136 MB
% 19.07/5.14 % (1449341)Instructions burned: 141 (million)
% 19.07/5.14 % (1449339)Instruction limit reached!
% 19.07/5.14 % (1449339)------------------------------
% 19.07/5.14 % (1449339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/5.14 % (1449339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/5.14 % (1449339)CaDiCaL version: 2.1.3
% 19.07/5.14 % (1449339)Termination reason: Instruction limit
% 19.07/5.14 % (1449339)Termination phase: SInE selection
% 19.07/5.14 % (1449339)Time elapsed: 0.079 s
% 19.07/5.14 % (1449339)Peak memory usage: 135 MB
% 19.07/5.14 % (1449339)Instructions burned: 110 (million)
% 19.07/5.14 % (1449340)Instruction limit reached!
% 19.07/5.14 % (1449340)------------------------------
% 19.07/5.14 % (1449340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/5.14 % (1449340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/5.14 % (1449340)CaDiCaL version: 2.1.3
% 19.07/5.14 % (1449340)Termination reason: Instruction limit
% 19.07/5.14 % (1449340)Termination phase: SInE selection
% 19.07/5.14 % (1449340)Time elapsed: 0.088 s
% 19.07/5.14 % (1449340)Peak memory usage: 135 MB
% 19.07/5.14 % (1449340)Instructions burned: 119 (million)
% 19.07/5.14 % (1449342)Instruction limit reached!
% 19.07/5.14 % (1449342)------------------------------
% 19.07/5.14 % (1449342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/5.14 % (1449342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/5.14 % (1449342)CaDiCaL version: 2.1.3
% 19.07/5.14 % (1449342)Termination reason: Instruction limit
% 19.07/5.14 % (1449342)Termination phase: SInE selection
% 19.07/5.14 % (1449342)Time elapsed: 0.096 s
% 19.07/5.14 % (1449342)Peak memory usage: 136 MB
% 19.07/5.14 % (1449342)Instructions burned: 131 (million)
% 19.07/5.14 % (1449350)lrs+10_1_sil=8000:sp=occurrence:random_seed=690738414:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 19.07/5.14 % (1449351)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2979680101:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 19.07/5.14 % (1449352)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3952812377:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 19.07/5.14 % (1449353)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=3489702498:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 19.07/5.14 % (1449351)Instruction limit reached!
% 26.71/6.21 % (1449351)------------------------------
% 26.71/6.21 % (1449351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449351)CaDiCaL version: 2.1.3
% 26.71/6.21 % (1449351)Termination reason: Instruction limit
% 26.71/6.21 % (1449351)Termination phase: Property scanning
% 26.71/6.21 % (1449351)Time elapsed: 0.069 s
% 26.71/6.21 % (1449351)Peak memory usage: 136 MB
% 26.71/6.21 % (1449351)Instructions burned: 157 (million)
% 26.71/6.21 % (1449353)Instruction limit reached!
% 26.71/6.21 % (1449353)------------------------------
% 26.71/6.21 % (1449353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449353)CaDiCaL version: 2.1.3
% 26.71/6.21 % (1449353)Termination reason: Instruction limit
% 26.71/6.21 % (1449353)Termination phase: Property scanning
% 26.71/6.21 % (1449353)Time elapsed: 0.108 s
% 26.71/6.21 % (1449353)Peak memory usage: 136 MB
% 26.71/6.21 % (1449353)Instructions burned: 248 (million)
% 26.71/6.21 % (1449350)Instruction limit reached!
% 26.71/6.21 % (1449350)------------------------------
% 26.71/6.21 % (1449350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449350)CaDiCaL version: 2.1.3
% 26.71/6.21 % (1449350)Termination reason: Instruction limit
% 26.71/6.21 % (1449350)Termination phase: Preprocessing 3
% 26.71/6.21 % (1449350)Time elapsed: 0.238 s
% 26.71/6.21 % (1449350)Peak memory usage: 139 MB
% 26.71/6.21 % (1449350)Instructions burned: 285 (million)
% 26.71/6.21 % (1449358)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3125739875:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 26.71/6.21 % (1449352)Instruction limit reached!
% 26.71/6.21 % (1449352)------------------------------
% 26.71/6.21 % (1449352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449352)CaDiCaL version: 2.1.3
% 26.71/6.21 % (1449352)Termination reason: Instruction limit
% 26.71/6.21 % (1449352)Termination phase: Saturation
% 26.71/6.21 % (1449352)Time elapsed: 0.262 s
% 26.71/6.21 % (1449352)Peak memory usage: 142 MB
% 26.71/6.21 % (1449352)Instructions burned: 326 (million)
% 26.71/6.21 % (1449359)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2287283379:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 26.71/6.21 % (1449361)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2926896023:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 26.71/6.21 % (1449358)Instruction limit reached!
% 26.71/6.21 % (1449358)------------------------------
% 26.71/6.21 % (1449358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449358)CaDiCaL version: 2.1.3
% 26.71/6.21 % (1449358)Termination reason: Instruction limit
% 26.71/6.21 % (1449358)Termination phase: SInE selection
% 26.71/6.21 % (1449358)Time elapsed: 0.191 s
% 26.71/6.21 % (1449358)Peak memory usage: 136 MB
% 26.71/6.21 % (1449358)Instructions burned: 295 (million)
% 26.71/6.21 % (1449362)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=92832042:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 26.71/6.21 % (1449361)Instruction limit reached!
% 26.71/6.21 % (1449361)------------------------------
% 26.71/6.21 % (1449361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449361)CaDiCaL version: 2.1.3
% 26.71/6.21 % (1449361)Termination reason: Instruction limit
% 26.71/6.21 % (1449361)Termination phase: SInE selection
% 26.71/6.21 % (1449361)Time elapsed: 0.086 s
% 26.71/6.21 % (1449361)Peak memory usage: 136 MB
% 26.71/6.21 % (1449361)Instructions burned: 113 (million)
% 26.71/6.21 % (1449362)Instruction limit reached!
% 26.71/6.21 % (1449362)------------------------------
% 26.71/6.21 % (1449362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.71/6.21 % (1449362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.71/6.21 % (1449362)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449362)Termination reason: Instruction limit
% 15.49/6.51 % (1449362)Termination phase: Preprocessing 1
% 15.49/6.51 % (1449362)Time elapsed: 0.096 s
% 15.49/6.51 % (1449362)Peak memory usage: 137 MB
% 15.49/6.51 % (1449362)Instructions burned: 127 (million)
% 15.49/6.51 % (1449365)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2285345141:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 15.49/6.51 % (1449367)lrs+10_1_sil=8000:sp=occurrence:random_seed=281084740:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 15.49/6.51 % (1449365)Instruction limit reached!
% 15.49/6.51 % (1449365)------------------------------
% 15.49/6.51 % (1449365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449365)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449365)Termination reason: Instruction limit
% 15.49/6.51 % (1449365)Termination phase: Property scanning
% 15.49/6.51 % (1449365)Time elapsed: 0.054 s
% 15.49/6.51 % (1449365)Peak memory usage: 136 MB
% 15.49/6.51 % (1449365)Instructions burned: 116 (million)
% 15.49/6.51 % (1449368)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1947054801:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 15.49/6.51 % (1449371)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3110148077:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 15.49/6.51 % (1449368)Instruction limit reached!
% 15.49/6.51 % (1449368)------------------------------
% 15.49/6.51 % (1449368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449368)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449368)Termination reason: Instruction limit
% 15.49/6.51 % (1449368)Termination phase: Saturation
% 15.49/6.51 % (1449368)Time elapsed: 0.313 s
% 15.49/6.51 % (1449368)Peak memory usage: 144 MB
% 15.49/6.51 % (1449368)Instructions burned: 439 (million)
% 15.49/6.51 % (1449374)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1011518486:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 15.49/6.51 % (1449367)Instruction limit reached!
% 15.49/6.51 % (1449367)------------------------------
% 15.49/6.51 % (1449367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449367)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449367)Termination reason: Instruction limit
% 15.49/6.51 % (1449367)Termination phase: Property scanning
% 15.49/6.51 % (1449367)Time elapsed: 0.590 s
% 15.49/6.51 % (1449367)Peak memory usage: 158 MB
% 15.49/6.51 % (1449367)Instructions burned: 910 (million)
% 15.49/6.51 % (1449374)Instruction limit reached!
% 15.49/6.51 % (1449374)------------------------------
% 15.49/6.51 % (1449374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449374)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449374)Termination reason: Instruction limit
% 15.49/6.51 % (1449374)Termination phase: SInE selection
% 15.49/6.51 % (1449374)Time elapsed: 0.102 s
% 15.49/6.51 % (1449374)Peak memory usage: 136 MB
% 15.49/6.51 % (1449374)Instructions burned: 134 (million)
% 15.49/6.51 % (1449376)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=411020071:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 15.49/6.51 % (1449377)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1761743013:st=3:i=13193:sd=3:ss=axioms_2961 on theBenchmark for (2961ds/13193Mi)
% 15.49/6.51 % (1449376)Instruction limit reached!
% 15.49/6.51 % (1449376)------------------------------
% 15.49/6.51 % (1449376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449376)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449376)Termination reason: Instruction limit
% 15.49/6.51 % (1449376)Termination phase: Preprocessing 2
% 15.49/6.51 % (1449376)Time elapsed: 0.452 s
% 15.49/6.51 % (1449376)Peak memory usage: 153 MB
% 15.49/6.51 % (1449376)Instructions burned: 592 (million)
% 15.49/6.51 % (1449359)Instruction limit reached!
% 15.49/6.51 % (1449359)------------------------------
% 15.49/6.51 % (1449359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449359)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449359)Termination reason: Instruction limit
% 15.49/6.51 % (1449359)Termination phase: Property scanning
% 15.49/6.51 % (1449359)Time elapsed: 1.597 s
% 15.49/6.51 % (1449359)Peak memory usage: 232 MB
% 15.49/6.51 % (1449359)Instructions burned: 2352 (million)
% 15.49/6.51 % (1449380)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=2437878114:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/125Mi)
% 15.49/6.51 % (1449380)Instruction limit reached!
% 15.49/6.51 % (1449380)------------------------------
% 15.49/6.51 % (1449380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449380)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449380)Termination reason: Instruction limit
% 15.49/6.51 % (1449380)Termination phase: Property scanning
% 15.49/6.51 % (1449380)Time elapsed: 0.057 s
% 15.49/6.51 % (1449380)Peak memory usage: 136 MB
% 15.49/6.51 % (1449380)Instructions burned: 127 (million)
% 15.49/6.51 % (1449381)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3935510951:i=134:gtgl=5:slsql=off:gtg=exists_sym_2954 on theBenchmark for (2954ds/134Mi)
% 15.49/6.51 % (1449381)Instruction limit reached!
% 15.49/6.51 % (1449381)------------------------------
% 15.49/6.51 % (1449381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449381)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449381)Termination reason: Instruction limit
% 15.49/6.51 % (1449381)Termination phase: Property scanning
% 15.49/6.51 % (1449381)Time elapsed: 0.063 s
% 15.49/6.51 % (1449381)Peak memory usage: 136 MB
% 15.49/6.51 % (1449381)Instructions burned: 138 (million)
% 15.49/6.51 % (1449383)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2843884472:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 15.49/6.51 % (1449383)Instruction limit reached!
% 15.49/6.51 % (1449383)------------------------------
% 15.49/6.51 % (1449383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449383)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449383)Termination reason: Instruction limit
% 15.49/6.51 % (1449383)Termination phase: SInE selection
% 15.49/6.51 % (1449383)Time elapsed: 0.105 s
% 15.49/6.51 % (1449383)Peak memory usage: 136 MB
% 15.49/6.51 % (1449383)Instructions burned: 142 (million)
% 15.49/6.51 % (1449385)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2971801155:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2952 on theBenchmark for (2952ds/431Mi)
% 15.49/6.51 % (1449387)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=3417289208:i=6060:aac=none:ins=25_2950 on theBenchmark for (2950ds/6060Mi)
% 15.49/6.51 % (1449385)Instruction limit reached!
% 15.49/6.51 % (1449385)------------------------------
% 15.49/6.51 % (1449385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449385)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449385)Termination reason: Instruction limit
% 15.49/6.51 % (1449385)Termination phase: Saturation
% 15.49/6.51 % (1449385)Time elapsed: 0.327 s
% 15.49/6.51 % (1449385)Peak memory usage: 144 MB
% 15.49/6.51 % (1449385)Instructions burned: 431 (million)
% 15.49/6.51 % (1449390)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=1239046774:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2947 on theBenchmark for (2947ds/150Mi)
% 15.49/6.51 % (1449338)First to succeed.
% 15.49/6.51 % (1449338)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1449331"
% 15.49/6.51 % (1449390)Instruction limit reached!
% 15.49/6.51 % (1449390)------------------------------
% 15.49/6.51 % (1449390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.49/6.51 % (1449390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/6.51 % (1449390)CaDiCaL version: 2.1.3
% 15.49/6.51 % (1449390)Termination reason: Instruction limit
% 15.49/6.51 % (1449390)Termination phase: SInE selection
% 15.49/6.51 % (1449390)Time elapsed: 0.121 s
% 15.49/6.51 % (1449390)Peak memory usage: 136 MB
% 15.49/6.51 % (1449390)Instructions burned: 151 (million)
% 15.49/6.51 % (1449392)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3046899556:i=14155:bd=all_2944 on theBenchmark for (2944ds/14155Mi)
% 15.49/6.51 % (1449338)Refutation found. Thanks to Tanya!
% 15.49/6.51 % SZS status Theorem for theBenchmark
% 15.49/6.51 % SZS output start Proof for theBenchmark
% See solution above
% 28.85/6.76 % (1449338)------------------------------
% 28.85/6.76 % (1449338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.85/6.76 % (1449338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.85/6.76 % (1449338)CaDiCaL version: 2.1.3
% 28.85/6.76 % (1449338)Termination reason: Refutation
% 28.85/6.76 % (1449338)Time elapsed: 3.181 s
% 28.85/6.76 % (1449338)Peak memory usage: 217 MB
% 28.85/6.76 % (1449338)Instructions burned: 5302 (million)
% 28.85/6.76 % (1449338)------------------------------
% 28.85/6.76 % (1449338)------------------------------
% 28.85/6.76 % (1449331)Success in time 5.854 s
% 28.85/6.76 % Vampire exiting
%------------------------------------------------------------------------------