%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP023+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:52 PM UTC 2026
% Result : Theorem 21.57s 8.33s
% Output : Refutation 37.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 24
% Syntax : Number of formulae : 175 ( 37 unt; 19 def)
% Number of atoms : 663 ( 78 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 881 ( 393 ~; 391 |; 53 &)
% ( 22 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 20 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 117 ( 0 sgn 106 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18329,axiom,
! [X0] :
( l1_pre_topc(X0)
=> m1_subset_1(u1_pre_topc(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_pre_topc) ).
fof(f18331,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> ! [X2,X3] :
( g1_pre_topc(X0,X1) = g1_pre_topc(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g1_pre_topc) ).
fof(f34339,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) = g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
& X2 = X3
& v1_tsp_1(X2,X0) )
=> v1_tsp_1(X3,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_tsp_1) ).
fof(f34379,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ( v1_tsp_1(X2,X0)
& r1_tarski(X1,X2) )
=> X1 = X2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_tsp_2) ).
fof(f34380,conjecture,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) = g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
& X2 = X3
& v1_tsp_2(X2,X0) )
=> v1_tsp_2(X3,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_tsp_2) ).
fof(f34381,negated_conjecture,
~ ! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( l1_pre_topc(X1)
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
=> ( ( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) = g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
& X2 = X3
& v1_tsp_2(X2,X0) )
=> v1_tsp_2(X3,X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34380]) ).
fof(f34413,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& ! [X2] :
( X1 = X2
| ~ v1_tsp_1(X2,X0)
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34379]) ).
fof(f34414,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& ! [X2] :
( X1 = X2
| ~ v1_tsp_1(X2,X0)
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34413]) ).
fof(f34415,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ~ v1_tsp_2(X3,X1)
& g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) = g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
& X2 = X3
& v1_tsp_2(X2,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& l1_pre_topc(X1) )
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34381]) ).
fof(f34416,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ~ v1_tsp_2(X3,X1)
& g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) = g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
& X2 = X3
& v1_tsp_2(X2,X0)
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& l1_pre_topc(X1) )
& l1_pre_topc(X0) ),
inference(flattening,[],[f34415]) ).
fof(f34505,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v1_tsp_1(X3,X1)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
| X2 != X3
| ~ v1_tsp_1(X2,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34339]) ).
fof(f34506,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v1_tsp_1(X3,X1)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
| X2 != X3
| ~ v1_tsp_1(X2,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X1) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34505]) ).
fof(f34584,plain,
! [X0] :
( m1_subset_1(u1_pre_topc(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18329]) ).
fof(f34638,plain,
! [X0,X1] :
( ! [X2,X3] :
( ( X0 = X2
& X1 = X3 )
| g1_pre_topc(X0,X1) != g1_pre_topc(X2,X3) )
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(ennf_transformation,[],[f18331]) ).
fof(f34651,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| ? [X2] :
( X1 != X2
& v1_tsp_1(X2,X0)
& r1_tarski(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( v1_tsp_1(X1,X0)
& ! [X2] :
( X1 = X2
| ~ v1_tsp_1(X2,X0)
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34414]) ).
fof(f34652,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| ? [X2] :
( X1 != X2
& v1_tsp_1(X2,X0)
& r1_tarski(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( v1_tsp_1(X1,X0)
& ! [X2] :
( X1 = X2
| ~ v1_tsp_1(X2,X0)
| ~ r1_tarski(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f34651]) ).
fof(f34653,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| ? [X2] :
( X1 != X2
& v1_tsp_1(X2,X0)
& r1_tarski(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( v1_tsp_1(X1,X0)
& ! [X3] :
( X1 = X3
| ~ v1_tsp_1(X3,X0)
| ~ r1_tarski(X1,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f34652]) ).
fof(f34654,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| ( sK5(X0,X1) != X1
& v1_tsp_1(sK5(X0,X1),X0)
& r1_tarski(X1,sK5(X0,X1))
& m1_subset_1(sK5(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ) )
& ( ( v1_tsp_1(X1,X0)
& ! [X3] :
( X1 = X3
| ~ v1_tsp_1(X3,X0)
| ~ r1_tarski(X1,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) ) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f34653]) ).
fof(f34655,plain,
( ~ v1_tsp_2(sK9,sK7)
& g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6)) = g1_pre_topc(u1_struct_0(sK7),u1_pre_topc(sK7))
& sK8 = sK9
& v1_tsp_2(sK8,sK6)
& m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK7)))
& m1_subset_1(sK8,k1_zfmisc_1(u1_struct_0(sK6)))
& l1_pre_topc(sK7)
& l1_pre_topc(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9)],[f34416]) ).
fof(f34770,plain,
! [X3,X0,X1] :
( X1 = X3
| ~ v1_tsp_1(X3,X0)
| ~ r1_tarski(X1,X3)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34654]) ).
fof(f34771,plain,
! [X0,X1] :
( v1_tsp_1(X1,X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34654]) ).
fof(f34772,plain,
! [X0,X1] :
( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| m1_subset_1(sK5(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34654]) ).
fof(f34773,plain,
! [X0,X1] :
( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| r1_tarski(X1,sK5(X0,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34654]) ).
fof(f34774,plain,
! [X0,X1] :
( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| v1_tsp_1(sK5(X0,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34654]) ).
fof(f34775,plain,
! [X0,X1] :
( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| sK5(X0,X1) != X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34654]) ).
fof(f34776,plain,
l1_pre_topc(sK6),
inference(cnf_transformation,[],[f34655]) ).
fof(f34777,plain,
l1_pre_topc(sK7),
inference(cnf_transformation,[],[f34655]) ).
fof(f34778,plain,
m1_subset_1(sK8,k1_zfmisc_1(u1_struct_0(sK6))),
inference(cnf_transformation,[],[f34655]) ).
fof(f34779,plain,
m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK7))),
inference(cnf_transformation,[],[f34655]) ).
fof(f34780,plain,
v1_tsp_2(sK8,sK6),
inference(cnf_transformation,[],[f34655]) ).
fof(f34781,plain,
sK8 = sK9,
inference(cnf_transformation,[],[f34655]) ).
fof(f34782,plain,
g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6)) = g1_pre_topc(u1_struct_0(sK7),u1_pre_topc(sK7)),
inference(cnf_transformation,[],[f34655]) ).
fof(f34783,plain,
~ v1_tsp_2(sK9,sK7),
inference(cnf_transformation,[],[f34655]) ).
fof(f34904,plain,
! [X2,X3,X0,X1] :
( v1_tsp_1(X3,X1)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
| X2 != X3
| ~ v1_tsp_1(X2,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34506]) ).
fof(f35067,plain,
! [X0] :
( m1_subset_1(u1_pre_topc(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34584]) ).
fof(f35131,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| g1_pre_topc(X0,X1) != g1_pre_topc(X2,X3)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0))) ),
inference(cnf_transformation,[],[f34638]) ).
fof(f35135,plain,
v1_tsp_2(sK9,sK6),
inference(definition_unfolding,[],[f34780,f34781]) ).
fof(f35136,plain,
m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK6))),
inference(definition_unfolding,[],[f34778,f34781]) ).
fof(f35143,plain,
! [X3,X0,X1] :
( v1_tsp_1(X3,X1)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1))
| ~ v1_tsp_1(X3,X0)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(equality_resolution,[],[f34904]) ).
fof(f35212,definition,
( spl85_1
<=> v1_tsp_2(sK9,sK6) ),
introduced(definition,[new_symbols(definition,[spl85_1])],[avatar_definition]) ).
fof(f35214,plain,
( v1_tsp_2(sK9,sK6)
| ~ spl85_1 ),
inference(avatar_component_clause,[],[f35212]) ).
fof(f35215,plain,
spl85_1,
inference(avatar_split_clause,[],[f35135,f35212]) ).
fof(f35217,definition,
( spl85_2
<=> m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK7))) ),
introduced(definition,[new_symbols(definition,[spl85_2])],[avatar_definition]) ).
fof(f35219,plain,
( m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ spl85_2 ),
inference(avatar_component_clause,[],[f35217]) ).
fof(f35220,plain,
spl85_2,
inference(avatar_split_clause,[],[f34779,f35217]) ).
fof(f35242,plain,
( v1_tsp_2(sK9,sK7)
| ~ v1_tsp_1(sK9,sK7)
| m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(resolution,[],[f35219,f34772]) ).
fof(f35243,plain,
( v1_tsp_2(sK9,sK7)
| ~ v1_tsp_1(sK9,sK7)
| r1_tarski(sK9,sK5(sK7,sK9))
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(resolution,[],[f35219,f34773]) ).
fof(f35244,plain,
( v1_tsp_2(sK9,sK7)
| ~ v1_tsp_1(sK9,sK7)
| v1_tsp_1(sK5(sK7,sK9),sK7)
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(resolution,[],[f35219,f34774]) ).
fof(f35245,plain,
( v1_tsp_2(sK9,sK7)
| ~ v1_tsp_1(sK9,sK7)
| sK9 != sK5(sK7,sK9)
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(resolution,[],[f35219,f34775]) ).
fof(f35567,plain,
( ~ v1_tsp_1(sK9,sK7)
| sK9 != sK5(sK7,sK9)
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35245,f34783]) ).
fof(f35568,plain,
( ~ v1_tsp_1(sK9,sK7)
| v1_tsp_1(sK5(sK7,sK9),sK7)
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35244,f34783]) ).
fof(f35569,plain,
( ~ v1_tsp_1(sK9,sK7)
| r1_tarski(sK9,sK5(sK7,sK9))
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35243,f34783]) ).
fof(f35570,plain,
( ~ v1_tsp_1(sK9,sK7)
| m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(sK7)
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35242,f34783]) ).
fof(f35644,plain,
( ~ v1_tsp_1(sK9,sK7)
| sK9 != sK5(sK7,sK9)
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35567,f34777]) ).
fof(f35645,plain,
( ~ v1_tsp_1(sK9,sK7)
| v1_tsp_1(sK5(sK7,sK9),sK7)
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35568,f34777]) ).
fof(f35646,plain,
( ~ v1_tsp_1(sK9,sK7)
| r1_tarski(sK9,sK5(sK7,sK9))
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35569,f34777]) ).
fof(f35647,plain,
( ~ v1_tsp_1(sK9,sK7)
| m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK7)))
| ~ spl85_2 ),
inference(forward_subsumption_resolution,[],[f35570,f34777]) ).
fof(f35702,definition,
( spl85_3
<=> m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK6))) ),
introduced(definition,[new_symbols(definition,[spl85_3])],[avatar_definition]) ).
fof(f35704,plain,
( m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ spl85_3 ),
inference(avatar_component_clause,[],[f35702]) ).
fof(f35705,plain,
spl85_3,
inference(avatar_split_clause,[],[f35136,f35702]) ).
fof(f35724,plain,
( ! [X0] :
( sK9 = X0
| ~ v1_tsp_1(X0,sK6)
| ~ r1_tarski(sK9,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ v1_tsp_2(sK9,sK6)
| ~ l1_pre_topc(sK6) )
| ~ spl85_3 ),
inference(resolution,[],[f35704,f34770]) ).
fof(f35726,plain,
( v1_tsp_1(sK9,sK6)
| ~ v1_tsp_2(sK9,sK6)
| ~ l1_pre_topc(sK6)
| ~ spl85_3 ),
inference(resolution,[],[f35704,f34771]) ).
fof(f35855,plain,
( ! [X0] :
( v1_tsp_1(sK9,X0)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| ~ v1_tsp_1(sK9,sK6)
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ l1_pre_topc(sK6) )
| ~ spl85_3 ),
inference(resolution,[],[f35704,f35143]) ).
fof(f35928,plain,
( ! [X0] :
( v1_tsp_1(sK9,X0)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| ~ v1_tsp_1(sK9,sK6)
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) )
| ~ spl85_3 ),
inference(forward_subsumption_resolution,[],[f35855,f34776]) ).
fof(f36052,plain,
( v1_tsp_1(sK9,sK6)
| ~ l1_pre_topc(sK6)
| ~ spl85_1
| ~ spl85_3 ),
inference(forward_subsumption_resolution,[],[f35726,f35214]) ).
fof(f36054,plain,
( ! [X0] :
( sK9 = X0
| ~ v1_tsp_1(X0,sK6)
| ~ r1_tarski(sK9,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ l1_pre_topc(sK6) )
| ~ spl85_1
| ~ spl85_3 ),
inference(forward_subsumption_resolution,[],[f35724,f35214]) ).
fof(f36123,plain,
( v1_tsp_1(sK9,sK6)
| ~ spl85_1
| ~ spl85_3 ),
inference(forward_subsumption_resolution,[],[f36052,f34776]) ).
fof(f36124,plain,
( ! [X0] :
( sK9 = X0
| ~ v1_tsp_1(X0,sK6)
| ~ r1_tarski(sK9,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6))) )
| ~ spl85_1
| ~ spl85_3 ),
inference(forward_subsumption_resolution,[],[f36054,f34776]) ).
fof(f36165,plain,
( ! [X0] :
( v1_tsp_1(sK9,X0)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) )
| ~ spl85_1
| ~ spl85_3 ),
inference(backward_subsumption_resolution,[],[f35928,f36123]) ).
fof(f36221,definition,
( spl85_4
<=> l1_pre_topc(sK6) ),
introduced(definition,[new_symbols(definition,[spl85_4])],[avatar_definition]) ).
fof(f36223,plain,
( l1_pre_topc(sK6)
| ~ spl85_4 ),
inference(avatar_component_clause,[],[f36221]) ).
fof(f36224,plain,
spl85_4,
inference(avatar_split_clause,[],[f34776,f36221]) ).
fof(f36226,definition,
( spl85_5
<=> l1_pre_topc(sK7) ),
introduced(definition,[new_symbols(definition,[spl85_5])],[avatar_definition]) ).
fof(f36228,plain,
( l1_pre_topc(sK7)
| ~ spl85_5 ),
inference(avatar_component_clause,[],[f36226]) ).
fof(f36229,plain,
spl85_5,
inference(avatar_split_clause,[],[f34777,f36226]) ).
fof(f36893,plain,
( m1_subset_1(u1_pre_topc(sK7),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK7))))
| ~ spl85_5 ),
inference(resolution,[],[f36228,f35067]) ).
fof(f36975,plain,
( ! [X0,X1] :
( v1_tsp_1(X0,X1)
| g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(sK7),u1_pre_topc(sK7))
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(X1) )
| ~ spl85_5 ),
inference(resolution,[],[f36228,f35143]) ).
fof(f37042,plain,
( ! [X0,X1] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| v1_tsp_1(X0,X1)
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(X1) )
| ~ spl85_5 ),
inference(forward_demodulation,[],[f36975,f34782]) ).
fof(f37206,definition,
( spl85_8
<=> g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6)) = g1_pre_topc(u1_struct_0(sK7),u1_pre_topc(sK7)) ),
introduced(definition,[new_symbols(definition,[spl85_8])],[avatar_definition]) ).
fof(f37208,plain,
( g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6)) = g1_pre_topc(u1_struct_0(sK7),u1_pre_topc(sK7))
| ~ spl85_8 ),
inference(avatar_component_clause,[],[f37206]) ).
fof(f37209,plain,
spl85_8,
inference(avatar_split_clause,[],[f34782,f37206]) ).
fof(f37367,plain,
( ! [X0,X1] :
( g1_pre_topc(X0,X1) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| u1_struct_0(sK7) = X0
| ~ m1_subset_1(u1_pre_topc(sK7),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK7)))) )
| ~ spl85_8 ),
inference(superposition,[],[f35131,f37208]) ).
fof(f37373,plain,
( ! [X0,X1] :
( g1_pre_topc(X0,X1) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| u1_struct_0(sK7) = X0 )
| ~ spl85_5
| ~ spl85_8 ),
inference(forward_subsumption_resolution,[],[f37367,f36893]) ).
fof(f37589,definition,
( spl85_10
<=> sK9 = sK5(sK7,sK9) ),
introduced(definition,[new_symbols(definition,[spl85_10])],[avatar_definition]) ).
fof(f37591,plain,
( sK9 != sK5(sK7,sK9)
| spl85_10 ),
inference(avatar_component_clause,[],[f37589]) ).
fof(f37593,definition,
( spl85_11
<=> v1_tsp_1(sK9,sK7) ),
introduced(definition,[new_symbols(definition,[spl85_11])],[avatar_definition]) ).
fof(f37596,plain,
( ~ spl85_10
| ~ spl85_11
| ~ spl85_2 ),
inference(avatar_split_clause,[],[f35644,f35217,f37593,f37589]) ).
fof(f37598,definition,
( spl85_12
<=> ! [X0] :
( v1_tsp_1(sK9,X0)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ) ),
introduced(definition,[new_symbols(definition,[spl85_12])],[avatar_definition]) ).
fof(f37599,plain,
( ! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| v1_tsp_1(sK9,X0)
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) )
| ~ spl85_12 ),
inference(avatar_component_clause,[],[f37598]) ).
fof(f37600,plain,
( spl85_12
| ~ spl85_1
| ~ spl85_3 ),
inference(avatar_split_clause,[],[f36165,f35702,f35212,f37598]) ).
fof(f37646,plain,
( g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| v1_tsp_1(sK9,sK7)
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(sK7)
| ~ spl85_8
| ~ spl85_12 ),
inference(superposition,[],[f37599,f37208]) ).
fof(f37693,plain,
( v1_tsp_1(sK9,sK7)
| ~ m1_subset_1(sK9,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(sK7)
| ~ spl85_8
| ~ spl85_12 ),
inference(trivial_inequality_removal,[],[f37646]) ).
fof(f37773,plain,
( v1_tsp_1(sK9,sK7)
| ~ l1_pre_topc(sK7)
| ~ spl85_2
| ~ spl85_8
| ~ spl85_12 ),
inference(forward_subsumption_resolution,[],[f37693,f35219]) ).
fof(f37781,plain,
( v1_tsp_1(sK9,sK7)
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(forward_subsumption_resolution,[],[f37773,f36228]) ).
fof(f37798,plain,
( v1_tsp_1(sK5(sK7,sK9),sK7)
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(backward_subsumption_resolution,[],[f35645,f37781]) ).
fof(f37799,plain,
( r1_tarski(sK9,sK5(sK7,sK9))
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(backward_subsumption_resolution,[],[f35646,f37781]) ).
fof(f37800,plain,
( m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK7)))
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(backward_subsumption_resolution,[],[f35647,f37781]) ).
fof(f37842,definition,
( spl85_13
<=> r1_tarski(sK9,sK5(sK7,sK9)) ),
introduced(definition,[new_symbols(definition,[spl85_13])],[avatar_definition]) ).
fof(f37844,plain,
( r1_tarski(sK9,sK5(sK7,sK9))
| ~ spl85_13 ),
inference(avatar_component_clause,[],[f37842]) ).
fof(f37845,plain,
( spl85_13
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(avatar_split_clause,[],[f37799,f37598,f37206,f36226,f35217,f37842]) ).
fof(f37846,plain,
( spl85_11
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(avatar_split_clause,[],[f37781,f37598,f37206,f36226,f35217,f37593]) ).
fof(f37985,definition,
( spl85_14
<=> m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK7))) ),
introduced(definition,[new_symbols(definition,[spl85_14])],[avatar_definition]) ).
fof(f37987,plain,
( m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK7)))
| ~ spl85_14 ),
inference(avatar_component_clause,[],[f37985]) ).
fof(f37988,plain,
( spl85_14
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(avatar_split_clause,[],[f37800,f37598,f37206,f36226,f35217,f37985]) ).
fof(f38530,definition,
( spl85_16
<=> v1_tsp_1(sK5(sK7,sK9),sK7) ),
introduced(definition,[new_symbols(definition,[spl85_16])],[avatar_definition]) ).
fof(f38532,plain,
( v1_tsp_1(sK5(sK7,sK9),sK7)
| ~ spl85_16 ),
inference(avatar_component_clause,[],[f38530]) ).
fof(f38533,plain,
( spl85_16
| ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12 ),
inference(avatar_split_clause,[],[f37798,f37598,f37206,f36226,f35217,f38530]) ).
fof(f41887,definition,
( spl85_70
<=> ! [X0,X1] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| v1_tsp_1(X0,X1)
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(X1) ) ),
introduced(definition,[new_symbols(definition,[spl85_70])],[avatar_definition]) ).
fof(f41888,plain,
( ! [X0,X1] :
( g1_pre_topc(u1_struct_0(X1),u1_pre_topc(X1)) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| v1_tsp_1(X0,X1)
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(X1) )
| ~ spl85_70 ),
inference(avatar_component_clause,[],[f41887]) ).
fof(f41889,plain,
( spl85_70
| ~ spl85_5 ),
inference(avatar_split_clause,[],[f37042,f36226,f41887]) ).
fof(f41981,plain,
( ! [X0] :
( v1_tsp_1(X0,sK6)
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ l1_pre_topc(sK6) )
| ~ spl85_70 ),
inference(equality_resolution,[],[f41888]) ).
fof(f42021,plain,
( ! [X0] :
( v1_tsp_1(X0,sK6)
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7))) )
| ~ spl85_4
| ~ spl85_70 ),
inference(forward_subsumption_resolution,[],[f41981,f36223]) ).
fof(f42057,definition,
( spl85_71
<=> ! [X0] :
( v1_tsp_1(X0,sK6)
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7))) ) ),
introduced(definition,[new_symbols(definition,[spl85_71])],[avatar_definition]) ).
fof(f42058,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK7)))
| ~ v1_tsp_1(X0,sK7)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| v1_tsp_1(X0,sK6) )
| ~ spl85_71 ),
inference(avatar_component_clause,[],[f42057]) ).
fof(f42059,plain,
( spl85_71
| ~ spl85_4
| ~ spl85_70 ),
inference(avatar_split_clause,[],[f42021,f41887,f36221,f42057]) ).
fof(f42061,plain,
( ~ v1_tsp_1(sK5(sK7,sK9),sK7)
| ~ m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK6)))
| v1_tsp_1(sK5(sK7,sK9),sK6)
| ~ spl85_14
| ~ spl85_71 ),
inference(resolution,[],[f42058,f37987]) ).
fof(f42151,plain,
( ~ m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK6)))
| v1_tsp_1(sK5(sK7,sK9),sK6)
| ~ spl85_14
| ~ spl85_16
| ~ spl85_71 ),
inference(forward_subsumption_resolution,[],[f42061,f38532]) ).
fof(f43647,definition,
( spl85_89
<=> ! [X0] :
( sK9 = X0
| ~ v1_tsp_1(X0,sK6)
| ~ r1_tarski(sK9,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6))) ) ),
introduced(definition,[new_symbols(definition,[spl85_89])],[avatar_definition]) ).
fof(f43648,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK6)))
| ~ v1_tsp_1(X0,sK6)
| ~ r1_tarski(sK9,X0)
| sK9 = X0 )
| ~ spl85_89 ),
inference(avatar_component_clause,[],[f43647]) ).
fof(f43649,plain,
( spl85_89
| ~ spl85_1
| ~ spl85_3 ),
inference(avatar_split_clause,[],[f36124,f35702,f35212,f43647]) ).
fof(f46221,definition,
( spl85_137
<=> ! [X0,X1] :
( g1_pre_topc(X0,X1) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| u1_struct_0(sK7) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl85_137])],[avatar_definition]) ).
fof(f46222,plain,
( ! [X0,X1] :
( g1_pre_topc(X0,X1) != g1_pre_topc(u1_struct_0(sK6),u1_pre_topc(sK6))
| u1_struct_0(sK7) = X0 )
| ~ spl85_137 ),
inference(avatar_component_clause,[],[f46221]) ).
fof(f46223,plain,
( spl85_137
| ~ spl85_5
| ~ spl85_8 ),
inference(avatar_split_clause,[],[f37373,f37206,f36226,f46221]) ).
fof(f46314,plain,
( u1_struct_0(sK6) = u1_struct_0(sK7)
| ~ spl85_137 ),
inference(equality_resolution,[],[f46222]) ).
fof(f46389,definition,
( spl85_138
<=> u1_struct_0(sK6) = u1_struct_0(sK7) ),
introduced(definition,[new_symbols(definition,[spl85_138])],[avatar_definition]) ).
fof(f46391,plain,
( u1_struct_0(sK6) = u1_struct_0(sK7)
| ~ spl85_138 ),
inference(avatar_component_clause,[],[f46389]) ).
fof(f46392,plain,
( spl85_138
| ~ spl85_137 ),
inference(avatar_split_clause,[],[f46314,f46221,f46389]) ).
fof(f46395,plain,
( m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK6)))
| ~ spl85_14
| ~ spl85_138 ),
inference(superposition,[],[f37987,f46391]) ).
fof(f47300,plain,
( v1_tsp_1(sK5(sK7,sK9),sK6)
| ~ spl85_14
| ~ spl85_16
| ~ spl85_71
| ~ spl85_138 ),
inference(backward_subsumption_resolution,[],[f42151,f46395]) ).
fof(f47613,definition,
( spl85_141
<=> v1_tsp_1(sK5(sK7,sK9),sK6) ),
introduced(definition,[new_symbols(definition,[spl85_141])],[avatar_definition]) ).
fof(f47615,plain,
( v1_tsp_1(sK5(sK7,sK9),sK6)
| ~ spl85_141 ),
inference(avatar_component_clause,[],[f47613]) ).
fof(f47616,plain,
( spl85_141
| ~ spl85_14
| ~ spl85_16
| ~ spl85_71
| ~ spl85_138 ),
inference(avatar_split_clause,[],[f47300,f46389,f42057,f38530,f37985,f47613]) ).
fof(f47898,definition,
( spl85_160
<=> m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK6))) ),
introduced(definition,[new_symbols(definition,[spl85_160])],[avatar_definition]) ).
fof(f47900,plain,
( m1_subset_1(sK5(sK7,sK9),k1_zfmisc_1(u1_struct_0(sK6)))
| ~ spl85_160 ),
inference(avatar_component_clause,[],[f47898]) ).
fof(f47901,plain,
( spl85_160
| ~ spl85_14
| ~ spl85_138 ),
inference(avatar_split_clause,[],[f46395,f46389,f37985,f47898]) ).
fof(f47904,plain,
( ~ v1_tsp_1(sK5(sK7,sK9),sK6)
| ~ r1_tarski(sK9,sK5(sK7,sK9))
| sK9 = sK5(sK7,sK9)
| ~ spl85_89
| ~ spl85_160 ),
inference(resolution,[],[f47900,f43648]) ).
fof(f48136,plain,
( ~ r1_tarski(sK9,sK5(sK7,sK9))
| sK9 = sK5(sK7,sK9)
| ~ spl85_89
| ~ spl85_141
| ~ spl85_160 ),
inference(forward_subsumption_resolution,[],[f47904,f47615]) ).
fof(f48138,plain,
( sK9 = sK5(sK7,sK9)
| ~ spl85_13
| ~ spl85_89
| ~ spl85_141
| ~ spl85_160 ),
inference(forward_subsumption_resolution,[],[f48136,f37844]) ).
fof(f48139,plain,
( $false
| spl85_10
| ~ spl85_13
| ~ spl85_89
| ~ spl85_141
| ~ spl85_160 ),
inference(forward_subsumption_resolution,[],[f48138,f37591]) ).
fof(f48140,plain,
( spl85_10
| ~ spl85_13
| ~ spl85_89
| ~ spl85_141
| ~ spl85_160 ),
inference(avatar_contradiction_clause,[],[f48139]) ).
cnf(s1,plain,
spl85_1,
inference(sat_conversion,[],[f35215]) ).
cnf(s2,plain,
spl85_2,
inference(sat_conversion,[],[f35220]) ).
cnf(s3,plain,
spl85_3,
inference(sat_conversion,[],[f35705]) ).
cnf(s4,plain,
spl85_4,
inference(sat_conversion,[],[f36224]) ).
cnf(s5,plain,
spl85_5,
inference(sat_conversion,[],[f36229]) ).
cnf(s8,plain,
spl85_8,
inference(sat_conversion,[],[f37209]) ).
cnf(s10,plain,
( ~ spl85_2
| ~ spl85_10
| ~ spl85_11 ),
inference(sat_conversion,[],[f37596]) ).
cnf(s11,plain,
( ~ spl85_1
| ~ spl85_3
| spl85_12 ),
inference(sat_conversion,[],[f37600]) ).
cnf(s12,plain,
( ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12
| spl85_13 ),
inference(sat_conversion,[],[f37845]) ).
cnf(s13,plain,
( ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| spl85_11
| ~ spl85_12 ),
inference(sat_conversion,[],[f37846]) ).
cnf(s14,plain,
( ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12
| spl85_14 ),
inference(sat_conversion,[],[f37988]) ).
cnf(s16,plain,
( ~ spl85_2
| ~ spl85_5
| ~ spl85_8
| ~ spl85_12
| spl85_16 ),
inference(sat_conversion,[],[f38533]) ).
cnf(s66,plain,
( ~ spl85_5
| spl85_70 ),
inference(sat_conversion,[],[f41889]) ).
cnf(s67,plain,
( ~ spl85_4
| ~ spl85_70
| spl85_71 ),
inference(sat_conversion,[],[f42059]) ).
cnf(s86,plain,
( ~ spl85_1
| ~ spl85_3
| spl85_89 ),
inference(sat_conversion,[],[f43649]) ).
cnf(s134,plain,
( ~ spl85_5
| ~ spl85_8
| spl85_137 ),
inference(sat_conversion,[],[f46223]) ).
cnf(s135,plain,
( ~ spl85_137
| spl85_138 ),
inference(sat_conversion,[],[f46392]) ).
cnf(s138,plain,
( ~ spl85_14
| ~ spl85_16
| ~ spl85_71
| ~ spl85_138
| spl85_141 ),
inference(sat_conversion,[],[f47616]) ).
cnf(s157,plain,
( ~ spl85_14
| ~ spl85_138
| spl85_160 ),
inference(sat_conversion,[],[f47901]) ).
cnf(s158,plain,
( spl85_10
| ~ spl85_13
| ~ spl85_89
| ~ spl85_141
| ~ spl85_160 ),
inference(sat_conversion,[],[f48140]) ).
cnf(s165,plain,
spl85_137,
inference(rat,[],[s134,s8,s5]) ).
cnf(s178,plain,
spl85_70,
inference(rat,[],[s66,s5]) ).
cnf(s183,plain,
spl85_138,
inference(rat,[],[s135,s165]) ).
cnf(s189,plain,
spl85_71,
inference(rat,[],[s67,s178,s4]) ).
cnf(s211,plain,
spl85_89,
inference(rat,[],[s86,s3,s1]) ).
cnf(s219,plain,
spl85_12,
inference(rat,[],[s11,s3,s1]) ).
cnf(s236,plain,
spl85_16,
inference(rat,[],[s16,s2,s5,s8,s219]) ).
cnf(s238,plain,
spl85_14,
inference(rat,[],[s14,s2,s5,s8,s219]) ).
cnf(s239,plain,
spl85_13,
inference(rat,[],[s12,s2,s5,s8,s219]) ).
cnf(s240,plain,
spl85_11,
inference(rat,[],[s13,s2,s5,s8,s219]) ).
cnf(s242,plain,
spl85_160,
inference(rat,[],[s157,s183,s238]) ).
cnf(s244,plain,
spl85_141,
inference(rat,[],[s138,s236,s183,s189,s238]) ).
cnf(s247,plain,
spl85_10,
inference(rat,[],[s158,s242,s244,s211,s239]) ).
cnf(s251,plain,
$false,
inference(rat,[],[s10,s2,s240,s247]) ).
fof(f48141,plain,
$false,
inference(avatar_sat_refutation,[],[s251]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP023+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 18:49:53 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 25.95/6.71 % (2053582)Detected formulas, will run a generic FOF schedule.
% 25.95/6.71 % (2053734)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1376205380:i=109:sd=1:ins=1:gsp=on:ss=axioms_2972 on theBenchmark for (2972ds/109Mi)
% 25.95/6.71 % (2053736)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3318407480:s2a=on:i=139:gtg=position_2972 on theBenchmark for (2972ds/139Mi)
% 25.95/6.71 % (2053731)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=1846673387:i=141193_2972 on theBenchmark for (2972ds/141193Mi)
% 25.95/6.71 % (2053732)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=3332202619:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2972 on theBenchmark for (2972ds/134677Mi)
% 25.95/6.71 % (2053733)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=3121267334:i=141695:sd=1:nm=32:gsp=on:ss=included_2972 on theBenchmark for (2972ds/141695Mi)
% 25.95/6.71 % (2053735)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1534236033:i=119:av=off:ss=axioms_2972 on theBenchmark for (2972ds/119Mi)
% 25.95/6.71 % (2053736)Instruction limit reached!
% 25.95/6.71 % (2053736)------------------------------
% 25.95/6.71 % (2053736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.95/6.71 % (2053736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.95/6.71 % (2053736)CaDiCaL version: 2.1.3
% 25.95/6.71 % (2053736)Termination reason: Instruction limit
% 25.95/6.71 % (2053736)Termination phase: Property scanning
% 25.95/6.71 % (2053736)Time elapsed: 0.064 s
% 25.95/6.71 % (2053736)Peak memory usage: 136 MB
% 25.95/6.71 % (2053736)Instructions burned: 139 (million)
% 25.95/6.71 % (2053737)dis-21_1_sil=8000:lcm=predicate:random_seed=1886966395:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2972 on theBenchmark for (2972ds/129Mi)
% 25.95/6.71 % (2053734)Instruction limit reached!
% 25.95/6.71 % (2053734)------------------------------
% 25.95/6.71 % (2053734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.95/6.71 % (2053734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.95/6.71 % (2053734)CaDiCaL version: 2.1.3
% 25.95/6.71 % (2053734)Termination reason: Instruction limit
% 25.95/6.71 % (2053734)Termination phase: SInE selection
% 25.95/6.71 % (2053734)Time elapsed: 0.119 s
% 25.95/6.71 % (2053734)Peak memory usage: 136 MB
% 25.95/6.71 % (2053734)Instructions burned: 110 (million)
% 25.95/6.71 % (2053735)Instruction limit reached!
% 25.95/6.71 % (2053735)------------------------------
% 25.95/6.71 % (2053735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.95/6.71 % (2053735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.95/6.71 % (2053735)CaDiCaL version: 2.1.3
% 25.95/6.71 % (2053735)Termination reason: Instruction limit
% 25.95/6.71 % (2053735)Termination phase: SInE selection
% 25.95/6.71 % (2053735)Time elapsed: 0.132 s
% 25.95/6.71 % (2053735)Peak memory usage: 135 MB
% 25.95/6.71 % (2053735)Instructions burned: 119 (million)
% 25.95/6.71 % (2053737)Instruction limit reached!
% 25.95/6.71 % (2053737)------------------------------
% 25.95/6.71 % (2053737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.95/6.71 % (2053737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.95/6.71 % (2053737)CaDiCaL version: 2.1.3
% 25.95/6.71 % (2053737)Termination reason: Instruction limit
% 25.95/6.71 % (2053737)Termination phase: SInE selection
% 25.95/6.71 % (2053737)Time elapsed: 0.146 s
% 25.95/6.71 % (2053737)Peak memory usage: 136 MB
% 25.95/6.71 % (2053737)Instructions burned: 130 (million)
% 25.95/6.71 % (2053744)lrs+10_1_sil=8000:sp=occurrence:random_seed=113907067:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 25.95/6.71 % (2053748)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3853063021:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/157Mi)
% 25.95/6.71 % (2053749)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1697641256:i=325:sd=1:ss=axioms:sgt=32_2968 on theBenchmark for (2968ds/325Mi)
% 25.95/6.71 % (2053750)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=2384541765:s2a=on:i=248:s2at=1.23:gtg=position_2967 on theBenchmark for (2967ds/248Mi)
% 25.95/6.71 % (2053744)Instruction limit reached!
% 21.57/8.33 % (2053744)------------------------------
% 21.57/8.33 % (2053744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053744)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053744)Termination reason: Instruction limit
% 21.57/8.33 % (2053744)Termination phase: Property scanning
% 21.57/8.33 % (2053744)Time elapsed: 0.202 s
% 21.57/8.33 % (2053744)Peak memory usage: 139 MB
% 21.57/8.33 % (2053744)Instructions burned: 285 (million)
% 21.57/8.33 % (2053748)Instruction limit reached!
% 21.57/8.33 % (2053748)------------------------------
% 21.57/8.33 % (2053748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053748)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053748)Termination reason: Instruction limit
% 21.57/8.33 % (2053748)Termination phase: Property scanning
% 21.57/8.33 % (2053748)Time elapsed: 0.127 s
% 21.57/8.33 % (2053748)Peak memory usage: 136 MB
% 21.57/8.33 % (2053748)Instructions burned: 157 (million)
% 21.57/8.33 % (2053750)Instruction limit reached!
% 21.57/8.33 % (2053750)------------------------------
% 21.57/8.33 % (2053750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053750)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053750)Termination reason: Instruction limit
% 21.57/8.33 % (2053750)Termination phase: Property scanning
% 21.57/8.33 % (2053750)Time elapsed: 0.204 s
% 21.57/8.33 % (2053750)Peak memory usage: 136 MB
% 21.57/8.33 % (2053750)Instructions burned: 249 (million)
% 21.57/8.33 % (2053755)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3885707287:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2965 on theBenchmark for (2965ds/294Mi)
% 21.57/8.33 % (2053749)Instruction limit reached!
% 21.57/8.33 % (2053749)------------------------------
% 21.57/8.33 % (2053749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053749)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053749)Termination reason: Instruction limit
% 21.57/8.33 % (2053749)Termination phase: Saturation
% 21.57/8.33 % (2053749)Time elapsed: 0.317 s
% 21.57/8.33 % (2053749)Peak memory usage: 142 MB
% 21.57/8.33 % (2053749)Instructions burned: 325 (million)
% 21.57/8.33 % (2053756)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2407070418:i=2350_2964 on theBenchmark for (2964ds/2350Mi)
% 21.57/8.33 % (2053755)Instruction limit reached!
% 21.57/8.33 % (2053755)------------------------------
% 21.57/8.33 % (2053755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053755)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053755)Termination reason: Instruction limit
% 21.57/8.33 % (2053755)Termination phase: SInE selection
% 21.57/8.33 % (2053755)Time elapsed: 0.162 s
% 21.57/8.33 % (2053755)Peak memory usage: 136 MB
% 21.57/8.33 % (2053755)Instructions burned: 295 (million)
% 21.57/8.33 % (2053757)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3215671942:cts=off:i=113:fsr=off:ss=included:sgt=4_2962 on theBenchmark for (2962ds/113Mi)
% 21.57/8.33 % (2053759)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2028319474:i=127:av=off:fsr=off:sup=off_2962 on theBenchmark for (2962ds/127Mi)
% 21.57/8.33 % (2053757)Instruction limit reached!
% 21.57/8.33 % (2053757)------------------------------
% 21.57/8.33 % (2053757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053757)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053757)Termination reason: Instruction limit
% 21.57/8.33 % (2053757)Termination phase: SInE selection
% 21.57/8.33 % (2053757)Time elapsed: 0.126 s
% 21.57/8.33 % (2053757)Peak memory usage: 135 MB
% 21.57/8.33 % (2053757)Instructions burned: 114 (million)
% 21.57/8.33 % (2053761)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3026481015:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2961 on theBenchmark for (2961ds/114Mi)
% 21.57/8.33 % (2053761)Instruction limit reached!
% 21.57/8.33 % (2053761)------------------------------
% 21.57/8.33 % (2053761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053761)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053761)Termination reason: Instruction limit
% 21.57/8.33 % (2053761)Termination phase: Property scanning
% 21.57/8.33 % (2053761)Time elapsed: 0.051 s
% 21.57/8.33 % (2053761)Peak memory usage: 136 MB
% 21.57/8.33 % (2053761)Instructions burned: 116 (million)
% 21.57/8.33 % (2053759)Instruction limit reached!
% 21.57/8.33 % (2053759)------------------------------
% 21.57/8.33 % (2053759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053759)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053759)Termination reason: Instruction limit
% 21.57/8.33 % (2053759)Termination phase: Preprocessing 1
% 21.57/8.33 % (2053759)Time elapsed: 0.153 s
% 21.57/8.33 % (2053759)Peak memory usage: 137 MB
% 21.57/8.33 % (2053759)Instructions burned: 127 (million)
% 21.57/8.33 % (2053765)lrs+10_1_sil=8000:sp=occurrence:random_seed=3760983723:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2958 on theBenchmark for (2958ds/907Mi)
% 21.57/8.33 % (2053766)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=111699506:i=437:sd=1:aac=none:ss=included_2958 on theBenchmark for (2958ds/437Mi)
% 21.57/8.33 % (2053767)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1968950161:i=5202:ss=axioms:sgt=16_2958 on theBenchmark for (2958ds/5202Mi)
% 21.57/8.33 % (2053765)Instruction limit reached!
% 21.57/8.33 % (2053765)------------------------------
% 21.57/8.33 % (2053765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053765)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053765)Termination reason: Instruction limit
% 21.57/8.33 % (2053765)Termination phase: Saturation
% 21.57/8.33 % (2053765)Time elapsed: 0.486 s
% 21.57/8.33 % (2053765)Peak memory usage: 151 MB
% 21.57/8.33 % (2053765)Instructions burned: 908 (million)
% 21.57/8.33 % (2053766)Instruction limit reached!
% 21.57/8.33 % (2053766)------------------------------
% 21.57/8.33 % (2053766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053766)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053766)Termination reason: Instruction limit
% 21.57/8.33 % (2053766)Termination phase: Saturation
% 21.57/8.33 % (2053766)Time elapsed: 0.463 s
% 21.57/8.33 % (2053766)Peak memory usage: 142 MB
% 21.57/8.33 % (2053766)Instructions burned: 438 (million)
% 21.57/8.33 % (2053771)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=960031619:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2952 on theBenchmark for (2952ds/134Mi)
% 21.57/8.33 % (2053771)Instruction limit reached!
% 21.57/8.33 % (2053771)------------------------------
% 21.57/8.33 % (2053771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053771)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053771)Termination reason: Instruction limit
% 21.57/8.33 % (2053771)Termination phase: SInE selection
% 21.57/8.33 % (2053771)Time elapsed: 0.092 s
% 21.57/8.33 % (2053771)Peak memory usage: 135 MB
% 21.57/8.33 % (2053771)Instructions burned: 134 (million)
% 21.57/8.33 % (2053772)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=979286270:st=8:i=592:sd=3:ep=RST:ss=axioms_2951 on theBenchmark for (2951ds/592Mi)
% 21.57/8.33 % (2053774)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2186014558:st=3:i=13193:sd=3:ss=axioms_2948 on theBenchmark for (2948ds/13193Mi)
% 21.57/8.33 % (2053772)Instruction limit reached!
% 21.57/8.33 % (2053772)------------------------------
% 21.57/8.33 % (2053772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053772)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053772)Termination reason: Instruction limit
% 21.57/8.33 % (2053772)Termination phase: Naming
% 21.57/8.33 % (2053772)Time elapsed: 0.680 s
% 21.57/8.33 % (2053772)Peak memory usage: 153 MB
% 21.57/8.33 % (2053772)Instructions burned: 593 (million)
% 21.57/8.33 % (2053779)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=3632603269:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/125Mi)
% 21.57/8.33 % (2053779)Instruction limit reached!
% 21.57/8.33 % (2053779)------------------------------
% 21.57/8.33 % (2053779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053779)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053779)Termination reason: Instruction limit
% 21.57/8.33 % (2053779)Termination phase: Property scanning
% 21.57/8.33 % (2053779)Time elapsed: 0.062 s
% 21.57/8.33 % (2053779)Peak memory usage: 136 MB
% 21.57/8.33 % (2053779)Instructions burned: 127 (million)
% 21.57/8.33 % (2053756)Instruction limit reached!
% 21.57/8.33 % (2053756)------------------------------
% 21.57/8.33 % (2053756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053756)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053756)Termination reason: Instruction limit
% 21.57/8.33 % (2053756)Termination phase: Property scanning
% 21.57/8.33 % (2053756)Time elapsed: 2.432 s
% 21.57/8.33 % (2053756)Peak memory usage: 232 MB
% 21.57/8.33 % (2053756)Instructions burned: 2350 (million)
% 21.57/8.33 % (2053783)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3846196584:i=134:gtgl=5:slsql=off:gtg=exists_sym_2938 on theBenchmark for (2938ds/134Mi)
% 21.57/8.33 % (2053783)Instruction limit reached!
% 21.57/8.33 % (2053783)------------------------------
% 21.57/8.33 % (2053783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053783)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053783)Termination reason: Instruction limit
% 21.57/8.33 % (2053783)Termination phase: Property scanning
% 21.57/8.33 % (2053783)Time elapsed: 0.115 s
% 21.57/8.33 % (2053783)Peak memory usage: 136 MB
% 21.57/8.33 % (2053783)Instructions burned: 135 (million)
% 21.57/8.33 % (2053784)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3727532659:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2937 on theBenchmark for (2937ds/141Mi)
% 21.57/8.33 % (2053784)Instruction limit reached!
% 21.57/8.33 % (2053784)------------------------------
% 21.57/8.33 % (2053784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053784)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053784)Termination reason: Instruction limit
% 21.57/8.33 % (2053784)Termination phase: SInE selection
% 21.57/8.33 % (2053784)Time elapsed: 0.156 s
% 21.57/8.33 % (2053784)Peak memory usage: 135 MB
% 21.57/8.33 % (2053784)Instructions burned: 142 (million)
% 21.57/8.33 % (2053786)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2621400505:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2934 on theBenchmark for (2934ds/431Mi)
% 21.57/8.33 % (2053790)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=2587595222:i=6060:aac=none:ins=25_2932 on theBenchmark for (2932ds/6060Mi)
% 21.57/8.33 % (2053786)Refutation not found, incomplete strategy
% 21.57/8.33 % (2053786)------------------------------
% 21.57/8.33 % (2053786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.57/8.33 % (2053786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.57/8.33 % (2053786)CaDiCaL version: 2.1.3
% 21.57/8.33 % (2053786)Termination reason: Refutation not found, incomplete strategy
% 21.57/8.33 % (2053786)Time elapsed: 0.292 s
% 21.57/8.33 % (2053786)Peak memory usage: 141 MB
% 21.57/8.33 % (2053786)Instructions burned: 245 (million)
% 21.57/8.33 % (2053733)First to succeed.
% 21.57/8.33 % (2053733)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2053582"
% 21.57/8.33 % (2053786)------------------------------
% 21.57/8.33 % (2053786)------------------------------
% 21.57/8.33 % (2053733)Refutation found. Thanks to Tanya!
% 21.57/8.33 % SZS status Theorem for theBenchmark
% 21.57/8.33 % SZS output start Proof for theBenchmark
% See solution above
% 37.79/8.64 % (2053733)------------------------------
% 37.79/8.64 % (2053733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.79/8.64 % (2053733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.79/8.64 % (2053733)CaDiCaL version: 2.1.3
% 37.79/8.64 % (2053733)Termination reason: Refutation
% 37.79/8.64 % (2053733)Time elapsed: 4.062 s
% 37.79/8.64 % (2053733)Peak memory usage: 204 MB
% 37.79/8.64 % (2053733)Instructions burned: 4143 (million)
% 37.79/8.64 % (2053733)------------------------------
% 37.79/8.64 % (2053733)------------------------------
% 37.79/8.64 % (2053582)Success in time 7.653 s
% 37.79/8.64 % Vampire exiting
%------------------------------------------------------------------------------