%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP035+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:33:59 PM UTC 2026
% Result : Theorem 11.60s 4.18s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 105 ( 20 unt; 5 def)
% Number of atoms : 547 ( 29 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 760 ( 318 ~; 345 |; 65 &)
% ( 10 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 6 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-4 aty)
% Number of variables : 79 ( 0 sgn 71 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34366,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f34369,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(k1_tsp_2(X0,X1))
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_tsp_2) ).
fof(f34419,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)) )
=> ( v3_borsuk_1(X2,X0,X1)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( X3 = X4
=> k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4))) = k6_pre_topc(X0,k1_struct_0(X0,X3)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l33_tsp_2) ).
fof(f34424,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 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_tsp_2) ).
fof(f34425,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,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X2 = X3
=> k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X3))) = k6_pre_topc(X0,k1_struct_0(X0,X2)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_tsp_2) ).
fof(f34426,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,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X2 = X3
=> k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X3))) = k6_pre_topc(X0,k1_struct_0(X0,X2)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34425]) ).
fof(f34496,plain,
! [X0,X1] :
( ( v1_funct_1(k1_tsp_2(X0,X1))
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k1_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,[],[f34369]) ).
fof(f34497,plain,
! [X0,X1] :
( ( v1_funct_1(k1_tsp_2(X0,X1))
& v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k1_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,[],[f34496]) ).
fof(f34596,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4))) = k6_pre_topc(X0,k1_struct_0(X0,X3))
| X3 != X4
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v3_borsuk_1(X2,X0,X1)
| ~ 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,[],[f34419]) ).
fof(f34597,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4))) = k6_pre_topc(X0,k1_struct_0(X0,X3))
| X3 != X4
| ~ m1_subset_1(X4,u1_struct_0(X1)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v3_borsuk_1(X2,X0,X1)
| ~ 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,[],[f34596]) ).
fof(f34606,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ 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,[],[f34424]) ).
fof(f34607,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k1_tsp_2(X0,X1)
<=> v3_borsuk_1(X2,X0,X1) )
| ~ 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,[],[f34606]) ).
fof(f34608,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k6_pre_topc(X0,k1_struct_0(X0,X2)) != k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X3)))
& X2 = X3
& m1_subset_1(X3,u1_struct_0(X1)) )
& m1_subset_1(X2,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,[],[f34426]) ).
fof(f34609,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k6_pre_topc(X0,k1_struct_0(X0,X2)) != k5_pre_topc(X0,X1,k1_tsp_2(X0,X1),k6_pre_topc(X1,k1_struct_0(X1,X3)))
& X2 = X3
& m1_subset_1(X3,u1_struct_0(X1)) )
& m1_subset_1(X2,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,[],[f34608]) ).
fof(f35132,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f35453,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k1_tsp_2(X0,X1)
| ~ v3_borsuk_1(X2,X0,X1) )
& ( v3_borsuk_1(X2,X0,X1)
| k1_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,[],[f34607]) ).
fof(f35454,plain,
( k6_pre_topc(sK50,k1_struct_0(sK50,sK52)) != k5_pre_topc(sK50,sK51,k1_tsp_2(sK50,sK51),k6_pre_topc(sK51,k1_struct_0(sK51,sK53)))
& sK52 = sK53
& m1_subset_1(sK53,u1_struct_0(sK51))
& m1_subset_1(sK52,u1_struct_0(sK50))
& ~ v3_struct_0(sK51)
& v2_tsp_2(sK51,sK50)
& m2_tsp_1(sK51,sK50)
& ~ v3_struct_0(sK50)
& v2_pre_topc(sK50)
& l1_pre_topc(sK50) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50,sK51,sK52,sK53]),skolemize(X0,sK50),skolemize(X1,sK51),skolemize(X2,sK52),skolemize(X3,sK53)],[f34609]) ).
fof(f35647,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,[],[f35132]) ).
fof(f35780,plain,
! [X0,X1] :
( m2_relset_1(k1_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,[],[f34497]) ).
fof(f35781,plain,
! [X0,X1] :
( v5_pre_topc(k1_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,[],[f34497]) ).
fof(f35782,plain,
! [X0,X1] :
( v1_funct_2(k1_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,[],[f34497]) ).
fof(f35783,plain,
! [X0,X1] :
( v1_funct_1(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(cnf_transformation,[],[f34497]) ).
fof(f35936,plain,
! [X2,X3,X0,X1,X4] :
( k6_pre_topc(X0,k1_struct_0(X0,X3)) = k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4)))
| X3 != X4
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v3_borsuk_1(X2,X0,X1)
| ~ 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,[],[f34597]) ).
fof(f35941,plain,
! [X2,X0,X1] :
( v3_borsuk_1(X2,X0,X1)
| k1_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,[],[f35453]) ).
fof(f35943,plain,
l1_pre_topc(sK50),
inference(cnf_transformation,[],[f35454]) ).
fof(f35944,plain,
v2_pre_topc(sK50),
inference(cnf_transformation,[],[f35454]) ).
fof(f35945,plain,
~ v3_struct_0(sK50),
inference(cnf_transformation,[],[f35454]) ).
fof(f35946,plain,
m2_tsp_1(sK51,sK50),
inference(cnf_transformation,[],[f35454]) ).
fof(f35947,plain,
v2_tsp_2(sK51,sK50),
inference(cnf_transformation,[],[f35454]) ).
fof(f35948,plain,
~ v3_struct_0(sK51),
inference(cnf_transformation,[],[f35454]) ).
fof(f35949,plain,
m1_subset_1(sK52,u1_struct_0(sK50)),
inference(cnf_transformation,[],[f35454]) ).
fof(f35950,plain,
m1_subset_1(sK53,u1_struct_0(sK51)),
inference(cnf_transformation,[],[f35454]) ).
fof(f35951,plain,
sK52 = sK53,
inference(cnf_transformation,[],[f35454]) ).
fof(f35952,plain,
k6_pre_topc(sK50,k1_struct_0(sK50,sK52)) != k5_pre_topc(sK50,sK51,k1_tsp_2(sK50,sK51),k6_pre_topc(sK51,k1_struct_0(sK51,sK53))),
inference(cnf_transformation,[],[f35454]) ).
fof(f36606,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f35647]) ).
fof(f37154,plain,
! [X2,X0,X1,X4] :
( k6_pre_topc(X0,k1_struct_0(X0,X4)) = k5_pre_topc(X0,X1,X2,k6_pre_topc(X1,k1_struct_0(X1,X4)))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v3_borsuk_1(X2,X0,X1)
| ~ 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,[],[f35936]) ).
fof(f37159,plain,
! [X0,X1] :
( ~ v1_funct_2(k1_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(k1_tsp_2(X0,X1))
| v3_borsuk_1(k1_tsp_2(X0,X1),X0,X1)
| ~ v5_pre_topc(k1_tsp_2(X0,X1),X0,X1)
| ~ m2_relset_1(k1_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,[],[f35941]) ).
fof(f37307,definition,
( spl225_3
<=> m1_pre_topc(sK51,sK50) ),
introduced(definition,[new_symbols(definition,[spl225_3])],[avatar_definition]) ).
fof(f37308,plain,
( ~ m1_pre_topc(sK51,sK50)
| spl225_3 ),
inference(avatar_component_clause,[],[f37307]) ).
fof(f37345,plain,
( ~ m2_tsp_1(sK51,sK50)
| ~ l1_pre_topc(sK50)
| spl225_3 ),
inference(resolution,[],[f37308,f36606]) ).
fof(f37348,plain,
( ~ l1_pre_topc(sK50)
| spl225_3 ),
inference(forward_subsumption_resolution,[],[f37345,f35946]) ).
fof(f37353,plain,
( $false
| spl225_3 ),
inference(forward_subsumption_resolution,[],[f37348,f35943]) ).
fof(f37354,plain,
spl225_3,
inference(avatar_contradiction_clause,[],[f37353]) ).
fof(f37360,plain,
m1_subset_1(sK52,u1_struct_0(sK51)),
inference(forward_demodulation,[],[f35950,f35951]) ).
fof(f37445,plain,
k6_pre_topc(sK50,k1_struct_0(sK50,sK52)) != k5_pre_topc(sK50,sK51,k1_tsp_2(sK50,sK51),k6_pre_topc(sK51,k1_struct_0(sK51,sK52))),
inference(forward_demodulation,[],[f35952,f35951]) ).
fof(f37475,plain,
( k6_pre_topc(sK50,k1_struct_0(sK50,sK52)) != k6_pre_topc(sK50,k1_struct_0(sK50,sK52))
| ~ m1_subset_1(sK52,u1_struct_0(sK51))
| ~ m1_subset_1(sK52,u1_struct_0(sK50))
| ~ v3_borsuk_1(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(superposition,[],[f37445,f37154]) ).
fof(f37477,plain,
( ~ m1_subset_1(sK52,u1_struct_0(sK51))
| ~ m1_subset_1(sK52,u1_struct_0(sK50))
| ~ v3_borsuk_1(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(trivial_inequality_removal,[],[f37475]) ).
fof(f37479,plain,
( ~ m1_subset_1(sK52,u1_struct_0(sK51))
| ~ m1_subset_1(sK52,u1_struct_0(sK50))
| ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37477,f37159]) ).
fof(f37487,plain,
( ~ m1_subset_1(sK52,u1_struct_0(sK50))
| ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37479,f37360]) ).
fof(f37508,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37487,f35949]) ).
fof(f37514,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v2_tsp_2(sK51,sK50)
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37508,f35948]) ).
fof(f37516,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ m2_tsp_1(sK51,sK50)
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37514,f35947]) ).
fof(f37518,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37516,f35946]) ).
fof(f37520,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37518,f35945]) ).
fof(f37522,definition,
( spl225_23
<=> m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51)) ),
introduced(definition,[new_symbols(definition,[spl225_23])],[avatar_definition]) ).
fof(f37523,plain,
( ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| spl225_23 ),
inference(avatar_component_clause,[],[f37522]) ).
fof(f37525,definition,
( spl225_24
<=> v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51) ),
introduced(definition,[new_symbols(definition,[spl225_24])],[avatar_definition]) ).
fof(f37526,plain,
( ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| spl225_24 ),
inference(avatar_component_clause,[],[f37525]) ).
fof(f37528,definition,
( spl225_25
<=> v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51)) ),
introduced(definition,[new_symbols(definition,[spl225_25])],[avatar_definition]) ).
fof(f37529,plain,
( ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| spl225_25 ),
inference(avatar_component_clause,[],[f37528]) ).
fof(f37531,definition,
( spl225_26
<=> v1_funct_1(k1_tsp_2(sK50,sK51)) ),
introduced(definition,[new_symbols(definition,[spl225_26])],[avatar_definition]) ).
fof(f37532,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| spl225_26 ),
inference(avatar_component_clause,[],[f37531]) ).
fof(f37543,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ l1_pre_topc(sK50) ),
inference(forward_subsumption_resolution,[],[f37520,f35944]) ).
fof(f37544,plain,
( ~ v1_funct_1(k1_tsp_2(sK50,sK51))
| ~ v1_funct_2(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51))
| ~ v5_pre_topc(k1_tsp_2(sK50,sK51),sK50,sK51)
| ~ m2_relset_1(k1_tsp_2(sK50,sK51),u1_struct_0(sK50),u1_struct_0(sK51)) ),
inference(forward_subsumption_resolution,[],[f37543,f35943]) ).
fof(f37545,plain,
( ~ spl225_23
| ~ spl225_24
| ~ spl225_25
| ~ spl225_26 ),
inference(avatar_split_clause,[],[f37544,f37531,f37528,f37525,f37522]) ).
fof(f37629,plain,
( v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_26 ),
inference(resolution,[],[f37532,f35783]) ).
fof(f37631,plain,
( ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_26 ),
inference(forward_subsumption_resolution,[],[f37629,f35945]) ).
fof(f37632,plain,
( ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_26 ),
inference(forward_subsumption_resolution,[],[f37631,f35944]) ).
fof(f37633,plain,
( v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_26 ),
inference(forward_subsumption_resolution,[],[f37632,f35943]) ).
fof(f37634,plain,
( ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_26 ),
inference(forward_subsumption_resolution,[],[f37633,f35948]) ).
fof(f37635,plain,
( ~ m1_pre_topc(sK51,sK50)
| spl225_26 ),
inference(forward_subsumption_resolution,[],[f37634,f35947]) ).
fof(f37636,plain,
( ~ spl225_3
| spl225_26 ),
inference(avatar_split_clause,[],[f37635,f37531,f37307]) ).
fof(f37648,plain,
( v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_23 ),
inference(resolution,[],[f37523,f35780]) ).
fof(f37676,plain,
( ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_23 ),
inference(forward_subsumption_resolution,[],[f37648,f35945]) ).
fof(f37677,plain,
( ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_23 ),
inference(forward_subsumption_resolution,[],[f37676,f35944]) ).
fof(f37678,plain,
( v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_23 ),
inference(forward_subsumption_resolution,[],[f37677,f35943]) ).
fof(f37679,plain,
( ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_23 ),
inference(forward_subsumption_resolution,[],[f37678,f35948]) ).
fof(f37680,plain,
( ~ m1_pre_topc(sK51,sK50)
| spl225_23 ),
inference(forward_subsumption_resolution,[],[f37679,f35947]) ).
fof(f37681,plain,
( ~ spl225_3
| spl225_23 ),
inference(avatar_split_clause,[],[f37680,f37522,f37307]) ).
fof(f37684,plain,
( v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_24 ),
inference(resolution,[],[f37526,f35781]) ).
fof(f37685,plain,
( ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_24 ),
inference(forward_subsumption_resolution,[],[f37684,f35945]) ).
fof(f37686,plain,
( ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_24 ),
inference(forward_subsumption_resolution,[],[f37685,f35944]) ).
fof(f37687,plain,
( v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_24 ),
inference(forward_subsumption_resolution,[],[f37686,f35943]) ).
fof(f37688,plain,
( ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_24 ),
inference(forward_subsumption_resolution,[],[f37687,f35948]) ).
fof(f37689,plain,
( ~ m1_pre_topc(sK51,sK50)
| spl225_24 ),
inference(forward_subsumption_resolution,[],[f37688,f35947]) ).
fof(f37690,plain,
( ~ spl225_3
| spl225_24 ),
inference(avatar_split_clause,[],[f37689,f37525,f37307]) ).
fof(f37691,plain,
( v3_struct_0(sK50)
| ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_25 ),
inference(resolution,[],[f37529,f35782]) ).
fof(f37692,plain,
( ~ v2_pre_topc(sK50)
| ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_25 ),
inference(forward_subsumption_resolution,[],[f37691,f35945]) ).
fof(f37693,plain,
( ~ l1_pre_topc(sK50)
| v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_25 ),
inference(forward_subsumption_resolution,[],[f37692,f35944]) ).
fof(f37694,plain,
( v3_struct_0(sK51)
| ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_25 ),
inference(forward_subsumption_resolution,[],[f37693,f35943]) ).
fof(f37695,plain,
( ~ v2_tsp_2(sK51,sK50)
| ~ m1_pre_topc(sK51,sK50)
| spl225_25 ),
inference(forward_subsumption_resolution,[],[f37694,f35948]) ).
fof(f37696,plain,
( ~ m1_pre_topc(sK51,sK50)
| spl225_25 ),
inference(forward_subsumption_resolution,[],[f37695,f35947]) ).
fof(f37697,plain,
( ~ spl225_3
| spl225_25 ),
inference(avatar_split_clause,[],[f37696,f37528,f37307]) ).
cnf(s12,plain,
spl225_3,
inference(sat_conversion,[],[f37354]) ).
cnf(s32,plain,
( ~ spl225_23
| ~ spl225_24
| ~ spl225_25
| ~ spl225_26 ),
inference(sat_conversion,[],[f37545]) ).
cnf(s45,plain,
( ~ spl225_3
| spl225_26 ),
inference(sat_conversion,[],[f37636]) ).
cnf(s50,plain,
( ~ spl225_3
| spl225_23 ),
inference(sat_conversion,[],[f37681]) ).
cnf(s51,plain,
( ~ spl225_3
| spl225_24 ),
inference(sat_conversion,[],[f37690]) ).
cnf(s52,plain,
( ~ spl225_3
| spl225_25 ),
inference(sat_conversion,[],[f37697]) ).
cnf(s54,plain,
spl225_25,
inference(rat,[],[s52,s12]) ).
cnf(s55,plain,
spl225_24,
inference(rat,[],[s51,s12]) ).
cnf(s56,plain,
spl225_23,
inference(rat,[],[s50,s12]) ).
cnf(s57,plain,
spl225_26,
inference(rat,[],[s45,s12]) ).
cnf(s58,plain,
$false,
inference(rat,[],[s32,s57,s54,s55,s56]) ).
fof(f37698,plain,
$false,
inference(avatar_sat_refutation,[],[s58]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP035+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n016.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 19:03:42 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.60/4.17 % (3898480)Detected formulas, will run a generic FOF schedule.
% 11.60/4.17 % (3898490)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3821176416:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 11.60/4.17 % (3898485)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=1630016520:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 11.60/4.17 % (3898490)Instruction limit reached!
% 11.60/4.17 % (3898490)------------------------------
% 11.60/4.17 % (3898490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898490)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898490)Termination reason: Instruction limit
% 11.60/4.17 % (3898490)Termination phase: Property scanning
% 11.60/4.17 % (3898490)Time elapsed: 0.035 s
% 11.60/4.17 % (3898490)Peak memory usage: 136 MB
% 11.60/4.17 % (3898490)Instructions burned: 142 (million)
% 11.60/4.17 % (3898486)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=2097437681:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 11.60/4.17 % (3898489)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2334690067:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 11.60/4.17 % (3898487)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=3214474128:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 11.60/4.17 % (3898488)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=687910712:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 11.60/4.17 % (3898491)dis-21_1_sil=8000:lcm=predicate:random_seed=3482874214: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)
% 11.60/4.17 % (3898488)Instruction limit reached!
% 11.60/4.17 % (3898488)------------------------------
% 11.60/4.17 % (3898488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898488)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898488)Termination reason: Instruction limit
% 11.60/4.17 % (3898488)Termination phase: SInE selection
% 11.60/4.17 % (3898488)Time elapsed: 0.080 s
% 11.60/4.17 % (3898488)Peak memory usage: 136 MB
% 11.60/4.17 % (3898488)Instructions burned: 110 (million)
% 11.60/4.17 % (3898489)Instruction limit reached!
% 11.60/4.17 % (3898489)------------------------------
% 11.60/4.17 % (3898489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898489)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898489)Termination reason: Instruction limit
% 11.60/4.17 % (3898489)Termination phase: SInE selection
% 11.60/4.17 % (3898489)Time elapsed: 0.085 s
% 11.60/4.17 % (3898489)Peak memory usage: 136 MB
% 11.60/4.17 % (3898489)Instructions burned: 119 (million)
% 11.60/4.17 % (3898491)Instruction limit reached!
% 11.60/4.17 % (3898491)------------------------------
% 11.60/4.17 % (3898491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898491)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898491)Termination reason: Instruction limit
% 11.60/4.17 % (3898491)Termination phase: SInE selection
% 11.60/4.17 % (3898491)Time elapsed: 0.098 s
% 11.60/4.17 % (3898491)Peak memory usage: 136 MB
% 11.60/4.17 % (3898491)Instructions burned: 130 (million)
% 11.60/4.17 % (3898498)lrs+10_1_sil=8000:sp=occurrence:random_seed=1911004154:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 11.60/4.17 % (3898501)lrs+1011_1_sil=32000:sp=occurrence:random_seed=162139361:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 11.60/4.17 % (3898500)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3392336851:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 11.60/4.17 % (3898498)Instruction limit reached!
% 11.60/4.17 % (3898498)------------------------------
% 11.60/4.17 % (3898498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898498)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898498)Termination reason: Instruction limit
% 11.60/4.17 % (3898498)Termination phase: Preprocessing 3
% 11.60/4.17 % (3898498)Time elapsed: 0.137 s
% 11.60/4.17 % (3898498)Peak memory usage: 140 MB
% 11.60/4.17 % (3898498)Instructions burned: 287 (million)
% 11.60/4.17 % (3898503)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=4106857655:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 11.60/4.17 % (3898500)Instruction limit reached!
% 11.60/4.17 % (3898500)------------------------------
% 11.60/4.17 % (3898500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898500)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898500)Termination reason: Instruction limit
% 11.60/4.17 % (3898500)Termination phase: Property scanning
% 11.60/4.17 % (3898500)Time elapsed: 0.071 s
% 11.60/4.17 % (3898500)Peak memory usage: 136 MB
% 11.60/4.17 % (3898500)Instructions burned: 157 (million)
% 11.60/4.17 % (3898503)Instruction limit reached!
% 11.60/4.17 % (3898503)------------------------------
% 11.60/4.17 % (3898503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898503)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898503)Termination reason: Instruction limit
% 11.60/4.17 % (3898503)Termination phase: Property scanning
% 11.60/4.17 % (3898503)Time elapsed: 0.108 s
% 11.60/4.17 % (3898503)Peak memory usage: 136 MB
% 11.60/4.17 % (3898503)Instructions burned: 250 (million)
% 11.60/4.17 % (3898506)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3225154898:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 11.60/4.17 % (3898508)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3890310910:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 11.60/4.17 % (3898506)Instruction limit reached!
% 11.60/4.17 % (3898506)------------------------------
% 11.60/4.17 % (3898506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898506)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898506)Termination reason: Instruction limit
% 11.60/4.17 % (3898506)Termination phase: SInE selection
% 11.60/4.17 % (3898506)Time elapsed: 0.104 s
% 11.60/4.17 % (3898506)Peak memory usage: 136 MB
% 11.60/4.17 % (3898506)Instructions burned: 294 (million)
% 11.60/4.17 % (3898501)Instruction limit reached!
% 11.60/4.17 % (3898501)------------------------------
% 11.60/4.17 % (3898501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898501)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898501)Termination reason: Instruction limit
% 11.60/4.17 % (3898501)Termination phase: Saturation
% 11.60/4.17 % (3898501)Time elapsed: 0.253 s
% 11.60/4.17 % (3898501)Peak memory usage: 142 MB
% 11.60/4.17 % (3898501)Instructions burned: 325 (million)
% 11.60/4.17 % (3898510)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2351383035:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 11.60/4.17 % (3898512)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3107413106:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 11.60/4.17 % (3898510)Instruction limit reached!
% 11.60/4.17 % (3898510)------------------------------
% 11.60/4.17 % (3898510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898510)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898510)Termination reason: Instruction limit
% 11.60/4.17 % (3898510)Termination phase: SInE selection
% 11.60/4.17 % (3898510)Time elapsed: 0.086 s
% 11.60/4.17 % (3898510)Peak memory usage: 135 MB
% 11.60/4.17 % (3898510)Instructions burned: 113 (million)
% 11.60/4.17 % (3898513)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1592467717:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2971 on theBenchmark for (2971ds/114Mi)
% 11.60/4.17 % (3898512)Instruction limit reached!
% 11.60/4.17 % (3898512)------------------------------
% 11.60/4.17 % (3898512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898512)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898512)Termination reason: Instruction limit
% 11.60/4.17 % (3898512)Termination phase: Preprocessing 1
% 11.60/4.17 % (3898512)Time elapsed: 0.057 s
% 11.60/4.17 % (3898512)Peak memory usage: 137 MB
% 11.60/4.17 % (3898512)Instructions burned: 129 (million)
% 11.60/4.17 % (3898513)Instruction limit reached!
% 11.60/4.17 % (3898513)------------------------------
% 11.60/4.17 % (3898513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/4.17 % (3898513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/4.17 % (3898513)CaDiCaL version: 2.1.3
% 11.60/4.17 % (3898513)Termination reason: Instruction limit
% 11.60/4.17 % (3898513)Termination phase: Property scanning
% 11.60/4.17 % (3898513)Time elapsed: 0.051 s
% 11.60/4.17 % (3898513)Peak memory usage: 136 MB
% 11.60/4.17 % (3898513)Instructions burned: 114 (million)
% 11.60/4.17 % (3898516)lrs+10_1_sil=8000:sp=occurrence:random_seed=3780438628:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 11.60/4.18 % (3898518)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=304541311:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 11.60/4.18 % (3898519)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4201690278:i=5202:ss=axioms:sgt=16_2969 on theBenchmark for (2969ds/5202Mi)
% 11.60/4.18 % (3898518)First to succeed.
% 11.60/4.18 % (3898518)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3898480"
% 11.60/4.18 % (3898518)Refutation found. Thanks to Tanya!
% 11.60/4.18 % SZS status Theorem for theBenchmark
% 11.60/4.18 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/4.42 % (3898518)------------------------------
% 0.20/4.42 % (3898518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/4.42 % (3898518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/4.42 % (3898518)CaDiCaL version: 2.1.3
% 0.20/4.42 % (3898518)Termination reason: Refutation
% 0.20/4.42 % (3898518)Time elapsed: 0.147 s
% 0.20/4.42 % (3898518)Peak memory usage: 144 MB
% 0.20/4.42 % (3898518)Instructions burned: 352 (million)
% 0.20/4.42 % (3898518)------------------------------
% 0.20/4.42 % (3898518)------------------------------
% 0.20/4.42 % (3898480)Success in time 3.497 s
% 0.20/4.42 % Vampire exiting
%------------------------------------------------------------------------------