%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP653+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:21 AM UTC 2026
% Result : Theorem 8.84s 4.90s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 18
% Syntax : Number of formulae : 169 ( 39 unt; 11 def)
% Number of atoms : 1103 ( 0 equ)
% Maximal formula atoms : 16 ( 6 avg)
% Number of connectives : 1534 ( 600 ~; 672 |; 215 &)
% ( 14 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 36 ( 35 usr; 12 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(f22885,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/sandbox/benchmark/theBenchmark.p',fc1_group_4) ).
fof(f23007,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/sandbox/benchmark/theBenchmark.p',dt_k11_group_4) ).
fof(f36466,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/sandbox/benchmark/theBenchmark.p',t11_vectsp_8) ).
fof(f36478,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/sandbox/benchmark/theBenchmark.p',dt_m4_vectsp_8) ).
fof(f36528,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/sandbox/benchmark/theBenchmark.p',t36_latsubgr) ).
fof(f36529,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/sandbox/benchmark/theBenchmark.p',t37_latsubgr) ).
fof(f36530,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/sandbox/benchmark/theBenchmark.p',t38_latsubgr) ).
fof(f36531,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)],[f36530]) ).
fof(f36546,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,[],[f22885]) ).
fof(f36561,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,[],[f36546]) ).
fof(f36562,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,[],[f36561]) ).
fof(f36563,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,[],[f36562]) ).
fof(f36564,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,[],[f36563]) ).
fof(f36565,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,[],[f36564]) ).
fof(f36566,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,[],[f36565]) ).
fof(f36567,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,[],[f36566]) ).
fof(f36568,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,[],[f36567]) ).
fof(f36569,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,[],[f36568]) ).
fof(f36570,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,[],[f23007]) ).
fof(f36653,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,[],[f36528]) ).
fof(f36654,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,[],[f36653]) ).
fof(f36655,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,[],[f36529]) ).
fof(f36656,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,[],[f36655]) ).
fof(f36657,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,[],[f36531]) ).
fof(f36658,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,[],[f36657]) ).
fof(f36707,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,[],[f36570]) ).
fof(f36708,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,[],[f36707]) ).
fof(f36715,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,[],[f36569]) ).
fof(f36716,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,[],[f36715]) ).
fof(f37288,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,[],[f36466]) ).
fof(f37289,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,[],[f37288]) ).
fof(f37294,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,[],[f36478]) ).
fof(f37295,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,[],[f37294]) ).
fof(f37327,plain,
( ~ m1_lattice4(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
& v2_funct_1(sK11)
& v1_funct_1(sK11)
& v1_funct_2(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
& v1_group_6(sK11,sK9,sK10)
& m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
& ~ v3_struct_0(sK10)
& v3_group_1(sK10)
& v4_group_1(sK10)
& l1_group_1(sK10)
& ~ v3_struct_0(sK9)
& v3_group_1(sK9)
& v4_group_1(sK9)
& l1_group_1(sK9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X2,sK11)],[f36658]) ).
fof(f37538,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,[],[f37289]) ).
fof(f37539,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,[],[f37538]) ).
fof(f37612,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,[],[f36654]) ).
fof(f37613,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,[],[f36656]) ).
fof(f37614,plain,
l1_group_1(sK9),
inference(cnf_transformation,[],[f37327]) ).
fof(f37615,plain,
v4_group_1(sK9),
inference(cnf_transformation,[],[f37327]) ).
fof(f37616,plain,
v3_group_1(sK9),
inference(cnf_transformation,[],[f37327]) ).
fof(f37617,plain,
~ v3_struct_0(sK9),
inference(cnf_transformation,[],[f37327]) ).
fof(f37618,plain,
l1_group_1(sK10),
inference(cnf_transformation,[],[f37327]) ).
fof(f37619,plain,
v4_group_1(sK10),
inference(cnf_transformation,[],[f37327]) ).
fof(f37620,plain,
v3_group_1(sK10),
inference(cnf_transformation,[],[f37327]) ).
fof(f37621,plain,
~ v3_struct_0(sK10),
inference(cnf_transformation,[],[f37327]) ).
fof(f37622,plain,
m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10)),
inference(cnf_transformation,[],[f37327]) ).
fof(f37623,plain,
v1_group_6(sK11,sK9,sK10),
inference(cnf_transformation,[],[f37327]) ).
fof(f37624,plain,
v1_funct_2(sK11,u1_struct_0(sK9),u1_struct_0(sK10)),
inference(cnf_transformation,[],[f37327]) ).
fof(f37625,plain,
v1_funct_1(sK11),
inference(cnf_transformation,[],[f37327]) ).
fof(f37626,plain,
v2_funct_1(sK11),
inference(cnf_transformation,[],[f37327]) ).
fof(f37627,plain,
~ m1_lattice4(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10)),
inference(cnf_transformation,[],[f37327]) ).
fof(f37705,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,[],[f36708]) ).
fof(f37711,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,[],[f36716]) ).
fof(f37712,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,[],[f36716]) ).
fof(f38546,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,[],[f37539]) ).
fof(f38552,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,[],[f37295]) ).
fof(f38553,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,[],[f37295]) ).
fof(f38554,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,[],[f37295]) ).
fof(f38883,definition,
( spl203_1
<=> v3_struct_0(sK10) ),
introduced(definition,[new_symbols(definition,[spl203_1])],[avatar_definition]) ).
fof(f38885,plain,
( ~ v3_struct_0(sK10)
| spl203_1 ),
inference(avatar_component_clause,[],[f38883]) ).
fof(f38886,plain,
~ spl203_1,
inference(avatar_split_clause,[],[f37621,f38883]) ).
fof(f38888,definition,
( spl203_2
<=> v3_struct_0(sK9) ),
introduced(definition,[new_symbols(definition,[spl203_2])],[avatar_definition]) ).
fof(f38890,plain,
( ~ v3_struct_0(sK9)
| spl203_2 ),
inference(avatar_component_clause,[],[f38888]) ).
fof(f38891,plain,
~ spl203_2,
inference(avatar_split_clause,[],[f37617,f38888]) ).
fof(f38893,definition,
( spl203_3
<=> m1_lattice4(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10)) ),
introduced(definition,[new_symbols(definition,[spl203_3])],[avatar_definition]) ).
fof(f38895,plain,
( ~ m1_lattice4(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| spl203_3 ),
inference(avatar_component_clause,[],[f38893]) ).
fof(f38896,plain,
~ spl203_3,
inference(avatar_split_clause,[],[f37627,f38893]) ).
fof(f38898,definition,
( spl203_4
<=> l1_group_1(sK9) ),
introduced(definition,[new_symbols(definition,[spl203_4])],[avatar_definition]) ).
fof(f38900,plain,
( l1_group_1(sK9)
| ~ spl203_4 ),
inference(avatar_component_clause,[],[f38898]) ).
fof(f38901,plain,
spl203_4,
inference(avatar_split_clause,[],[f37614,f38898]) ).
fof(f38903,definition,
( spl203_5
<=> l1_group_1(sK10) ),
introduced(definition,[new_symbols(definition,[spl203_5])],[avatar_definition]) ).
fof(f38905,plain,
( l1_group_1(sK10)
| ~ spl203_5 ),
inference(avatar_component_clause,[],[f38903]) ).
fof(f38906,plain,
spl203_5,
inference(avatar_split_clause,[],[f37618,f38903]) ).
fof(f38908,definition,
( spl203_6
<=> v2_funct_1(sK11) ),
introduced(definition,[new_symbols(definition,[spl203_6])],[avatar_definition]) ).
fof(f38910,plain,
( v2_funct_1(sK11)
| ~ spl203_6 ),
inference(avatar_component_clause,[],[f38908]) ).
fof(f38911,plain,
spl203_6,
inference(avatar_split_clause,[],[f37626,f38908]) ).
fof(f38915,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v1_funct_1(k3_latsubgr(sK9,sK10,sK11))
| ~ v1_funct_2(k3_latsubgr(sK9,sK10,sK11),u1_struct_0(k11_group_4(sK9)),u1_struct_0(k11_group_4(sK10)))
| ~ m2_relset_1(k3_latsubgr(sK9,sK10,sK11),u1_struct_0(k11_group_4(sK9)),u1_struct_0(k11_group_4(sK10)))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK9))
| ~ v10_lattices(k11_group_4(sK9))
| ~ l3_lattices(k11_group_4(sK9))
| spl203_3 ),
inference(resolution,[],[f38895,f38546]) ).
fof(f38926,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v1_funct_2(k3_latsubgr(sK9,sK10,sK11),u1_struct_0(k11_group_4(sK9)),u1_struct_0(k11_group_4(sK10)))
| ~ m2_relset_1(k3_latsubgr(sK9,sK10,sK11),u1_struct_0(k11_group_4(sK9)),u1_struct_0(k11_group_4(sK10)))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK9))
| ~ v10_lattices(k11_group_4(sK9))
| ~ l3_lattices(k11_group_4(sK9))
| spl203_3 ),
inference(forward_subsumption_resolution,[],[f38915,f38554]) ).
fof(f38932,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m2_relset_1(k3_latsubgr(sK9,sK10,sK11),u1_struct_0(k11_group_4(sK9)),u1_struct_0(k11_group_4(sK10)))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK9))
| ~ v10_lattices(k11_group_4(sK9))
| ~ l3_lattices(k11_group_4(sK9))
| spl203_3 ),
inference(forward_subsumption_resolution,[],[f38926,f38553]) ).
fof(f38938,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK9))
| ~ v10_lattices(k11_group_4(sK9))
| ~ l3_lattices(k11_group_4(sK9))
| spl203_3 ),
inference(forward_subsumption_resolution,[],[f38932,f38552]) ).
fof(f38980,definition,
( spl203_7
<=> v4_group_1(sK9) ),
introduced(definition,[new_symbols(definition,[spl203_7])],[avatar_definition]) ).
fof(f38982,plain,
( v4_group_1(sK9)
| ~ spl203_7 ),
inference(avatar_component_clause,[],[f38980]) ).
fof(f38983,plain,
spl203_7,
inference(avatar_split_clause,[],[f37615,f38980]) ).
fof(f39066,plain,
( l3_lattices(k11_group_4(sK9))
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ spl203_4 ),
inference(resolution,[],[f38900,f37705]) ).
fof(f39072,plain,
( v10_lattices(k11_group_4(sK9))
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ spl203_4 ),
inference(resolution,[],[f38900,f37711]) ).
fof(f39073,plain,
( ~ v3_struct_0(k11_group_4(sK9))
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ spl203_4 ),
inference(resolution,[],[f38900,f37712]) ).
fof(f39663,plain,
( ~ v3_struct_0(k11_group_4(sK9))
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| spl203_2
| ~ spl203_4 ),
inference(forward_subsumption_resolution,[],[f39073,f38890]) ).
fof(f39664,plain,
( v10_lattices(k11_group_4(sK9))
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| spl203_2
| ~ spl203_4 ),
inference(forward_subsumption_resolution,[],[f39072,f38890]) ).
fof(f39670,plain,
( l3_lattices(k11_group_4(sK9))
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| spl203_2
| ~ spl203_4 ),
inference(forward_subsumption_resolution,[],[f39066,f38890]) ).
fof(f40010,plain,
( ~ v3_struct_0(k11_group_4(sK9))
| ~ v4_group_1(sK9)
| spl203_2
| ~ spl203_4 ),
inference(forward_subsumption_resolution,[],[f39663,f37616]) ).
fof(f40011,plain,
( v10_lattices(k11_group_4(sK9))
| ~ v4_group_1(sK9)
| spl203_2
| ~ spl203_4 ),
inference(forward_subsumption_resolution,[],[f39664,f37616]) ).
fof(f40017,plain,
( l3_lattices(k11_group_4(sK9))
| ~ v4_group_1(sK9)
| spl203_2
| ~ spl203_4 ),
inference(forward_subsumption_resolution,[],[f39670,f37616]) ).
fof(f40345,plain,
( ~ v3_struct_0(k11_group_4(sK9))
| spl203_2
| ~ spl203_4
| ~ spl203_7 ),
inference(forward_subsumption_resolution,[],[f40010,f38982]) ).
fof(f40346,plain,
( v10_lattices(k11_group_4(sK9))
| spl203_2
| ~ spl203_4
| ~ spl203_7 ),
inference(forward_subsumption_resolution,[],[f40011,f38982]) ).
fof(f40352,plain,
( l3_lattices(k11_group_4(sK9))
| spl203_2
| ~ spl203_4
| ~ spl203_7 ),
inference(forward_subsumption_resolution,[],[f40017,f38982]) ).
fof(f40440,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK9))
| ~ l3_lattices(k11_group_4(sK9))
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_7 ),
inference(backward_subsumption_resolution,[],[f38938,f40345]) ).
fof(f40465,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK9))
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_7 ),
inference(forward_subsumption_resolution,[],[f40440,f40346]) ).
fof(f40483,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_7 ),
inference(forward_subsumption_resolution,[],[f40465,f40352]) ).
fof(f40509,definition,
( spl203_8
<=> v4_group_1(sK10) ),
introduced(definition,[new_symbols(definition,[spl203_8])],[avatar_definition]) ).
fof(f40511,plain,
( v4_group_1(sK10)
| ~ spl203_8 ),
inference(avatar_component_clause,[],[f40509]) ).
fof(f40512,plain,
spl203_8,
inference(avatar_split_clause,[],[f37619,f40509]) ).
fof(f40595,plain,
( l3_lattices(k11_group_4(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ spl203_5 ),
inference(resolution,[],[f38905,f37705]) ).
fof(f40601,plain,
( v10_lattices(k11_group_4(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ spl203_5 ),
inference(resolution,[],[f38905,f37711]) ).
fof(f40602,plain,
( ~ v3_struct_0(k11_group_4(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ spl203_5 ),
inference(resolution,[],[f38905,f37712]) ).
fof(f41192,plain,
( ~ v3_struct_0(k11_group_4(sK10))
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| spl203_1
| ~ spl203_5 ),
inference(forward_subsumption_resolution,[],[f40602,f38885]) ).
fof(f41193,plain,
( v10_lattices(k11_group_4(sK10))
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| spl203_1
| ~ spl203_5 ),
inference(forward_subsumption_resolution,[],[f40601,f38885]) ).
fof(f41199,plain,
( l3_lattices(k11_group_4(sK10))
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| spl203_1
| ~ spl203_5 ),
inference(forward_subsumption_resolution,[],[f40595,f38885]) ).
fof(f41539,plain,
( ~ v3_struct_0(k11_group_4(sK10))
| ~ v4_group_1(sK10)
| spl203_1
| ~ spl203_5 ),
inference(forward_subsumption_resolution,[],[f41192,f37620]) ).
fof(f41540,plain,
( v10_lattices(k11_group_4(sK10))
| ~ v4_group_1(sK10)
| spl203_1
| ~ spl203_5 ),
inference(forward_subsumption_resolution,[],[f41193,f37620]) ).
fof(f41546,plain,
( l3_lattices(k11_group_4(sK10))
| ~ v4_group_1(sK10)
| spl203_1
| ~ spl203_5 ),
inference(forward_subsumption_resolution,[],[f41199,f37620]) ).
fof(f41874,plain,
( ~ v3_struct_0(k11_group_4(sK10))
| spl203_1
| ~ spl203_5
| ~ spl203_8 ),
inference(forward_subsumption_resolution,[],[f41539,f40511]) ).
fof(f41875,plain,
( v10_lattices(k11_group_4(sK10))
| spl203_1
| ~ spl203_5
| ~ spl203_8 ),
inference(forward_subsumption_resolution,[],[f41540,f40511]) ).
fof(f41881,plain,
( l3_lattices(k11_group_4(sK10))
| spl203_1
| ~ spl203_5
| ~ spl203_8 ),
inference(forward_subsumption_resolution,[],[f41546,f40511]) ).
fof(f41972,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v10_lattices(k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_7
| ~ spl203_8 ),
inference(backward_subsumption_resolution,[],[f40483,f41874]) ).
fof(f41997,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ l3_lattices(k11_group_4(sK10))
| spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_7
| ~ spl203_8 ),
inference(forward_subsumption_resolution,[],[f41972,f41875]) ).
fof(f42015,plain,
( ~ m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_7
| ~ spl203_8 ),
inference(forward_subsumption_resolution,[],[f41997,f41881]) ).
fof(f42036,definition,
( spl203_9
<=> v3_group_1(sK9) ),
introduced(definition,[new_symbols(definition,[spl203_9])],[avatar_definition]) ).
fof(f42038,plain,
( v3_group_1(sK9)
| ~ spl203_9 ),
inference(avatar_component_clause,[],[f42036]) ).
fof(f42039,plain,
spl203_9,
inference(avatar_split_clause,[],[f37616,f42036]) ).
fof(f42041,definition,
( spl203_10
<=> v3_group_1(sK10) ),
introduced(definition,[new_symbols(definition,[spl203_10])],[avatar_definition]) ).
fof(f42043,plain,
( v3_group_1(sK10)
| ~ spl203_10 ),
inference(avatar_component_clause,[],[f42041]) ).
fof(f42044,plain,
spl203_10,
inference(avatar_split_clause,[],[f37620,f42041]) ).
fof(f42046,definition,
( spl203_11
<=> v1_funct_2(sK11,u1_struct_0(sK9),u1_struct_0(sK10)) ),
introduced(definition,[new_symbols(definition,[spl203_11])],[avatar_definition]) ).
fof(f42048,plain,
( v1_funct_2(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| ~ spl203_11 ),
inference(avatar_component_clause,[],[f42046]) ).
fof(f42049,plain,
spl203_11,
inference(avatar_split_clause,[],[f37624,f42046]) ).
fof(f42067,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v2_funct_1(sK11)
| ~ v1_funct_1(sK11)
| ~ v1_group_6(sK11,sK9,sK10)
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_11 ),
inference(resolution,[],[f42048,f37612]) ).
fof(f42068,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v1_funct_1(sK11)
| ~ v1_group_6(sK11,sK9,sK10)
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_11 ),
inference(resolution,[],[f42048,f37613]) ).
fof(f42255,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v1_group_6(sK11,sK9,sK10)
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42068,f37625]) ).
fof(f42256,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v1_funct_1(sK11)
| ~ v1_group_6(sK11,sK9,sK10)
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_6
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42067,f38910]) ).
fof(f42356,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42255,f37623]) ).
fof(f42357,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v1_group_6(sK11,sK9,sK10)
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_6
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42256,f37625]) ).
fof(f42411,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42356,f37622]) ).
fof(f42412,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ m2_relset_1(sK11,u1_struct_0(sK9),u1_struct_0(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_6
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42357,f37623]) ).
fof(f42461,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42411,f38885]) ).
fof(f42462,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(sK10)
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| ~ spl203_6
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42412,f37622]) ).
fof(f42495,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42461,f42043]) ).
fof(f42496,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v3_group_1(sK10)
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_6
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42462,f38885]) ).
fof(f42529,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_8
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42495,f40511]) ).
fof(f42530,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v4_group_1(sK10)
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_6
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42496,f42043]) ).
fof(f42563,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_5
| ~ spl203_8
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42529,f38905]) ).
fof(f42564,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ l1_group_1(sK10)
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_6
| ~ spl203_8
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42530,f40511]) ).
fof(f42596,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| spl203_2
| ~ spl203_5
| ~ spl203_8
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42563,f38890]) ).
fof(f42597,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| v3_struct_0(sK9)
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| ~ spl203_5
| ~ spl203_6
| ~ spl203_8
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42564,f38905]) ).
fof(f42629,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| spl203_2
| ~ spl203_5
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42596,f42038]) ).
fof(f42630,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v3_group_1(sK9)
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| spl203_2
| ~ spl203_5
| ~ spl203_6
| ~ spl203_8
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42597,f38890]) ).
fof(f42662,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ l1_group_1(sK9)
| spl203_1
| spl203_2
| ~ spl203_5
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42629,f38982]) ).
fof(f42663,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ v4_group_1(sK9)
| ~ l1_group_1(sK9)
| spl203_1
| spl203_2
| ~ spl203_5
| ~ spl203_6
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42630,f42038]) ).
fof(f42693,plain,
( m4_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| spl203_1
| spl203_2
| ~ spl203_4
| ~ spl203_5
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42662,f38900]) ).
fof(f42694,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| ~ l1_group_1(sK9)
| spl203_1
| spl203_2
| ~ spl203_5
| ~ spl203_6
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42663,f38982]) ).
fof(f42711,plain,
( ~ m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(backward_subsumption_resolution,[],[f42015,f42693]) ).
fof(f42712,plain,
( m3_vectsp_8(k3_latsubgr(sK9,sK10,sK11),k11_group_4(sK9),k11_group_4(sK10))
| spl203_1
| spl203_2
| ~ spl203_4
| ~ spl203_5
| ~ spl203_6
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42694,f38900]) ).
fof(f42720,plain,
( $false
| spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_6
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(forward_subsumption_resolution,[],[f42712,f42711]) ).
fof(f42721,plain,
( spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_6
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(avatar_contradiction_clause,[],[f42720]) ).
cnf(s1,plain,
~ spl203_1,
inference(sat_conversion,[],[f38886]) ).
cnf(s2,plain,
~ spl203_2,
inference(sat_conversion,[],[f38891]) ).
cnf(s3,plain,
~ spl203_3,
inference(sat_conversion,[],[f38896]) ).
cnf(s4,plain,
spl203_4,
inference(sat_conversion,[],[f38901]) ).
cnf(s5,plain,
spl203_5,
inference(sat_conversion,[],[f38906]) ).
cnf(s6,plain,
spl203_6,
inference(sat_conversion,[],[f38911]) ).
cnf(s7,plain,
spl203_7,
inference(sat_conversion,[],[f38983]) ).
cnf(s8,plain,
spl203_8,
inference(sat_conversion,[],[f40512]) ).
cnf(s9,plain,
spl203_9,
inference(sat_conversion,[],[f42039]) ).
cnf(s10,plain,
spl203_10,
inference(sat_conversion,[],[f42044]) ).
cnf(s11,plain,
spl203_11,
inference(sat_conversion,[],[f42049]) ).
cnf(s12,plain,
( spl203_1
| spl203_2
| spl203_3
| ~ spl203_4
| ~ spl203_5
| ~ spl203_6
| ~ spl203_7
| ~ spl203_8
| ~ spl203_9
| ~ spl203_10
| ~ spl203_11 ),
inference(sat_conversion,[],[f42721]) ).
cnf(s13,plain,
spl203_1,
inference(rat,[],[s12,s11,s10,s9,s8,s7,s6,s5,s4,s3,s2]) ).
cnf(s14,plain,
$false,
inference(rat,[],[s1,s13]) ).
fof(f42733,plain,
$false,
inference(avatar_sat_refutation,[],[s14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP653+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:29:17 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 Running first-order theorem proving
% 0.12/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.84/4.90 % (1216292)Detected formulas, will run a generic FOF schedule.
% 8.84/4.90 % (1216301)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=404434654:i=119:av=off:ss=axioms_2976 on theBenchmark for (2976ds/119Mi)
% 8.84/4.90 % (1216299)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=942412462:i=141695:sd=1:nm=32:gsp=on:ss=included_2976 on theBenchmark for (2976ds/141695Mi)
% 8.84/4.90 % (1216297)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=895783297:i=141193_2976 on theBenchmark for (2976ds/141193Mi)
% 8.84/4.90 % (1216298)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=3327474092:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2976 on theBenchmark for (2976ds/134677Mi)
% 8.84/4.90 % (1216300)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3248771427:i=109:sd=1:ins=1:gsp=on:ss=axioms_2976 on theBenchmark for (2976ds/109Mi)
% 8.84/4.90 % (1216302)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=679411236:s2a=on:i=139:gtg=position_2976 on theBenchmark for (2976ds/139Mi)
% 8.84/4.90 % (1216303)dis-21_1_sil=8000:lcm=predicate:random_seed=3312759767:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2976 on theBenchmark for (2976ds/129Mi)
% 8.84/4.90 % (1216301)Instruction limit reached!
% 8.84/4.90 % (1216301)------------------------------
% 8.84/4.90 % (1216301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216301)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216301)Termination reason: Instruction limit
% 8.84/4.90 % (1216301)Termination phase: SInE selection
% 8.84/4.90 % (1216301)Time elapsed: 0.056 s
% 8.84/4.90 % (1216301)Peak memory usage: 139 MB
% 8.84/4.90 % (1216301)Instructions burned: 121 (million)
% 8.84/4.90 % (1216302)Instruction limit reached!
% 8.84/4.90 % (1216302)------------------------------
% 8.84/4.90 % (1216302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216302)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216302)Termination reason: Instruction limit
% 8.84/4.90 % (1216302)Termination phase: Property scanning
% 8.84/4.90 % (1216302)Time elapsed: 0.063 s
% 8.84/4.90 % (1216302)Peak memory usage: 139 MB
% 8.84/4.90 % (1216302)Instructions burned: 141 (million)
% 8.84/4.90 % (1216300)Instruction limit reached!
% 8.84/4.90 % (1216300)------------------------------
% 8.84/4.90 % (1216300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216300)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216300)Termination reason: Instruction limit
% 8.84/4.90 % (1216300)Termination phase: SInE selection
% 8.84/4.90 % (1216300)Time elapsed: 0.084 s
% 8.84/4.90 % (1216300)Peak memory usage: 139 MB
% 8.84/4.90 % (1216300)Instructions burned: 109 (million)
% 8.84/4.90 % (1216311)lrs+10_1_sil=8000:sp=occurrence:random_seed=3733813089:i=285:sd=3:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/285Mi)
% 8.84/4.90 % (1216303)Instruction limit reached!
% 8.84/4.90 % (1216303)------------------------------
% 8.84/4.90 % (1216303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216303)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216303)Termination reason: Instruction limit
% 8.84/4.90 % (1216303)Termination phase: SInE selection
% 8.84/4.90 % (1216303)Time elapsed: 0.100 s
% 8.84/4.90 % (1216303)Peak memory usage: 139 MB
% 8.84/4.90 % (1216303)Instructions burned: 129 (million)
% 8.84/4.90 % (1216313)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2523376242:i=325:sd=1:ss=axioms:sgt=32_2974 on theBenchmark for (2974ds/325Mi)
% 8.84/4.90 % (1216312)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4270390895:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/157Mi)
% 8.84/4.90 % (1216315)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=444257080:s2a=on:i=248:s2at=1.23:gtg=position_2973 on theBenchmark for (2973ds/248Mi)
% 8.84/4.90 % (1216311)Instruction limit reached!
% 8.84/4.90 % (1216311)------------------------------
% 8.84/4.90 % (1216311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216311)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216311)Termination reason: Instruction limit
% 8.84/4.90 % (1216311)Termination phase: Preprocessing 3
% 8.84/4.90 % (1216311)Time elapsed: 0.136 s
% 8.84/4.90 % (1216311)Peak memory usage: 142 MB
% 8.84/4.90 % (1216311)Instructions burned: 286 (million)
% 8.84/4.90 % (1216312)Instruction limit reached!
% 8.84/4.90 % (1216312)------------------------------
% 8.84/4.90 % (1216312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216312)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216312)Termination reason: Instruction limit
% 8.84/4.90 % (1216312)Termination phase: Property scanning
% 8.84/4.90 % (1216312)Time elapsed: 0.072 s
% 8.84/4.90 % (1216312)Peak memory usage: 139 MB
% 8.84/4.90 % (1216312)Instructions burned: 159 (million)
% 8.84/4.90 % (1216319)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2066214824:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2972 on theBenchmark for (2972ds/294Mi)
% 8.84/4.90 % (1216315)Instruction limit reached!
% 8.84/4.90 % (1216315)------------------------------
% 8.84/4.90 % (1216315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216315)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216315)Termination reason: Instruction limit
% 8.84/4.90 % (1216315)Termination phase: Property scanning
% 8.84/4.90 % (1216315)Time elapsed: 0.110 s
% 8.84/4.90 % (1216315)Peak memory usage: 139 MB
% 8.84/4.90 % (1216315)Instructions burned: 250 (million)
% 8.84/4.90 % (1216320)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1786960983:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 8.84/4.90 % (1216319)Instruction limit reached!
% 8.84/4.90 % (1216319)------------------------------
% 8.84/4.90 % (1216319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216319)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216319)Termination reason: Instruction limit
% 8.84/4.90 % (1216319)Termination phase: SInE selection
% 8.84/4.90 % (1216319)Time elapsed: 0.106 s
% 8.84/4.90 % (1216319)Peak memory usage: 140 MB
% 8.84/4.90 % (1216319)Instructions burned: 297 (million)
% 8.84/4.90 % (1216313)Instruction limit reached!
% 8.84/4.90 % (1216313)------------------------------
% 8.84/4.90 % (1216313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216313)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216313)Termination reason: Instruction limit
% 8.84/4.90 % (1216313)Termination phase: Saturation
% 8.84/4.90 % (1216313)Time elapsed: 0.251 s
% 8.84/4.90 % (1216313)Peak memory usage: 145 MB
% 8.84/4.90 % (1216313)Instructions burned: 325 (million)
% 8.84/4.90 % (1216322)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=755008266:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 8.84/4.90 % (1216324)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1818076024:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 8.84/4.90 % (1216322)Instruction limit reached!
% 8.84/4.90 % (1216322)------------------------------
% 8.84/4.90 % (1216322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216322)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216322)Termination reason: Instruction limit
% 8.84/4.90 % (1216322)Termination phase: SInE selection
% 8.84/4.90 % (1216322)Time elapsed: 0.092 s
% 8.84/4.90 % (1216322)Peak memory usage: 139 MB
% 8.84/4.90 % (1216322)Instructions burned: 114 (million)
% 8.84/4.90 % (1216324)Instruction limit reached!
% 8.84/4.90 % (1216324)------------------------------
% 8.84/4.90 % (1216324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216324)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216324)Termination reason: Instruction limit
% 8.84/4.90 % (1216324)Termination phase: Preprocessing 1
% 8.84/4.90 % (1216324)Time elapsed: 0.056 s
% 8.84/4.90 % (1216324)Peak memory usage: 140 MB
% 8.84/4.90 % (1216324)Instructions burned: 129 (million)
% 8.84/4.90 % (1216325)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1821164771:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 8.84/4.90 % (1216325)Instruction limit reached!
% 8.84/4.90 % (1216325)------------------------------
% 8.84/4.90 % (1216325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216325)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216325)Termination reason: Instruction limit
% 8.84/4.90 % (1216325)Termination phase: Property scanning
% 8.84/4.90 % (1216325)Time elapsed: 0.053 s
% 8.84/4.90 % (1216325)Peak memory usage: 139 MB
% 8.84/4.90 % (1216325)Instructions burned: 116 (million)
% 8.84/4.90 % (1216330)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2936425920:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 8.84/4.90 % (1216328)lrs+10_1_sil=8000:sp=occurrence:random_seed=4145462766:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 8.84/4.90 % (1216331)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1533742913:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 8.84/4.90 % (1216330)Refutation not found, incomplete strategy
% 8.84/4.90 % (1216330)------------------------------
% 8.84/4.90 % (1216330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216330)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216330)Termination reason: Refutation not found, incomplete strategy
% 8.84/4.90 % (1216330)Time elapsed: 0.160 s
% 8.84/4.90 % (1216330)Peak memory usage: 146 MB
% 8.84/4.90 % (1216330)Instructions burned: 373 (million)
% 8.84/4.90 % (1216330)------------------------------
% 8.84/4.90 % (1216330)------------------------------
% 8.84/4.90 % (1216335)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=420800793:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 8.84/4.90 % (1216335)Instruction limit reached!
% 8.84/4.90 % (1216335)------------------------------
% 8.84/4.90 % (1216335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216335)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216335)Termination reason: Instruction limit
% 8.84/4.90 % (1216335)Termination phase: SInE selection
% 8.84/4.90 % (1216335)Time elapsed: 0.099 s
% 8.84/4.90 % (1216335)Peak memory usage: 139 MB
% 8.84/4.90 % (1216335)Instructions burned: 135 (million)
% 8.84/4.90 % (1216299)First to succeed.
% 8.84/4.90 % (1216328)Instruction limit reached!
% 8.84/4.90 % (1216328)------------------------------
% 8.84/4.90 % (1216328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.84/4.90 % (1216328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/4.90 % (1216328)CaDiCaL version: 2.1.3
% 8.84/4.90 % (1216328)Termination reason: Instruction limit
% 8.84/4.90 % (1216328)Termination phase: Property scanning
% 8.84/4.90 % (1216328)Time elapsed: 0.634 s
% 8.84/4.90 % (1216328)Peak memory usage: 163 MB
% 8.84/4.90 % (1216328)Instructions burned: 909 (million)
% 8.84/4.90 % (1216299)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1216292"
% 8.84/4.90 % (1216337)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3574653346:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 8.84/4.90 % (1216338)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1609615206:st=3:i=13193:sd=3:ss=axioms_2961 on theBenchmark for (2961ds/13193Mi)
% 8.84/4.90 % (1216299)Refutation found. Thanks to Tanya!
% 8.84/4.90 % SZS status Theorem for theBenchmark
% 8.84/4.90 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/5.15 % (1216299)------------------------------
% 0.17/5.15 % (1216299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/5.15 % (1216299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/5.15 % (1216299)CaDiCaL version: 2.1.3
% 0.17/5.15 % (1216299)Termination reason: Refutation
% 0.17/5.15 % (1216299)Time elapsed: 1.373 s
% 0.17/5.15 % (1216299)Peak memory usage: 207 MB
% 0.17/5.15 % (1216299)Instructions burned: 2484 (million)
% 0.17/5.15 % (1216299)------------------------------
% 0.17/5.15 % (1216299)------------------------------
% 0.17/5.15 % (1216292)Success in time 4.059 s
% 0.17/5.15 % Vampire exiting
%------------------------------------------------------------------------------