%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP023+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 15.48s 4.53s
% Output : Refutation 21.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 15
% Syntax : Number of formulae : 155 ( 39 unt; 5 def)
% Number of atoms : 536 ( 89 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 662 ( 281 ~; 288 |; 59 &)
% ( 10 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 6 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 145 ( 1 sgn 134 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f677,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f6850,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f6861,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/sandbox2/benchmark/theBenchmark.p',dt_u1_pre_topc) ).
fof(f6863,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/sandbox2/benchmark/theBenchmark.p',free_g1_pre_topc) ).
fof(f13434,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/sandbox2/benchmark/theBenchmark.p',t5_tsp_1) ).
fof(f13474,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/sandbox2/benchmark/theBenchmark.p',d4_tsp_2) ).
fof(f13475,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/sandbox2/benchmark/theBenchmark.p',t1_tsp_2) ).
fof(f13476,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)],[f13475]) ).
fof(f13481,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f13538,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,[],[f13474]) ).
fof(f13539,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,[],[f13538]) ).
fof(f13540,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,[],[f13476]) ).
fof(f13541,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,[],[f13540]) ).
fof(f13631,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,[],[f13434]) ).
fof(f13632,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,[],[f13631]) ).
fof(f13733,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,[],[f6861]) ).
fof(f13777,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,[],[f6863]) ).
fof(f14365,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f6850]) ).
fof(f15865,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f16870,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,[],[f13539]) ).
fof(f16871,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,[],[f16870]) ).
fof(f16872,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,[],[f16871]) ).
fof(f16873,plain,
! [X0] :
( ! [X1] :
( ( ( v1_tsp_2(X1,X0)
| ~ v1_tsp_1(X1,X0)
| ( sK31(X0,X1) != X1
& v1_tsp_1(sK31(X0,X1),X0)
& r1_tarski(X1,sK31(X0,X1))
& m1_subset_1(sK31(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,[sK31]),skolemize(X2,sK31(X0,X1))],[f16872]) ).
fof(f16874,plain,
( ~ v1_tsp_2(sK35,sK33)
& g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32)) = g1_pre_topc(u1_struct_0(sK33),u1_pre_topc(sK33))
& sK34 = sK35
& v1_tsp_2(sK34,sK32)
& m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
& m1_subset_1(sK34,k1_zfmisc_1(u1_struct_0(sK32)))
& l1_pre_topc(sK33)
& l1_pre_topc(sK32) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33,sK34,sK35]),skolemize(X0,sK32),skolemize(X1,sK33),skolemize(X2,sK34),skolemize(X3,sK35)],[f13541]) ).
fof(f16940,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(f16946,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f16947,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f16946]) ).
fof(f18060,plain,
! [X3,X0,X1] :
( ~ v1_tsp_1(X3,X0)
| X1 = X3
| ~ 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,[],[f16873]) ).
fof(f18061,plain,
! [X0,X1] :
( ~ v1_tsp_2(X1,X0)
| v1_tsp_1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f16873]) ).
fof(f18062,plain,
! [X0,X1] :
( m1_subset_1(sK31(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ 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,[],[f16873]) ).
fof(f18063,plain,
! [X0,X1] :
( r1_tarski(X1,sK31(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,[],[f16873]) ).
fof(f18064,plain,
! [X0,X1] :
( ~ v1_tsp_1(X1,X0)
| v1_tsp_2(X1,X0)
| v1_tsp_1(sK31(X0,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f16873]) ).
fof(f18065,plain,
! [X0,X1] :
( sK31(X0,X1) != 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,[],[f16873]) ).
fof(f18066,plain,
l1_pre_topc(sK32),
inference(cnf_transformation,[],[f16874]) ).
fof(f18067,plain,
l1_pre_topc(sK33),
inference(cnf_transformation,[],[f16874]) ).
fof(f18068,plain,
m1_subset_1(sK34,k1_zfmisc_1(u1_struct_0(sK32))),
inference(cnf_transformation,[],[f16874]) ).
fof(f18069,plain,
m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33))),
inference(cnf_transformation,[],[f16874]) ).
fof(f18070,plain,
v1_tsp_2(sK34,sK32),
inference(cnf_transformation,[],[f16874]) ).
fof(f18071,plain,
sK34 = sK35,
inference(cnf_transformation,[],[f16874]) ).
fof(f18072,plain,
g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32)) = g1_pre_topc(u1_struct_0(sK33),u1_pre_topc(sK33)),
inference(cnf_transformation,[],[f16874]) ).
fof(f18073,plain,
~ v1_tsp_2(sK35,sK33),
inference(cnf_transformation,[],[f16874]) ).
fof(f18221,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,[],[f13632]) ).
fof(f18342,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f16940]) ).
fof(f18343,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f16940]) ).
fof(f18357,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f16947]) ).
fof(f18358,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f13481]) ).
fof(f18367,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,[],[f13733]) ).
fof(f18409,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| g1_pre_topc(X0,X1) != g1_pre_topc(X2,X3)
| X0 = X2 ),
inference(cnf_transformation,[],[f13777]) ).
fof(f19391,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f14365]) ).
fof(f21755,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f15865]) ).
fof(f23039,plain,
v1_tsp_2(sK35,sK32),
inference(definition_unfolding,[],[f18070,f18071]) ).
fof(f23040,plain,
m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK32))),
inference(definition_unfolding,[],[f18068,f18071]) ).
fof(f23931,plain,
! [X3,X0,X1] :
( ~ v1_tsp_1(X3,X0)
| 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,X1)
| ~ 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,[],[f18221]) ).
fof(f24672,plain,
( v1_tsp_1(sK35,sK32)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK32)))
| ~ l1_pre_topc(sK32) ),
inference(resolution,[],[f18061,f23039]) ).
fof(f24674,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f21755,f19391]) ).
fof(f24675,plain,
u1_struct_0(sK32) = k2_pre_topc(sK32),
inference(resolution,[],[f24674,f18066]) ).
fof(f24676,plain,
u1_struct_0(sK33) = k2_pre_topc(sK33),
inference(resolution,[],[f24674,f18067]) ).
fof(f24677,plain,
m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK32))),
inference(superposition,[],[f23040,f24675]) ).
fof(f24682,plain,
g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32)) = g1_pre_topc(k2_pre_topc(sK33),u1_pre_topc(sK33)),
inference(superposition,[],[f18072,f24676]) ).
fof(f24683,plain,
m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33))),
inference(superposition,[],[f18069,f24676]) ).
fof(f24684,plain,
( m1_subset_1(u1_pre_topc(sK33),k1_zfmisc_1(k1_zfmisc_1(k2_pre_topc(sK33))))
| ~ l1_pre_topc(sK33) ),
inference(superposition,[],[f18367,f24676]) ).
fof(f24685,plain,
! [X0] :
( m1_subset_1(sK31(sK33,X0),k1_zfmisc_1(k2_pre_topc(sK33)))
| ~ v1_tsp_1(X0,sK33)
| v1_tsp_2(X0,sK33)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK33)))
| ~ l1_pre_topc(sK33) ),
inference(superposition,[],[f18062,f24676]) ).
fof(f24686,plain,
! [X0] :
( m1_subset_1(sK31(sK33,X0),k1_zfmisc_1(k2_pre_topc(sK33)))
| ~ v1_tsp_1(X0,sK33)
| v1_tsp_2(X0,sK33)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK33))) ),
inference(forward_subsumption_resolution,[],[f24685,f18067]) ).
fof(f24687,plain,
m1_subset_1(u1_pre_topc(sK33),k1_zfmisc_1(k1_zfmisc_1(k2_pre_topc(sK33)))),
inference(forward_subsumption_resolution,[],[f24684,f18067]) ).
fof(f24688,plain,
g1_pre_topc(k2_pre_topc(sK33),u1_pre_topc(sK33)) = g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32)),
inference(forward_demodulation,[],[f24682,f24675]) ).
fof(f24726,plain,
! [X0] :
( ~ v1_tsp_1(X0,sK33)
| r1_tarski(sK31(sK33,X0),k2_pre_topc(sK33))
| v1_tsp_2(X0,sK33)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK33))) ),
inference(resolution,[],[f18342,f24686]) ).
fof(f24777,plain,
! [X0,X1] :
( g1_pre_topc(X0,X1) != g1_pre_topc(k2_pre_topc(sK33),u1_pre_topc(sK33))
| k2_pre_topc(sK33) = X0 ),
inference(resolution,[],[f24687,f18409]) ).
fof(f24788,plain,
! [X0,X1] :
( g1_pre_topc(X0,X1) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| k2_pre_topc(sK33) = X0 ),
inference(forward_demodulation,[],[f24777,f24688]) ).
fof(f24802,plain,
! [X0,X1] :
( ~ l1_pre_topc(X1)
| ~ v1_tsp_1(X0,X1)
| v1_tsp_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| m1_subset_1(X0,k1_zfmisc_1(sK31(X1,X0))) ),
inference(resolution,[],[f18343,f18063]) ).
fof(f24868,plain,
( v1_tsp_1(sK35,sK32)
| ~ l1_pre_topc(sK32) ),
inference(forward_subsumption_resolution,[],[f24672,f23040]) ).
fof(f24869,plain,
v1_tsp_1(sK35,sK32),
inference(forward_subsumption_resolution,[],[f24868,f18066]) ).
fof(f24871,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK35,X0)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK32)))
| ~ l1_pre_topc(X0)
| ~ l1_pre_topc(sK32) ),
inference(resolution,[],[f24869,f23931]) ).
fof(f24875,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK35,X0)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0)
| ~ l1_pre_topc(sK32) ),
inference(forward_subsumption_resolution,[],[f24871,f23040]) ).
fof(f24877,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK35,X0)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f24875,f18066]) ).
fof(f24879,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| v1_tsp_1(sK35,X0)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(X0)))
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32)) ),
inference(forward_demodulation,[],[f24877,f24675]) ).
fof(f24881,plain,
( v1_tsp_1(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| g1_pre_topc(u1_struct_0(sK33),u1_pre_topc(sK33)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32)) ),
inference(resolution,[],[f24879,f18067]) ).
fof(f24882,plain,
( v1_tsp_1(sK35,sK33)
| g1_pre_topc(u1_struct_0(sK33),u1_pre_topc(sK33)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32)) ),
inference(forward_subsumption_resolution,[],[f24881,f18069]) ).
fof(f24883,plain,
( g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK35,sK33) ),
inference(forward_demodulation,[],[f24882,f18072]) ).
fof(f24884,plain,
( g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK35,sK33) ),
inference(forward_demodulation,[],[f24883,f24675]) ).
fof(f24885,plain,
v1_tsp_1(sK35,sK33),
inference(trivial_inequality_removal,[],[f24884]) ).
fof(f24891,plain,
( v1_tsp_2(sK35,sK33)
| v1_tsp_1(sK31(sK33,sK35),sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(sK33) ),
inference(resolution,[],[f24885,f18064]) ).
fof(f24892,plain,
( v1_tsp_1(sK31(sK33,sK35),sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(sK33) ),
inference(forward_subsumption_resolution,[],[f24891,f18073]) ).
fof(f24898,plain,
( v1_tsp_1(sK31(sK33,sK35),sK33)
| ~ l1_pre_topc(sK33) ),
inference(forward_subsumption_resolution,[],[f24892,f18069]) ).
fof(f24904,plain,
v1_tsp_1(sK31(sK33,sK35),sK33),
inference(forward_subsumption_resolution,[],[f24898,f18067]) ).
fof(f24914,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK33),u1_pre_topc(sK33))
| v1_tsp_1(sK31(sK33,sK35),X0)
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(X0)
| ~ l1_pre_topc(sK33) ),
inference(resolution,[],[f24904,f23931]) ).
fof(f24919,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK33),u1_pre_topc(sK33))
| v1_tsp_1(sK31(sK33,sK35),X0)
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(X0) ),
inference(forward_subsumption_resolution,[],[f24914,f18067]) ).
fof(f24921,definition,
( spl734_21
<=> m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK33))) ),
introduced(definition,[new_symbols(definition,[spl734_21])],[avatar_definition]) ).
fof(f24922,plain,
( ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK33)))
| spl734_21 ),
inference(avatar_component_clause,[],[f24921]) ).
fof(f24940,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK31(sK33,sK35),X0)
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f24919,f18072]) ).
fof(f24946,plain,
! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK31(sK33,sK35),X0)
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f24940,f24675]) ).
fof(f24951,plain,
! [X0] :
( ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK33)))
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| v1_tsp_1(sK31(sK33,sK35),X0)
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_pre_topc(X0) ),
inference(forward_demodulation,[],[f24946,f24676]) ).
fof(f24953,definition,
( spl734_28
<=> ! [X0] :
( g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| ~ l1_pre_topc(X0)
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| v1_tsp_1(sK31(sK33,sK35),X0) ) ),
introduced(definition,[new_symbols(definition,[spl734_28])],[avatar_definition]) ).
fof(f24954,plain,
( ! [X0] :
( ~ l1_pre_topc(X0)
| g1_pre_topc(u1_struct_0(X0),u1_pre_topc(X0)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(X0)))
| v1_tsp_1(sK31(sK33,sK35),X0) )
| ~ spl734_28 ),
inference(avatar_component_clause,[],[f24953]) ).
fof(f24955,plain,
( spl734_28
| ~ spl734_21 ),
inference(avatar_split_clause,[],[f24951,f24921,f24953]) ).
fof(f24960,plain,
( ~ v1_tsp_1(sK35,sK33)
| v1_tsp_2(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33)))
| spl734_21 ),
inference(resolution,[],[f24922,f24686]) ).
fof(f24962,plain,
( v1_tsp_2(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33)))
| spl734_21 ),
inference(forward_subsumption_resolution,[],[f24960,f24885]) ).
fof(f24963,plain,
( ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33)))
| spl734_21 ),
inference(forward_subsumption_resolution,[],[f24962,f18073]) ).
fof(f24964,plain,
( $false
| spl734_21 ),
inference(forward_subsumption_resolution,[],[f24963,f24683]) ).
fof(f24965,plain,
spl734_21,
inference(avatar_contradiction_clause,[],[f24964]) ).
fof(f24975,plain,
( g1_pre_topc(u1_struct_0(sK32),u1_pre_topc(sK32)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK32)))
| v1_tsp_1(sK31(sK33,sK35),sK32)
| ~ spl734_28 ),
inference(resolution,[],[f24954,f18066]) ).
fof(f24977,plain,
( g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32)) != g1_pre_topc(k2_pre_topc(sK32),u1_pre_topc(sK32))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK32)))
| v1_tsp_1(sK31(sK33,sK35),sK32)
| ~ spl734_28 ),
inference(forward_demodulation,[],[f24975,f24675]) ).
fof(f24978,plain,
( ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK32)))
| v1_tsp_1(sK31(sK33,sK35),sK32)
| ~ spl734_28 ),
inference(trivial_inequality_removal,[],[f24977]) ).
fof(f24979,plain,
( ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK32)))
| v1_tsp_1(sK31(sK33,sK35),sK32)
| ~ spl734_28 ),
inference(forward_demodulation,[],[f24978,f24675]) ).
fof(f24981,definition,
( spl734_29
<=> v1_tsp_1(sK31(sK33,sK35),sK32) ),
introduced(definition,[new_symbols(definition,[spl734_29])],[avatar_definition]) ).
fof(f24982,plain,
( v1_tsp_1(sK31(sK33,sK35),sK32)
| ~ spl734_29 ),
inference(avatar_component_clause,[],[f24981]) ).
fof(f24984,definition,
( spl734_30
<=> m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK32))) ),
introduced(definition,[new_symbols(definition,[spl734_30])],[avatar_definition]) ).
fof(f24985,plain,
( ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK32)))
| spl734_30 ),
inference(avatar_component_clause,[],[f24984]) ).
fof(f24986,plain,
( spl734_29
| ~ spl734_30
| ~ spl734_28 ),
inference(avatar_split_clause,[],[f24979,f24953,f24984,f24981]) ).
fof(f24994,definition,
( spl734_32
<=> sK35 = sK31(sK33,sK35) ),
introduced(definition,[new_symbols(definition,[spl734_32])],[avatar_definition]) ).
fof(f24995,plain,
( sK35 = sK31(sK33,sK35)
| ~ spl734_32 ),
inference(avatar_component_clause,[],[f24994]) ).
fof(f25023,plain,
! [X0] :
( ~ v1_tsp_1(X0,sK33)
| v1_tsp_2(X0,sK33)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK33)))
| m1_subset_1(X0,k1_zfmisc_1(sK31(sK33,X0))) ),
inference(resolution,[],[f24802,f18067]) ).
fof(f25024,plain,
! [X0] :
( ~ v1_tsp_1(X0,sK33)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK33)))
| v1_tsp_2(X0,sK33)
| m1_subset_1(X0,k1_zfmisc_1(sK31(sK33,X0))) ),
inference(forward_demodulation,[],[f25023,f24676]) ).
fof(f25026,plain,
( ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33)))
| v1_tsp_2(sK35,sK33)
| m1_subset_1(sK35,k1_zfmisc_1(sK31(sK33,sK35))) ),
inference(resolution,[],[f25024,f24885]) ).
fof(f25028,plain,
( v1_tsp_2(sK35,sK33)
| m1_subset_1(sK35,k1_zfmisc_1(sK31(sK33,sK35))) ),
inference(forward_subsumption_resolution,[],[f25026,f24683]) ).
fof(f25029,plain,
m1_subset_1(sK35,k1_zfmisc_1(sK31(sK33,sK35))),
inference(forward_subsumption_resolution,[],[f25028,f18073]) ).
fof(f25031,plain,
r1_tarski(sK35,sK31(sK33,sK35)),
inference(resolution,[],[f25029,f18342]) ).
fof(f25916,plain,
k2_pre_topc(sK32) = k2_pre_topc(sK33),
inference(equality_resolution,[],[f24788]) ).
fof(f26597,plain,
! [X0,X1] :
( ~ r1_tarski(sK31(X0,X1),X1)
| sK31(X0,X1) = 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(resolution,[],[f18357,f18063]) ).
fof(f26661,plain,
! [X0,X1] :
( ~ r1_tarski(sK31(X0,X1),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(forward_subsumption_resolution,[],[f26597,f18065]) ).
fof(f26944,plain,
( r1_tarski(sK31(sK33,sK35),k2_pre_topc(sK33))
| v1_tsp_2(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33))) ),
inference(resolution,[],[f24726,f24885]) ).
fof(f26946,plain,
( r1_tarski(sK31(sK33,sK35),k2_pre_topc(sK33))
| ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK33))) ),
inference(forward_subsumption_resolution,[],[f26944,f18073]) ).
fof(f26947,plain,
r1_tarski(sK31(sK33,sK35),k2_pre_topc(sK33)),
inference(forward_subsumption_resolution,[],[f26946,f24683]) ).
fof(f26948,plain,
r1_tarski(sK31(sK33,sK35),k2_pre_topc(sK32)),
inference(forward_demodulation,[],[f26947,f25916]) ).
fof(f26951,plain,
m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(resolution,[],[f26948,f18343]) ).
fof(f26953,plain,
( $false
| spl734_30 ),
inference(forward_subsumption_resolution,[],[f26951,f24985]) ).
fof(f26954,plain,
spl734_30,
inference(avatar_contradiction_clause,[],[f26953]) ).
fof(f26999,plain,
( ! [X0] :
( sK31(sK33,sK35) = X0
| ~ r1_tarski(X0,sK31(sK33,sK35))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK32)))
| ~ v1_tsp_2(X0,sK32)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK32)))
| ~ l1_pre_topc(sK32) )
| ~ spl734_29 ),
inference(resolution,[],[f24982,f18060]) ).
fof(f27002,plain,
( ! [X0] :
( sK31(sK33,sK35) = X0
| ~ r1_tarski(X0,sK31(sK33,sK35))
| ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(u1_struct_0(sK32)))
| ~ v1_tsp_2(X0,sK32)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK32))) )
| ~ spl734_29 ),
inference(forward_subsumption_resolution,[],[f26999,f18066]) ).
fof(f27017,plain,
( ! [X0] :
( ~ m1_subset_1(sK31(sK33,sK35),k1_zfmisc_1(k2_pre_topc(sK32)))
| sK31(sK33,sK35) = X0
| ~ r1_tarski(X0,sK31(sK33,sK35))
| ~ v1_tsp_2(X0,sK32)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK32))) )
| ~ spl734_29 ),
inference(forward_demodulation,[],[f27002,f24675]) ).
fof(f27071,plain,
( ! [X0] :
( sK31(sK33,sK35) = X0
| ~ r1_tarski(X0,sK31(sK33,sK35))
| ~ v1_tsp_2(X0,sK32)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK32))) )
| ~ spl734_29 ),
inference(forward_subsumption_resolution,[],[f27017,f26951]) ).
fof(f27076,plain,
( ! [X0] :
( ~ v1_tsp_2(X0,sK32)
| sK31(sK33,sK35) = X0
| ~ r1_tarski(X0,sK31(sK33,sK35))
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK32))) )
| ~ spl734_29 ),
inference(forward_demodulation,[],[f27071,f24675]) ).
fof(f27077,plain,
( sK35 = sK31(sK33,sK35)
| ~ r1_tarski(sK35,sK31(sK33,sK35))
| ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK32)))
| ~ spl734_29 ),
inference(resolution,[],[f27076,f23039]) ).
fof(f27078,plain,
( sK35 = sK31(sK33,sK35)
| ~ m1_subset_1(sK35,k1_zfmisc_1(k2_pre_topc(sK32)))
| ~ spl734_29 ),
inference(forward_subsumption_resolution,[],[f27077,f25031]) ).
fof(f27079,plain,
( sK35 = sK31(sK33,sK35)
| ~ spl734_29 ),
inference(forward_subsumption_resolution,[],[f27078,f24677]) ).
fof(f27080,plain,
( spl734_32
| ~ spl734_29 ),
inference(avatar_split_clause,[],[f27079,f24981,f24994]) ).
fof(f27183,plain,
( ~ r1_tarski(sK35,sK35)
| ~ v1_tsp_1(sK35,sK33)
| v1_tsp_2(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(sK33)
| ~ spl734_32 ),
inference(superposition,[],[f26661,f24995]) ).
fof(f27190,plain,
( ~ v1_tsp_1(sK35,sK33)
| v1_tsp_2(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(sK33)
| ~ spl734_32 ),
inference(forward_subsumption_resolution,[],[f27183,f18358]) ).
fof(f27223,plain,
( v1_tsp_2(sK35,sK33)
| ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(sK33)
| ~ spl734_32 ),
inference(forward_subsumption_resolution,[],[f27190,f24885]) ).
fof(f27226,plain,
( ~ m1_subset_1(sK35,k1_zfmisc_1(u1_struct_0(sK33)))
| ~ l1_pre_topc(sK33)
| ~ spl734_32 ),
inference(forward_subsumption_resolution,[],[f27223,f18073]) ).
fof(f27229,plain,
( ~ l1_pre_topc(sK33)
| ~ spl734_32 ),
inference(forward_subsumption_resolution,[],[f27226,f18069]) ).
fof(f27230,plain,
( $false
| ~ spl734_32 ),
inference(forward_subsumption_resolution,[],[f27229,f18067]) ).
fof(f27231,plain,
~ spl734_32,
inference(avatar_contradiction_clause,[],[f27230]) ).
cnf(s23,plain,
( ~ spl734_21
| spl734_28 ),
inference(sat_conversion,[],[f24955]) ).
cnf(s25,plain,
spl734_21,
inference(sat_conversion,[],[f24965]) ).
cnf(s26,plain,
( ~ spl734_28
| spl734_29
| ~ spl734_30 ),
inference(sat_conversion,[],[f24986]) ).
cnf(s59,plain,
spl734_30,
inference(sat_conversion,[],[f26954]) ).
cnf(s78,plain,
( ~ spl734_29
| spl734_32 ),
inference(sat_conversion,[],[f27080]) ).
cnf(s83,plain,
~ spl734_32,
inference(sat_conversion,[],[f27231]) ).
cnf(s84,plain,
~ spl734_29,
inference(rat,[],[s78,s83]) ).
cnf(s90,plain,
~ spl734_28,
inference(rat,[],[s26,s59,s84]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s23,s90,s25]) ).
fof(f27232,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP023+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.24 % Computer : n019.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.25 % DateTime : Mon Sep 28 18:50:06 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.30 Running first-order theorem proving
% 0.25/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.35/3.68 % (101719)Detected formulas, will run a generic FOF schedule.
% 14.35/3.68 % (101811)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2934491616:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 14.35/3.68 % (101805)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=1660949208:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 14.35/3.68 % (101807)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=2097072766:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 14.35/3.68 % (101809)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=1744277003:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 14.35/3.68 % (101813)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=588405097:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 14.35/3.68 % (101815)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1416460944:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 14.35/3.68 % (101816)dis-21_1_sil=8000:lcm=predicate:random_seed=4166888422:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2992 on theBenchmark for (2992ds/129Mi)
% 14.35/3.68 % (101811)Instruction limit reached!
% 14.35/3.68 % (101811)------------------------------
% 14.35/3.68 % (101811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.35/3.68 % (101811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/3.68 % (101811)CaDiCaL version: 2.1.3
% 14.35/3.68 % (101811)Termination reason: Instruction limit
% 14.35/3.68 % (101811)Termination phase: Saturation
% 14.35/3.68 % (101811)Time elapsed: 0.050 s
% 14.35/3.68 % (101811)Peak memory usage: 107 MB
% 14.35/3.68 % (101811)Instructions burned: 109 (million)
% 14.35/3.68 % (101815)Instruction limit reached!
% 14.35/3.68 % (101815)------------------------------
% 14.35/3.68 % (101815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.35/3.68 % (101815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/3.68 % (101815)CaDiCaL version: 2.1.3
% 14.35/3.68 % (101815)Termination reason: Instruction limit
% 14.35/3.68 % (101815)Termination phase: Property scanning
% 14.35/3.68 % (101815)Time elapsed: 0.059 s
% 14.35/3.68 % (101815)Peak memory usage: 102 MB
% 14.35/3.68 % (101815)Instructions burned: 140 (million)
% 14.35/3.68 % (101816)Instruction limit reached!
% 14.35/3.68 % (101816)------------------------------
% 14.35/3.68 % (101816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.35/3.68 % (101816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/3.68 % (101816)CaDiCaL version: 2.1.3
% 14.35/3.68 % (101816)Termination reason: Instruction limit
% 14.35/3.68 % (101816)Termination phase: Preprocessing 1
% 14.35/3.68 % (101816)Time elapsed: 0.094 s
% 14.35/3.68 % (101816)Peak memory usage: 103 MB
% 14.35/3.68 % (101816)Instructions burned: 130 (million)
% 14.35/3.68 % (101813)Instruction limit reached!
% 14.35/3.68 % (101813)------------------------------
% 14.35/3.68 % (101813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.35/3.68 % (101813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/3.68 % (101813)CaDiCaL version: 2.1.3
% 14.35/3.68 % (101813)Termination reason: Instruction limit
% 14.35/3.68 % (101813)Termination phase: Preprocessing 3
% 14.35/3.68 % (101813)Time elapsed: 0.096 s
% 14.35/3.68 % (101813)Peak memory usage: 105 MB
% 14.35/3.68 % (101813)Instructions burned: 119 (million)
% 14.35/3.68 % (101856)lrs+10_1_sil=8000:sp=occurrence:random_seed=3381245134:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 14.35/3.68 % (101857)lrs+10_1_sil=32000:urr=on:br=off:random_seed=16067931:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 14.35/3.68 % (101856)Instruction limit reached!
% 14.35/3.68 % (101856)------------------------------
% 14.35/3.68 % (101856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.35/3.68 % (101856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.35/3.68 % (101856)CaDiCaL version: 2.1.3
% 14.35/3.68 % (101856)Termination reason: Instruction limit
% 14.35/3.68 % (101856)Termination phase: Saturation
% 15.48/4.53 % (101856)Time elapsed: 0.108 s
% 15.48/4.53 % (101856)Peak memory usage: 110 MB
% 15.48/4.53 % (101856)Instructions burned: 285 (million)
% 15.48/4.53 % (101864)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=1511333934:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 15.48/4.53 % (101863)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2668669784:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.48/4.53 % (101857)Instruction limit reached!
% 15.48/4.53 % (101857)------------------------------
% 15.48/4.53 % (101857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101857)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101857)Termination reason: Instruction limit
% 15.48/4.53 % (101857)Termination phase: Property scanning
% 15.48/4.53 % (101857)Time elapsed: 0.069 s
% 15.48/4.53 % (101857)Peak memory usage: 102 MB
% 15.48/4.53 % (101857)Instructions burned: 161 (million)
% 15.48/4.53 % (101909)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2085465328:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 15.48/4.53 % (101864)Instruction limit reached!
% 15.48/4.53 % (101864)------------------------------
% 15.48/4.53 % (101864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101864)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101864)Termination reason: Instruction limit
% 15.48/4.53 % (101864)Termination phase: SInE selection
% 15.48/4.53 % (101864)Time elapsed: 0.126 s
% 15.48/4.53 % (101864)Peak memory usage: 102 MB
% 15.48/4.53 % (101864)Instructions burned: 248 (million)
% 15.48/4.53 % (101909)Instruction limit reached!
% 15.48/4.53 % (101909)------------------------------
% 15.48/4.53 % (101909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101909)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101909)Termination reason: Instruction limit
% 15.48/4.53 % (101909)Termination phase: Saturation
% 15.48/4.53 % (101909)Time elapsed: 0.103 s
% 15.48/4.53 % (101909)Peak memory usage: 110 MB
% 15.48/4.53 % (101909)Instructions burned: 295 (million)
% 15.48/4.53 % (101912)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3647257002:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 15.48/4.53 % (101863)Instruction limit reached!
% 15.48/4.53 % (101863)------------------------------
% 15.48/4.53 % (101863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101863)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101863)Termination reason: Instruction limit
% 15.48/4.53 % (101863)Termination phase: Saturation
% 15.48/4.53 % (101863)Time elapsed: 0.221 s
% 15.48/4.53 % (101863)Peak memory usage: 109 MB
% 15.48/4.53 % (101863)Instructions burned: 326 (million)
% 15.48/4.53 % (101914)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3341943001:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 15.48/4.53 % (101915)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=651173716:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 15.48/4.53 % (101917)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4282208290:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 15.48/4.53 % (101915)Instruction limit reached!
% 15.48/4.53 % (101915)------------------------------
% 15.48/4.53 % (101915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101915)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101915)Termination reason: Instruction limit
% 15.48/4.53 % (101915)Termination phase: Preprocessing 2
% 15.48/4.53 % (101915)Time elapsed: 0.060 s
% 15.48/4.53 % (101915)Peak memory usage: 106 MB
% 15.48/4.53 % (101915)Instructions burned: 127 (million)
% 15.48/4.53 % (101914)Instruction limit reached!
% 15.48/4.53 % (101914)------------------------------
% 15.48/4.53 % (101914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101914)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101914)Termination reason: Instruction limit
% 15.48/4.53 % (101914)Termination phase: Preprocessing 3
% 15.48/4.53 % (101914)Time elapsed: 0.101 s
% 15.48/4.53 % (101914)Peak memory usage: 105 MB
% 15.48/4.53 % (101914)Instructions burned: 113 (million)
% 15.48/4.53 % (101917)Instruction limit reached!
% 15.48/4.53 % (101917)------------------------------
% 15.48/4.53 % (101917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101917)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101917)Termination reason: Instruction limit
% 15.48/4.53 % (101917)Termination phase: Property scanning
% 15.48/4.53 % (101917)Time elapsed: 0.049 s
% 15.48/4.53 % (101917)Peak memory usage: 102 MB
% 15.48/4.53 % (101917)Instructions burned: 114 (million)
% 15.48/4.53 % (101921)lrs+10_1_sil=8000:sp=occurrence:random_seed=2405153314:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 15.48/4.53 % (101922)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3629272947:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 15.48/4.53 % (101923)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=826704367:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 15.48/4.53 % (101921)Instruction limit reached!
% 15.48/4.53 % (101921)------------------------------
% 15.48/4.53 % (101921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101921)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101921)Termination reason: Instruction limit
% 15.48/4.53 % (101921)Termination phase: Saturation
% 15.48/4.53 % (101921)Time elapsed: 0.299 s
% 15.48/4.53 % (101921)Peak memory usage: 121 MB
% 15.48/4.53 % (101921)Instructions burned: 907 (million)
% 15.48/4.53 % (101922)Instruction limit reached!
% 15.48/4.53 % (101922)------------------------------
% 15.48/4.53 % (101922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101922)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101922)Termination reason: Instruction limit
% 15.48/4.53 % (101922)Termination phase: Saturation
% 15.48/4.53 % (101922)Time elapsed: 0.270 s
% 15.48/4.53 % (101922)Peak memory usage: 109 MB
% 15.48/4.53 % (101922)Instructions burned: 438 (million)
% 15.48/4.53 % (101927)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2963092295:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 15.48/4.53 % (101927)Instruction limit reached!
% 15.48/4.53 % (101927)------------------------------
% 15.48/4.53 % (101927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101927)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101927)Termination reason: Instruction limit
% 15.48/4.53 % (101927)Termination phase: Saturation
% 15.48/4.53 % (101927)Time elapsed: 0.057 s
% 15.48/4.53 % (101927)Peak memory usage: 107 MB
% 15.48/4.53 % (101927)Instructions burned: 137 (million)
% 15.48/4.53 % (101928)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1020537738:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 15.48/4.53 % (101931)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=834163342:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 15.48/4.53 % (101928)Instruction limit reached!
% 15.48/4.53 % (101928)------------------------------
% 15.48/4.53 % (101928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101928)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101928)Termination reason: Instruction limit
% 15.48/4.53 % (101928)Termination phase: Property scanning
% 15.48/4.53 % (101928)Time elapsed: 0.370 s
% 15.48/4.53 % (101928)Peak memory usage: 120 MB
% 15.48/4.53 % (101928)Instructions burned: 594 (million)
% 15.48/4.53 % (101933)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=2693616166:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi)
% 15.48/4.53 % (101933)Instruction limit reached!
% 15.48/4.53 % (101933)------------------------------
% 15.48/4.53 % (101933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101933)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101933)Termination reason: Instruction limit
% 15.48/4.53 % (101933)Termination phase: Property scanning
% 15.48/4.53 % (101933)Time elapsed: 0.053 s
% 15.48/4.53 % (101933)Peak memory usage: 102 MB
% 15.48/4.53 % (101933)Instructions burned: 125 (million)
% 15.48/4.53 % (101912)Instruction limit reached!
% 15.48/4.53 % (101912)------------------------------
% 15.48/4.53 % (101912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101912)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101912)Termination reason: Instruction limit
% 15.48/4.53 % (101912)Termination phase: Saturation
% 15.48/4.53 % (101912)Time elapsed: 1.435 s
% 15.48/4.53 % (101912)Peak memory usage: 237 MB
% 15.48/4.53 % (101912)Instructions burned: 2350 (million)
% 15.48/4.53 % (101935)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1306936649:i=134:gtgl=5:slsql=off:gtg=exists_sym_2973 on theBenchmark for (2973ds/134Mi)
% 15.48/4.53 % (101935)Instruction limit reached!
% 15.48/4.53 % (101935)------------------------------
% 15.48/4.53 % (101935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101935)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101935)Termination reason: Instruction limit
% 15.48/4.53 % (101935)Termination phase: Property scanning
% 15.48/4.53 % (101935)Time elapsed: 0.057 s
% 15.48/4.53 % (101935)Peak memory usage: 102 MB
% 15.48/4.53 % (101935)Instructions burned: 135 (million)
% 15.48/4.53 % (101936)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2332178758:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 15.48/4.53 % (101936)Refutation not found, incomplete strategy
% 15.48/4.53 % (101936)------------------------------
% 15.48/4.53 % (101936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101936)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101936)Termination reason: Refutation not found, incomplete strategy
% 15.48/4.53 % (101936)Time elapsed: 0.073 s
% 15.48/4.53 % (101936)Peak memory usage: 107 MB
% 15.48/4.53 % (101936)Instructions burned: 85 (million)
% 15.48/4.53 % (101938)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=554039851:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 15.48/4.53 % (101938)Refutation not found, incomplete strategy
% 15.48/4.53 % (101938)------------------------------
% 15.48/4.53 % (101938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.48/4.53 % (101938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/4.53 % (101938)CaDiCaL version: 2.1.3
% 15.48/4.53 % (101938)Termination reason: Refutation not found, incomplete strategy
% 15.48/4.53 % (101938)Time elapsed: 0.071 s
% 15.48/4.53 % (101938)Peak memory usage: 107 MB
% 15.48/4.53 % (101938)Instructions burned: 86 (million)
% 15.48/4.53 % (101807)First to succeed.
% 15.48/4.53 % (101807)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-101719"
% 15.48/4.53 % (101936)------------------------------
% 15.48/4.53 % (101936)------------------------------
% 15.48/4.53 % (101938)------------------------------
% 15.48/4.53 % (101938)------------------------------
% 15.48/4.53 % (101941)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=2703429149:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi)
% 15.48/4.53 % (101807)Refutation found. Thanks to Tanya!
% 15.48/4.53 % SZS status Theorem for theBenchmark
% 15.48/4.53 % SZS output start Proof for theBenchmark
% See solution above
% 21.53/4.73 % (101807)------------------------------
% 21.53/4.73 % (101807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.53/4.73 % (101807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.53/4.73 % (101807)CaDiCaL version: 2.1.3
% 21.53/4.73 % (101807)Termination reason: Refutation
% 21.53/4.73 % (101807)Time elapsed: 2.368 s
% 21.53/4.73 % (101807)Peak memory usage: 204 MB
% 21.53/4.73 % (101807)Instructions burned: 3818 (million)
% 21.53/4.73 % (101807)------------------------------
% 21.53/4.73 % (101807)------------------------------
% 21.53/4.73 % (101719)Success in time 3.549 s
% 21.53/4.73 % Vampire exiting
%------------------------------------------------------------------------------