%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP028+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 : n005.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:55 PM UTC 2026
% Result : Theorem 11.04s 3.91s
% Output : Refutation 19.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 18
% Syntax : Number of formulae : 133 ( 24 unt; 5 def)
% Number of atoms : 483 ( 37 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 596 ( 246 ~; 263 |; 54 &)
% ( 12 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 6 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-3 aty)
% Number of variables : 117 ( 1 sgn 109 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f677,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f6434,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_struct_0) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6850,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f6865,axiom,
! [X0,X1] :
( ( v2_pre_topc(X0)
& l1_pre_topc(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> v4_pre_topc(k6_pre_topc(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_tops_1) ).
fof(f6914,axiom,
! [X0] :
( l1_pre_topc(X0)
=> k6_pre_topc(X0,k2_pre_topc(X0)) = k2_pre_topc(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_tops_1) ).
fof(f13332,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v4_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_tex_4) ).
fof(f13446,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> v1_tsp_1(k1_struct_0(X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14_tsp_1) ).
fof(f13472,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
=> k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tsp_2) ).
fof(f13476,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tsp_2) ).
fof(f13485,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( v1_tsp_1(X1,X0)
& ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( r1_tarski(X1,X2)
& v1_tsp_2(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_tsp_2) ).
fof(f13486,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ? [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
& v1_tsp_2(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_tsp_2) ).
fof(f13487,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ? [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
& v1_tsp_2(X1,X0) ) ),
inference(negated_conjecture,[status(cth)],[f13486]) ).
fof(f13492,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f13545,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13472]) ).
fof(f13546,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_1(X1,X0)
<=> ! [X2] :
( k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13545]) ).
fof(f13553,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13476]) ).
fof(f13554,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13553]) ).
fof(f13571,plain,
! [X0] :
( ! [X1] :
( ~ v1_tsp_1(X1,X0)
| ? [X2] :
( r1_tarski(X1,X2)
& v1_tsp_2(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13485]) ).
fof(f13572,plain,
! [X0] :
( ! [X1] :
( ~ v1_tsp_1(X1,X0)
| ? [X2] :
( r1_tarski(X1,X2)
& v1_tsp_2(X2,X0)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13571]) ).
fof(f13573,plain,
? [X0] :
( ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13487]) ).
fof(f13574,plain,
? [X0] :
( ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f13573]) ).
fof(f13640,plain,
! [X0] :
( ! [X1] :
( v1_tsp_1(k1_struct_0(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13446]) ).
fof(f13641,plain,
! [X0] :
( ! [X1] :
( v1_tsp_1(k1_struct_0(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13640]) ).
fof(f13711,plain,
! [X0,X1] :
( m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f6434]) ).
fof(f13712,plain,
! [X0,X1] :
( m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13711]) ).
fof(f13826,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f13332]) ).
fof(f13827,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f13826]) ).
fof(f14021,plain,
! [X0,X1] :
( v4_pre_topc(k6_pre_topc(X0,X1),X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f6865]) ).
fof(f14022,plain,
! [X0,X1] :
( v4_pre_topc(k6_pre_topc(X0,X1),X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f14021]) ).
fof(f14606,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6850]) ).
fof(f14970,plain,
! [X0] :
( k6_pre_topc(X0,k2_pre_topc(X0)) = k2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6914]) ).
fof(f14988,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f16897,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ? [X2] :
( k1_struct_0(X0,X2) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2))
& r2_hidden(X2,X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2)) = k1_struct_0(X0,X2)
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_tsp_1(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f13546]) ).
fof(f16898,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ? [X2] :
( k1_struct_0(X0,X2) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X2))
& r2_hidden(X2,X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X3] :
( k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v1_tsp_1(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(rectify,[],[f16897]) ).
fof(f16899,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_1(X1,X0)
| ( k1_struct_0(X0,sK28(X0,X1)) != k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,sK28(X0,X1)))
& r2_hidden(sK28(X0,X1),X1)
& m1_subset_1(sK28(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X3] :
( k1_struct_0(X0,X3) = k5_subset_1(u1_struct_0(X0),X1,k4_tex_4(X0,X3))
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v1_tsp_1(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X2,sK28(X0,X1))],[f16898]) ).
fof(f16907,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| u1_struct_0(X0) != k3_tex_4(X0,X1) )
& ( ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f13554]) ).
fof(f16908,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| u1_struct_0(X0) != k3_tex_4(X0,X1) )
& ( ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) )
| ~ v1_tsp_2(X1,X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f16907]) ).
fof(f16912,plain,
! [X0] :
( ! [X1] :
( ~ v1_tsp_1(X1,X0)
| ( r1_tarski(X1,sK34(X0,X1))
& v1_tsp_2(sK34(X0,X1),X0)
& m1_subset_1(sK34(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X2,sK34(X0,X1))],[f13572]) ).
fof(f16913,plain,
( ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v1_tsp_2(X1,sK35) )
& ~ v3_struct_0(sK35)
& v2_pre_topc(sK35)
& l1_pre_topc(sK35) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X0,sK35)],[f13574]) ).
fof(f16979,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f677]) ).
fof(f18090,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| m1_subset_1(sK28(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| v1_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f16899]) ).
fof(f18108,plain,
! [X0,X1] :
( u1_struct_0(X0) != k3_tex_4(X0,X1)
| ~ v1_tsp_1(X1,X0)
| v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f16908]) ).
fof(f18122,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| m1_subset_1(sK34(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f16912]) ).
fof(f18123,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v1_tsp_2(sK34(X0,X1),X0)
| ~ v1_tsp_1(X1,X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f16912]) ).
fof(f18125,plain,
l1_pre_topc(sK35),
inference(cnf_transformation,[],[f16913]) ).
fof(f18126,plain,
v2_pre_topc(sK35),
inference(cnf_transformation,[],[f16913]) ).
fof(f18127,plain,
~ v3_struct_0(sK35),
inference(cnf_transformation,[],[f16913]) ).
fof(f18128,plain,
! [X1] :
( ~ v1_tsp_2(X1,sK35)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK35))) ),
inference(cnf_transformation,[],[f16913]) ).
fof(f18240,plain,
! [X0,X1] :
( v1_tsp_1(k1_struct_0(X0,X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13641]) ).
fof(f18359,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f13712]) ).
fof(f18398,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f16979]) ).
fof(f18413,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f13492]) ).
fof(f18476,plain,
! [X0,X1] :
( ~ v4_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f13827]) ).
fof(f18751,plain,
! [X0,X1] :
( ~ v2_pre_topc(X0)
| v4_pre_topc(k6_pre_topc(X0,X1),X0)
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f14022]) ).
fof(f19699,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14606]) ).
fof(f20363,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| k2_pre_topc(X0) = k6_pre_topc(X0,k2_pre_topc(X0)) ),
inference(cnf_transformation,[],[f14970]) ).
fof(f20390,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f14988]) ).
fof(f24743,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f20390,f19699]) ).
fof(f24744,plain,
u1_struct_0(sK35) = k2_pre_topc(sK35),
inference(resolution,[],[f24743,f18125]) ).
fof(f24769,plain,
k2_pre_topc(sK35) = k6_pre_topc(sK35,k2_pre_topc(sK35)),
inference(resolution,[],[f20363,f18125]) ).
fof(f24770,plain,
u1_struct_0(sK35) = k6_pre_topc(sK35,u1_struct_0(sK35)),
inference(forward_demodulation,[],[f24769,f24744]) ).
fof(f24776,plain,
! [X0] :
( v4_pre_topc(k6_pre_topc(sK35,X0),sK35)
| ~ l1_pre_topc(sK35)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35))) ),
inference(resolution,[],[f18751,f18126]) ).
fof(f24777,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| v4_pre_topc(k6_pre_topc(sK35,X0),sK35) ),
inference(forward_subsumption_resolution,[],[f24776,f18125]) ).
fof(f24780,plain,
! [X0] : m1_subset_1(X0,k1_zfmisc_1(X0)),
inference(resolution,[],[f18413,f18398]) ).
fof(f24790,plain,
v4_pre_topc(k6_pre_topc(sK35,u1_struct_0(sK35)),sK35),
inference(resolution,[],[f24780,f24777]) ).
fof(f24797,plain,
v4_pre_topc(u1_struct_0(sK35),sK35),
inference(forward_demodulation,[],[f24790,f24770]) ).
fof(f24798,plain,
( u1_struct_0(sK35) = k3_tex_4(sK35,u1_struct_0(sK35))
| ~ m1_subset_1(u1_struct_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(resolution,[],[f24797,f18476]) ).
fof(f24799,plain,
( u1_struct_0(sK35) = k3_tex_4(sK35,u1_struct_0(sK35))
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24798,f24780]) ).
fof(f24800,plain,
( u1_struct_0(sK35) = k3_tex_4(sK35,u1_struct_0(sK35))
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24799,f18127]) ).
fof(f24801,plain,
( u1_struct_0(sK35) = k3_tex_4(sK35,u1_struct_0(sK35))
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24800,f18126]) ).
fof(f24802,plain,
u1_struct_0(sK35) = k3_tex_4(sK35,u1_struct_0(sK35)),
inference(forward_subsumption_resolution,[],[f24801,f18125]) ).
fof(f24803,plain,
( u1_struct_0(sK35) != u1_struct_0(sK35)
| ~ v1_tsp_1(u1_struct_0(sK35),sK35)
| v1_tsp_2(u1_struct_0(sK35),sK35)
| ~ m1_subset_1(u1_struct_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(superposition,[],[f18108,f24802]) ).
fof(f24804,plain,
( ~ v1_tsp_1(u1_struct_0(sK35),sK35)
| v1_tsp_2(u1_struct_0(sK35),sK35)
| ~ m1_subset_1(u1_struct_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(trivial_inequality_removal,[],[f24803]) ).
fof(f24805,plain,
( ~ v1_tsp_1(u1_struct_0(sK35),sK35)
| ~ m1_subset_1(u1_struct_0(sK35),k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24804,f18128]) ).
fof(f24806,plain,
( ~ v1_tsp_1(u1_struct_0(sK35),sK35)
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24805,f24780]) ).
fof(f24807,plain,
( ~ v1_tsp_1(u1_struct_0(sK35),sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24806,f18127]) ).
fof(f24808,plain,
( ~ v1_tsp_1(u1_struct_0(sK35),sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f24807,f18126]) ).
fof(f24809,plain,
~ v1_tsp_1(u1_struct_0(sK35),sK35),
inference(forward_subsumption_resolution,[],[f24808,f18125]) ).
fof(f25160,plain,
! [X0] :
( m1_subset_1(sK28(sK35,X0),u1_struct_0(sK35))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| v3_struct_0(sK35)
| v1_tsp_1(X0,sK35)
| ~ l1_pre_topc(sK35) ),
inference(resolution,[],[f18090,f18126]) ).
fof(f25161,plain,
! [X0] :
( m1_subset_1(sK28(sK35,X0),u1_struct_0(sK35))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| v1_tsp_1(X0,sK35)
| ~ l1_pre_topc(sK35) ),
inference(forward_subsumption_resolution,[],[f25160,f18127]) ).
fof(f25162,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK35)))
| m1_subset_1(sK28(sK35,X0),u1_struct_0(sK35))
| v1_tsp_1(X0,sK35) ),
inference(forward_subsumption_resolution,[],[f25161,f18125]) ).
fof(f25165,plain,
( m1_subset_1(sK28(sK35,u1_struct_0(sK35)),u1_struct_0(sK35))
| v1_tsp_1(u1_struct_0(sK35),sK35) ),
inference(resolution,[],[f25162,f24780]) ).
fof(f25166,plain,
m1_subset_1(sK28(sK35,u1_struct_0(sK35)),u1_struct_0(sK35)),
inference(forward_subsumption_resolution,[],[f25165,f24809]) ).
fof(f25178,plain,
( v3_struct_0(sK35)
| ~ l1_struct_0(sK35)
| m1_subset_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),k1_zfmisc_1(u1_struct_0(sK35))) ),
inference(resolution,[],[f25166,f18359]) ).
fof(f25208,plain,
( ~ l1_struct_0(sK35)
| m1_subset_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),k1_zfmisc_1(u1_struct_0(sK35))) ),
inference(forward_subsumption_resolution,[],[f25178,f18127]) ).
fof(f25217,definition,
( spl734_43
<=> l1_struct_0(sK35) ),
introduced(definition,[new_symbols(definition,[spl734_43])],[avatar_definition]) ).
fof(f25218,plain,
( ~ l1_struct_0(sK35)
| spl734_43 ),
inference(avatar_component_clause,[],[f25217]) ).
fof(f25228,definition,
( spl734_45
<=> m1_subset_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),k1_zfmisc_1(u1_struct_0(sK35))) ),
introduced(definition,[new_symbols(definition,[spl734_45])],[avatar_definition]) ).
fof(f25229,plain,
( m1_subset_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ spl734_45 ),
inference(avatar_component_clause,[],[f25228]) ).
fof(f25230,plain,
( spl734_45
| ~ spl734_43 ),
inference(avatar_split_clause,[],[f25208,f25217,f25228]) ).
fof(f25239,plain,
( ~ l1_pre_topc(sK35)
| spl734_43 ),
inference(resolution,[],[f25218,f19699]) ).
fof(f25241,plain,
( $false
| spl734_43 ),
inference(forward_subsumption_resolution,[],[f25239,f18125]) ).
fof(f25242,plain,
spl734_43,
inference(avatar_contradiction_clause,[],[f25241]) ).
fof(f25358,plain,
( m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| ~ spl734_45 ),
inference(resolution,[],[f25229,f18122]) ).
fof(f25359,plain,
( v1_tsp_2(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),sK35)
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| ~ spl734_45 ),
inference(resolution,[],[f25229,f18123]) ).
fof(f25394,plain,
( v1_tsp_2(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),sK35)
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| ~ spl734_45 ),
inference(forward_subsumption_resolution,[],[f25359,f18127]) ).
fof(f25395,plain,
( m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| ~ spl734_45 ),
inference(forward_subsumption_resolution,[],[f25358,f18127]) ).
fof(f25399,definition,
( spl734_51
<=> v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35) ),
introduced(definition,[new_symbols(definition,[spl734_51])],[avatar_definition]) ).
fof(f25408,plain,
( v1_tsp_2(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),sK35)
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| ~ l1_pre_topc(sK35)
| ~ spl734_45 ),
inference(forward_subsumption_resolution,[],[f25394,f18126]) ).
fof(f25409,plain,
( m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| ~ l1_pre_topc(sK35)
| ~ spl734_45 ),
inference(forward_subsumption_resolution,[],[f25395,f18126]) ).
fof(f25417,plain,
( ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| spl734_51 ),
inference(avatar_component_clause,[],[f25399]) ).
fof(f25421,plain,
( v1_tsp_2(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),sK35)
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| ~ spl734_45 ),
inference(forward_subsumption_resolution,[],[f25408,f18125]) ).
fof(f25422,plain,
( m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ v1_tsp_1(k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35))),sK35)
| ~ spl734_45 ),
inference(forward_subsumption_resolution,[],[f25409,f18125]) ).
fof(f25432,definition,
( spl734_57
<=> v1_tsp_2(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),sK35) ),
introduced(definition,[new_symbols(definition,[spl734_57])],[avatar_definition]) ).
fof(f25433,plain,
( v1_tsp_2(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),sK35)
| ~ spl734_57 ),
inference(avatar_component_clause,[],[f25432]) ).
fof(f25434,plain,
( ~ spl734_51
| spl734_57
| ~ spl734_45 ),
inference(avatar_split_clause,[],[f25421,f25228,f25432,f25399]) ).
fof(f25436,definition,
( spl734_58
<=> m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35))) ),
introduced(definition,[new_symbols(definition,[spl734_58])],[avatar_definition]) ).
fof(f25437,plain,
( m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ spl734_58 ),
inference(avatar_component_clause,[],[f25436]) ).
fof(f25438,plain,
( ~ spl734_51
| spl734_58
| ~ spl734_45 ),
inference(avatar_split_clause,[],[f25422,f25228,f25436,f25399]) ).
fof(f25466,plain,
( ~ m1_subset_1(sK28(sK35,u1_struct_0(sK35)),u1_struct_0(sK35))
| v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| spl734_51 ),
inference(resolution,[],[f25417,f18240]) ).
fof(f25468,plain,
( v3_struct_0(sK35)
| ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| spl734_51 ),
inference(forward_subsumption_resolution,[],[f25466,f25166]) ).
fof(f25469,plain,
( ~ v2_pre_topc(sK35)
| ~ l1_pre_topc(sK35)
| spl734_51 ),
inference(forward_subsumption_resolution,[],[f25468,f18127]) ).
fof(f25470,plain,
( ~ l1_pre_topc(sK35)
| spl734_51 ),
inference(forward_subsumption_resolution,[],[f25469,f18126]) ).
fof(f25471,plain,
( $false
| spl734_51 ),
inference(forward_subsumption_resolution,[],[f25470,f18125]) ).
fof(f25472,plain,
spl734_51,
inference(avatar_contradiction_clause,[],[f25471]) ).
fof(f25697,plain,
( ~ m1_subset_1(sK34(sK35,k1_struct_0(sK35,sK28(sK35,u1_struct_0(sK35)))),k1_zfmisc_1(u1_struct_0(sK35)))
| ~ spl734_57 ),
inference(resolution,[],[f25433,f18128]) ).
fof(f25704,plain,
( $false
| ~ spl734_57
| ~ spl734_58 ),
inference(forward_subsumption_resolution,[],[f25697,f25437]) ).
fof(f25705,plain,
( ~ spl734_57
| ~ spl734_58 ),
inference(avatar_contradiction_clause,[],[f25704]) ).
cnf(s39,plain,
( ~ spl734_43
| spl734_45 ),
inference(sat_conversion,[],[f25230]) ).
cnf(s41,plain,
spl734_43,
inference(sat_conversion,[],[f25242]) ).
cnf(s52,plain,
( ~ spl734_45
| ~ spl734_51
| spl734_57 ),
inference(sat_conversion,[],[f25434]) ).
cnf(s53,plain,
( ~ spl734_45
| ~ spl734_51
| spl734_58 ),
inference(sat_conversion,[],[f25438]) ).
cnf(s60,plain,
spl734_51,
inference(sat_conversion,[],[f25472]) ).
cnf(s80,plain,
( ~ spl734_57
| ~ spl734_58 ),
inference(sat_conversion,[],[f25705]) ).
cnf(s83,plain,
( ~ spl734_45
| spl734_58 ),
inference(rat,[],[s53,s60]) ).
cnf(s84,plain,
( ~ spl734_45
| spl734_57 ),
inference(rat,[],[s52,s60]) ).
cnf(s87,plain,
spl734_45,
inference(rat,[],[s39,s41]) ).
cnf(s89,plain,
spl734_58,
inference(rat,[],[s83,s87]) ).
cnf(s90,plain,
spl734_57,
inference(rat,[],[s84,s87]) ).
cnf(s93,plain,
$false,
inference(rat,[],[s80,s89,s90]) ).
fof(f25712,plain,
$false,
inference(avatar_sat_refutation,[],[s93]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP028+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 : n005.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 18:53:48 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
% 15.64/3.47 % (1041783)Detected formulas, will run a generic FOF schedule.
% 15.64/3.47 % (1041788)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=2232491595:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 15.64/3.47 % (1041794)dis-21_1_sil=8000:lcm=predicate:random_seed=1279725923: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)
% 15.64/3.47 % (1041792)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3337585237:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 15.64/3.47 % (1041793)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3967495937:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 15.64/3.47 % (1041791)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1121726616:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 15.64/3.47 % (1041789)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=4031723326:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 15.64/3.47 % (1041790)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=3010603204:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 15.64/3.47 % (1041793)Instruction limit reached!
% 15.64/3.47 % (1041793)------------------------------
% 15.64/3.47 % (1041793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.47 % (1041793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.47 % (1041793)CaDiCaL version: 2.1.3
% 15.64/3.47 % (1041793)Termination reason: Instruction limit
% 15.64/3.47 % (1041793)Termination phase: Property scanning
% 15.64/3.47 % (1041793)Time elapsed: 0.058 s
% 15.64/3.47 % (1041793)Peak memory usage: 102 MB
% 15.64/3.47 % (1041793)Instructions burned: 139 (million)
% 15.64/3.47 % (1041791)Refutation not found, incomplete strategy
% 15.64/3.47 % (1041791)------------------------------
% 15.64/3.47 % (1041791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.47 % (1041791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.47 % (1041791)CaDiCaL version: 2.1.3
% 15.64/3.47 % (1041791)Termination reason: Refutation not found, incomplete strategy
% 15.64/3.47 % (1041791)Time elapsed: 0.067 s
% 15.64/3.47 % (1041791)Peak memory usage: 107 MB
% 15.64/3.47 % (1041791)Instructions burned: 81 (million)
% 15.64/3.47 % (1041794)Instruction limit reached!
% 15.64/3.47 % (1041794)------------------------------
% 15.64/3.47 % (1041794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.47 % (1041794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.47 % (1041794)CaDiCaL version: 2.1.3
% 15.64/3.47 % (1041794)Termination reason: Instruction limit
% 15.64/3.47 % (1041794)Termination phase: Preprocessing 1
% 15.64/3.47 % (1041794)Time elapsed: 0.094 s
% 15.64/3.47 % (1041794)Peak memory usage: 103 MB
% 15.64/3.47 % (1041794)Instructions burned: 129 (million)
% 15.64/3.47 % (1041792)Instruction limit reached!
% 15.64/3.47 % (1041792)------------------------------
% 15.64/3.47 % (1041792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.47 % (1041792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/3.47 % (1041792)CaDiCaL version: 2.1.3
% 15.64/3.47 % (1041792)Termination reason: Instruction limit
% 15.64/3.47 % (1041792)Termination phase: Preprocessing 3
% 15.64/3.47 % (1041792)Time elapsed: 0.101 s
% 15.64/3.47 % (1041792)Peak memory usage: 106 MB
% 15.64/3.47 % (1041792)Instructions burned: 119 (million)
% 15.64/3.47 % (1041802)lrs+10_1_sil=8000:sp=occurrence:random_seed=2448226074:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 15.64/3.47 % (1041803)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2018089376:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 15.64/3.47 % (1041804)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2630121673:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.64/3.47 % (1041803)Instruction limit reached!
% 15.64/3.47 % (1041803)------------------------------
% 15.64/3.47 % (1041803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/3.47 % (1041803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041803)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041803)Termination reason: Instruction limit
% 11.04/3.91 % (1041803)Termination phase: Property scanning
% 11.04/3.91 % (1041803)Time elapsed: 0.067 s
% 11.04/3.91 % (1041803)Peak memory usage: 102 MB
% 11.04/3.91 % (1041803)Instructions burned: 157 (million)
% 11.04/3.91 % (1041791)------------------------------
% 11.04/3.91 % (1041791)------------------------------
% 11.04/3.91 % (1041802)Instruction limit reached!
% 11.04/3.91 % (1041802)------------------------------
% 11.04/3.91 % (1041802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041802)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041802)Termination reason: Instruction limit
% 11.04/3.91 % (1041802)Termination phase: Saturation
% 11.04/3.91 % (1041802)Time elapsed: 0.187 s
% 11.04/3.91 % (1041802)Peak memory usage: 110 MB
% 11.04/3.91 % (1041802)Instructions burned: 286 (million)
% 11.04/3.91 % (1041808)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=763596403:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 11.04/3.91 % (1041804)Instruction limit reached!
% 11.04/3.91 % (1041804)------------------------------
% 11.04/3.91 % (1041804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041804)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041804)Termination reason: Instruction limit
% 11.04/3.91 % (1041804)Termination phase: Saturation
% 11.04/3.91 % (1041804)Time elapsed: 0.173 s
% 11.04/3.91 % (1041804)Peak memory usage: 107 MB
% 11.04/3.91 % (1041804)Instructions burned: 325 (million)
% 11.04/3.91 % (1041809)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=440243281:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 11.04/3.91 % (1041810)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1767429555:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 11.04/3.91 % (1041808)Instruction limit reached!
% 11.04/3.91 % (1041808)------------------------------
% 11.04/3.91 % (1041808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041808)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041808)Termination reason: Instruction limit
% 11.04/3.91 % (1041808)Termination phase: SInE selection
% 11.04/3.91 % (1041808)Time elapsed: 0.127 s
% 11.04/3.91 % (1041808)Peak memory usage: 103 MB
% 11.04/3.91 % (1041808)Instructions burned: 249 (million)
% 11.04/3.91 % (1041812)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=891345990:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 11.04/3.91 % (1041809)Instruction limit reached!
% 11.04/3.91 % (1041809)------------------------------
% 11.04/3.91 % (1041809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041809)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041809)Termination reason: Instruction limit
% 11.04/3.91 % (1041809)Termination phase: Saturation
% 11.04/3.91 % (1041809)Time elapsed: 0.183 s
% 11.04/3.91 % (1041809)Peak memory usage: 109 MB
% 11.04/3.91 % (1041809)Instructions burned: 295 (million)
% 11.04/3.91 % (1041812)Instruction limit reached!
% 11.04/3.91 % (1041812)------------------------------
% 11.04/3.91 % (1041812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041812)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041812)Termination reason: Instruction limit
% 11.04/3.91 % (1041812)Termination phase: Preprocessing 3
% 11.04/3.91 % (1041812)Time elapsed: 0.095 s
% 11.04/3.91 % (1041812)Peak memory usage: 105 MB
% 11.04/3.91 % (1041812)Instructions burned: 113 (million)
% 11.04/3.91 % (1041815)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1814902753:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 11.04/3.91 % (1041817)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2505611142:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 11.04/3.91 % (1041815)Instruction limit reached!
% 11.04/3.91 % (1041815)------------------------------
% 11.04/3.91 % (1041815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041815)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041815)Termination reason: Instruction limit
% 11.04/3.91 % (1041815)Termination phase: Preprocessing 2
% 11.04/3.91 % (1041815)Time elapsed: 0.103 s
% 11.04/3.91 % (1041815)Peak memory usage: 106 MB
% 11.04/3.91 % (1041815)Instructions burned: 128 (million)
% 11.04/3.91 % (1041818)lrs+10_1_sil=8000:sp=occurrence:random_seed=3704437053:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 11.04/3.91 % (1041817)Instruction limit reached!
% 11.04/3.91 % (1041817)------------------------------
% 11.04/3.91 % (1041817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041817)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041817)Termination reason: Instruction limit
% 11.04/3.91 % (1041817)Termination phase: Property scanning
% 11.04/3.91 % (1041817)Time elapsed: 0.049 s
% 11.04/3.91 % (1041817)Peak memory usage: 102 MB
% 11.04/3.91 % (1041817)Instructions burned: 116 (million)
% 11.04/3.91 % (1041821)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2960490614:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 11.04/3.91 % (1041823)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3756801123:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 11.04/3.91 % (1041821)Instruction limit reached!
% 11.04/3.91 % (1041821)------------------------------
% 11.04/3.91 % (1041821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041821)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041821)Termination reason: Instruction limit
% 11.04/3.91 % (1041821)Termination phase: Saturation
% 11.04/3.91 % (1041821)Time elapsed: 0.283 s
% 11.04/3.91 % (1041821)Peak memory usage: 109 MB
% 11.04/3.91 % (1041821)Instructions burned: 438 (million)
% 11.04/3.91 % (1041826)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1886581072:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 11.04/3.91 % (1041818)Instruction limit reached!
% 11.04/3.91 % (1041818)------------------------------
% 11.04/3.91 % (1041818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041818)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041818)Termination reason: Instruction limit
% 11.04/3.91 % (1041818)Termination phase: Saturation
% 11.04/3.91 % (1041818)Time elapsed: 0.556 s
% 11.04/3.91 % (1041818)Peak memory usage: 121 MB
% 11.04/3.91 % (1041818)Instructions burned: 908 (million)
% 11.04/3.91 % (1041826)Instruction limit reached!
% 11.04/3.91 % (1041826)------------------------------
% 11.04/3.91 % (1041826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041826)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041826)Termination reason: Instruction limit
% 11.04/3.91 % (1041826)Termination phase: Function definition elimination
% 11.04/3.91 % (1041826)Time elapsed: 0.103 s
% 11.04/3.91 % (1041826)Peak memory usage: 106 MB
% 11.04/3.91 % (1041826)Instructions burned: 136 (million)
% 11.04/3.91 % (1041828)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=257794060:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 11.04/3.91 % (1041829)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2545047470:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 11.04/3.91 % (1041828)Instruction limit reached!
% 11.04/3.91 % (1041828)------------------------------
% 11.04/3.91 % (1041828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041828)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041828)Termination reason: Instruction limit
% 11.04/3.91 % (1041828)Termination phase: Function definition elimination
% 11.04/3.91 % (1041828)Time elapsed: 0.374 s
% 11.04/3.91 % (1041828)Peak memory usage: 120 MB
% 11.04/3.91 % (1041828)Instructions burned: 593 (million)
% 11.04/3.91 % (1041810)Instruction limit reached!
% 11.04/3.91 % (1041810)------------------------------
% 11.04/3.91 % (1041810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041810)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041810)Termination reason: Instruction limit
% 11.04/3.91 % (1041810)Termination phase: Saturation
% 11.04/3.91 % (1041810)Time elapsed: 1.444 s
% 11.04/3.91 % (1041810)Peak memory usage: 239 MB
% 11.04/3.91 % (1041810)Instructions burned: 2350 (million)
% 11.04/3.91 % (1041832)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=1508690062:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 11.04/3.91 % (1041832)Instruction limit reached!
% 11.04/3.91 % (1041832)------------------------------
% 11.04/3.91 % (1041832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041832)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041832)Termination reason: Instruction limit
% 11.04/3.91 % (1041832)Termination phase: Property scanning
% 11.04/3.91 % (1041832)Time elapsed: 0.055 s
% 11.04/3.91 % (1041832)Peak memory usage: 102 MB
% 11.04/3.91 % (1041832)Instructions burned: 125 (million)
% 11.04/3.91 % (1041789)First to succeed.
% 11.04/3.91 % (1041789)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1041783"
% 11.04/3.91 % (1041833)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1742444562:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi)
% 11.04/3.91 % (1041833)Instruction limit reached!
% 11.04/3.91 % (1041833)------------------------------
% 11.04/3.91 % (1041833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041833)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041833)Termination reason: Instruction limit
% 11.04/3.91 % (1041833)Termination phase: Property scanning
% 11.04/3.91 % (1041833)Time elapsed: 0.059 s
% 11.04/3.91 % (1041833)Peak memory usage: 102 MB
% 11.04/3.91 % (1041833)Instructions burned: 135 (million)
% 11.04/3.91 % (1041835)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3560838074:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 11.04/3.91 % (1041835)Refutation not found, incomplete strategy
% 11.04/3.91 % (1041835)------------------------------
% 11.04/3.91 % (1041835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.04/3.91 % (1041835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.04/3.91 % (1041835)CaDiCaL version: 2.1.3
% 11.04/3.91 % (1041835)Termination reason: Refutation not found, incomplete strategy
% 11.04/3.91 % (1041835)Time elapsed: 0.066 s
% 11.04/3.91 % (1041835)Peak memory usage: 107 MB
% 11.04/3.91 % (1041835)Instructions burned: 77 (million)
% 11.04/3.91 % (1041837)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2030572985:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi)
% 11.04/3.91 % (1041789)Refutation found. Thanks to Tanya!
% 11.04/3.91 % SZS status Theorem for theBenchmark
% 11.04/3.91 % SZS output start Proof for theBenchmark
% See solution above
% 19.29/4.10 % (1041789)------------------------------
% 19.29/4.10 % (1041789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/4.10 % (1041789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/4.10 % (1041789)CaDiCaL version: 2.1.3
% 19.29/4.10 % (1041789)Termination reason: Refutation
% 19.29/4.10 % (1041789)Time elapsed: 2.103 s
% 19.29/4.10 % (1041789)Peak memory usage: 220 MB
% 19.29/4.10 % (1041789)Instructions burned: 3371 (million)
% 19.29/4.10 % (1041789)------------------------------
% 19.29/4.10 % (1041789)------------------------------
% 19.29/4.10 % (1041783)Success in time 3.228 s
% 19.29/4.10 % Vampire exiting
%------------------------------------------------------------------------------