%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP621+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:02 AM UTC 2026
% Result : Theorem 26.31s 10.05s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 29
% Syntax : Number of formulae : 360 ( 38 unt; 14 def)
% Number of atoms : 2470 ( 51 equ)
% Maximal formula atoms : 25 ( 6 avg)
% Number of connectives : 3839 (1729 ~;1858 |; 184 &)
% ( 35 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 14 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-5 aty)
% Number of variables : 281 ( 0 sgn 272 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2104,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m1_relset_1(X3,X0,X1)
& v1_funct_1(X4)
& v1_funct_2(X4,X1,X2)
& m1_relset_1(X4,X1,X2) )
=> k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f3367,axiom,
! [X0,X1,X2] :
( m1_fraenkel(X2,X0,X1)
=> ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
fof(f3371,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f17596,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f26982,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] :
( ( ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_group_6(X4,X1,X2)
& m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( ( v4_group_6(X3,X0,X1)
& v4_group_6(X4,X1,X2) )
=> v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t74_group_6) ).
fof(f27019,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1)
& ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2)
& v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_group_6(X4,X1,X2)
& m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> ( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
& v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
& v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k8_group_6) ).
fof(f27020,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1)
& ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2)
& v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_group_6(X4,X1,X2)
& m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
=> k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_group_6) ).
fof(f33385,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_autgroup) ).
fof(f33394,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) ) )
& ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X2,X1)
<=> ( v2_funct_1(X2)
& v3_group_6(X2,X0,X0) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_autgroup) ).
fof(f33398,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X1,X0,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_autgroup) ).
fof(f33402,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_autgroup) ).
fof(f33403,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f33402]) ).
fof(f33410,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) ) )
& ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) ) ) ) ) ) ),
inference(rectify,[],[f33394]) ).
fof(f33933,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f33403]) ).
fof(f33934,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_fraenkel(k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X2,X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f33933]) ).
fof(f33969,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(ennf_transformation,[],[f2104]) ).
fof(f33970,plain,
! [X0,X1,X2,X3,X4] :
( k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,X1,X2)
| ~ m1_relset_1(X4,X1,X2) ),
inference(flattening,[],[f33969]) ).
fof(f34005,plain,
! [X0] :
( ! [X1] :
( ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33398]) ).
fof(f34006,plain,
! [X0] :
( ! [X1] :
( ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34005]) ).
fof(f34011,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33410]) ).
fof(f34012,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34011]) ).
fof(f34013,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33385]) ).
fof(f34014,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34013]) ).
fof(f34026,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f34037,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f35629,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v4_group_6(X3,X0,X1)
| ~ v4_group_6(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) )
| 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,[],[f26982]) ).
fof(f35630,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v4_group_6(X3,X0,X1)
| ~ v4_group_6(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) )
| 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,[],[f35629]) ).
fof(f35732,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3371]) ).
fof(f35733,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f35732]) ).
fof(f35738,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3367]) ).
fof(f38329,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f38372,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17596]) ).
fof(f38373,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f38372]) ).
fof(f41842,plain,
! [X0,X1,X2,X3,X4] :
( k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(ennf_transformation,[],[f27020]) ).
fof(f41843,plain,
! [X0,X1,X2,X3,X4] :
( k8_group_6(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(flattening,[],[f41842]) ).
fof(f41844,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
& v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
& v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(ennf_transformation,[],[f27019]) ).
fof(f41845,plain,
! [X0,X1,X2,X3,X4] :
( ( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
& v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
& v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
& m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(flattening,[],[f41844]) ).
fof(f41985,definition,
! [X0,X1] :
( sP4(X0,X1)
<=> ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f41986,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP4(X0,X1) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(definition_folding,[],[f34012,f41985]) ).
fof(f42447,plain,
( ~ m2_fraenkel(k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302),k1_autgroup(sK302))
& m2_fraenkel(sK304,u1_struct_0(sK302),u1_struct_0(sK302),k1_autgroup(sK302))
& m2_fraenkel(sK303,u1_struct_0(sK302),u1_struct_0(sK302),k1_autgroup(sK302))
& ~ v3_struct_0(sK302)
& v1_group_1(sK302)
& v3_group_1(sK302)
& v4_group_1(sK302)
& l1_group_1(sK302) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK302,sK303,sK304]),skolemize(X0,sK302),skolemize(X1,sK303),skolemize(X2,sK304)],[f33934]) ).
fof(f42479,plain,
! [X0] :
( ! [X1] :
( ( ( r2_hidden(X1,k1_autgroup(X0))
| ~ v4_group_6(X1,X0,X0) )
& ( v4_group_6(X1,X0,X0)
| ~ r2_hidden(X1,k1_autgroup(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f34006]) ).
fof(f42484,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP4(X0,X1) )
& ( ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP4(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f41986]) ).
fof(f42485,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP4(X0,X1) )
& ( ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP4(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f42484]) ).
fof(f42486,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP4(X0,X1) )
& ( ( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP4(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f42485]) ).
fof(f42487,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ( ( ~ v1_funct_1(sK336(X0,X1))
| ~ v1_funct_2(sK336(X0,X1),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(sK336(X0,X1),X0,X0)
| ~ m2_relset_1(sK336(X0,X1),u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(sK336(X0,X1),u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP4(X0,X1) )
& ( ( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP4(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK336]),skolemize(X2,sK336(X0,X1))],[f42486]) ).
fof(f42501,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f34037]) ).
fof(f42906,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f43058,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( m2_fraenkel(X3,X0,X1,X2)
| ~ m1_subset_1(X3,X2) )
& ( m1_subset_1(X3,X2)
| ~ m2_fraenkel(X3,X0,X1,X2) ) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(nnf_transformation,[],[f35733]) ).
fof(f45332,plain,
l1_group_1(sK302),
inference(cnf_transformation,[],[f42447]) ).
fof(f45333,plain,
v4_group_1(sK302),
inference(cnf_transformation,[],[f42447]) ).
fof(f45334,plain,
v3_group_1(sK302),
inference(cnf_transformation,[],[f42447]) ).
fof(f45335,plain,
v1_group_1(sK302),
inference(cnf_transformation,[],[f42447]) ).
fof(f45336,plain,
~ v3_struct_0(sK302),
inference(cnf_transformation,[],[f42447]) ).
fof(f45337,plain,
m2_fraenkel(sK303,u1_struct_0(sK302),u1_struct_0(sK302),k1_autgroup(sK302)),
inference(cnf_transformation,[],[f42447]) ).
fof(f45338,plain,
m2_fraenkel(sK304,u1_struct_0(sK302),u1_struct_0(sK302),k1_autgroup(sK302)),
inference(cnf_transformation,[],[f42447]) ).
fof(f45339,plain,
~ m2_fraenkel(k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302),k1_autgroup(sK302)),
inference(cnf_transformation,[],[f42447]) ).
fof(f45408,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X4,X1,X2)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_1(X4)
| k5_relat_1(X3,X4) = k7_funct_2(X0,X1,X2,X3,X4)
| ~ m1_relset_1(X4,X1,X2) ),
inference(cnf_transformation,[],[f33970]) ).
fof(f45469,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ r2_hidden(X1,k1_autgroup(X0))
| ~ v1_funct_1(X1)
| v4_group_6(X1,X0,X0)
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42479]) ).
fof(f45470,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v4_group_6(X1,X0,X0)
| ~ v1_funct_1(X1)
| r2_hidden(X1,k1_autgroup(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42479]) ).
fof(f45484,plain,
! [X3,X0,X1] :
( m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1)
| k1_autgroup(X0) != X1
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42487]) ).
fof(f45485,plain,
! [X3,X0,X1] :
( v1_group_6(X3,X0,X0)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1)
| k1_autgroup(X0) != X1
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42487]) ).
fof(f45486,plain,
! [X3,X0,X1] :
( v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1)
| k1_autgroup(X0) != X1
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42487]) ).
fof(f45487,plain,
! [X3,X0,X1] :
( v1_funct_1(X3)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1)
| k1_autgroup(X0) != X1
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42487]) ).
fof(f45490,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34014]) ).
fof(f45504,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f34026]) ).
fof(f45520,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f42501]) ).
fof(f47346,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f42906]) ).
fof(f47691,plain,
! [X2,X3,X0,X1,X4] :
( v4_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| ~ v4_group_6(X3,X0,X1)
| ~ v4_group_6(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| 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,[],[f35630]) ).
fof(f47884,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| m1_subset_1(X3,X2)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f43058]) ).
fof(f47885,plain,
! [X2,X3,X0,X1] :
( m2_fraenkel(X3,X0,X1,X2)
| ~ m1_subset_1(X3,X2)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f43058]) ).
fof(f47892,plain,
! [X2,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f35738]) ).
fof(f51644,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f38329]) ).
fof(f51681,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f38373]) ).
fof(f57365,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| k5_relat_1(X3,X4) = k8_group_6(X0,X1,X2,X3,X4)
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f41843]) ).
fof(f57366,plain,
! [X2,X3,X0,X1,X4] :
( m2_relset_1(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f41845]) ).
fof(f57367,plain,
! [X2,X3,X0,X1,X4] :
( v1_group_6(k8_group_6(X0,X1,X2,X3,X4),X0,X2)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f41845]) ).
fof(f57368,plain,
! [X2,X3,X0,X1,X4] :
( v1_funct_2(k8_group_6(X0,X1,X2,X3,X4),u1_struct_0(X0),u1_struct_0(X2))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f41845]) ).
fof(f57369,plain,
! [X2,X3,X0,X1,X4] :
( v1_funct_1(k8_group_6(X0,X1,X2,X3,X4))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m1_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_group_6(X4,X1,X2)
| ~ m1_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f41845]) ).
fof(f59489,plain,
! [X3,X0] :
( v1_funct_1(X3)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f45487]) ).
fof(f59490,plain,
! [X3,X0] :
( v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f45486]) ).
fof(f59491,plain,
! [X3,X0] :
( v1_group_6(X3,X0,X0)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f45485]) ).
fof(f59492,plain,
! [X3,X0] :
( m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f45484]) ).
fof(f61426,plain,
! [X3,X0] :
( ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f59492,f45490]) ).
fof(f61427,plain,
! [X3,X0] :
( ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_group_6(X3,X0,X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f59491,f45490]) ).
fof(f61428,plain,
! [X3,X0] :
( ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f59490,f45490]) ).
fof(f61429,plain,
! [X3,X0] :
( ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_funct_1(X3)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f59489,f45490]) ).
fof(f62088,plain,
( ~ m1_subset_1(k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303),k1_autgroup(sK302))
| v1_xboole_0(u1_struct_0(sK302))
| ~ m1_fraenkel(k1_autgroup(sK302),u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(resolution,[],[f47885,f45339]) ).
fof(f62089,plain,
( v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61428,f45338]) ).
fof(f62090,plain,
( v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61428,f45337]) ).
fof(f62093,plain,
( m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61426,f45338]) ).
fof(f62094,plain,
( m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61426,f45337]) ).
fof(f62097,plain,
( v1_funct_1(sK304)
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61429,f45338]) ).
fof(f62098,plain,
( v1_funct_1(sK303)
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61429,f45337]) ).
fof(f62105,plain,
l1_struct_0(sK302),
inference(resolution,[],[f51644,f45332]) ).
fof(f62106,plain,
( v1_group_6(sK304,sK302,sK302)
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61427,f45338]) ).
fof(f62107,plain,
( v1_group_6(sK303,sK302,sK302)
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f61427,f45337]) ).
fof(f62115,plain,
( m1_subset_1(sK304,k1_autgroup(sK302))
| v1_xboole_0(u1_struct_0(sK302))
| ~ m1_fraenkel(k1_autgroup(sK302),u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(resolution,[],[f47884,f45338]) ).
fof(f62116,plain,
( m1_subset_1(sK303,k1_autgroup(sK302))
| v1_xboole_0(u1_struct_0(sK302))
| ~ m1_fraenkel(k1_autgroup(sK302),u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(resolution,[],[f47884,f45337]) ).
fof(f62333,plain,
( v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62090,f45336]) ).
fof(f62334,plain,
( v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62089,f45336]) ).
fof(f62335,plain,
( m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62094,f45336]) ).
fof(f62336,plain,
( m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62093,f45336]) ).
fof(f62337,plain,
( v1_funct_1(sK303)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62098,f45336]) ).
fof(f62338,plain,
( v1_funct_1(sK304)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62097,f45336]) ).
fof(f62339,plain,
( v1_group_6(sK303,sK302,sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62107,f45336]) ).
fof(f62340,plain,
( v1_group_6(sK304,sK302,sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62106,f45336]) ).
fof(f62369,plain,
( v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62333,f45335]) ).
fof(f62370,plain,
( v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62334,f45335]) ).
fof(f62371,plain,
( m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62335,f45335]) ).
fof(f62372,plain,
( m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62336,f45335]) ).
fof(f62373,plain,
( v1_funct_1(sK303)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62337,f45335]) ).
fof(f62374,plain,
( v1_funct_1(sK304)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62338,f45335]) ).
fof(f62375,plain,
( v1_group_6(sK303,sK302,sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62339,f45335]) ).
fof(f62376,plain,
( v1_group_6(sK304,sK302,sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62340,f45335]) ).
fof(f62396,plain,
( v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62369,f45334]) ).
fof(f62397,plain,
( v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62370,f45334]) ).
fof(f62398,plain,
( m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62371,f45334]) ).
fof(f62399,plain,
( m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62372,f45334]) ).
fof(f62400,plain,
( v1_funct_1(sK303)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62373,f45334]) ).
fof(f62401,plain,
( v1_funct_1(sK304)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62374,f45334]) ).
fof(f62402,plain,
( v1_group_6(sK303,sK302,sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62375,f45334]) ).
fof(f62403,plain,
( v1_group_6(sK304,sK302,sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62376,f45334]) ).
fof(f62422,plain,
( v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62396,f45333]) ).
fof(f62423,plain,
( v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62397,f45333]) ).
fof(f62424,plain,
( m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62398,f45333]) ).
fof(f62425,plain,
( m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62399,f45333]) ).
fof(f62426,plain,
( v1_funct_1(sK303)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62400,f45333]) ).
fof(f62427,plain,
( v1_funct_1(sK304)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62401,f45333]) ).
fof(f62428,plain,
( v1_group_6(sK303,sK302,sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62402,f45333]) ).
fof(f62429,plain,
( v1_group_6(sK304,sK302,sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62403,f45333]) ).
fof(f62443,plain,
v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302)),
inference(forward_subsumption_resolution,[],[f62422,f45332]) ).
fof(f62444,plain,
v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302)),
inference(forward_subsumption_resolution,[],[f62423,f45332]) ).
fof(f62445,plain,
m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)),
inference(forward_subsumption_resolution,[],[f62424,f45332]) ).
fof(f62446,plain,
m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302)),
inference(forward_subsumption_resolution,[],[f62425,f45332]) ).
fof(f62447,plain,
v1_funct_1(sK303),
inference(forward_subsumption_resolution,[],[f62426,f45332]) ).
fof(f62448,plain,
v1_funct_1(sK304),
inference(forward_subsumption_resolution,[],[f62427,f45332]) ).
fof(f62449,plain,
v1_group_6(sK303,sK302,sK302),
inference(forward_subsumption_resolution,[],[f62428,f45332]) ).
fof(f62450,plain,
v1_group_6(sK304,sK302,sK302),
inference(forward_subsumption_resolution,[],[f62429,f45332]) ).
fof(f62463,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ v1_funct_1(sK303)
| v4_group_6(sK303,sK302,sK302)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f62443,f45469]) ).
fof(f62467,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(resolution,[],[f62443,f57365]) ).
fof(f62468,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(sK302))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,u1_struct_0(sK302))
| ~ m1_relset_1(X0,X1,u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X0,sK303) = k7_funct_2(X1,u1_struct_0(sK302),u1_struct_0(sK302),X0,sK303)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(resolution,[],[f62443,f45408]) ).
fof(f62469,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(duplicate_literal_removal,[],[f62467]) ).
fof(f62472,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62469,f45336]) ).
fof(f62475,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62472,f45334]) ).
fof(f62478,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62475,f45333]) ).
fof(f62480,definition,
( spl2013_65
<=> m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_65])],[avatar_definition]) ).
fof(f62481,plain,
( m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_65 ),
inference(avatar_component_clause,[],[f62480]) ).
fof(f62482,plain,
( ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| spl2013_65 ),
inference(avatar_component_clause,[],[f62480]) ).
fof(f62488,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62478,f45332]) ).
fof(f62490,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62488,f62447]) ).
fof(f62492,plain,
! [X0,X1] :
( v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62490,f62449]) ).
fof(f62495,definition,
( spl2013_67
<=> ! [X0,X1] :
( v3_struct_0(X0)
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2013_67])],[avatar_definition]) ).
fof(f62496,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK302))
| k5_relat_1(X1,sK303) = k8_group_6(X0,sK302,sK302,X1,sK303)
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK302))
| ~ v1_group_6(X1,X0,sK302)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) )
| ~ spl2013_67 ),
inference(avatar_component_clause,[],[f62495]) ).
fof(f62497,plain,
( ~ spl2013_65
| spl2013_67 ),
inference(avatar_split_clause,[],[f62492,f62495,f62480]) ).
fof(f62499,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ v1_funct_1(sK304)
| v4_group_6(sK304,sK302,sK302)
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(resolution,[],[f62444,f45469]) ).
fof(f62516,definition,
( spl2013_68
<=> m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_68])],[avatar_definition]) ).
fof(f62517,plain,
( m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_68 ),
inference(avatar_component_clause,[],[f62516]) ).
fof(f62518,plain,
( ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| spl2013_68 ),
inference(avatar_component_clause,[],[f62516]) ).
fof(f62536,plain,
m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)),
inference(resolution,[],[f62445,f47346]) ).
fof(f62537,plain,
( $false
| spl2013_65 ),
inference(forward_subsumption_resolution,[],[f62536,f62482]) ).
fof(f62538,plain,
spl2013_65,
inference(avatar_contradiction_clause,[],[f62537]) ).
fof(f62540,plain,
m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302)),
inference(resolution,[],[f62446,f47346]) ).
fof(f62541,plain,
( $false
| spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62540,f62518]) ).
fof(f62542,plain,
spl2013_68,
inference(avatar_contradiction_clause,[],[f62541]) ).
fof(f62623,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ v1_funct_1(sK304)
| v3_struct_0(sK302)
| ~ l1_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ spl2013_67 ),
inference(resolution,[],[f62496,f62444]) ).
fof(f62626,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ v1_group_6(sK304,sK302,sK302)
| ~ v1_funct_1(sK304)
| v3_struct_0(sK302)
| ~ l1_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62623,f62517]) ).
fof(f62630,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ v1_funct_1(sK304)
| v3_struct_0(sK302)
| ~ l1_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62626,f62450]) ).
fof(f62634,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| v3_struct_0(sK302)
| ~ l1_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62630,f62448]) ).
fof(f62638,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ l1_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62634,f45336]) ).
fof(f62642,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ v4_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62638,f45332]) ).
fof(f62646,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ v3_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62642,f45333]) ).
fof(f62649,plain,
( k5_relat_1(sK304,sK303) = k8_group_6(sK302,sK302,sK302,sK304,sK303)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62646,f45334]) ).
fof(f62703,definition,
( spl2013_77
<=> v4_group_6(sK303,sK302,sK302) ),
introduced(definition,[new_symbols(definition,[spl2013_77])],[avatar_definition]) ).
fof(f62704,plain,
( v4_group_6(sK303,sK302,sK302)
| ~ spl2013_77 ),
inference(avatar_component_clause,[],[f62703]) ).
fof(f62705,plain,
( ~ v4_group_6(sK303,sK302,sK302)
| spl2013_77 ),
inference(avatar_component_clause,[],[f62703]) ).
fof(f62711,plain,
( v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v4_group_6(sK304,sK302,sK302)
| ~ v4_group_6(sK303,sK302,sK302)
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(superposition,[],[f47691,f62649]) ).
fof(f62712,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(superposition,[],[f57369,f62649]) ).
fof(f62713,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(superposition,[],[f57366,f62649]) ).
fof(f62714,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(superposition,[],[f57367,f62649]) ).
fof(f62715,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(superposition,[],[f57368,f62649]) ).
fof(f62716,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(duplicate_literal_removal,[],[f62715]) ).
fof(f62717,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(duplicate_literal_removal,[],[f62714]) ).
fof(f62718,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(duplicate_literal_removal,[],[f62713]) ).
fof(f62719,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(duplicate_literal_removal,[],[f62712]) ).
fof(f62720,plain,
( v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v4_group_6(sK304,sK302,sK302)
| ~ v4_group_6(sK303,sK302,sK302)
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68 ),
inference(duplicate_literal_removal,[],[f62711]) ).
fof(f62721,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62716,f45336]) ).
fof(f62722,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62717,f45336]) ).
fof(f62723,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62718,f45336]) ).
fof(f62724,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62719,f45336]) ).
fof(f62725,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62721,f45334]) ).
fof(f62726,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62722,f45334]) ).
fof(f62727,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62723,f45334]) ).
fof(f62728,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62724,f45334]) ).
fof(f62729,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62725,f45333]) ).
fof(f62730,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62726,f45333]) ).
fof(f62731,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62727,f45333]) ).
fof(f62732,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ l1_group_1(sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62728,f45333]) ).
fof(f62733,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62729,f45332]) ).
fof(f62734,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62730,f45332]) ).
fof(f62735,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62731,f45332]) ).
fof(f62736,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62732,f45332]) ).
fof(f62737,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62733,f62448]) ).
fof(f62738,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62734,f62448]) ).
fof(f62739,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62735,f62448]) ).
fof(f62740,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62736,f62448]) ).
fof(f62741,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62737,f62444]) ).
fof(f62742,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62738,f62444]) ).
fof(f62743,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62739,f62444]) ).
fof(f62744,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62740,f62444]) ).
fof(f62745,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62741,f62450]) ).
fof(f62746,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62742,f62450]) ).
fof(f62747,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62743,f62450]) ).
fof(f62748,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62744,f62450]) ).
fof(f62749,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62745,f62517]) ).
fof(f62750,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62746,f62517]) ).
fof(f62751,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62747,f62517]) ).
fof(f62752,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62748,f62517]) ).
fof(f62753,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62749,f62447]) ).
fof(f62754,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62750,f62447]) ).
fof(f62755,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62751,f62447]) ).
fof(f62756,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62752,f62447]) ).
fof(f62757,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62753,f62443]) ).
fof(f62758,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62754,f62443]) ).
fof(f62759,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62755,f62443]) ).
fof(f62760,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62756,f62443]) ).
fof(f62761,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62757,f62449]) ).
fof(f62762,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62758,f62449]) ).
fof(f62763,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62759,f62449]) ).
fof(f62764,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62760,f62449]) ).
fof(f62765,plain,
( v1_funct_2(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62761,f62481]) ).
fof(f62766,plain,
( v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62762,f62481]) ).
fof(f62767,plain,
( m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62763,f62481]) ).
fof(f62768,plain,
( v1_funct_1(k5_relat_1(sK304,sK303))
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f62764,f62481]) ).
fof(f62913,definition,
( spl2013_79
<=> v4_group_6(sK304,sK302,sK302) ),
introduced(definition,[new_symbols(definition,[spl2013_79])],[avatar_definition]) ).
fof(f62914,plain,
( v4_group_6(sK304,sK302,sK302)
| ~ spl2013_79 ),
inference(avatar_component_clause,[],[f62913]) ).
fof(f62915,plain,
( ~ v4_group_6(sK304,sK302,sK302)
| spl2013_79 ),
inference(avatar_component_clause,[],[f62913]) ).
fof(f63326,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ v1_funct_1(k5_relat_1(sK304,sK303))
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(resolution,[],[f62765,f45470]) ).
fof(f64631,definition,
( spl2013_81
<=> m1_fraenkel(k1_autgroup(sK302),u1_struct_0(sK302),u1_struct_0(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_81])],[avatar_definition]) ).
fof(f64632,plain,
( m1_fraenkel(k1_autgroup(sK302),u1_struct_0(sK302),u1_struct_0(sK302))
| ~ spl2013_81 ),
inference(avatar_component_clause,[],[f64631]) ).
fof(f64633,plain,
( ~ m1_fraenkel(k1_autgroup(sK302),u1_struct_0(sK302),u1_struct_0(sK302))
| spl2013_81 ),
inference(avatar_component_clause,[],[f64631]) ).
fof(f64635,definition,
( spl2013_82
<=> v1_xboole_0(u1_struct_0(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_82])],[avatar_definition]) ).
fof(f64637,plain,
( v1_xboole_0(u1_struct_0(sK302))
| ~ spl2013_82 ),
inference(avatar_component_clause,[],[f64635]) ).
fof(f64639,definition,
( spl2013_83
<=> m1_subset_1(k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303),k1_autgroup(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_83])],[avatar_definition]) ).
fof(f64641,plain,
( ~ m1_subset_1(k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303),k1_autgroup(sK302))
| spl2013_83 ),
inference(avatar_component_clause,[],[f64639]) ).
fof(f64642,plain,
( ~ spl2013_81
| spl2013_82
| ~ spl2013_83 ),
inference(avatar_split_clause,[],[f62088,f64639,f64635,f64631]) ).
fof(f64644,definition,
( spl2013_84
<=> m1_subset_1(sK303,k1_autgroup(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_84])],[avatar_definition]) ).
fof(f64646,plain,
( m1_subset_1(sK303,k1_autgroup(sK302))
| ~ spl2013_84 ),
inference(avatar_component_clause,[],[f64644]) ).
fof(f64647,plain,
( ~ spl2013_81
| spl2013_82
| spl2013_84 ),
inference(avatar_split_clause,[],[f62116,f64644,f64635,f64631]) ).
fof(f64649,definition,
( spl2013_85
<=> m1_subset_1(sK304,k1_autgroup(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_85])],[avatar_definition]) ).
fof(f64651,plain,
( m1_subset_1(sK304,k1_autgroup(sK302))
| ~ spl2013_85 ),
inference(avatar_component_clause,[],[f64649]) ).
fof(f64652,plain,
( ~ spl2013_81
| spl2013_82
| spl2013_85 ),
inference(avatar_split_clause,[],[f62115,f64649,f64635,f64631]) ).
fof(f64662,plain,
! [X0,X1] :
( v1_xboole_0(u1_struct_0(sK302))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,u1_struct_0(sK302))
| ~ m1_relset_1(X0,X1,u1_struct_0(sK302))
| k5_relat_1(X0,sK303) = k7_funct_2(X1,u1_struct_0(sK302),u1_struct_0(sK302),X0,sK303)
| ~ m1_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302)) ),
inference(forward_subsumption_resolution,[],[f62468,f62447]) ).
fof(f64663,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| v4_group_6(sK303,sK302,sK302)
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62463,f62447]) ).
fof(f64665,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| v4_group_6(sK304,sK302,sK302)
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302) ),
inference(forward_subsumption_resolution,[],[f62499,f62448]) ).
fof(f64684,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ v1_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| ~ m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f63326,f62768]) ).
fof(f64704,plain,
( ! [X0,X1] :
( v1_xboole_0(u1_struct_0(sK302))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,u1_struct_0(sK302))
| ~ m1_relset_1(X0,X1,u1_struct_0(sK302))
| k5_relat_1(X0,sK303) = k7_funct_2(X1,u1_struct_0(sK302),u1_struct_0(sK302),X0,sK303) )
| ~ spl2013_65 ),
inference(forward_subsumption_resolution,[],[f64662,f62481]) ).
fof(f64705,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64663,f62705]) ).
fof(f64707,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64665,f62915]) ).
fof(f64726,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ m2_relset_1(k5_relat_1(sK304,sK303),u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64684,f62766]) ).
fof(f64741,definition,
( spl2013_86
<=> ! [X0,X1] :
( ~ v1_funct_1(X0)
| k5_relat_1(X0,sK303) = k7_funct_2(X1,u1_struct_0(sK302),u1_struct_0(sK302),X0,sK303)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK302))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK302)) ) ),
introduced(definition,[new_symbols(definition,[spl2013_86])],[avatar_definition]) ).
fof(f64742,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,X1,u1_struct_0(sK302))
| k5_relat_1(X0,sK303) = k7_funct_2(X1,u1_struct_0(sK302),u1_struct_0(sK302),X0,sK303)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK302))
| ~ v1_funct_1(X0) )
| ~ spl2013_86 ),
inference(avatar_component_clause,[],[f64741]) ).
fof(f64743,plain,
( spl2013_86
| spl2013_82
| ~ spl2013_65 ),
inference(avatar_split_clause,[],[f64704,f62480,f64635,f64741]) ).
fof(f64744,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64705,f62449]) ).
fof(f64749,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64707,f62450]) ).
fof(f64784,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64726,f62767]) ).
fof(f64810,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64744,f62445]) ).
fof(f64811,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64749,f62446]) ).
fof(f64822,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64784,f45336]) ).
fof(f64832,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64810,f45336]) ).
fof(f64833,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64811,f45336]) ).
fof(f64844,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64822,f45335]) ).
fof(f64854,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64832,f45335]) ).
fof(f64855,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64833,f45335]) ).
fof(f64866,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64844,f45334]) ).
fof(f64876,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64854,f45334]) ).
fof(f64877,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64855,f45334]) ).
fof(f64888,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ l1_group_1(sK302)
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64866,f45333]) ).
fof(f64898,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| ~ l1_group_1(sK302)
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64876,f45333]) ).
fof(f64899,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| ~ l1_group_1(sK302)
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64877,f45333]) ).
fof(f64910,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(forward_subsumption_resolution,[],[f64888,f45332]) ).
fof(f64920,plain,
( ~ r2_hidden(sK303,k1_autgroup(sK302))
| spl2013_77 ),
inference(forward_subsumption_resolution,[],[f64898,f45332]) ).
fof(f64921,plain,
( ~ r2_hidden(sK304,k1_autgroup(sK302))
| spl2013_79 ),
inference(forward_subsumption_resolution,[],[f64899,f45332]) ).
fof(f64965,definition,
( spl2013_106
<=> r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302)) ),
introduced(definition,[new_symbols(definition,[spl2013_106])],[avatar_definition]) ).
fof(f64967,plain,
( r2_hidden(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ spl2013_106 ),
inference(avatar_component_clause,[],[f64965]) ).
fof(f64969,definition,
( spl2013_107
<=> v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302) ),
introduced(definition,[new_symbols(definition,[spl2013_107])],[avatar_definition]) ).
fof(f64971,plain,
( ~ v4_group_6(k5_relat_1(sK304,sK303),sK302,sK302)
| spl2013_107 ),
inference(avatar_component_clause,[],[f64969]) ).
fof(f64972,plain,
( spl2013_106
| ~ spl2013_107
| ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68 ),
inference(avatar_split_clause,[],[f64910,f62516,f62495,f62480,f64969,f64965]) ).
fof(f65014,plain,
( v3_struct_0(sK302)
| ~ l1_struct_0(sK302)
| ~ spl2013_82 ),
inference(resolution,[],[f64637,f51681]) ).
fof(f65015,plain,
( ~ l1_struct_0(sK302)
| ~ spl2013_82 ),
inference(forward_subsumption_resolution,[],[f65014,f45336]) ).
fof(f65016,plain,
( $false
| ~ spl2013_82 ),
inference(forward_subsumption_resolution,[],[f65015,f62105]) ).
fof(f65017,plain,
~ spl2013_82,
inference(avatar_contradiction_clause,[],[f65016]) ).
fof(f65018,plain,
( v3_struct_0(sK302)
| ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_81 ),
inference(resolution,[],[f64633,f45490]) ).
fof(f65019,plain,
( ~ v1_group_1(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_81 ),
inference(forward_subsumption_resolution,[],[f65018,f45336]) ).
fof(f65020,plain,
( ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_81 ),
inference(forward_subsumption_resolution,[],[f65019,f45335]) ).
fof(f65021,plain,
( ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| spl2013_81 ),
inference(forward_subsumption_resolution,[],[f65020,f45334]) ).
fof(f65022,plain,
( ~ l1_group_1(sK302)
| spl2013_81 ),
inference(forward_subsumption_resolution,[],[f65021,f45333]) ).
fof(f65023,plain,
( $false
| spl2013_81 ),
inference(forward_subsumption_resolution,[],[f65022,f45332]) ).
fof(f65024,plain,
spl2013_81,
inference(avatar_contradiction_clause,[],[f65023]) ).
fof(f65025,plain,
( ~ v1_xboole_0(k1_autgroup(sK302))
| ~ spl2013_81 ),
inference(resolution,[],[f64632,f47892]) ).
fof(f65026,plain,
( r2_hidden(sK303,k1_autgroup(sK302))
| v1_xboole_0(k1_autgroup(sK302))
| ~ spl2013_84 ),
inference(resolution,[],[f64646,f45520]) ).
fof(f65027,plain,
( v1_xboole_0(k1_autgroup(sK302))
| spl2013_77
| ~ spl2013_84 ),
inference(forward_subsumption_resolution,[],[f65026,f64920]) ).
fof(f65028,plain,
( $false
| spl2013_77
| ~ spl2013_81
| ~ spl2013_84 ),
inference(forward_subsumption_resolution,[],[f65027,f65025]) ).
fof(f65029,plain,
( spl2013_77
| ~ spl2013_81
| ~ spl2013_84 ),
inference(avatar_contradiction_clause,[],[f65028]) ).
fof(f65047,plain,
( r2_hidden(sK304,k1_autgroup(sK302))
| v1_xboole_0(k1_autgroup(sK302))
| ~ spl2013_85 ),
inference(resolution,[],[f64651,f45520]) ).
fof(f65048,plain,
( v1_xboole_0(k1_autgroup(sK302))
| spl2013_79
| ~ spl2013_85 ),
inference(forward_subsumption_resolution,[],[f65047,f64921]) ).
fof(f65049,plain,
( $false
| spl2013_79
| ~ spl2013_81
| ~ spl2013_85 ),
inference(forward_subsumption_resolution,[],[f65048,f65025]) ).
fof(f65050,plain,
( spl2013_79
| ~ spl2013_81
| ~ spl2013_85 ),
inference(avatar_contradiction_clause,[],[f65049]) ).
fof(f65054,plain,
( ~ v4_group_6(sK304,sK302,sK302)
| ~ v4_group_6(sK303,sK302,sK302)
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f62720,f64971]) ).
fof(f65060,plain,
( ~ v4_group_6(sK303,sK302,sK302)
| ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65054,f62914]) ).
fof(f65064,plain,
( ~ v1_funct_1(sK303)
| ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65060,f62704]) ).
fof(f65068,plain,
( ~ v1_funct_2(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65064,f62447]) ).
fof(f65072,plain,
( ~ v1_group_6(sK303,sK302,sK302)
| ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65068,f62443]) ).
fof(f65076,plain,
( ~ m2_relset_1(sK303,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65072,f62449]) ).
fof(f65080,plain,
( ~ v1_funct_1(sK304)
| ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65076,f62445]) ).
fof(f65084,plain,
( ~ v1_funct_2(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65080,f62448]) ).
fof(f65088,plain,
( ~ v1_group_6(sK304,sK302,sK302)
| ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65084,f62444]) ).
fof(f65092,plain,
( ~ m2_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65088,f62450]) ).
fof(f65096,plain,
( v3_struct_0(sK302)
| ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65092,f62446]) ).
fof(f65100,plain,
( ~ v3_group_1(sK302)
| ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65096,f45336]) ).
fof(f65104,plain,
( ~ v4_group_1(sK302)
| ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65100,f45334]) ).
fof(f65108,plain,
( ~ l1_group_1(sK302)
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65104,f45333]) ).
fof(f65110,plain,
( $false
| ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(forward_subsumption_resolution,[],[f65108,f45332]) ).
fof(f65111,plain,
( ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(avatar_contradiction_clause,[],[f65110]) ).
fof(f65172,plain,
( m1_subset_1(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ spl2013_106 ),
inference(resolution,[],[f64967,f45504]) ).
fof(f65188,plain,
( k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303) = k5_relat_1(sK304,sK303)
| ~ m1_relset_1(sK304,u1_struct_0(sK302),u1_struct_0(sK302))
| ~ v1_funct_1(sK304)
| ~ spl2013_86 ),
inference(resolution,[],[f64742,f62444]) ).
fof(f65189,plain,
( k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303) = k5_relat_1(sK304,sK303)
| ~ v1_funct_1(sK304)
| ~ spl2013_68
| ~ spl2013_86 ),
inference(forward_subsumption_resolution,[],[f65188,f62517]) ).
fof(f65205,plain,
( k7_funct_2(u1_struct_0(sK302),u1_struct_0(sK302),u1_struct_0(sK302),sK304,sK303) = k5_relat_1(sK304,sK303)
| ~ spl2013_68
| ~ spl2013_86 ),
inference(forward_subsumption_resolution,[],[f65189,f62448]) ).
fof(f65243,plain,
( ~ m1_subset_1(k5_relat_1(sK304,sK303),k1_autgroup(sK302))
| ~ spl2013_68
| spl2013_83
| ~ spl2013_86 ),
inference(superposition,[],[f64641,f65205]) ).
fof(f65256,plain,
( $false
| ~ spl2013_68
| spl2013_83
| ~ spl2013_86
| ~ spl2013_106 ),
inference(forward_subsumption_resolution,[],[f65243,f65172]) ).
fof(f65257,plain,
( ~ spl2013_68
| spl2013_83
| ~ spl2013_86
| ~ spl2013_106 ),
inference(avatar_contradiction_clause,[],[f65256]) ).
cnf(s65,plain,
( ~ spl2013_65
| spl2013_67 ),
inference(sat_conversion,[],[f62497]) ).
cnf(s68,plain,
spl2013_65,
inference(sat_conversion,[],[f62538]) ).
cnf(s69,plain,
spl2013_68,
inference(sat_conversion,[],[f62542]) ).
cnf(s79,plain,
( ~ spl2013_81
| spl2013_82
| ~ spl2013_83 ),
inference(sat_conversion,[],[f64642]) ).
cnf(s80,plain,
( ~ spl2013_81
| spl2013_82
| spl2013_84 ),
inference(sat_conversion,[],[f64647]) ).
cnf(s81,plain,
( ~ spl2013_81
| spl2013_82
| spl2013_85 ),
inference(sat_conversion,[],[f64652]) ).
cnf(s82,plain,
( ~ spl2013_65
| spl2013_82
| spl2013_86 ),
inference(sat_conversion,[],[f64743]) ).
cnf(s104,plain,
( ~ spl2013_65
| ~ spl2013_67
| ~ spl2013_68
| spl2013_106
| ~ spl2013_107 ),
inference(sat_conversion,[],[f64972]) ).
cnf(s114,plain,
~ spl2013_82,
inference(sat_conversion,[],[f65017]) ).
cnf(s115,plain,
spl2013_81,
inference(sat_conversion,[],[f65024]) ).
cnf(s116,plain,
( spl2013_77
| ~ spl2013_81
| ~ spl2013_84 ),
inference(sat_conversion,[],[f65029]) ).
cnf(s117,plain,
( spl2013_79
| ~ spl2013_81
| ~ spl2013_85 ),
inference(sat_conversion,[],[f65050]) ).
cnf(s118,plain,
( ~ spl2013_67
| ~ spl2013_68
| ~ spl2013_77
| ~ spl2013_79
| spl2013_107 ),
inference(sat_conversion,[],[f65111]) ).
cnf(s121,plain,
( ~ spl2013_68
| spl2013_83
| ~ spl2013_86
| ~ spl2013_106 ),
inference(sat_conversion,[],[f65257]) ).
cnf(s133,plain,
( ~ spl2013_65
| spl2013_86 ),
inference(rat,[],[s82,s114]) ).
cnf(s134,plain,
spl2013_85,
inference(rat,[],[s81,s114,s115]) ).
cnf(s135,plain,
spl2013_79,
inference(rat,[],[s117,s115,s134]) ).
cnf(s136,plain,
spl2013_84,
inference(rat,[],[s80,s114,s115]) ).
cnf(s137,plain,
spl2013_77,
inference(rat,[],[s116,s115,s136]) ).
cnf(s138,plain,
~ spl2013_83,
inference(rat,[],[s79,s114,s115]) ).
cnf(s148,plain,
spl2013_86,
inference(rat,[],[s133,s68]) ).
cnf(s149,plain,
~ spl2013_106,
inference(rat,[],[s121,s69,s138,s148]) ).
cnf(s160,plain,
spl2013_67,
inference(rat,[],[s65,s68]) ).
cnf(s161,plain,
spl2013_107,
inference(rat,[],[s118,s69,s135,s137,s160]) ).
cnf(s162,plain,
$false,
inference(rat,[],[s104,s149,s68,s69,s161,s160]) ).
fof(f65258,plain,
$false,
inference(avatar_sat_refutation,[],[s162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP621+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n012.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 10:09:56 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 18.36/5.28 % (2158333)Detected formulas, will run a generic FOF schedule.
% 18.36/5.28 % (2158338)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=3760385690:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 18.36/5.28 % (2158339)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=2048362713:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 18.36/5.28 % (2158340)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=1574437333:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 18.36/5.28 % (2158341)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1957788788:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 18.36/5.28 % (2158342)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4254952353:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 18.36/5.28 % (2158344)dis-21_1_sil=8000:lcm=predicate:random_seed=3690224662:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 18.36/5.28 % (2158343)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=378674155:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 18.36/5.28 % (2158343)Instruction limit reached!
% 18.36/5.28 % (2158343)------------------------------
% 18.36/5.28 % (2158343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/5.28 % (2158343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/5.28 % (2158343)CaDiCaL version: 2.1.3
% 18.36/5.28 % (2158343)Termination reason: Instruction limit
% 18.36/5.28 % (2158343)Termination phase: Property scanning
% 18.36/5.28 % (2158343)Time elapsed: 0.065 s
% 18.36/5.28 % (2158343)Peak memory usage: 133 MB
% 18.36/5.28 % (2158343)Instructions burned: 140 (million)
% 18.36/5.28 % (2158341)Instruction limit reached!
% 18.36/5.28 % (2158341)------------------------------
% 18.36/5.28 % (2158341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/5.28 % (2158341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/5.28 % (2158341)CaDiCaL version: 2.1.3
% 18.36/5.28 % (2158341)Termination reason: Instruction limit
% 18.36/5.28 % (2158341)Termination phase: SInE selection
% 18.36/5.28 % (2158341)Time elapsed: 0.077 s
% 18.36/5.28 % (2158341)Peak memory usage: 133 MB
% 18.36/5.28 % (2158341)Instructions burned: 111 (million)
% 18.36/5.28 % (2158344)Instruction limit reached!
% 18.36/5.28 % (2158344)------------------------------
% 18.36/5.28 % (2158344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/5.28 % (2158344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/5.28 % (2158344)CaDiCaL version: 2.1.3
% 18.36/5.28 % (2158344)Termination reason: Instruction limit
% 18.36/5.28 % (2158344)Termination phase: SInE selection
% 18.36/5.28 % (2158344)Time elapsed: 0.079 s
% 18.36/5.28 % (2158344)Peak memory usage: 133 MB
% 18.36/5.28 % (2158344)Instructions burned: 133 (million)
% 18.36/5.28 % (2158342)Instruction limit reached!
% 18.36/5.28 % (2158342)------------------------------
% 18.36/5.28 % (2158342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/5.28 % (2158342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/5.28 % (2158342)CaDiCaL version: 2.1.3
% 18.36/5.28 % (2158342)Termination reason: Instruction limit
% 18.36/5.28 % (2158342)Termination phase: SInE selection
% 18.36/5.28 % (2158342)Time elapsed: 0.083 s
% 18.36/5.28 % (2158342)Peak memory usage: 133 MB
% 18.36/5.28 % (2158342)Instructions burned: 124 (million)
% 18.36/5.28 % (2158352)lrs+10_1_sil=8000:sp=occurrence:random_seed=2960764862:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 18.36/5.28 % (2158353)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1393145829:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 18.36/5.28 % (2158354)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2499718042:i=325:sd=1:ss=axioms:sgt=32_2976 on theBenchmark for (2976ds/325Mi)
% 18.36/5.28 % (2158355)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=2380190671:s2a=on:i=248:s2at=1.23:gtg=position_2976 on theBenchmark for (2976ds/248Mi)
% 18.36/5.28 % (2158353)Instruction limit reached!
% 26.55/6.45 % (2158353)------------------------------
% 26.55/6.45 % (2158353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.55/6.45 % (2158353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.55/6.45 % (2158353)CaDiCaL version: 2.1.3
% 26.55/6.45 % (2158353)Termination reason: Instruction limit
% 26.55/6.45 % (2158353)Termination phase: Property scanning
% 26.55/6.45 % (2158353)Time elapsed: 0.076 s
% 26.55/6.45 % (2158353)Peak memory usage: 133 MB
% 26.55/6.45 % (2158353)Instructions burned: 157 (million)
% 26.55/6.45 % (2158355)Instruction limit reached!
% 26.55/6.45 % (2158355)------------------------------
% 26.55/6.45 % (2158355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.55/6.45 % (2158355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.55/6.45 % (2158355)CaDiCaL version: 2.1.3
% 26.55/6.45 % (2158355)Termination reason: Instruction limit
% 26.55/6.45 % (2158355)Termination phase: Property scanning
% 26.55/6.45 % (2158355)Time elapsed: 0.117 s
% 26.55/6.45 % (2158355)Peak memory usage: 133 MB
% 26.55/6.45 % (2158355)Instructions burned: 250 (million)
% 26.55/6.45 % (2158354)Refutation not found, incomplete strategy
% 26.55/6.45 % (2158354)------------------------------
% 26.55/6.45 % (2158354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.55/6.45 % (2158354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.55/6.45 % (2158354)CaDiCaL version: 2.1.3
% 26.55/6.45 % (2158354)Termination reason: Refutation not found, incomplete strategy
% 26.55/6.45 % (2158354)Time elapsed: 0.186 s
% 26.55/6.45 % (2158354)Peak memory usage: 139 MB
% 26.55/6.45 % (2158354)Instructions burned: 239 (million)
% 26.55/6.45 % (2158352)Instruction limit reached!
% 26.55/6.45 % (2158352)------------------------------
% 26.55/6.45 % (2158352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.55/6.45 % (2158352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.55/6.45 % (2158352)CaDiCaL version: 2.1.3
% 26.55/6.45 % (2158352)Termination reason: Instruction limit
% 26.55/6.45 % (2158352)Termination phase: Property scanning
% 26.55/6.45 % (2158352)Time elapsed: 0.224 s
% 26.55/6.45 % (2158352)Peak memory usage: 138 MB
% 26.55/6.45 % (2158352)Instructions burned: 287 (million)
% 26.55/6.45 % (2158360)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1723805130:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 26.55/6.45 % (2158361)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=850876555:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 26.55/6.45 % (2158362)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3889628847:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 26.55/6.45 % (2158360)Instruction limit reached!
% 26.55/6.45 % (2158360)------------------------------
% 26.55/6.45 % (2158360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.55/6.45 % (2158360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.55/6.45 % (2158360)CaDiCaL version: 2.1.3
% 26.55/6.45 % (2158360)Termination reason: Instruction limit
% 26.55/6.45 % (2158360)Termination phase: SInE selection
% 26.55/6.45 % (2158360)Time elapsed: 0.180 s
% 26.55/6.45 % (2158360)Peak memory usage: 134 MB
% 26.55/6.45 % (2158360)Instructions burned: 294 (million)
% 26.55/6.45 % (2158354)------------------------------
% 26.55/6.45 % (2158354)------------------------------
% 26.55/6.45 % (2158362)Instruction limit reached!
% 26.55/6.45 % (2158362)------------------------------
% 26.55/6.45 % (2158362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.55/6.45 % (2158362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.55/6.45 % (2158362)CaDiCaL version: 2.1.3
% 26.55/6.45 % (2158362)Termination reason: Instruction limit
% 26.55/6.45 % (2158362)Termination phase: SInE selection
% 26.55/6.45 % (2158362)Time elapsed: 0.083 s
% 26.55/6.45 % (2158362)Peak memory usage: 133 MB
% 26.55/6.45 % (2158362)Instructions burned: 113 (million)
% 26.55/6.45 % (2158366)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3753790542:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 26.55/6.45 % (2158367)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1474037894:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 26.55/6.45 % (2158368)lrs+10_1_sil=8000:sp=occurrence:random_seed=704721006:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 47.72/9.49 % (2158367)Instruction limit reached!
% 47.72/9.49 % (2158367)------------------------------
% 47.72/9.49 % (2158367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.72/9.49 % (2158367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.72/9.49 % (2158367)CaDiCaL version: 2.1.3
% 47.72/9.49 % (2158367)Termination reason: Instruction limit
% 47.72/9.49 % (2158367)Termination phase: Property scanning
% 47.72/9.49 % (2158367)Time elapsed: 0.054 s
% 47.72/9.49 % (2158367)Peak memory usage: 133 MB
% 47.72/9.49 % (2158367)Instructions burned: 114 (million)
% 47.72/9.49 % (2158366)Instruction limit reached!
% 47.72/9.49 % (2158366)------------------------------
% 47.72/9.49 % (2158366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.72/9.49 % (2158366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.72/9.49 % (2158366)CaDiCaL version: 2.1.3
% 47.72/9.49 % (2158366)Termination reason: Instruction limit
% 47.72/9.49 % (2158366)Termination phase: Preprocessing 1
% 47.72/9.49 % (2158366)Time elapsed: 0.089 s
% 47.72/9.49 % (2158366)Peak memory usage: 136 MB
% 47.72/9.49 % (2158366)Instructions burned: 127 (million)
% 47.72/9.49 % (2158373)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=132181736:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 47.72/9.49 % (2158372)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=273842668:i=437:sd=1:aac=none:ss=included_2967 on theBenchmark for (2967ds/437Mi)
% 47.72/9.49 % (2158372)Instruction limit reached!
% 47.72/9.49 % (2158372)------------------------------
% 47.72/9.49 % (2158372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.72/9.49 % (2158372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.72/9.49 % (2158372)CaDiCaL version: 2.1.3
% 47.72/9.49 % (2158372)Termination reason: Instruction limit
% 47.72/9.49 % (2158372)Termination phase: Saturation
% 47.72/9.49 % (2158372)Time elapsed: 0.289 s
% 47.72/9.49 % (2158372)Peak memory usage: 141 MB
% 47.72/9.49 % (2158372)Instructions burned: 437 (million)
% 47.72/9.49 % (2158368)Instruction limit reached!
% 47.72/9.49 % (2158368)------------------------------
% 47.72/9.49 % (2158368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.72/9.49 % (2158368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.72/9.49 % (2158368)CaDiCaL version: 2.1.3
% 47.72/9.49 % (2158368)Termination reason: Instruction limit
% 47.72/9.49 % (2158368)Termination phase: Equality resolution with deletion
% 47.72/9.49 % (2158368)Time elapsed: 0.578 s
% 47.72/9.49 % (2158368)Peak memory usage: 154 MB
% 47.72/9.49 % (2158368)Instructions burned: 908 (million)
% 47.72/9.49 % (2158376)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1582286339:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2962 on theBenchmark for (2962ds/134Mi)
% 47.72/9.49 % (2158377)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1023958391:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 47.72/9.49 % (2158376)Instruction limit reached!
% 47.72/9.49 % (2158376)------------------------------
% 47.72/9.49 % (2158376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.72/9.49 % (2158376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.72/9.49 % (2158376)CaDiCaL version: 2.1.3
% 47.72/9.49 % (2158376)Termination reason: Instruction limit
% 47.72/9.49 % (2158376)Termination phase: SInE selection
% 47.72/9.49 % (2158376)Time elapsed: 0.102 s
% 47.72/9.49 % (2158376)Peak memory usage: 133 MB
% 47.72/9.49 % (2158376)Instructions burned: 135 (million)
% 47.72/9.49 % (2158380)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=266590326:st=3:i=13193:sd=3:ss=axioms_2959 on theBenchmark for (2959ds/13193Mi)
% 47.72/9.49 % (2158361)Instruction limit reached!
% 47.72/9.49 % (2158361)------------------------------
% 47.72/9.49 % (2158361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.72/9.49 % (2158361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.72/9.49 % (2158361)CaDiCaL version: 2.1.3
% 47.72/9.49 % (2158361)Termination reason: Instruction limit
% 47.72/9.49 % (2158361)Termination phase: Property scanning
% 47.72/9.49 % (2158361)Time elapsed: 1.500 s
% 47.72/9.49 % (2158361)Peak memory usage: 227 MB
% 47.72/9.49 % (2158361)Instructions burned: 2351 (million)
% 47.72/9.49 % (2158377)Instruction limit reached!
% 26.31/10.05 % (2158377)------------------------------
% 26.31/10.05 % (2158377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158377)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158377)Termination reason: Instruction limit
% 26.31/10.05 % (2158377)Termination phase: Preprocessing 2
% 26.31/10.05 % (2158377)Time elapsed: 0.444 s
% 26.31/10.05 % (2158377)Peak memory usage: 142 MB
% 26.31/10.05 % (2158377)Instructions burned: 592 (million)
% 26.31/10.05 % (2158382)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=1617653253:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 26.31/10.05 % (2158383)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1501676426:i=134:gtgl=5:slsql=off:gtg=exists_sym_2955 on theBenchmark for (2955ds/134Mi)
% 26.31/10.05 % (2158382)Instruction limit reached!
% 26.31/10.05 % (2158382)------------------------------
% 26.31/10.05 % (2158382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158382)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158382)Termination reason: Instruction limit
% 26.31/10.05 % (2158382)Termination phase: Property scanning
% 26.31/10.05 % (2158382)Time elapsed: 0.065 s
% 26.31/10.05 % (2158382)Peak memory usage: 133 MB
% 26.31/10.05 % (2158382)Instructions burned: 126 (million)
% 26.31/10.05 % (2158383)Instruction limit reached!
% 26.31/10.05 % (2158383)------------------------------
% 26.31/10.05 % (2158383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158383)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158383)Termination reason: Instruction limit
% 26.31/10.05 % (2158383)Termination phase: Property scanning
% 26.31/10.05 % (2158383)Time elapsed: 0.063 s
% 26.31/10.05 % (2158383)Peak memory usage: 133 MB
% 26.31/10.05 % (2158383)Instructions burned: 136 (million)
% 26.31/10.05 % (2158386)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2486466207:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 26.31/10.05 % (2158387)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2468436176:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 26.31/10.05 % (2158386)Instruction limit reached!
% 26.31/10.05 % (2158386)------------------------------
% 26.31/10.05 % (2158386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158386)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158386)Termination reason: Instruction limit
% 26.31/10.05 % (2158386)Termination phase: SInE selection
% 26.31/10.05 % (2158386)Time elapsed: 0.103 s
% 26.31/10.05 % (2158386)Peak memory usage: 133 MB
% 26.31/10.05 % (2158386)Instructions burned: 141 (million)
% 26.31/10.05 % (2158387)Refutation not found, incomplete strategy
% 26.31/10.05 % (2158387)------------------------------
% 26.31/10.05 % (2158387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158387)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158387)Termination reason: Refutation not found, incomplete strategy
% 26.31/10.05 % (2158387)Time elapsed: 0.179 s
% 26.31/10.05 % (2158387)Peak memory usage: 139 MB
% 26.31/10.05 % (2158387)Instructions burned: 232 (million)
% 26.31/10.05 % (2158390)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1715555579:i=6060:aac=none:ins=25_2950 on theBenchmark for (2950ds/6060Mi)
% 26.31/10.05 % (2158387)------------------------------
% 26.31/10.05 % (2158387)------------------------------
% 26.31/10.05 % (2158392)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3795366326:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2946 on theBenchmark for (2946ds/150Mi)
% 26.31/10.05 % (2158392)Instruction limit reached!
% 26.31/10.05 % (2158392)------------------------------
% 26.31/10.05 % (2158392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158392)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158392)Termination reason: Instruction limit
% 26.31/10.05 % (2158392)Termination phase: SInE selection
% 26.31/10.05 % (2158392)Time elapsed: 0.109 s
% 26.31/10.05 % (2158392)Peak memory usage: 133 MB
% 26.31/10.05 % (2158392)Instructions burned: 150 (million)
% 26.31/10.05 % (2158394)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3767228444:i=14155:bd=all_2943 on theBenchmark for (2943ds/14155Mi)
% 26.31/10.05 % (2158373)Instruction limit reached!
% 26.31/10.05 % (2158373)------------------------------
% 26.31/10.05 % (2158373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158373)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158373)Termination reason: Instruction limit
% 26.31/10.05 % (2158373)Termination phase: Saturation
% 26.31/10.05 % (2158373)Time elapsed: 3.581 s
% 26.31/10.05 % (2158373)Peak memory usage: 522 MB
% 26.31/10.05 % (2158373)Instructions burned: 5202 (million)
% 26.31/10.05 % (2158396)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2417208304:i=667:av=off:fsr=off_2929 on theBenchmark for (2929ds/667Mi)
% 26.31/10.05 % (2158396)Instruction limit reached!
% 26.31/10.05 % (2158396)------------------------------
% 26.31/10.05 % (2158396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158396)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158396)Termination reason: Instruction limit
% 26.31/10.05 % (2158396)Termination phase: NewCNF
% 26.31/10.05 % (2158396)Time elapsed: 0.504 s
% 26.31/10.05 % (2158396)Peak memory usage: 183 MB
% 26.31/10.05 % (2158396)Instructions burned: 669 (million)
% 26.31/10.05 % (2158398)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=207995303:s2a=on:i=185:s2at=1.8:fdi=4_2921 on theBenchmark for (2921ds/185Mi)
% 26.31/10.05 % (2158398)Instruction limit reached!
% 26.31/10.05 % (2158398)------------------------------
% 26.31/10.05 % (2158398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158398)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158398)Termination reason: Instruction limit
% 26.31/10.05 % (2158398)Termination phase: SInE selection
% 26.31/10.05 % (2158398)Time elapsed: 0.121 s
% 26.31/10.05 % (2158398)Peak memory usage: 134 MB
% 26.31/10.05 % (2158398)Instructions burned: 185 (million)
% 26.31/10.05 % (2158400)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1191384021:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2918 on theBenchmark for (2918ds/193Mi)
% 26.31/10.05 % (2158390)Instruction limit reached!
% 26.31/10.05 % (2158390)------------------------------
% 26.31/10.05 % (2158390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158390)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158390)Termination reason: Instruction limit
% 26.31/10.05 % (2158390)Termination phase: Function definition elimination
% 26.31/10.05 % (2158390)Time elapsed: 3.310 s
% 26.31/10.05 % (2158390)Peak memory usage: 244 MB
% 26.31/10.05 % (2158390)Instructions burned: 6061 (million)
% 26.31/10.05 % (2158400)Instruction limit reached!
% 26.31/10.05 % (2158400)------------------------------
% 26.31/10.05 % (2158400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.31/10.05 % (2158400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.31/10.05 % (2158400)CaDiCaL version: 2.1.3
% 26.31/10.05 % (2158400)Termination reason: Instruction limit
% 26.31/10.05 % (2158400)Termination phase: SInE selection
% 26.31/10.05 % (2158400)Time elapsed: 0.137 s
% 26.31/10.05 % (2158400)Peak memory usage: 134 MB
% 26.31/10.05 % (2158400)Instructions burned: 194 (million)
% 26.31/10.05 % (2158402)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4102363159:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2915 on theBenchmark for (2915ds/4850Mi)
% 26.31/10.05 % (2158403)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1440229091:i=12111:sd=1:ss=included_2915 on theBenchmark for (2915ds/12111Mi)
% 26.31/10.05 % (2158380)First to succeed.
% 26.31/10.05 % (2158380)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2158333"
% 26.31/10.05 % (2158380)Refutation found. Thanks to Tanya!
% 26.31/10.05 % SZS status Theorem for theBenchmark
% 26.31/10.05 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/10.30 % (2158380)------------------------------
% 0.16/10.30 % (2158380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/10.30 % (2158380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/10.30 % (2158380)CaDiCaL version: 2.1.3
% 0.16/10.30 % (2158380)Termination reason: Refutation
% 0.16/10.30 % (2158380)Time elapsed: 4.444 s
% 0.16/10.30 % (2158380)Peak memory usage: 305 MB
% 0.16/10.30 % (2158380)Instructions burned: 7927 (million)
% 0.16/10.30 % (2158380)------------------------------
% 0.16/10.30 % (2158380)------------------------------
% 0.16/10.30 % (2158333)Success in time 9.202 s
% 0.16/10.30 % Vampire exiting
%------------------------------------------------------------------------------