%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP653+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 : n004.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 10:15:20 AM UTC 2026
% Result : Theorem 12.74s 3.27s
% Output : Refutation 13.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 13
% Syntax : Number of formulae : 149 ( 29 unt; 6 def)
% Number of atoms : 991 ( 0 equ)
% Maximal formula atoms : 16 ( 6 avg)
% Number of connectives : 1355 ( 513 ~; 585 |; 215 &)
% ( 9 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 7 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 92 ( 0 sgn 86 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9466,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0))
& v14_lattices(k11_group_4(X0))
& v15_lattices(k11_group_4(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_group_4) ).
fof(f9588,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_group_4) ).
fof(f13940,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( m1_lattice4(X2,X0,X1)
<=> ( m4_vectsp_8(X2,X0,X1)
& m3_vectsp_8(X2,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_vectsp_8) ).
fof(f13952,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m4_vectsp_8(X2,X0,X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m4_vectsp_8) ).
fof(f14002,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v2_funct_1(X2)
=> m3_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t36_latsubgr) ).
fof(f14003,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> m4_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_latsubgr) ).
fof(f14004,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v2_funct_1(X2)
=> m1_lattice4(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_latsubgr) ).
fof(f14005,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v2_funct_1(X2)
=> m1_lattice4(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f14004]) ).
fof(f14019,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0))
& v14_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f9466]) ).
fof(f14020,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14019]) ).
fof(f14021,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14020]) ).
fof(f14022,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14021]) ).
fof(f14023,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14022]) ).
fof(f14024,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14023]) ).
fof(f14025,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14024]) ).
fof(f14026,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14025]) ).
fof(f14027,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14026]) ).
fof(f14028,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f9588]) ).
fof(f14029,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f14027]) ).
fof(f14104,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m3_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v2_funct_1(X2)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f14002]) ).
fof(f14105,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m3_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v2_funct_1(X2)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14104]) ).
fof(f14106,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m4_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f14003]) ).
fof(f14107,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m4_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14106]) ).
fof(f14108,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m1_lattice4(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
& v2_funct_1(X2)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f14005]) ).
fof(f14109,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m1_lattice4(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
& v2_funct_1(X2)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f14108]) ).
fof(f14156,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f14028]) ).
fof(f14157,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14156]) ).
fof(f14162,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f14029]) ).
fof(f14163,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14162]) ).
fof(f14637,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( m1_lattice4(X2,X0,X1)
<=> ( m4_vectsp_8(X2,X0,X1)
& m3_vectsp_8(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13940]) ).
fof(f14638,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( m1_lattice4(X2,X0,X1)
<=> ( m4_vectsp_8(X2,X0,X1)
& m3_vectsp_8(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14637]) ).
fof(f14643,plain,
! [X0,X1] :
( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ m4_vectsp_8(X2,X0,X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(ennf_transformation,[],[f13952]) ).
fof(f14644,plain,
! [X0,X1] :
( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ m4_vectsp_8(X2,X0,X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(flattening,[],[f14643]) ).
fof(f14672,plain,
( ~ m1_lattice4(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
& v2_funct_1(sK9)
& v1_funct_1(sK9)
& v1_funct_2(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
& v1_group_6(sK9,sK7,sK8)
& m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
& ~ v3_struct_0(sK8)
& v3_group_1(sK8)
& v4_group_1(sK8)
& l1_group_1(sK8)
& ~ v3_struct_0(sK7)
& v3_group_1(sK7)
& v4_group_1(sK7)
& l1_group_1(sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9)],[f14109]) ).
fof(f14840,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( m1_lattice4(X2,X0,X1)
| ~ m4_vectsp_8(X2,X0,X1)
| ~ m3_vectsp_8(X2,X0,X1) )
& ( ( m4_vectsp_8(X2,X0,X1)
& m3_vectsp_8(X2,X0,X1) )
| ~ m1_lattice4(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f14638]) ).
fof(f14841,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( m1_lattice4(X2,X0,X1)
| ~ m4_vectsp_8(X2,X0,X1)
| ~ m3_vectsp_8(X2,X0,X1) )
& ( ( m4_vectsp_8(X2,X0,X1)
& m3_vectsp_8(X2,X0,X1) )
| ~ m1_lattice4(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14840]) ).
fof(f14914,plain,
! [X2,X0,X1] :
( m3_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v2_funct_1(X2)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14105]) ).
fof(f14915,plain,
! [X2,X0,X1] :
( m4_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14107]) ).
fof(f14916,plain,
l1_group_1(sK7),
inference(cnf_transformation,[],[f14672]) ).
fof(f14917,plain,
v4_group_1(sK7),
inference(cnf_transformation,[],[f14672]) ).
fof(f14918,plain,
v3_group_1(sK7),
inference(cnf_transformation,[],[f14672]) ).
fof(f14919,plain,
~ v3_struct_0(sK7),
inference(cnf_transformation,[],[f14672]) ).
fof(f14920,plain,
l1_group_1(sK8),
inference(cnf_transformation,[],[f14672]) ).
fof(f14921,plain,
v4_group_1(sK8),
inference(cnf_transformation,[],[f14672]) ).
fof(f14922,plain,
v3_group_1(sK8),
inference(cnf_transformation,[],[f14672]) ).
fof(f14923,plain,
~ v3_struct_0(sK8),
inference(cnf_transformation,[],[f14672]) ).
fof(f14924,plain,
m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8)),
inference(cnf_transformation,[],[f14672]) ).
fof(f14925,plain,
v1_group_6(sK9,sK7,sK8),
inference(cnf_transformation,[],[f14672]) ).
fof(f14926,plain,
v1_funct_2(sK9,u1_struct_0(sK7),u1_struct_0(sK8)),
inference(cnf_transformation,[],[f14672]) ).
fof(f14927,plain,
v1_funct_1(sK9),
inference(cnf_transformation,[],[f14672]) ).
fof(f14928,plain,
v2_funct_1(sK9),
inference(cnf_transformation,[],[f14672]) ).
fof(f14929,plain,
~ m1_lattice4(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8)),
inference(cnf_transformation,[],[f14672]) ).
fof(f14997,plain,
! [X0] :
( l3_lattices(k11_group_4(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14157]) ).
fof(f15002,plain,
! [X0] :
( v10_lattices(k11_group_4(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14163]) ).
fof(f15003,plain,
! [X0] :
( ~ v3_struct_0(k11_group_4(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14163]) ).
fof(f15684,plain,
! [X2,X0,X1] :
( m1_lattice4(X2,X0,X1)
| ~ m4_vectsp_8(X2,X0,X1)
| ~ m3_vectsp_8(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14841]) ).
fof(f15690,plain,
! [X2,X0,X1] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m4_vectsp_8(X2,X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f14644]) ).
fof(f15691,plain,
! [X2,X0,X1] :
( v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m4_vectsp_8(X2,X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f14644]) ).
fof(f15692,plain,
! [X2,X0,X1] :
( v1_funct_1(X2)
| ~ m4_vectsp_8(X2,X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(cnf_transformation,[],[f14644]) ).
fof(f15865,definition,
( spl162_1
<=> v3_struct_0(sK7) ),
introduced(definition,[new_symbols(definition,[spl162_1])],[avatar_definition]) ).
fof(f15867,plain,
( ~ v3_struct_0(sK7)
| spl162_1 ),
inference(avatar_component_clause,[],[f15865]) ).
fof(f15868,plain,
~ spl162_1,
inference(avatar_split_clause,[],[f14919,f15865]) ).
fof(f15870,definition,
( spl162_2
<=> v3_struct_0(sK8) ),
introduced(definition,[new_symbols(definition,[spl162_2])],[avatar_definition]) ).
fof(f15872,plain,
( ~ v3_struct_0(sK8)
| spl162_2 ),
inference(avatar_component_clause,[],[f15870]) ).
fof(f15873,plain,
~ spl162_2,
inference(avatar_split_clause,[],[f14923,f15870]) ).
fof(f15875,definition,
( spl162_3
<=> m1_lattice4(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8)) ),
introduced(definition,[new_symbols(definition,[spl162_3])],[avatar_definition]) ).
fof(f15877,plain,
( ~ m1_lattice4(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| spl162_3 ),
inference(avatar_component_clause,[],[f15875]) ).
fof(f15878,plain,
~ spl162_3,
inference(avatar_split_clause,[],[f14929,f15875]) ).
fof(f15880,definition,
( spl162_4
<=> l1_group_1(sK7) ),
introduced(definition,[new_symbols(definition,[spl162_4])],[avatar_definition]) ).
fof(f15882,plain,
( l1_group_1(sK7)
| ~ spl162_4 ),
inference(avatar_component_clause,[],[f15880]) ).
fof(f15883,plain,
spl162_4,
inference(avatar_split_clause,[],[f14916,f15880]) ).
fof(f15885,definition,
( spl162_5
<=> l1_group_1(sK8) ),
introduced(definition,[new_symbols(definition,[spl162_5])],[avatar_definition]) ).
fof(f15887,plain,
( l1_group_1(sK8)
| ~ spl162_5 ),
inference(avatar_component_clause,[],[f15885]) ).
fof(f15888,plain,
spl162_5,
inference(avatar_split_clause,[],[f14920,f15885]) ).
fof(f15892,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v1_funct_1(k3_latsubgr(sK7,sK8,sK9))
| ~ v1_funct_2(k3_latsubgr(sK7,sK8,sK9),u1_struct_0(k11_group_4(sK7)),u1_struct_0(k11_group_4(sK8)))
| ~ m2_relset_1(k3_latsubgr(sK7,sK8,sK9),u1_struct_0(k11_group_4(sK7)),u1_struct_0(k11_group_4(sK8)))
| v3_struct_0(k11_group_4(sK8))
| ~ v10_lattices(k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_3 ),
inference(resolution,[],[f15877,f15684]) ).
fof(f15903,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v1_funct_2(k3_latsubgr(sK7,sK8,sK9),u1_struct_0(k11_group_4(sK7)),u1_struct_0(k11_group_4(sK8)))
| ~ m2_relset_1(k3_latsubgr(sK7,sK8,sK9),u1_struct_0(k11_group_4(sK7)),u1_struct_0(k11_group_4(sK8)))
| v3_struct_0(k11_group_4(sK8))
| ~ v10_lattices(k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_3 ),
inference(forward_subsumption_resolution,[],[f15892,f15692]) ).
fof(f15909,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m2_relset_1(k3_latsubgr(sK7,sK8,sK9),u1_struct_0(k11_group_4(sK7)),u1_struct_0(k11_group_4(sK8)))
| v3_struct_0(k11_group_4(sK8))
| ~ v10_lattices(k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_3 ),
inference(forward_subsumption_resolution,[],[f15903,f15691]) ).
fof(f15915,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK8))
| ~ v10_lattices(k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_3 ),
inference(forward_subsumption_resolution,[],[f15909,f15690]) ).
fof(f16038,plain,
( l3_lattices(k11_group_4(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ spl162_5 ),
inference(resolution,[],[f15887,f14997]) ).
fof(f16043,plain,
( v10_lattices(k11_group_4(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ spl162_5 ),
inference(resolution,[],[f15887,f15002]) ).
fof(f16044,plain,
( ~ v3_struct_0(k11_group_4(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ spl162_5 ),
inference(resolution,[],[f15887,f15003]) ).
fof(f16590,plain,
( ~ v3_struct_0(k11_group_4(sK8))
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16044,f15872]) ).
fof(f16591,plain,
( v10_lattices(k11_group_4(sK8))
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16043,f15872]) ).
fof(f16596,plain,
( l3_lattices(k11_group_4(sK8))
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16038,f15872]) ).
fof(f16918,plain,
( ~ v3_struct_0(k11_group_4(sK8))
| ~ v4_group_1(sK8)
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16590,f14922]) ).
fof(f16919,plain,
( v10_lattices(k11_group_4(sK8))
| ~ v4_group_1(sK8)
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16591,f14922]) ).
fof(f16924,plain,
( l3_lattices(k11_group_4(sK8))
| ~ v4_group_1(sK8)
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16596,f14922]) ).
fof(f17234,plain,
( ~ v3_struct_0(k11_group_4(sK8))
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16918,f14921]) ).
fof(f17235,plain,
( v10_lattices(k11_group_4(sK8))
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16919,f14921]) ).
fof(f17240,plain,
( l3_lattices(k11_group_4(sK8))
| spl162_2
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f16924,f14921]) ).
fof(f17326,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v10_lattices(k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_2
| spl162_3
| ~ spl162_5 ),
inference(backward_subsumption_resolution,[],[f15915,f17234]) ).
fof(f17351,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_2
| spl162_3
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f17326,f17235]) ).
fof(f17369,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| v3_struct_0(k11_group_4(sK7))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_2
| spl162_3
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f17351,f17240]) ).
fof(f17474,plain,
( l3_lattices(k11_group_4(sK7))
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ spl162_4 ),
inference(resolution,[],[f15882,f14997]) ).
fof(f17479,plain,
( v10_lattices(k11_group_4(sK7))
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ spl162_4 ),
inference(resolution,[],[f15882,f15002]) ).
fof(f17480,plain,
( ~ v3_struct_0(k11_group_4(sK7))
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ spl162_4 ),
inference(resolution,[],[f15882,f15003]) ).
fof(f18026,plain,
( ~ v3_struct_0(k11_group_4(sK7))
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f17480,f15867]) ).
fof(f18027,plain,
( v10_lattices(k11_group_4(sK7))
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f17479,f15867]) ).
fof(f18032,plain,
( l3_lattices(k11_group_4(sK7))
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f17474,f15867]) ).
fof(f18354,plain,
( ~ v3_struct_0(k11_group_4(sK7))
| ~ v4_group_1(sK7)
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f18026,f14918]) ).
fof(f18355,plain,
( v10_lattices(k11_group_4(sK7))
| ~ v4_group_1(sK7)
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f18027,f14918]) ).
fof(f18360,plain,
( l3_lattices(k11_group_4(sK7))
| ~ v4_group_1(sK7)
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f18032,f14918]) ).
fof(f18670,plain,
( ~ v3_struct_0(k11_group_4(sK7))
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f18354,f14917]) ).
fof(f18671,plain,
( v10_lattices(k11_group_4(sK7))
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f18355,f14917]) ).
fof(f18676,plain,
( l3_lattices(k11_group_4(sK7))
| spl162_1
| ~ spl162_4 ),
inference(forward_subsumption_resolution,[],[f18360,f14917]) ).
fof(f18765,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v10_lattices(k11_group_4(sK7))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5 ),
inference(backward_subsumption_resolution,[],[f17369,f18670]) ).
fof(f18790,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ l3_lattices(k11_group_4(sK7))
| spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f18765,f18671]) ).
fof(f18808,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f18790,f18676]) ).
fof(f20075,definition,
( spl162_6
<=> v1_funct_2(sK9,u1_struct_0(sK7),u1_struct_0(sK8)) ),
introduced(definition,[new_symbols(definition,[spl162_6])],[avatar_definition]) ).
fof(f20077,plain,
( v1_funct_2(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| ~ spl162_6 ),
inference(avatar_component_clause,[],[f20075]) ).
fof(f20078,plain,
spl162_6,
inference(avatar_split_clause,[],[f14926,f20075]) ).
fof(f20096,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v2_funct_1(sK9)
| ~ v1_funct_1(sK9)
| ~ v1_group_6(sK9,sK7,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(resolution,[],[f20077,f14914]) ).
fof(f20097,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v1_funct_1(sK9)
| ~ v1_group_6(sK9,sK7,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(resolution,[],[f20077,f14915]) ).
fof(f20253,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v1_group_6(sK9,sK7,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20097,f14927]) ).
fof(f20254,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v1_funct_1(sK9)
| ~ v1_group_6(sK9,sK7,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20096,f14928]) ).
fof(f20337,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20253,f14925]) ).
fof(f20338,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v1_group_6(sK9,sK7,sK8)
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20254,f14927]) ).
fof(f20383,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20337,f14924]) ).
fof(f20384,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ m2_relset_1(sK9,u1_struct_0(sK7),u1_struct_0(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20338,f14925]) ).
fof(f20424,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20383,f15872]) ).
fof(f20425,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| v3_struct_0(sK8)
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20384,f14924]) ).
fof(f20452,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20424,f14922]) ).
fof(f20453,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v3_group_1(sK8)
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20425,f15872]) ).
fof(f20480,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20452,f14921]) ).
fof(f20481,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v4_group_1(sK8)
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20453,f14922]) ).
fof(f20508,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20480,f15887]) ).
fof(f20509,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ l1_group_1(sK8)
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20481,f14921]) ).
fof(f20535,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_1
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20508,f15867]) ).
fof(f20536,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| v3_struct_0(sK7)
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20509,f15887]) ).
fof(f20562,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_1
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20535,f14918]) ).
fof(f20563,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v3_group_1(sK7)
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_1
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20536,f15867]) ).
fof(f20589,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ l1_group_1(sK7)
| spl162_1
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20562,f14917]) ).
fof(f20590,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ v4_group_1(sK7)
| ~ l1_group_1(sK7)
| spl162_1
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20563,f14918]) ).
fof(f20614,plain,
( m4_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| spl162_1
| spl162_2
| ~ spl162_4
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20589,f15882]) ).
fof(f20615,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| ~ l1_group_1(sK7)
| spl162_1
| spl162_2
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20590,f14917]) ).
fof(f20632,plain,
( ~ m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_6 ),
inference(backward_subsumption_resolution,[],[f18808,f20614]) ).
fof(f20633,plain,
( m3_vectsp_8(k3_latsubgr(sK7,sK8,sK9),k11_group_4(sK7),k11_group_4(sK8))
| spl162_1
| spl162_2
| ~ spl162_4
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20615,f15882]) ).
fof(f20641,plain,
( $false
| spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_6 ),
inference(forward_subsumption_resolution,[],[f20633,f20632]) ).
fof(f20642,plain,
( spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_6 ),
inference(avatar_contradiction_clause,[],[f20641]) ).
cnf(s1,plain,
~ spl162_1,
inference(sat_conversion,[],[f15868]) ).
cnf(s2,plain,
~ spl162_2,
inference(sat_conversion,[],[f15873]) ).
cnf(s3,plain,
~ spl162_3,
inference(sat_conversion,[],[f15878]) ).
cnf(s4,plain,
spl162_4,
inference(sat_conversion,[],[f15883]) ).
cnf(s5,plain,
spl162_5,
inference(sat_conversion,[],[f15888]) ).
cnf(s6,plain,
spl162_6,
inference(sat_conversion,[],[f20078]) ).
cnf(s7,plain,
( spl162_1
| spl162_2
| spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_6 ),
inference(sat_conversion,[],[f20642]) ).
cnf(s8,plain,
spl162_1,
inference(rat,[],[s7,s6,s5,s4,s3,s2]) ).
cnf(s9,plain,
$false,
inference(rat,[],[s1,s8]) ).
fof(f20654,plain,
$false,
inference(avatar_sat_refutation,[],[s9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP653+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.35 % Computer : n004.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 27 10:30:39 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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
% 11.68/3.10 % (3311809)Detected formulas, will run a generic FOF schedule.
% 11.68/3.10 % (3311817)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4031034977:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 11.68/3.10 % (3311818)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3284482112:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 11.68/3.10 % (3311814)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=1987731175:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 11.68/3.10 % (3311815)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=1918238190:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 11.68/3.10 % (3311816)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=308917817:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 11.68/3.10 % (3311819)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4212174795:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 11.68/3.10 % (3311817)Refutation not found, incomplete strategy
% 11.68/3.10 % (3311817)------------------------------
% 11.68/3.10 % (3311817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/3.10 % (3311817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/3.10 % (3311817)CaDiCaL version: 2.1.3
% 11.68/3.10 % (3311817)Termination reason: Refutation not found, incomplete strategy
% 11.68/3.10 % (3311817)Time elapsed: 0.048 s
% 11.68/3.10 % (3311817)Peak memory usage: 108 MB
% 11.68/3.10 % (3311817)Instructions burned: 102 (million)
% 11.68/3.10 % (3311820)dis-21_1_sil=8000:lcm=predicate:random_seed=3197580698: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)
% 11.68/3.10 % (3311819)Instruction limit reached!
% 11.68/3.10 % (3311819)------------------------------
% 11.68/3.10 % (3311819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/3.10 % (3311819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/3.10 % (3311819)CaDiCaL version: 2.1.3
% 11.68/3.10 % (3311819)Termination reason: Instruction limit
% 11.68/3.10 % (3311819)Termination phase: Property scanning
% 11.68/3.10 % (3311819)Time elapsed: 0.067 s
% 11.68/3.10 % (3311819)Peak memory usage: 103 MB
% 11.68/3.10 % (3311819)Instructions burned: 141 (million)
% 11.68/3.10 % (3311818)Instruction limit reached!
% 11.68/3.10 % (3311818)------------------------------
% 11.68/3.10 % (3311818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/3.10 % (3311818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/3.10 % (3311818)CaDiCaL version: 2.1.3
% 11.68/3.10 % (3311818)Termination reason: Instruction limit
% 11.68/3.10 % (3311818)Termination phase: Preprocessing 3
% 11.68/3.10 % (3311818)Time elapsed: 0.100 s
% 11.68/3.10 % (3311818)Peak memory usage: 106 MB
% 11.68/3.10 % (3311818)Instructions burned: 119 (million)
% 11.68/3.10 % (3311820)Instruction limit reached!
% 11.68/3.10 % (3311820)------------------------------
% 11.68/3.10 % (3311820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/3.10 % (3311820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/3.10 % (3311820)CaDiCaL version: 2.1.3
% 11.68/3.10 % (3311820)Termination reason: Instruction limit
% 11.68/3.10 % (3311820)Termination phase: Preprocessing 1
% 11.68/3.10 % (3311820)Time elapsed: 0.099 s
% 11.68/3.10 % (3311820)Peak memory usage: 104 MB
% 11.68/3.10 % (3311820)Instructions burned: 129 (million)
% 11.68/3.10 % (3311817)------------------------------
% 11.68/3.10 % (3311817)------------------------------
% 11.68/3.10 % (3311828)lrs+10_1_sil=8000:sp=occurrence:random_seed=816261921:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 11.68/3.10 % (3311829)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3148038359:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 11.68/3.10 % (3311831)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=1190843427:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 11.68/3.10 % (3311830)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3921750184:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 12.74/3.27 % (3311829)Instruction limit reached!
% 12.74/3.27 % (3311829)------------------------------
% 12.74/3.27 % (3311829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311829)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311829)Termination reason: Instruction limit
% 12.74/3.27 % (3311829)Termination phase: Property scanning
% 12.74/3.27 % (3311829)Time elapsed: 0.066 s
% 12.74/3.27 % (3311829)Peak memory usage: 103 MB
% 12.74/3.27 % (3311829)Instructions burned: 157 (million)
% 12.74/3.27 % (3311831)Instruction limit reached!
% 12.74/3.27 % (3311831)------------------------------
% 12.74/3.27 % (3311831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311831)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311831)Termination reason: Instruction limit
% 12.74/3.27 % (3311831)Termination phase: SInE selection
% 12.74/3.27 % (3311831)Time elapsed: 0.066 s
% 12.74/3.27 % (3311831)Peak memory usage: 103 MB
% 12.74/3.27 % (3311831)Instructions burned: 248 (million)
% 12.74/3.27 % (3311837)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2590355276:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 12.74/3.27 % (3311828)Instruction limit reached!
% 12.74/3.27 % (3311828)------------------------------
% 12.74/3.27 % (3311828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311828)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311828)Termination reason: Instruction limit
% 12.74/3.27 % (3311828)Termination phase: Saturation
% 12.74/3.27 % (3311828)Time elapsed: 0.185 s
% 12.74/3.27 % (3311828)Peak memory usage: 112 MB
% 12.74/3.27 % (3311828)Instructions burned: 285 (million)
% 12.74/3.27 % (3311836)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4277082397:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 12.74/3.27 % (3311830)Instruction limit reached!
% 12.74/3.27 % (3311830)------------------------------
% 12.74/3.27 % (3311830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311830)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311830)Termination reason: Instruction limit
% 12.74/3.27 % (3311830)Termination phase: Saturation
% 12.74/3.27 % (3311830)Time elapsed: 0.212 s
% 12.74/3.27 % (3311830)Peak memory usage: 110 MB
% 12.74/3.27 % (3311830)Instructions burned: 325 (million)
% 12.74/3.27 % (3311839)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3809665703:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 12.74/3.27 % (3311841)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=979906949:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 12.74/3.27 % (3311836)Instruction limit reached!
% 12.74/3.27 % (3311836)------------------------------
% 12.74/3.27 % (3311836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311836)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311836)Termination reason: Instruction limit
% 12.74/3.27 % (3311836)Termination phase: Property scanning
% 12.74/3.27 % (3311836)Time elapsed: 0.192 s
% 12.74/3.27 % (3311836)Peak memory usage: 110 MB
% 12.74/3.27 % (3311836)Instructions burned: 295 (million)
% 12.74/3.27 % (3311839)Instruction limit reached!
% 12.74/3.27 % (3311839)------------------------------
% 12.74/3.27 % (3311839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311839)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311839)Termination reason: Instruction limit
% 12.74/3.27 % (3311839)Termination phase: Preprocessing 2
% 12.74/3.27 % (3311839)Time elapsed: 0.097 s
% 12.74/3.27 % (3311839)Peak memory usage: 106 MB
% 12.74/3.27 % (3311839)Instructions burned: 114 (million)
% 12.74/3.27 % (3311841)Instruction limit reached!
% 12.74/3.27 % (3311841)------------------------------
% 12.74/3.27 % (3311841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311841)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311841)Termination reason: Instruction limit
% 12.74/3.27 % (3311841)Termination phase: Preprocessing 2
% 12.74/3.27 % (3311841)Time elapsed: 0.105 s
% 12.74/3.27 % (3311841)Peak memory usage: 106 MB
% 12.74/3.27 % (3311841)Instructions burned: 128 (million)
% 12.74/3.27 % (3311845)lrs+10_1_sil=8000:sp=occurrence:random_seed=3626727278:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 12.74/3.27 % (3311844)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1838063282:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 12.74/3.27 % (3311844)Instruction limit reached!
% 12.74/3.27 % (3311844)------------------------------
% 12.74/3.27 % (3311844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311844)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311844)Termination reason: Instruction limit
% 12.74/3.27 % (3311844)Termination phase: Property scanning
% 12.74/3.27 % (3311844)Time elapsed: 0.050 s
% 12.74/3.27 % (3311844)Peak memory usage: 103 MB
% 12.74/3.27 % (3311844)Instructions burned: 115 (million)
% 12.74/3.27 % (3311846)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4030233397:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 12.74/3.27 % (3311849)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2069062240:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 12.74/3.27 % (3311846)Instruction limit reached!
% 12.74/3.27 % (3311846)------------------------------
% 12.74/3.27 % (3311846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311846)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311846)Termination reason: Instruction limit
% 12.74/3.27 % (3311846)Termination phase: Saturation
% 12.74/3.27 % (3311846)Time elapsed: 0.276 s
% 12.74/3.27 % (3311846)Peak memory usage: 110 MB
% 12.74/3.27 % (3311846)Instructions burned: 438 (million)
% 12.74/3.27 % (3311837)Instruction limit reached!
% 12.74/3.27 % (3311837)------------------------------
% 12.74/3.27 % (3311837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311837)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311837)Termination reason: Instruction limit
% 12.74/3.27 % (3311837)Termination phase: Saturation
% 12.74/3.27 % (3311837)Time elapsed: 0.797 s
% 12.74/3.27 % (3311837)Peak memory usage: 222 MB
% 12.74/3.27 % (3311837)Instructions burned: 2350 (million)
% 12.74/3.27 % (3311852)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2804123361:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 12.74/3.27 % (3311845)Instruction limit reached!
% 12.74/3.27 % (3311845)------------------------------
% 12.74/3.27 % (3311845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311845)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311845)Termination reason: Instruction limit
% 12.74/3.27 % (3311845)Termination phase: Saturation
% 12.74/3.27 % (3311845)Time elapsed: 0.514 s
% 12.74/3.27 % (3311845)Peak memory usage: 123 MB
% 12.74/3.27 % (3311845)Instructions burned: 908 (million)
% 12.74/3.27 % (3311853)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1854190253:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 12.74/3.27 % (3311816)First to succeed.
% 12.74/3.27 % (3311816)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3311809"
% 12.74/3.27 % (3311852)Instruction limit reached!
% 12.74/3.27 % (3311852)------------------------------
% 12.74/3.27 % (3311852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311852)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311852)Termination reason: Instruction limit
% 12.74/3.27 % (3311852)Termination phase: Property scanning
% 12.74/3.27 % (3311852)Time elapsed: 0.110 s
% 12.74/3.27 % (3311852)Peak memory usage: 107 MB
% 12.74/3.27 % (3311852)Instructions burned: 135 (million)
% 12.74/3.27 % (3311855)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1798741577:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 12.74/3.27 % (3311857)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=1309509052:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 12.74/3.27 % (3311853)Instruction limit reached!
% 12.74/3.27 % (3311853)------------------------------
% 12.74/3.27 % (3311853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.74/3.27 % (3311853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.74/3.27 % (3311853)CaDiCaL version: 2.1.3
% 12.74/3.27 % (3311853)Termination reason: Instruction limit
% 12.74/3.27 % (3311853)Termination phase: Property scanning
% 12.74/3.27 % (3311853)Time elapsed: 0.256 s
% 12.74/3.27 % (3311853)Peak memory usage: 128 MB
% 12.74/3.27 % (3311853)Instructions burned: 593 (million)
% 12.74/3.27 % (3311816)Refutation found. Thanks to Tanya!
% 12.74/3.27 % SZS status Theorem for theBenchmark
% 12.74/3.27 % SZS output start Proof for theBenchmark
% See solution above
% 13.50/3.47 % (3311816)------------------------------
% 13.50/3.47 % (3311816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/3.47 % (3311816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/3.47 % (3311816)CaDiCaL version: 2.1.3
% 13.50/3.47 % (3311816)Termination reason: Refutation
% 13.50/3.47 % (3311816)Time elapsed: 1.307 s
% 13.50/3.47 % (3311816)Peak memory usage: 164 MB
% 13.50/3.47 % (3311816)Instructions burned: 2092 (million)
% 13.50/3.47 % (3311816)------------------------------
% 13.50/3.47 % (3311816)------------------------------
% 13.50/3.47 % (3311809)Success in time 2.44 s
% 13.50/3.47 % Vampire exiting
%------------------------------------------------------------------------------