%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG219+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:19:24 AM UTC 2026
% Result : Theorem 10.27s 5.21s
% Output : Refutation 19.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 9
% Syntax : Number of formulae : 96 ( 39 unt; 6 def)
% Number of atoms : 891 ( 46 equ)
% Maximal formula atoms : 27 ( 9 avg)
% Number of connectives : 1340 ( 545 ~; 630 |; 144 &)
% ( 6 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 10 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 7 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 45 ( 0 sgn 39 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24227,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> m1_rmod_2(X1,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_rmod_2) ).
fof(f24513,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ! [X3] :
( ( v3_vectsp_2(X3,X0)
& m1_rmod_2(X3,X0,X1) )
=> ( X2 = u1_struct_0(X3)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_rmod_5) ).
fof(f24514,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X2 = u1_struct_0(X1)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t14_rmod_5) ).
fof(f24515,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X2 = u1_struct_0(X1)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X1 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f24514]) ).
fof(f24565,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3
| u1_struct_0(X3) != X2
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24513]) ).
fof(f24566,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3
| u1_struct_0(X3) != X2
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f24565]) ).
fof(f24567,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_rlvect_1(X0) != k2_group_1(X0)
& k1_rmod_5(X0,X1,X2) != X1
& X2 = u1_struct_0(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24515]) ).
fof(f24568,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k1_rlvect_1(X0) != k2_group_1(X0)
& k1_rmod_5(X0,X1,X2) != X1
& X2 = u1_struct_0(X1)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v3_vectsp_2(X1,X0)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v7_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& ~ v10_vectsp_1(X0)
& v2_vectsp_2(X0)
& l3_vectsp_1(X0) ),
inference(flattening,[],[f24567]) ).
fof(f24616,plain,
! [X0] :
( ! [X1] :
( m1_rmod_2(X1,X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f24227]) ).
fof(f24617,plain,
! [X0] :
( ! [X1] :
( m1_rmod_2(X1,X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f24616]) ).
fof(f24778,plain,
( k1_rlvect_1(sK3) != k2_group_1(sK3)
& sK4 != k1_rmod_5(sK3,sK4,sK5)
& sK5 = u1_struct_0(sK4)
& m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
& ~ v3_struct_0(sK4)
& v3_rlvect_1(sK4)
& v4_rlvect_1(sK4)
& v5_rlvect_1(sK4)
& v6_rlvect_1(sK4)
& v3_vectsp_2(sK4,sK3)
& v5_vectsp_2(sK4,sK3)
& l1_vectsp_2(sK4,sK3)
& ~ v3_struct_0(sK3)
& v3_rlvect_1(sK3)
& v4_rlvect_1(sK3)
& v5_rlvect_1(sK3)
& v6_rlvect_1(sK3)
& v4_group_1(sK3)
& v7_group_1(sK3)
& v6_vectsp_1(sK3)
& v7_vectsp_1(sK3)
& v8_vectsp_1(sK3)
& ~ v10_vectsp_1(sK3)
& v2_vectsp_2(sK3)
& l3_vectsp_1(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f24568]) ).
fof(f24861,plain,
! [X2,X3,X0,X1] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,X2) = X3
| u1_struct_0(X3) != X2
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24566]) ).
fof(f24862,plain,
l3_vectsp_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24863,plain,
v2_vectsp_2(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24864,plain,
~ v10_vectsp_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24865,plain,
v8_vectsp_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24866,plain,
v7_vectsp_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24867,plain,
v6_vectsp_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24868,plain,
v7_group_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24869,plain,
v4_group_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24870,plain,
v6_rlvect_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24871,plain,
v5_rlvect_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24872,plain,
v4_rlvect_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24873,plain,
v3_rlvect_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24874,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24875,plain,
l1_vectsp_2(sK4,sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24876,plain,
v5_vectsp_2(sK4,sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24877,plain,
v3_vectsp_2(sK4,sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24878,plain,
v6_rlvect_1(sK4),
inference(cnf_transformation,[],[f24778]) ).
fof(f24879,plain,
v5_rlvect_1(sK4),
inference(cnf_transformation,[],[f24778]) ).
fof(f24880,plain,
v4_rlvect_1(sK4),
inference(cnf_transformation,[],[f24778]) ).
fof(f24881,plain,
v3_rlvect_1(sK4),
inference(cnf_transformation,[],[f24778]) ).
fof(f24882,plain,
~ v3_struct_0(sK4),
inference(cnf_transformation,[],[f24778]) ).
fof(f24883,plain,
m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4))),
inference(cnf_transformation,[],[f24778]) ).
fof(f24884,plain,
sK5 = u1_struct_0(sK4),
inference(cnf_transformation,[],[f24778]) ).
fof(f24885,plain,
sK4 != k1_rmod_5(sK3,sK4,sK5),
inference(cnf_transformation,[],[f24778]) ).
fof(f24886,plain,
k1_rlvect_1(sK3) != k2_group_1(sK3),
inference(cnf_transformation,[],[f24778]) ).
fof(f24980,plain,
! [X0,X1] :
( m1_rmod_2(X1,X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(cnf_transformation,[],[f24617]) ).
fof(f25189,plain,
! [X3,X0,X1] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| k1_rmod_5(X0,X1,u1_struct_0(X3)) = X3
| ~ v3_vectsp_2(X3,X0)
| ~ m1_rmod_2(X3,X0,X1)
| ~ m1_subset_1(u1_struct_0(X3),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v7_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| v10_vectsp_1(X0)
| ~ v2_vectsp_2(X0)
| ~ l3_vectsp_1(X0) ),
inference(equality_resolution,[],[f24861]) ).
fof(f25268,definition,
( spl65_1
<=> v10_vectsp_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl65_1])],[avatar_definition]) ).
fof(f25270,plain,
( ~ v10_vectsp_1(sK3)
| spl65_1 ),
inference(avatar_component_clause,[],[f25268]) ).
fof(f25271,plain,
~ spl65_1,
inference(avatar_split_clause,[],[f24864,f25268]) ).
fof(f25273,definition,
( spl65_2
<=> v3_struct_0(sK4) ),
introduced(definition,[new_symbols(definition,[spl65_2])],[avatar_definition]) ).
fof(f25275,plain,
( ~ v3_struct_0(sK4)
| spl65_2 ),
inference(avatar_component_clause,[],[f25273]) ).
fof(f25276,plain,
~ spl65_2,
inference(avatar_split_clause,[],[f24882,f25273]) ).
fof(f25278,definition,
( spl65_3
<=> v3_struct_0(sK3) ),
introduced(definition,[new_symbols(definition,[spl65_3])],[avatar_definition]) ).
fof(f25280,plain,
( ~ v3_struct_0(sK3)
| spl65_3 ),
inference(avatar_component_clause,[],[f25278]) ).
fof(f25281,plain,
~ spl65_3,
inference(avatar_split_clause,[],[f24874,f25278]) ).
fof(f25283,definition,
( spl65_4
<=> sK4 = k1_rmod_5(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl65_4])],[avatar_definition]) ).
fof(f25285,plain,
( sK4 != k1_rmod_5(sK3,sK4,sK5)
| spl65_4 ),
inference(avatar_component_clause,[],[f25283]) ).
fof(f25286,plain,
~ spl65_4,
inference(avatar_split_clause,[],[f24885,f25283]) ).
fof(f25310,definition,
( spl65_5
<=> sK5 = u1_struct_0(sK4) ),
introduced(definition,[new_symbols(definition,[spl65_5])],[avatar_definition]) ).
fof(f25312,plain,
( sK5 = u1_struct_0(sK4)
| ~ spl65_5 ),
inference(avatar_component_clause,[],[f25310]) ).
fof(f25313,plain,
spl65_5,
inference(avatar_split_clause,[],[f24884,f25310]) ).
fof(f25398,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(X0)))
| k1_rlvect_1(X1) = k2_group_1(X1)
| sK4 = k1_rmod_5(X1,X0,sK5)
| ~ v3_vectsp_2(sK4,X1)
| ~ m1_rmod_2(sK4,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) )
| ~ spl65_5 ),
inference(superposition,[],[f25189,f25312]) ).
fof(f25868,definition,
( spl65_6
<=> ! [X0,X1] :
( ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(X0)))
| k1_rlvect_1(X1) = k2_group_1(X1)
| sK4 = k1_rmod_5(X1,X0,sK5)
| ~ v3_vectsp_2(sK4,X1)
| ~ m1_rmod_2(sK4,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl65_6])],[avatar_definition]) ).
fof(f25869,plain,
( ! [X0,X1] :
( sK4 = k1_rmod_5(X1,X0,sK5)
| k1_rlvect_1(X1) = k2_group_1(X1)
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_vectsp_2(sK4,X1)
| ~ m1_rmod_2(sK4,X1,X0)
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_vectsp_2(X0,X1)
| ~ l1_vectsp_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| v10_vectsp_1(X1)
| ~ v2_vectsp_2(X1)
| ~ l3_vectsp_1(X1) )
| ~ spl65_6 ),
inference(avatar_component_clause,[],[f25868]) ).
fof(f25870,plain,
( spl65_6
| ~ spl65_5 ),
inference(avatar_split_clause,[],[f25398,f25310,f25868]) ).
fof(f25883,plain,
( sK4 != sK4
| k1_rlvect_1(sK3) = k2_group_1(sK3)
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_vectsp_2(sK4,sK3)
| ~ m1_rmod_2(sK4,sK3,sK4)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_4
| ~ spl65_6 ),
inference(superposition,[],[f25285,f25869]) ).
fof(f25884,plain,
( k1_rlvect_1(sK3) = k2_group_1(sK3)
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_vectsp_2(sK4,sK3)
| ~ m1_rmod_2(sK4,sK3,sK4)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_4
| ~ spl65_6 ),
inference(trivial_inequality_removal,[],[f25883]) ).
fof(f25897,plain,
( k1_rlvect_1(sK3) = k2_group_1(sK3)
| ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_vectsp_2(sK4,sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25884,f24980]) ).
fof(f25901,plain,
( ~ m1_subset_1(sK5,k1_zfmisc_1(u1_struct_0(sK4)))
| ~ v3_vectsp_2(sK4,sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25897,f24886]) ).
fof(f25902,plain,
( ~ v3_vectsp_2(sK4,sK3)
| v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25901,f24883]) ).
fof(f25903,plain,
( v3_struct_0(sK4)
| ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25902,f24877]) ).
fof(f25904,plain,
( ~ v3_rlvect_1(sK4)
| ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25903,f25275]) ).
fof(f25905,plain,
( ~ v4_rlvect_1(sK4)
| ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25904,f24881]) ).
fof(f25906,plain,
( ~ v5_rlvect_1(sK4)
| ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25905,f24880]) ).
fof(f25907,plain,
( ~ v6_rlvect_1(sK4)
| ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25906,f24879]) ).
fof(f25908,plain,
( ~ v5_vectsp_2(sK4,sK3)
| ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25907,f24878]) ).
fof(f25909,plain,
( ~ l1_vectsp_2(sK4,sK3)
| v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25908,f24876]) ).
fof(f25910,plain,
( v3_struct_0(sK3)
| ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25909,f24875]) ).
fof(f25911,plain,
( ~ v3_rlvect_1(sK3)
| ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25910,f25280]) ).
fof(f25912,plain,
( ~ v4_rlvect_1(sK3)
| ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25911,f24873]) ).
fof(f25913,plain,
( ~ v5_rlvect_1(sK3)
| ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25912,f24872]) ).
fof(f25914,plain,
( ~ v6_rlvect_1(sK3)
| ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25913,f24871]) ).
fof(f25915,plain,
( ~ v4_group_1(sK3)
| ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25914,f24870]) ).
fof(f25916,plain,
( ~ v7_group_1(sK3)
| ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25915,f24869]) ).
fof(f25917,plain,
( ~ v6_vectsp_1(sK3)
| ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25916,f24868]) ).
fof(f25918,plain,
( ~ v7_vectsp_1(sK3)
| ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25917,f24867]) ).
fof(f25919,plain,
( ~ v8_vectsp_1(sK3)
| v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25918,f24866]) ).
fof(f25920,plain,
( v10_vectsp_1(sK3)
| ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25919,f24865]) ).
fof(f25921,plain,
( ~ v2_vectsp_2(sK3)
| ~ l3_vectsp_1(sK3)
| spl65_1
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25920,f25270]) ).
fof(f25922,plain,
( ~ l3_vectsp_1(sK3)
| spl65_1
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25921,f24863]) ).
fof(f25923,plain,
( $false
| spl65_1
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(forward_subsumption_resolution,[],[f25922,f24862]) ).
fof(f25924,plain,
( spl65_1
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(avatar_contradiction_clause,[],[f25923]) ).
cnf(s1,plain,
~ spl65_1,
inference(sat_conversion,[],[f25271]) ).
cnf(s2,plain,
~ spl65_2,
inference(sat_conversion,[],[f25276]) ).
cnf(s3,plain,
~ spl65_3,
inference(sat_conversion,[],[f25281]) ).
cnf(s4,plain,
~ spl65_4,
inference(sat_conversion,[],[f25286]) ).
cnf(s5,plain,
spl65_5,
inference(sat_conversion,[],[f25313]) ).
cnf(s6,plain,
( ~ spl65_5
| spl65_6 ),
inference(sat_conversion,[],[f25870]) ).
cnf(s7,plain,
( spl65_1
| spl65_2
| spl65_3
| spl65_4
| ~ spl65_6 ),
inference(sat_conversion,[],[f25924]) ).
cnf(s8,plain,
spl65_6,
inference(rat,[],[s6,s5]) ).
cnf(s9,plain,
spl65_1,
inference(rat,[],[s7,s8,s4,s3,s2]) ).
cnf(s10,plain,
$false,
inference(rat,[],[s1,s9]) ).
fof(f25925,plain,
$false,
inference(avatar_sat_refutation,[],[s10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG219+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.28 % Computer : n003.cluster.edu
% 0.22/0.28 % Model : x86_64 x86_64
% 0.22/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.28 % Memory : 8046.5625MB
% 0.22/0.28 % OS : Linux 6.8.0-71-generic
% 0.22/0.28 % CPULimit : 300
% 0.22/0.28 % WCLimit : 300
% 0.22/0.28 % DateTime : Mon Sep 28 19:48:32 UTC 2026
% 0.22/0.28 % CPUTime :
% 0.22/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.32 Running first-order theorem proving
% 0.22/0.32 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
% 10.27/5.21 % (1912274)Detected formulas, will run a generic FOF schedule.
% 10.27/5.21 % (1912279)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=3864226698:i=141193_2982 on theBenchmark for (2982ds/141193Mi)
% 10.27/5.21 % (1912280)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=3647595209:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2982 on theBenchmark for (2982ds/134677Mi)
% 10.27/5.21 % (1912282)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4075027012:i=109:sd=1:ins=1:gsp=on:ss=axioms_2982 on theBenchmark for (2982ds/109Mi)
% 10.27/5.21 % (1912284)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2704729840:s2a=on:i=139:gtg=position_2982 on theBenchmark for (2982ds/139Mi)
% 10.27/5.21 % (1912283)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=907564549:i=119:av=off:ss=axioms_2982 on theBenchmark for (2982ds/119Mi)
% 10.27/5.21 % (1912281)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=1332186643:i=141695:sd=1:nm=32:gsp=on:ss=included_2982 on theBenchmark for (2982ds/141695Mi)
% 10.27/5.21 % (1912285)dis-21_1_sil=8000:lcm=predicate:random_seed=1715740871:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2982 on theBenchmark for (2982ds/129Mi)
% 10.27/5.21 % (1912282)Instruction limit reached!
% 10.27/5.21 % (1912282)------------------------------
% 10.27/5.21 % (1912282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912282)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912282)Termination reason: Instruction limit
% 10.27/5.21 % (1912282)Termination phase: SInE selection
% 10.27/5.21 % (1912282)Time elapsed: 0.124 s
% 10.27/5.21 % (1912282)Peak memory usage: 118 MB
% 10.27/5.21 % (1912282)Instructions burned: 109 (million)
% 10.27/5.21 % (1912284)Instruction limit reached!
% 10.27/5.21 % (1912284)------------------------------
% 10.27/5.21 % (1912284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912284)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912284)Termination reason: Instruction limit
% 10.27/5.21 % (1912284)Termination phase: Property scanning
% 10.27/5.21 % (1912284)Time elapsed: 0.107 s
% 10.27/5.21 % (1912284)Peak memory usage: 118 MB
% 10.27/5.21 % (1912284)Instructions burned: 140 (million)
% 10.27/5.21 % (1912283)Instruction limit reached!
% 10.27/5.21 % (1912283)------------------------------
% 10.27/5.21 % (1912283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912283)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912283)Termination reason: Instruction limit
% 10.27/5.21 % (1912283)Termination phase: SInE selection
% 10.27/5.21 % (1912283)Time elapsed: 0.136 s
% 10.27/5.21 % (1912283)Peak memory usage: 118 MB
% 10.27/5.21 % (1912283)Instructions burned: 119 (million)
% 10.27/5.21 % (1912285)Instruction limit reached!
% 10.27/5.21 % (1912285)------------------------------
% 10.27/5.21 % (1912285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912285)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912285)Termination reason: Instruction limit
% 10.27/5.21 % (1912285)Termination phase: SInE selection
% 10.27/5.21 % (1912285)Time elapsed: 0.129 s
% 10.27/5.21 % (1912285)Peak memory usage: 118 MB
% 10.27/5.21 % (1912285)Instructions burned: 130 (million)
% 10.27/5.21 % (1912293)lrs+10_1_sil=8000:sp=occurrence:random_seed=2210192481:i=285:sd=3:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/285Mi)
% 10.27/5.21 % (1912294)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1768285385:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/157Mi)
% 10.27/5.21 % (1912296)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=2006789590:s2a=on:i=248:s2at=1.23:gtg=position_2977 on theBenchmark for (2977ds/248Mi)
% 10.27/5.21 % (1912295)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1074991737:i=325:sd=1:ss=axioms:sgt=32_2977 on theBenchmark for (2977ds/325Mi)
% 10.27/5.21 % (1912294)Instruction limit reached!
% 10.27/5.21 % (1912294)------------------------------
% 10.27/5.21 % (1912294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912294)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912294)Termination reason: Instruction limit
% 10.27/5.21 % (1912294)Termination phase: Property scanning
% 10.27/5.21 % (1912294)Time elapsed: 0.130 s
% 10.27/5.21 % (1912294)Peak memory usage: 118 MB
% 10.27/5.21 % (1912294)Instructions burned: 157 (million)
% 10.27/5.21 % (1912296)Instruction limit reached!
% 10.27/5.21 % (1912296)------------------------------
% 10.27/5.21 % (1912296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912296)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912296)Termination reason: Instruction limit
% 10.27/5.21 % (1912296)Termination phase: Property scanning
% 10.27/5.21 % (1912296)Time elapsed: 0.205 s
% 10.27/5.21 % (1912296)Peak memory usage: 118 MB
% 10.27/5.21 % (1912296)Instructions burned: 249 (million)
% 10.27/5.21 % (1912293)Instruction limit reached!
% 10.27/5.21 % (1912293)------------------------------
% 10.27/5.21 % (1912293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912293)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912293)Termination reason: Instruction limit
% 10.27/5.21 % (1912293)Termination phase: Saturation
% 10.27/5.21 % (1912293)Time elapsed: 0.296 s
% 10.27/5.21 % (1912293)Peak memory usage: 125 MB
% 10.27/5.21 % (1912293)Instructions burned: 285 (million)
% 10.27/5.21 % (1912295)Instruction limit reached!
% 10.27/5.21 % (1912295)------------------------------
% 10.27/5.21 % (1912295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912295)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912295)Termination reason: Instruction limit
% 10.27/5.21 % (1912295)Termination phase: Saturation
% 10.27/5.21 % (1912295)Time elapsed: 0.332 s
% 10.27/5.21 % (1912295)Peak memory usage: 124 MB
% 10.27/5.21 % (1912295)Instructions burned: 326 (million)
% 10.27/5.21 % (1912301)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=843650606:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2974 on theBenchmark for (2974ds/294Mi)
% 10.27/5.21 % (1912302)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2407503729:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 10.27/5.21 % (1912303)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2360007204:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 10.27/5.21 % (1912303)Instruction limit reached!
% 10.27/5.21 % (1912303)------------------------------
% 10.27/5.21 % (1912303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912303)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912303)Termination reason: Instruction limit
% 10.27/5.21 % (1912303)Termination phase: SInE selection
% 10.27/5.21 % (1912303)Time elapsed: 0.072 s
% 10.27/5.21 % (1912303)Peak memory usage: 118 MB
% 10.27/5.21 % (1912303)Instructions burned: 114 (million)
% 10.27/5.21 % (1912304)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1661403279:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 10.27/5.21 % (1912301)Instruction limit reached!
% 10.27/5.21 % (1912301)------------------------------
% 10.27/5.21 % (1912301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912301)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912301)Termination reason: Instruction limit
% 10.27/5.21 % (1912301)Termination phase: Preprocessing 3
% 10.27/5.21 % (1912301)Time elapsed: 0.332 s
% 10.27/5.21 % (1912301)Peak memory usage: 124 MB
% 10.27/5.21 % (1912301)Instructions burned: 294 (million)
% 10.27/5.21 % (1912304)Instruction limit reached!
% 10.27/5.21 % (1912304)------------------------------
% 10.27/5.21 % (1912304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912304)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912304)Termination reason: Instruction limit
% 10.27/5.21 % (1912304)Termination phase: Preprocessing 1
% 10.27/5.21 % (1912304)Time elapsed: 0.147 s
% 10.27/5.21 % (1912304)Peak memory usage: 119 MB
% 10.27/5.21 % (1912304)Instructions burned: 127 (million)
% 10.27/5.21 % (1912308)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1237370105:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 10.27/5.21 % (1912308)Instruction limit reached!
% 10.27/5.21 % (1912308)------------------------------
% 10.27/5.21 % (1912308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/5.21 % (1912308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/5.21 % (1912308)CaDiCaL version: 2.1.3
% 10.27/5.21 % (1912308)Termination reason: Instruction limit
% 10.27/5.21 % (1912308)Termination phase: Property scanning
% 10.27/5.21 % (1912308)Time elapsed: 0.052 s
% 10.27/5.21 % (1912308)Peak memory usage: 118 MB
% 10.27/5.21 % (1912308)Instructions burned: 114 (million)
% 10.27/5.21 % (1912311)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3130935651:i=437:sd=1:aac=none:ss=included_2967 on theBenchmark for (2967ds/437Mi)
% 10.27/5.21 % (1912310)lrs+10_1_sil=8000:sp=occurrence:random_seed=760024012:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 10.27/5.21 % (1912313)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2946039918:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 10.27/5.21 % (1912281)First to succeed.
% 10.27/5.21 % (1912281)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1912274"
% 10.27/5.21 % (1912311)Also succeeded, but the first one will report.
% 10.27/5.21 % (1912281)Refutation found. Thanks to Tanya!
% 10.27/5.21 % SZS status Theorem for theBenchmark
% 10.27/5.21 % SZS output start Proof for theBenchmark
% See solution above
% 19.85/5.47 % (1912281)------------------------------
% 19.85/5.47 % (1912281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/5.47 % (1912281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/5.47 % (1912281)CaDiCaL version: 2.1.3
% 19.85/5.47 % (1912281)Termination reason: Refutation
% 19.85/5.47 % (1912281)Time elapsed: 1.666 s
% 19.85/5.47 % (1912281)Peak memory usage: 177 MB
% 19.85/5.47 % (1912281)Instructions burned: 1515 (million)
% 19.85/5.47 % (1912281)------------------------------
% 19.85/5.47 % (1912281)------------------------------
% 19.85/5.47 % (1912274)Success in time 4.223 s
% 19.85/5.47 % Vampire exiting
%------------------------------------------------------------------------------