%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG219+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:29:49 AM UTC 2026
% Result : Theorem 63.92s 9.46s
% Output : Refutation 63.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 4
% Syntax : Number of formulae : 55 ( 33 unt; 1 def)
% Number of atoms : 439 ( 38 equ)
% Maximal formula atoms : 26 ( 7 avg)
% Number of connectives : 607 ( 223 ~; 224 |; 144 &)
% ( 1 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 2 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 42 ( 0 sgn 36 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3171,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/sandbox/benchmark/Axioms/SET007/SET007+278.ax',t32_rmod_2) ).
fof(f3457,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/sandbox/benchmark/theBenchmark.p',t13_rmod_5) ).
fof(f3458,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/sandbox/benchmark/theBenchmark.p',t14_rmod_5) ).
fof(f3459,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)],[f3458]) ).
fof(f6886,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,[],[f3171]) ).
fof(f6887,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,[],[f6886]) ).
fof(f7360,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,[],[f3457]) ).
fof(f7361,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,[],[f7360]) ).
fof(f7362,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,[],[f3459]) ).
fof(f7363,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,[],[f7362]) ).
fof(f11507,plain,
( k1_rlvect_1(sK1807) != k2_group_1(sK1807)
& sK1808 != k1_rmod_5(sK1807,sK1808,sK1809)
& sK1809 = u1_struct_0(sK1808)
& m1_subset_1(sK1809,k1_zfmisc_1(u1_struct_0(sK1808)))
& ~ v3_struct_0(sK1808)
& v3_rlvect_1(sK1808)
& v4_rlvect_1(sK1808)
& v5_rlvect_1(sK1808)
& v6_rlvect_1(sK1808)
& v3_vectsp_2(sK1808,sK1807)
& v5_vectsp_2(sK1808,sK1807)
& l1_vectsp_2(sK1808,sK1807)
& ~ v3_struct_0(sK1807)
& v3_rlvect_1(sK1807)
& v4_rlvect_1(sK1807)
& v5_rlvect_1(sK1807)
& v6_rlvect_1(sK1807)
& v4_group_1(sK1807)
& v7_group_1(sK1807)
& v6_vectsp_1(sK1807)
& v7_vectsp_1(sK1807)
& v8_vectsp_1(sK1807)
& ~ v10_vectsp_1(sK1807)
& v2_vectsp_2(sK1807)
& l3_vectsp_1(sK1807) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1807,sK1808,sK1809]),skolemize(X0,sK1807),skolemize(X1,sK1808),skolemize(X2,sK1809)],[f7363]) ).
fof(f18030,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,[],[f6887]) ).
fof(f18573,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,[],[f7361]) ).
fof(f18574,plain,
l3_vectsp_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18575,plain,
v2_vectsp_2(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18576,plain,
~ v10_vectsp_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18577,plain,
v8_vectsp_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18578,plain,
v7_vectsp_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18579,plain,
v6_vectsp_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18580,plain,
v7_group_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18581,plain,
v4_group_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18582,plain,
v6_rlvect_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18583,plain,
v5_rlvect_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18584,plain,
v4_rlvect_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18585,plain,
v3_rlvect_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18586,plain,
~ v3_struct_0(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18587,plain,
l1_vectsp_2(sK1808,sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18588,plain,
v5_vectsp_2(sK1808,sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18589,plain,
v3_vectsp_2(sK1808,sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f18590,plain,
v6_rlvect_1(sK1808),
inference(cnf_transformation,[],[f11507]) ).
fof(f18591,plain,
v5_rlvect_1(sK1808),
inference(cnf_transformation,[],[f11507]) ).
fof(f18592,plain,
v4_rlvect_1(sK1808),
inference(cnf_transformation,[],[f11507]) ).
fof(f18593,plain,
v3_rlvect_1(sK1808),
inference(cnf_transformation,[],[f11507]) ).
fof(f18594,plain,
~ v3_struct_0(sK1808),
inference(cnf_transformation,[],[f11507]) ).
fof(f18595,plain,
m1_subset_1(sK1809,k1_zfmisc_1(u1_struct_0(sK1808))),
inference(cnf_transformation,[],[f11507]) ).
fof(f18596,plain,
sK1809 = u1_struct_0(sK1808),
inference(cnf_transformation,[],[f11507]) ).
fof(f18597,plain,
sK1808 != k1_rmod_5(sK1807,sK1808,sK1809),
inference(cnf_transformation,[],[f11507]) ).
fof(f18598,plain,
k1_rlvect_1(sK1807) != k2_group_1(sK1807),
inference(cnf_transformation,[],[f11507]) ).
fof(f20351,plain,
! [X3,X0,X1] :
( ~ v5_vectsp_2(X1,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)
| k1_rlvect_1(X0) = k2_group_1(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,[],[f18573]) ).
fof(f23327,plain,
m1_subset_1(sK1809,k1_zfmisc_1(sK1809)),
inference(superposition,[],[f18595,f18596]) ).
fof(f24307,plain,
! [X0] :
( k1_rmod_5(sK1807,sK1808,u1_struct_0(X0)) = X0
| ~ v3_vectsp_2(X0,sK1807)
| ~ m1_rmod_2(X0,sK1807,sK1808)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK1808)))
| v3_struct_0(sK1808)
| ~ v3_rlvect_1(sK1808)
| ~ v4_rlvect_1(sK1808)
| ~ v5_rlvect_1(sK1808)
| ~ v6_rlvect_1(sK1808)
| k1_rlvect_1(sK1807) = k2_group_1(sK1807)
| ~ l1_vectsp_2(sK1808,sK1807)
| v3_struct_0(sK1807)
| ~ v3_rlvect_1(sK1807)
| ~ v4_rlvect_1(sK1807)
| ~ v5_rlvect_1(sK1807)
| ~ v6_rlvect_1(sK1807)
| ~ v4_group_1(sK1807)
| ~ v7_group_1(sK1807)
| ~ v6_vectsp_1(sK1807)
| ~ v7_vectsp_1(sK1807)
| ~ v8_vectsp_1(sK1807)
| v10_vectsp_1(sK1807)
| ~ v2_vectsp_2(sK1807)
| ~ l3_vectsp_1(sK1807) ),
inference(resolution,[],[f20351,f18588]) ).
fof(f24308,plain,
! [X0] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sK1809))
| k1_rmod_5(sK1807,sK1808,u1_struct_0(X0)) = X0
| ~ v3_vectsp_2(X0,sK1807)
| ~ m1_rmod_2(X0,sK1807,sK1808)
| v3_struct_0(sK1808)
| ~ v3_rlvect_1(sK1808)
| ~ v4_rlvect_1(sK1808)
| ~ v5_rlvect_1(sK1808)
| ~ v6_rlvect_1(sK1808)
| k1_rlvect_1(sK1807) = k2_group_1(sK1807)
| ~ l1_vectsp_2(sK1808,sK1807)
| v3_struct_0(sK1807)
| ~ v3_rlvect_1(sK1807)
| ~ v4_rlvect_1(sK1807)
| ~ v5_rlvect_1(sK1807)
| ~ v6_rlvect_1(sK1807)
| ~ v4_group_1(sK1807)
| ~ v7_group_1(sK1807)
| ~ v6_vectsp_1(sK1807)
| ~ v7_vectsp_1(sK1807)
| ~ v8_vectsp_1(sK1807)
| v10_vectsp_1(sK1807)
| ~ v2_vectsp_2(sK1807)
| ~ l3_vectsp_1(sK1807) ),
inference(forward_demodulation,[],[f24307,f18596]) ).
fof(f24437,plain,
! [X0] :
( ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sK1809))
| k1_rmod_5(sK1807,sK1808,u1_struct_0(X0)) = X0
| ~ v3_vectsp_2(X0,sK1807)
| ~ m1_rmod_2(X0,sK1807,sK1808) ),
inference(global_subsumption,[],[f24308,f18598,f18594,f18593,f18592,f18591,f18590,f18587,f18586,f18585,f18584,f18583,f18582,f18581,f18580,f18579,f18578,f18577,f18576,f18575,f18574]) ).
fof(f24649,definition,
( spl1810_621
<=> m1_rmod_2(sK1808,sK1807,sK1808) ),
introduced(definition,[new_symbols(definition,[spl1810_621])],[avatar_definition]) ).
fof(f24651,plain,
( ~ m1_rmod_2(sK1808,sK1807,sK1808)
| spl1810_621 ),
inference(avatar_component_clause,[],[f24649]) ).
fof(f24656,plain,
( v3_struct_0(sK1808)
| ~ v3_rlvect_1(sK1808)
| ~ v4_rlvect_1(sK1808)
| ~ v5_rlvect_1(sK1808)
| ~ v6_rlvect_1(sK1808)
| ~ v5_vectsp_2(sK1808,sK1807)
| ~ l1_vectsp_2(sK1808,sK1807)
| v3_struct_0(sK1807)
| ~ v3_rlvect_1(sK1807)
| ~ v4_rlvect_1(sK1807)
| ~ v5_rlvect_1(sK1807)
| ~ v6_rlvect_1(sK1807)
| ~ v4_group_1(sK1807)
| ~ v6_vectsp_1(sK1807)
| ~ v7_vectsp_1(sK1807)
| ~ v8_vectsp_1(sK1807)
| ~ l3_vectsp_1(sK1807)
| spl1810_621 ),
inference(resolution,[],[f24651,f18030]) ).
fof(f24657,plain,
( $false
| spl1810_621 ),
inference(global_subsumption,[],[f24656,f18594,f18593,f18592,f18591,f18590,f18588,f18587,f18586,f18585,f18584,f18583,f18582,f18581,f18579,f18578,f18577,f18574]) ).
fof(f24658,plain,
spl1810_621,
inference(avatar_contradiction_clause,[],[f24657]) ).
fof(f24660,plain,
( ~ m1_subset_1(sK1809,k1_zfmisc_1(sK1809))
| sK1808 = k1_rmod_5(sK1807,sK1808,sK1809)
| ~ v3_vectsp_2(sK1808,sK1807)
| ~ m1_rmod_2(sK1808,sK1807,sK1808) ),
inference(superposition,[],[f24437,f18596]) ).
fof(f24661,plain,
~ m1_rmod_2(sK1808,sK1807,sK1808),
inference(global_subsumption,[],[f24660,f23327,f18597,f18589]) ).
fof(f24662,plain,
~ spl1810_621,
inference(avatar_split_clause,[],[f24661,f24649]) ).
cnf(s7871,plain,
spl1810_621,
inference(sat_conversion,[],[f24658]) ).
cnf(s7877,plain,
~ spl1810_621,
inference(sat_conversion,[],[f24662]) ).
cnf(s7878,plain,
$false,
inference(rat,[],[s7871,s7877]) ).
fof(f24663,plain,
$false,
inference(avatar_sat_refutation,[],[s7878]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG219+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 % Computer : n018.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 19:48:56 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.26 Running first-order model finding
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.50/3.70 % (3697036)Will run a generic schedule for satisfiability detection.
% 23.50/3.70 % (3697045)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1975926231:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 23.50/3.70 % (3697042)% WARNING: option uhcvi not known.
% 23.50/3.70 % (3697041)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3712442890_2998 on theBenchmark for (2998ds/0Mi)
% 23.50/3.70 % (3697042)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3664841073:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 23.50/3.70 % (3697043)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3796870104:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 23.50/3.70 % (3697044)dis+10_1_sil=32000:sp=arity:random_seed=806405504:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 23.50/3.70 % (3697046)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2488969255:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 23.50/3.70 % (3697047)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1927474923:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 23.50/3.70 % (3697045)Instruction limit reached!
% 23.50/3.70 % (3697045)------------------------------
% 23.50/3.70 % (3697045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.50/3.70 % (3697045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.50/3.70 % (3697045)CaDiCaL version: 2.1.3
% 23.50/3.70 % (3697045)Termination reason: Instruction limit
% 23.50/3.70 % (3697045)Termination phase: NewCNF
% 23.50/3.70 % (3697045)Time elapsed: 0.046 s
% 23.50/3.70 % (3697045)Peak memory usage: 22 MB
% 23.50/3.70 % (3697045)Instructions burned: 119 (million)
% 23.50/3.70 % (3697055)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3615239197:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 23.50/3.70 % (3697044)Instruction limit reached!
% 23.50/3.70 % (3697044)------------------------------
% 23.50/3.70 % (3697044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.50/3.70 % (3697044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.50/3.70 % (3697044)CaDiCaL version: 2.1.3
% 23.50/3.70 % (3697044)Termination reason: Instruction limit
% 23.50/3.70 % (3697044)Termination phase: Preprocessing 3
% 23.50/3.70 % (3697044)Time elapsed: 0.069 s
% 23.50/3.70 % (3697044)Peak memory usage: 20 MB
% 23.50/3.70 % (3697044)Instructions burned: 103 (million)
% 23.50/3.70 % (3697046)Instruction limit reached!
% 23.50/3.70 % (3697046)------------------------------
% 23.50/3.70 % (3697046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.50/3.70 % (3697046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.50/3.70 % (3697046)CaDiCaL version: 2.1.3
% 23.50/3.70 % (3697046)Termination reason: Instruction limit
% 23.50/3.70 % (3697046)Termination phase: Clausification
% 23.50/3.70 % (3697046)Time elapsed: 0.083 s
% 23.50/3.70 % (3697046)Peak memory usage: 21 MB
% 23.50/3.70 % (3697046)Instructions burned: 131 (million)
% 23.50/3.70 % (3697057)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1974367224:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 23.50/3.70 % (3697058)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2427061639:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 23.50/3.70 % (3697047)Instruction limit reached!
% 23.50/3.70 % (3697047)------------------------------
% 23.50/3.70 % (3697047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.50/3.70 % (3697047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.50/3.70 % (3697047)CaDiCaL version: 2.1.3
% 23.50/3.70 % (3697047)Termination reason: Instruction limit
% 23.50/3.70 % (3697047)Termination phase: Property scanning
% 23.50/3.70 % (3697047)Time elapsed: 0.101 s
% 23.50/3.70 % (3697047)Peak memory usage: 22 MB
% 23.50/3.70 % (3697047)Instructions burned: 161 (million)
% 23.50/3.70 % (3697061)ott-21_1_sil=16000:fs=off:random_seed=4151340304:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 23.50/3.70 % (3697057)Instruction limit reached!
% 23.50/3.70 % (3697057)------------------------------
% 23.50/3.70 % (3697057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.50/3.70 % (3697057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.11/8.34 % (3697057)CaDiCaL version: 2.1.3
% 56.11/8.34 % (3697057)Termination reason: Instruction limit
% 56.11/8.34 % (3697057)Termination phase: Clausification
% 56.11/8.34 % (3697057)Time elapsed: 0.083 s
% 56.11/8.34 % (3697057)Peak memory usage: 22 MB
% 56.11/8.34 % (3697057)Instructions burned: 132 (million)
% 56.11/8.34 % (3697063)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2441343935:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 56.11/8.34 % (3697061)Instruction limit reached!
% 56.11/8.34 % (3697061)------------------------------
% 56.11/8.34 % (3697061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.11/8.34 % (3697061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.11/8.34 % (3697061)CaDiCaL version: 2.1.3
% 56.11/8.34 % (3697061)Termination reason: Instruction limit
% 56.11/8.34 % (3697061)Termination phase: Property scanning
% 56.11/8.34 % (3697061)Time elapsed: 0.103 s
% 56.11/8.34 % (3697061)Peak memory usage: 22 MB
% 56.11/8.34 % (3697061)Instructions burned: 182 (million)
% 56.11/8.34 % (3697055)Instruction limit reached!
% 56.11/8.34 % (3697055)------------------------------
% 56.11/8.34 % (3697055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.11/8.34 % (3697055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.11/8.34 % (3697055)CaDiCaL version: 2.1.3
% 56.11/8.34 % (3697055)Termination reason: Instruction limit
% 56.11/8.34 % (3697055)Termination phase: Finite model building preprocessing
% 56.11/8.34 % (3697055)Time elapsed: 0.189 s
% 56.11/8.34 % (3697055)Peak memory usage: 32 MB
% 56.11/8.34 % (3697055)Instructions burned: 718 (million)
% 56.11/8.34 % (3697066)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3911460073:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 56.11/8.34 % (3697065)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1849435923:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 56.11/8.34 % (3697063)Instruction limit reached!
% 56.11/8.34 % (3697063)------------------------------
% 56.11/8.34 % (3697063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.11/8.34 % (3697063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.11/8.34 % (3697063)CaDiCaL version: 2.1.3
% 56.11/8.34 % (3697063)Termination reason: Instruction limit
% 56.11/8.34 % (3697063)Termination phase: Saturation
% 56.11/8.34 % (3697063)Time elapsed: 0.243 s
% 56.11/8.34 % (3697063)Peak memory usage: 26 MB
% 56.11/8.34 % (3697063)Instructions burned: 477 (million)
% 56.11/8.34 % (3697058)Instruction limit reached!
% 56.11/8.34 % (3697058)------------------------------
% 56.11/8.34 % (3697058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.11/8.34 % (3697058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.11/8.34 % (3697058)CaDiCaL version: 2.1.3
% 56.11/8.34 % (3697058)Termination reason: Instruction limit
% 56.11/8.34 % (3697058)Termination phase: Saturation
% 56.11/8.34 % (3697058)Time elapsed: 0.347 s
% 56.11/8.34 % (3697058)Peak memory usage: 29 MB
% 56.11/8.34 % (3697058)Instructions burned: 686 (million)
% 56.11/8.34 % (3697069)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1520116573:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 56.11/8.34 % (3697070)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1257525632:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 56.11/8.34 % (3697066)Instruction limit reached!
% 56.11/8.34 % (3697066)------------------------------
% 56.11/8.34 % (3697066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.11/8.34 % (3697066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.11/8.34 % (3697066)CaDiCaL version: 2.1.3
% 56.11/8.34 % (3697066)Termination reason: Instruction limit
% 56.11/8.34 % (3697066)Termination phase: Saturation
% 56.11/8.34 % (3697066)Time elapsed: 0.342 s
% 56.11/8.34 % (3697066)Peak memory usage: 40 MB
% 56.11/8.34 % (3697066)Instructions burned: 1180 (million)
% 56.11/8.34 % (3697073)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3248072413:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 56.11/8.34 % (3697065)Instruction limit reached!
% 56.11/8.34 % (3697065)------------------------------
% 56.11/8.34 % (3697065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.11/8.34 % (3697065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697065)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697065)Termination reason: Instruction limit
% 63.92/9.46 % (3697065)Termination phase: Finite model building preprocessing
% 63.92/9.46 % (3697065)Time elapsed: 0.403 s
% 63.92/9.46 % (3697065)Peak memory usage: 31 MB
% 63.92/9.46 % (3697065)Instructions burned: 866 (million)
% 63.92/9.46 % (3697075)fmb+10_1_sil=64000:random_seed=586249365:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 63.92/9.46 % (3697070)Instruction limit reached!
% 63.92/9.46 % (3697070)------------------------------
% 63.92/9.46 % (3697070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697070)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697070)Termination reason: Instruction limit
% 63.92/9.46 % (3697070)Termination phase: Saturation
% 63.92/9.46 % (3697070)Time elapsed: 0.354 s
% 63.92/9.46 % (3697070)Peak memory usage: 32 MB
% 63.92/9.46 % (3697070)Instructions burned: 693 (million)
% 63.92/9.46 % (3697073)Instruction limit reached!
% 63.92/9.46 % (3697073)------------------------------
% 63.92/9.46 % (3697073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697073)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697073)Termination reason: Instruction limit
% 63.92/9.46 % (3697073)Termination phase: Saturation
% 63.92/9.46 % (3697073)Time elapsed: 0.223 s
% 63.92/9.46 % (3697073)Peak memory usage: 34 MB
% 63.92/9.46 % (3697073)Instructions burned: 882 (million)
% 63.92/9.46 % (3697078)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2267757125:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 63.92/9.46 % (3697077)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2406982373:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 63.92/9.46 % (3697069)Instruction limit reached!
% 63.92/9.46 % (3697069)------------------------------
% 63.92/9.46 % (3697069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697069)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697069)Termination reason: Instruction limit
% 63.92/9.46 % (3697069)Termination phase: Finite model building preprocessing
% 63.92/9.46 % (3697069)Time elapsed: 0.420 s
% 63.92/9.46 % (3697069)Peak memory usage: 33 MB
% 63.92/9.46 % (3697069)Instructions burned: 890 (million)
% 63.92/9.46 % (3697081)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=80503226:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 63.92/9.46 % (3697078)Instruction limit reached!
% 63.92/9.46 % (3697078)------------------------------
% 63.92/9.46 % (3697078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697078)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697078)Termination reason: Instruction limit
% 63.92/9.46 % (3697078)Termination phase: Finite model building preprocessing
% 63.92/9.46 % (3697078)Time elapsed: 0.238 s
% 63.92/9.46 % (3697078)Peak memory usage: 33 MB
% 63.92/9.46 % (3697078)Instructions burned: 922 (million)
% 63.92/9.46 % (3697083)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=407041634:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 63.92/9.46 % (3697083)Instruction limit reached!
% 63.92/9.46 % (3697083)------------------------------
% 63.92/9.46 % (3697083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697083)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697083)Termination reason: Instruction limit
% 63.92/9.46 % (3697083)Termination phase: Saturation
% 63.92/9.46 % (3697083)Time elapsed: 0.363 s
% 63.92/9.46 % (3697083)Peak memory usage: 33 MB
% 63.92/9.46 % (3697083)Instructions burned: 1476 (million)
% 63.92/9.46 % (3697085)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2037138402:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 63.92/9.46 % (3697085)Instruction limit reached!
% 63.92/9.46 % (3697085)------------------------------
% 63.92/9.46 % (3697085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697085)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697085)Termination reason: Instruction limit
% 63.92/9.46 % (3697085)Termination phase: Finite model building preprocessing
% 63.92/9.46 % (3697085)Time elapsed: 1.785 s
% 63.92/9.46 % (3697085)Peak memory usage: 52 MB
% 63.92/9.46 % (3697085)Instructions burned: 6326 (million)
% 63.92/9.46 % (3697087)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3161412589:fmbsr=2.30978:i=2174_2965 on theBenchmark for (2965ds/2174Mi)
% 63.92/9.46 % (3697087)Instruction limit reached!
% 63.92/9.46 % (3697087)------------------------------
% 63.92/9.46 % (3697087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697087)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697087)Termination reason: Instruction limit
% 63.92/9.46 % (3697087)Termination phase: Finite model building preprocessing
% 63.92/9.46 % (3697087)Time elapsed: 0.493 s
% 63.92/9.46 % (3697087)Peak memory usage: 47 MB
% 63.92/9.46 % (3697087)Instructions burned: 2179 (million)
% 63.92/9.46 % (3697089)ott-2_1_sil=16000:newcnf=on:random_seed=2920500008:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2960 on theBenchmark for (2960ds/869Mi)
% 63.92/9.46 % (3697081)Instruction limit reached!
% 63.92/9.46 % (3697081)------------------------------
% 63.92/9.46 % (3697081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697081)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697081)Termination reason: Instruction limit
% 63.92/9.46 % (3697081)Termination phase: Saturation
% 63.92/9.46 % (3697081)Time elapsed: 2.926 s
% 63.92/9.46 % (3697081)Peak memory usage: 65 MB
% 63.92/9.46 % (3697081)Instructions burned: 5132 (million)
% 63.92/9.46 % (3697091)ott+10_1_sil=32000:tgt=ground:random_seed=3762645534:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi)
% 63.92/9.46 % (3697089)Instruction limit reached!
% 63.92/9.46 % (3697089)------------------------------
% 63.92/9.46 % (3697089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697089)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697089)Termination reason: Instruction limit
% 63.92/9.46 % (3697089)Termination phase: Saturation
% 63.92/9.46 % (3697089)Time elapsed: 0.227 s
% 63.92/9.46 % (3697089)Peak memory usage: 33 MB
% 63.92/9.46 % (3697089)Instructions burned: 871 (million)
% 63.92/9.46 % (3697093)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1546442672:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 63.92/9.46 % (3697077)Instruction limit reached!
% 63.92/9.46 % (3697077)------------------------------
% 63.92/9.46 % (3697077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697077)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697077)Termination reason: Instruction limit
% 63.92/9.46 % (3697077)Termination phase: Finite model building preprocessing
% 63.92/9.46 % (3697077)Time elapsed: 5.187 s
% 63.92/9.46 % (3697077)Peak memory usage: 57 MB
% 63.92/9.46 % (3697077)Instructions burned: 9515 (million)
% 63.92/9.46 % (3697095)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3606502646:i=3512:aac=none_2937 on theBenchmark for (2937ds/3512Mi)
% 63.92/9.46 % (3697091)Instruction limit reached!
% 63.92/9.46 % (3697091)------------------------------
% 63.92/9.46 % (3697091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697091)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697091)Termination reason: Instruction limit
% 63.92/9.46 % (3697091)Termination phase: Saturation
% 63.92/9.46 % (3697091)Time elapsed: 3.024 s
% 63.92/9.46 % (3697091)Peak memory usage: 87 MB
% 63.92/9.46 % (3697091)Instructions burned: 5115 (million)
% 63.92/9.46 % (3697097)dis+21_1_sil=32000:sas=cadical:random_seed=3626903529:i=3773:amm=off_2929 on theBenchmark for (2929ds/3773Mi)
% 63.92/9.46 % (3697095)Instruction limit reached!
% 63.92/9.46 % (3697095)------------------------------
% 63.92/9.46 % (3697095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697095)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697095)Termination reason: Instruction limit
% 63.92/9.46 % (3697095)Termination phase: Saturation
% 63.92/9.46 % (3697095)Time elapsed: 1.832 s
% 63.92/9.46 % (3697095)Peak memory usage: 53 MB
% 63.92/9.46 % (3697095)Instructions burned: 3514 (million)
% 63.92/9.46 % (3697099)ott+11_1_sil=16000:gs=on:random_seed=3572446816:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2919 on theBenchmark for (2919ds/2251Mi)
% 63.92/9.46 % (3697097)Instruction limit reached!
% 63.92/9.46 % (3697097)------------------------------
% 63.92/9.46 % (3697097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697097)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697097)Termination reason: Instruction limit
% 63.92/9.46 % (3697097)Termination phase: Saturation
% 63.92/9.46 % (3697097)Time elapsed: 2.009 s
% 63.92/9.46 % (3697097)Peak memory usage: 60 MB
% 63.92/9.46 % (3697097)Instructions burned: 3773 (million)
% 63.92/9.46 % (3697099) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3697036-3697099"...
% 63.92/9.46 % (3697101)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=392801337:fmbsr=1.6:i=67534_2909 on theBenchmark for (2909ds/67534Mi)
% 63.92/9.46 % (3697099)...printing done.
% 63.92/9.46 % (3697099)Refutation found. Thanks to Tanya!
% 63.92/9.46 % SZS status Theorem for theBenchmark
% 63.92/9.46 % SZS output start Proof for theBenchmark
% See solution above
% 63.92/9.46 % (3697099)------------------------------
% 63.92/9.46 % (3697099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 63.92/9.46 % (3697099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.92/9.46 % (3697099)CaDiCaL version: 2.1.3
% 63.92/9.46 % (3697099)Termination reason: Refutation
% 63.92/9.46 % (3697099)Time elapsed: 1.049 s
% 63.92/9.46 % (3697099)Peak memory usage: 49 MB
% 63.92/9.46 % (3697099)Instructions burned: 1945 (million)
% 63.92/9.46 % (3697036)Success in time 9.184 s
% 63.92/9.46 % Vampire exiting
%------------------------------------------------------------------------------