%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP037+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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.74s 5.37s
% Output : Refutation 29.24s
% 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(f13310,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(f13368,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(f13461,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f13469,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f13489,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l19_tsp_2) ).
fof(f13527,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X3 = u1_struct_0(X1)
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
=> k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_tsp_2) ).
fof(f13529,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(f13530,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)],[f13529]) ).
fof(f13597,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f13469]) ).
fof(f13598,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,[],[f13597]) ).
fof(f13637,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(u1_struct_0(X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13489]) ).
fof(f13638,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,[],[f13637]) ).
fof(f13713,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k4_tsp_2(X0,X1)
<=> ! [X3] :
( ! [X4] :
( k5_subset_1(u1_struct_0(X0),X3,k3_tex_4(X0,X4)) = k4_pre_topc(X0,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0))) )
| u1_struct_0(X1) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v5_pre_topc(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m2_tsp_1(X1,X0) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13527]) ).
fof(f13714,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,[],[f13713]) ).
fof(f13717,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,[],[f13530]) ).
fof(f13718,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,[],[f13717]) ).
fof(f13946,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,[],[f13368]) ).
fof(f13947,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,[],[f13946]) ).
fof(f13978,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,[],[f13310]) ).
fof(f13979,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,[],[f13978]) ).
fof(f14198,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13461]) ).
fof(f14461,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,[],[f13714]) ).
fof(f14462,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,[],[f14461]) ).
fof(f14463,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))],[f14462]) ).
fof(f14464,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)],[f13718]) ).
fof(f14630,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,[],[f14198]) ).
fof(f14750,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,[],[f13598]) ).
fof(f14751,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,[],[f13598]) ).
fof(f14752,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,[],[f13598]) ).
fof(f14753,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,[],[f13598]) ).
fof(f14806,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,[],[f13638]) ).
fof(f14912,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,[],[f14463]) ).
fof(f14918,plain,
l1_pre_topc(sK27),
inference(cnf_transformation,[],[f14464]) ).
fof(f14919,plain,
v2_pre_topc(sK27),
inference(cnf_transformation,[],[f14464]) ).
fof(f14920,plain,
~ v3_struct_0(sK27),
inference(cnf_transformation,[],[f14464]) ).
fof(f14921,plain,
m2_tsp_1(sK28,sK27),
inference(cnf_transformation,[],[f14464]) ).
fof(f14922,plain,
v2_tsp_2(sK28,sK27),
inference(cnf_transformation,[],[f14464]) ).
fof(f14923,plain,
~ v3_struct_0(sK28),
inference(cnf_transformation,[],[f14464]) ).
fof(f14924,plain,
m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27))),
inference(cnf_transformation,[],[f14464]) ).
fof(f14925,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,[],[f14464]) ).
fof(f15252,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,[],[f13947]) ).
fof(f15272,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,[],[f13979]) ).
fof(f15558,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14630]) ).
fof(f16068,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,[],[f14912]) ).
fof(f16069,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,[],[f16068]) ).
fof(f16205,definition,
( spl223_1
<=> m2_tsp_1(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl223_1])],[avatar_definition]) ).
fof(f16207,plain,
( m2_tsp_1(sK28,sK27)
| ~ spl223_1 ),
inference(avatar_component_clause,[],[f16205]) ).
fof(f16208,plain,
spl223_1,
inference(avatar_split_clause,[],[f14921,f16205]) ).
fof(f16212,plain,
( m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ l1_pre_topc(sK27)
| ~ spl223_1 ),
inference(resolution,[],[f16207,f14806]) ).
fof(f16256,plain,
( m1_pre_topc(sK28,sK27)
| ~ l1_pre_topc(sK27)
| ~ spl223_1 ),
inference(resolution,[],[f16207,f15558]) ).
fof(f16342,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) )
| ~ spl223_1 ),
inference(resolution,[],[f16207,f16069]) ).
fof(f16353,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) )
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16342,f14923]) ).
fof(f16436,plain,
( m1_pre_topc(sK28,sK27)
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16256,f14918]) ).
fof(f16475,plain,
( m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ l1_pre_topc(sK27)
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16212,f14920]) ).
fof(f16480,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) )
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16353,f14922]) ).
fof(f16584,plain,
( m1_subset_1(u1_struct_0(sK28),k1_zfmisc_1(u1_struct_0(sK27)))
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16475,f14918]) ).
fof(f16589,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) )
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16480,f14920]) ).
fof(f16659,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) )
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16589,f16584]) ).
fof(f16723,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) )
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16659,f14919]) ).
fof(f16769,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)) )
| ~ spl223_1 ),
inference(forward_subsumption_resolution,[],[f16723,f14918]) ).
fof(f16821,definition,
( spl223_2
<=> v3_struct_0(sK27) ),
introduced(definition,[new_symbols(definition,[spl223_2])],[avatar_definition]) ).
fof(f16823,plain,
( ~ v3_struct_0(sK27)
| spl223_2 ),
inference(avatar_component_clause,[],[f16821]) ).
fof(f16824,plain,
~ spl223_2,
inference(avatar_split_clause,[],[f14920,f16821]) ).
fof(f16826,definition,
( spl223_3
<=> v3_struct_0(sK28) ),
introduced(definition,[new_symbols(definition,[spl223_3])],[avatar_definition]) ).
fof(f16828,plain,
( ~ v3_struct_0(sK28)
| spl223_3 ),
inference(avatar_component_clause,[],[f16826]) ).
fof(f16829,plain,
~ spl223_3,
inference(avatar_split_clause,[],[f14923,f16826]) ).
fof(f16831,definition,
( spl223_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,[spl223_4])],[avatar_definition]) ).
fof(f16833,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))
| spl223_4 ),
inference(avatar_component_clause,[],[f16831]) ).
fof(f16834,plain,
~ spl223_4,
inference(avatar_split_clause,[],[f14925,f16831]) ).
fof(f16836,definition,
( spl223_5
<=> m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27))) ),
introduced(definition,[new_symbols(definition,[spl223_5])],[avatar_definition]) ).
fof(f16838,plain,
( m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| ~ spl223_5 ),
inference(avatar_component_clause,[],[f16836]) ).
fof(f16839,plain,
spl223_5,
inference(avatar_split_clause,[],[f14924,f16836]) ).
fof(f22645,definition,
( spl223_6
<=> v2_tsp_2(sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl223_6])],[avatar_definition]) ).
fof(f22647,plain,
( v2_tsp_2(sK28,sK27)
| ~ spl223_6 ),
inference(avatar_component_clause,[],[f22645]) ).
fof(f22648,plain,
spl223_6,
inference(avatar_split_clause,[],[f14922,f22645]) ).
fof(f22663,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)
| ~ spl223_6 ),
inference(resolution,[],[f22647,f14750]) ).
fof(f22664,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)
| ~ spl223_6 ),
inference(resolution,[],[f22647,f14751]) ).
fof(f22665,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)
| ~ spl223_6 ),
inference(resolution,[],[f22647,f14752]) ).
fof(f22666,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)
| ~ spl223_6 ),
inference(resolution,[],[f22647,f14753]) ).
fof(f22766,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22666,f16823]) ).
fof(f22767,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22665,f16823]) ).
fof(f22768,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22664,f16823]) ).
fof(f22769,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22663,f16823]) ).
fof(f22797,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22766,f14919]) ).
fof(f22798,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22767,f14919]) ).
fof(f22799,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ l1_pre_topc(sK27)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22768,f14919]) ).
fof(f22800,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22769,f14919]) ).
fof(f22828,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22797,f14918]) ).
fof(f22829,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22798,f14918]) ).
fof(f22830,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| v3_struct_0(sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22799,f14918]) ).
fof(f22831,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)
| spl223_2
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22800,f14918]) ).
fof(f22859,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22828,f16828]) ).
fof(f22860,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22829,f16828]) ).
fof(f22861,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22830,f16828]) ).
fof(f22862,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ m1_pre_topc(sK28,sK27)
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22831,f16828]) ).
fof(f22882,plain,
( v1_funct_1(k4_tsp_2(sK27,sK28))
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22859,f16436]) ).
fof(f22883,plain,
( v1_funct_2(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22860,f16436]) ).
fof(f22884,plain,
( v5_pre_topc(k4_tsp_2(sK27,sK28),sK27,sK28)
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22861,f16436]) ).
fof(f22885,plain,
( m2_relset_1(k4_tsp_2(sK27,sK28),u1_struct_0(sK27),u1_struct_0(sK28))
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22862,f16436]) ).
fof(f22902,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)) )
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(backward_subsumption_resolution,[],[f16769,f22882]) ).
fof(f22913,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)) )
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22902,f22883]) ).
fof(f22916,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)) )
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22913,f22884]) ).
fof(f22919,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))) )
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(forward_subsumption_resolution,[],[f22916,f22885]) ).
fof(f22925,definition,
( spl223_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,[spl223_7])],[avatar_definition]) ).
fof(f22926,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))) )
| ~ spl223_7 ),
inference(avatar_component_clause,[],[f22925]) ).
fof(f22927,plain,
( spl223_7
| ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6 ),
inference(avatar_split_clause,[],[f22919,f22645,f16826,f16821,f16205,f22925]) ).
fof(f22943,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) )
| ~ spl223_7 ),
inference(superposition,[],[f22926,f15272]) ).
fof(f23002,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) )
| ~ spl223_7 ),
inference(forward_subsumption_resolution,[],[f22943,f15252]) ).
fof(f23043,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) )
| spl223_2
| ~ spl223_7 ),
inference(forward_subsumption_resolution,[],[f23002,f16823]) ).
fof(f23068,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))) )
| spl223_2
| ~ spl223_7 ),
inference(forward_subsumption_resolution,[],[f23043,f14918]) ).
fof(f28148,definition,
( spl223_24
<=> ! [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,[spl223_24])],[avatar_definition]) ).
fof(f28149,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))) )
| ~ spl223_24 ),
inference(avatar_component_clause,[],[f28148]) ).
fof(f28150,plain,
( spl223_24
| spl223_2
| ~ spl223_7 ),
inference(avatar_split_clause,[],[f23068,f22925,f16821,f28148]) ).
fof(f28169,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)))
| spl223_4
| ~ spl223_24 ),
inference(superposition,[],[f16833,f28149]) ).
fof(f28182,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| spl223_4
| ~ spl223_7
| ~ spl223_24 ),
inference(forward_subsumption_resolution,[],[f28169,f22926]) ).
fof(f28193,plain,
( $false
| spl223_4
| ~ spl223_5
| ~ spl223_7
| ~ spl223_24 ),
inference(forward_subsumption_resolution,[],[f28182,f16838]) ).
fof(f28194,plain,
( spl223_4
| ~ spl223_5
| ~ spl223_7
| ~ spl223_24 ),
inference(avatar_contradiction_clause,[],[f28193]) ).
cnf(s1,plain,
spl223_1,
inference(sat_conversion,[],[f16208]) ).
cnf(s2,plain,
~ spl223_2,
inference(sat_conversion,[],[f16824]) ).
cnf(s3,plain,
~ spl223_3,
inference(sat_conversion,[],[f16829]) ).
cnf(s4,plain,
~ spl223_4,
inference(sat_conversion,[],[f16834]) ).
cnf(s5,plain,
spl223_5,
inference(sat_conversion,[],[f16839]) ).
cnf(s6,plain,
spl223_6,
inference(sat_conversion,[],[f22648]) ).
cnf(s7,plain,
( ~ spl223_1
| spl223_2
| spl223_3
| ~ spl223_6
| spl223_7 ),
inference(sat_conversion,[],[f22927]) ).
cnf(s24,plain,
( spl223_2
| ~ spl223_7
| spl223_24 ),
inference(sat_conversion,[],[f28150]) ).
cnf(s25,plain,
( spl223_4
| ~ spl223_5
| ~ spl223_7
| ~ spl223_24 ),
inference(sat_conversion,[],[f28194]) ).
cnf(s37,plain,
spl223_7,
inference(rat,[],[s7,s2,s6,s3,s1]) ).
cnf(s41,plain,
spl223_24,
inference(rat,[],[s24,s2,s37]) ).
cnf(s42,plain,
$false,
inference(rat,[],[s25,s4,s5,s41,s37]) ).
fof(f28229,plain,
$false,
inference(avatar_sat_refutation,[],[s42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP037+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 19:02:15 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 17.40/3.85 % (1877466)Detected formulas, will run a generic FOF schedule.
% 17.40/3.85 % (1877607)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4139528697:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 17.40/3.85 % (1877609)dis-21_1_sil=8000:lcm=predicate:random_seed=606967246:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 17.40/3.85 % (1877603)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=341490668:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 17.40/3.85 % (1877605)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=1667727892:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 17.40/3.85 % (1877608)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1160895945:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 17.40/3.85 % (1877604)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=3286970624:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 17.40/3.85 % (1877607)Instruction limit reached!
% 17.40/3.85 % (1877607)------------------------------
% 17.40/3.85 % (1877607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.85 % (1877607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.85 % (1877607)CaDiCaL version: 2.1.3
% 17.40/3.85 % (1877607)Termination reason: Instruction limit
% 17.40/3.85 % (1877607)Termination phase: Naming
% 17.40/3.85 % (1877607)Time elapsed: 0.061 s
% 17.40/3.85 % (1877607)Peak memory usage: 106 MB
% 17.40/3.85 % (1877607)Instructions burned: 120 (million)
% 17.40/3.85 % (1877606)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2649805248:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 17.40/3.85 % (1877608)Instruction limit reached!
% 17.40/3.85 % (1877608)------------------------------
% 17.40/3.85 % (1877608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.85 % (1877608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.85 % (1877608)CaDiCaL version: 2.1.3
% 17.40/3.85 % (1877608)Termination reason: Instruction limit
% 17.40/3.85 % (1877608)Termination phase: Property scanning
% 17.40/3.85 % (1877608)Time elapsed: 0.058 s
% 17.40/3.85 % (1877608)Peak memory usage: 102 MB
% 17.40/3.85 % (1877608)Instructions burned: 139 (million)
% 17.40/3.85 % (1877609)Instruction limit reached!
% 17.40/3.85 % (1877609)------------------------------
% 17.40/3.85 % (1877609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.85 % (1877609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.85 % (1877609)CaDiCaL version: 2.1.3
% 17.40/3.85 % (1877609)Termination reason: Instruction limit
% 17.40/3.85 % (1877609)Termination phase: Preprocessing 1
% 17.40/3.85 % (1877609)Time elapsed: 0.096 s
% 17.40/3.85 % (1877609)Peak memory usage: 103 MB
% 17.40/3.85 % (1877609)Instructions burned: 129 (million)
% 17.40/3.85 % (1877617)lrs+10_1_sil=8000:sp=occurrence:random_seed=4108124064:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 17.40/3.85 % (1877606)Instruction limit reached!
% 17.40/3.85 % (1877606)------------------------------
% 17.40/3.85 % (1877606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.85 % (1877606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.85 % (1877606)CaDiCaL version: 2.1.3
% 17.40/3.85 % (1877606)Termination reason: Instruction limit
% 17.40/3.85 % (1877606)Termination phase: Saturation
% 17.40/3.85 % (1877606)Time elapsed: 0.122 s
% 17.40/3.85 % (1877606)Peak memory usage: 107 MB
% 17.40/3.85 % (1877606)Instructions burned: 110 (million)
% 17.40/3.85 % (1877618)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3691466296:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 17.40/3.85 % (1877617)Instruction limit reached!
% 17.40/3.85 % (1877617)------------------------------
% 17.40/3.85 % (1877617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.85 % (1877617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.85 % (1877617)CaDiCaL version: 2.1.3
% 17.40/3.85 % (1877617)Termination reason: Instruction limit
% 15.74/5.37 % (1877617)Termination phase: Saturation
% 15.74/5.37 % (1877617)Time elapsed: 0.104 s
% 15.74/5.37 % (1877617)Peak memory usage: 110 MB
% 15.74/5.37 % (1877617)Instructions burned: 287 (million)
% 15.74/5.37 % (1877619)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1735650315:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.74/5.37 % (1877618)Instruction limit reached!
% 15.74/5.37 % (1877618)------------------------------
% 15.74/5.37 % (1877618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877618)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877618)Termination reason: Instruction limit
% 15.74/5.37 % (1877618)Termination phase: Property scanning
% 15.74/5.37 % (1877618)Time elapsed: 0.067 s
% 15.74/5.37 % (1877618)Peak memory usage: 102 MB
% 15.74/5.37 % (1877618)Instructions burned: 159 (million)
% 15.74/5.37 % (1877621)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=850209674:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 15.74/5.37 % (1877623)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3655119425:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 15.74/5.37 % (1877625)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1515965908:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 15.74/5.37 % (1877621)Instruction limit reached!
% 15.74/5.37 % (1877621)------------------------------
% 15.74/5.37 % (1877621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877621)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877621)Termination reason: Instruction limit
% 15.74/5.37 % (1877621)Termination phase: SInE selection
% 15.74/5.37 % (1877621)Time elapsed: 0.173 s
% 15.74/5.37 % (1877621)Peak memory usage: 103 MB
% 15.74/5.37 % (1877621)Instructions burned: 252 (million)
% 15.74/5.37 % (1877619)Instruction limit reached!
% 15.74/5.37 % (1877619)------------------------------
% 15.74/5.37 % (1877619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877619)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877619)Termination reason: Instruction limit
% 15.74/5.37 % (1877619)Termination phase: Saturation
% 15.74/5.37 % (1877619)Time elapsed: 0.303 s
% 15.74/5.37 % (1877619)Peak memory usage: 109 MB
% 15.74/5.37 % (1877619)Instructions burned: 325 (million)
% 15.74/5.37 % (1877623)Instruction limit reached!
% 15.74/5.37 % (1877623)------------------------------
% 15.74/5.37 % (1877623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877623)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877623)Termination reason: Instruction limit
% 15.74/5.37 % (1877623)Termination phase: Saturation
% 15.74/5.37 % (1877623)Time elapsed: 0.174 s
% 15.74/5.37 % (1877623)Peak memory usage: 110 MB
% 15.74/5.37 % (1877623)Instructions burned: 295 (million)
% 15.74/5.37 % (1877637)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3429059627:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 15.74/5.37 % (1877644)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2975683796:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 15.74/5.37 % (1877645)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2412905393:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 15.74/5.37 % (1877637)Instruction limit reached!
% 15.74/5.37 % (1877637)------------------------------
% 15.74/5.37 % (1877637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877637)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877637)Termination reason: Instruction limit
% 15.74/5.37 % (1877637)Termination phase: Preprocessing 2
% 15.74/5.37 % (1877637)Time elapsed: 0.143 s
% 15.74/5.37 % (1877637)Peak memory usage: 106 MB
% 15.74/5.37 % (1877637)Instructions burned: 113 (million)
% 15.74/5.37 % (1877644)Instruction limit reached!
% 15.74/5.37 % (1877644)------------------------------
% 15.74/5.37 % (1877644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877644)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877644)Termination reason: Instruction limit
% 15.74/5.37 % (1877644)Termination phase: Preprocessing 2
% 15.74/5.37 % (1877644)Time elapsed: 0.142 s
% 15.74/5.37 % (1877644)Peak memory usage: 106 MB
% 15.74/5.37 % (1877644)Instructions burned: 127 (million)
% 15.74/5.37 % (1877645)Instruction limit reached!
% 15.74/5.37 % (1877645)------------------------------
% 15.74/5.37 % (1877645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877645)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877645)Termination reason: Instruction limit
% 15.74/5.37 % (1877645)Termination phase: Property scanning
% 15.74/5.37 % (1877645)Time elapsed: 0.094 s
% 15.74/5.37 % (1877645)Peak memory usage: 102 MB
% 15.74/5.37 % (1877645)Instructions burned: 114 (million)
% 15.74/5.37 % (1877656)lrs+10_1_sil=8000:sp=occurrence:random_seed=1945085249:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 15.74/5.37 % (1877658)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2660786340:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 15.74/5.37 % (1877659)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=995847434:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 15.74/5.37 % (1877658)Instruction limit reached!
% 15.74/5.37 % (1877658)------------------------------
% 15.74/5.37 % (1877658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877658)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877658)Termination reason: Instruction limit
% 15.74/5.37 % (1877658)Termination phase: Saturation
% 15.74/5.37 % (1877658)Time elapsed: 0.364 s
% 15.74/5.37 % (1877658)Peak memory usage: 111 MB
% 15.74/5.37 % (1877658)Instructions burned: 437 (million)
% 15.74/5.37 % (1877673)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3451029241:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 15.74/5.37 % (1877673)Instruction limit reached!
% 15.74/5.37 % (1877673)------------------------------
% 15.74/5.37 % (1877673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877673)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877673)Termination reason: Instruction limit
% 15.74/5.37 % (1877673)Termination phase: Property scanning
% 15.74/5.37 % (1877673)Time elapsed: 0.165 s
% 15.74/5.37 % (1877673)Peak memory usage: 107 MB
% 15.74/5.37 % (1877673)Instructions burned: 134 (million)
% 15.74/5.37 % (1877625)Instruction limit reached!
% 15.74/5.37 % (1877625)------------------------------
% 15.74/5.37 % (1877625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877625)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877625)Termination reason: Instruction limit
% 15.74/5.37 % (1877625)Termination phase: Saturation
% 15.74/5.37 % (1877625)Time elapsed: 1.449 s
% 15.74/5.37 % (1877625)Peak memory usage: 239 MB
% 15.74/5.37 % (1877625)Instructions burned: 2350 (million)
% 15.74/5.37 % (1877656)Instruction limit reached!
% 15.74/5.37 % (1877656)------------------------------
% 15.74/5.37 % (1877656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877656)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877656)Termination reason: Instruction limit
% 15.74/5.37 % (1877656)Termination phase: Saturation
% 15.74/5.37 % (1877656)Time elapsed: 0.855 s
% 15.74/5.37 % (1877656)Peak memory usage: 123 MB
% 15.74/5.37 % (1877656)Instructions burned: 908 (million)
% 15.74/5.37 % (1877680)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1759788645:st=8:i=592:sd=3:ep=RST:ss=axioms_2972 on theBenchmark for (2972ds/592Mi)
% 15.74/5.37 % (1877682)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1304317284:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 15.74/5.37 % (1877683)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=747068198:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 15.74/5.37 % (1877683)Instruction limit reached!
% 15.74/5.37 % (1877683)------------------------------
% 15.74/5.37 % (1877683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877683)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877683)Termination reason: Instruction limit
% 15.74/5.37 % (1877683)Termination phase: Property scanning
% 15.74/5.37 % (1877683)Time elapsed: 0.106 s
% 15.74/5.37 % (1877683)Peak memory usage: 102 MB
% 15.74/5.37 % (1877683)Instructions burned: 125 (million)
% 15.74/5.37 % (1877688)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3072273268:i=134:gtgl=5:slsql=off:gtg=exists_sym_2967 on theBenchmark for (2967ds/134Mi)
% 15.74/5.37 % (1877680)Instruction limit reached!
% 15.74/5.37 % (1877680)------------------------------
% 15.74/5.37 % (1877680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877680)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877680)Termination reason: Instruction limit
% 15.74/5.37 % (1877680)Termination phase: Property scanning
% 15.74/5.37 % (1877680)Time elapsed: 0.623 s
% 15.74/5.37 % (1877680)Peak memory usage: 121 MB
% 15.74/5.37 % (1877680)Instructions burned: 593 (million)
% 15.74/5.37 % (1877688)Instruction limit reached!
% 15.74/5.37 % (1877688)------------------------------
% 15.74/5.37 % (1877688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877688)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877688)Termination reason: Instruction limit
% 15.74/5.37 % (1877688)Termination phase: Property scanning
% 15.74/5.37 % (1877688)Time elapsed: 0.112 s
% 15.74/5.37 % (1877688)Peak memory usage: 102 MB
% 15.74/5.37 % (1877688)Instructions burned: 135 (million)
% 15.74/5.37 % (1877694)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2732924294:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/141Mi)
% 15.74/5.37 % (1877695)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2656677771:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2962 on theBenchmark for (2962ds/431Mi)
% 15.74/5.37 % (1877694)Instruction limit reached!
% 15.74/5.37 % (1877694)------------------------------
% 15.74/5.37 % (1877694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877694)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877694)Termination reason: Instruction limit
% 15.74/5.37 % (1877694)Termination phase: Saturation
% 15.74/5.37 % (1877694)Time elapsed: 0.152 s
% 15.74/5.37 % (1877694)Peak memory usage: 108 MB
% 15.74/5.37 % (1877694)Instructions burned: 141 (million)
% 15.74/5.37 % (1877605)First to succeed.
% 15.74/5.37 % (1877605)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1877466"
% 15.74/5.37 % (1877699)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=1089442635:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 15.74/5.37 % (1877695)Instruction limit reached!
% 15.74/5.37 % (1877695)------------------------------
% 15.74/5.37 % (1877695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/5.37 % (1877695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/5.37 % (1877695)CaDiCaL version: 2.1.3
% 15.74/5.37 % (1877695)Termination reason: Instruction limit
% 15.74/5.37 % (1877695)Termination phase: Saturation
% 15.74/5.37 % (1877695)Time elapsed: 0.468 s
% 15.74/5.37 % (1877695)Peak memory usage: 111 MB
% 15.74/5.37 % (1877695)Instructions burned: 431 (million)
% 15.74/5.37 % (1877605)Refutation found. Thanks to Tanya!
% 15.74/5.37 % SZS status Theorem for theBenchmark
% 15.74/5.37 % SZS output start Proof for theBenchmark
% See solution above
% 29.24/5.69 % (1877605)------------------------------
% 29.24/5.69 % (1877605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.24/5.69 % (1877605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.24/5.69 % (1877605)CaDiCaL version: 2.1.3
% 29.24/5.69 % (1877605)Termination reason: Refutation
% 29.24/5.69 % (1877605)Time elapsed: 3.300 s
% 29.24/5.69 % (1877605)Peak memory usage: 175 MB
% 29.24/5.69 % (1877605)Instructions burned: 3561 (million)
% 29.24/5.69 % (1877605)------------------------------
% 29.24/5.69 % (1877605)------------------------------
% 29.24/5.69 % (1877466)Success in time 4.692 s
% 29.24/5.69 % Vampire exiting
%------------------------------------------------------------------------------