%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP632+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:09 AM UTC 2026
% Result : Theorem 16.67s 7.53s
% Output : Refutation 35.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 38
% Syntax : Number of formulae : 320 ( 33 unt; 19 def)
% Number of atoms : 1559 ( 109 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 2185 ( 946 ~;1087 |; 99 &)
% ( 26 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 36 usr; 20 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-5 aty)
% Number of variables : 191 ( 0 sgn 187 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1468,axiom,
! [X0,X1] :
( m2_relset_1(X1,X0,X0)
=> ( k5_relat_1(X1,k6_relat_1(X0)) = X1
& k5_relat_1(k6_relat_1(X0),X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1552,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> k5_relat_1(k6_relat_1(X0),X2) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_partfun1) ).
fof(f1725,axiom,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
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/sandbox/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f3369,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
=> ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_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/sandbox/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/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f18993,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_group_1) ).
fof(f26949,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_group_6) ).
fof(f33388,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_autgroup) ).
fof(f33389,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_autgroup) ).
fof(f33390,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_autgroup) ).
fof(f33413,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m2_fraenkel(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_autgroup) ).
fof(f33416,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& v1_group_3(X1,k3_autgroup(X0))
& m1_group_2(X1,k3_autgroup(X0)) )
=> ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_autgroup) ).
fof(f33418,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
=> ! [X3] :
( m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ! [X4] :
( m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ( ( X1 = X3
& X2 = X4 )
=> k1_group_1(k5_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_autgroup) ).
fof(f33423,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_autgroup) ).
fof(f33429,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),k4_autgroup(X0))
=> ( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) = X1
& k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,k6_autgroup(X0,k2_group_1(X0))) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_autgroup) ).
fof(f33430,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),k4_autgroup(X0))
=> ( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) = X1
& k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,k6_autgroup(X0,k2_group_1(X0))) = X1 ) ) ),
inference(negated_conjecture,[status(cth)],[f33429]) ).
fof(f33536,plain,
? [X0] :
( ? [X1] :
( ( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) != X1
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,k6_autgroup(X0,k2_group_1(X0))) != X1 )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_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,[],[f33430]) ).
fof(f33537,plain,
? [X0] :
( ? [X1] :
( ( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k2_group_1(X0)),X1) != X1
| k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X1,k6_autgroup(X0,k2_group_1(X0))) != X1 )
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f33536]) ).
fof(f33546,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(f33547,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,[],[f33546]) ).
fof(f33570,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18993]) ).
fof(f33571,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33570]) ).
fof(f33580,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k1_group_1(k5_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3)
| X1 != X3
| X2 != X4
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(k5_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,[],[f33418]) ).
fof(f33581,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k1_group_1(k5_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3)
| X1 != X3
| X2 != X4
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(X0))) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33580]) ).
fof(f33582,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_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,[],[f33416]) ).
fof(f33583,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33582]) ).
fof(f33588,plain,
! [X0] :
( m2_fraenkel(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0),k4_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,[],[f33413]) ).
fof(f33589,plain,
! [X0] :
( m2_fraenkel(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33588]) ).
fof(f33600,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f33390]) ).
fof(f33601,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f33600]) ).
fof(f33602,plain,
! [X0] :
( m1_fraenkel(k4_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,[],[f33388]) ).
fof(f33603,plain,
! [X0] :
( m1_fraenkel(k4_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,[],[f33602]) ).
fof(f33614,plain,
! [X0] :
( k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(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,[],[f33423]) ).
fof(f33615,plain,
! [X0] :
( k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(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,[],[f33614]) ).
fof(f34092,plain,
! [X0] :
( ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_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,[],[f33389]) ).
fof(f34093,plain,
! [X0] :
( ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34092]) ).
fof(f34178,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(f34179,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,[],[f34178]) ).
fof(f34182,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3369]) ).
fof(f34183,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
| ~ m2_fraenkel(X3,X0,X1,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(flattening,[],[f34182]) ).
fof(f35390,plain,
! [X0,X1,X2] :
( k5_relat_1(k6_relat_1(X0),X2) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1552]) ).
fof(f35392,plain,
! [X0,X1] :
( ( k5_relat_1(X1,k6_relat_1(X0)) = X1
& k5_relat_1(k6_relat_1(X0),X1) = X1 )
| ~ m2_relset_1(X1,X0,X0) ),
inference(ennf_transformation,[],[f1468]) ).
fof(f35714,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f26949]) ).
fof(f35715,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f35714]) ).
fof(f37701,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f37710,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17596]) ).
fof(f37711,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f37710]) ).
fof(f39682,plain,
( ( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_autgroup(sK95,k2_group_1(sK95))) )
& m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
& ~ v3_struct_0(sK95)
& v1_group_1(sK95)
& v3_group_1(sK95)
& v4_group_1(sK95)
& l1_group_1(sK95) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95,sK96]),skolemize(X0,sK95),skolemize(X1,sK96)],[f33537]) ).
fof(f39709,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k5_autgroup(X0)
| u1_struct_0(X1) != k4_autgroup(X0) )
& ( u1_struct_0(X1) = k4_autgroup(X0)
| k5_autgroup(X0) != X1 ) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f33583]) ).
fof(f39783,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(f39884,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,[],[f34179]) ).
fof(f41520,plain,
l1_group_1(sK95),
inference(cnf_transformation,[],[f39682]) ).
fof(f41521,plain,
v4_group_1(sK95),
inference(cnf_transformation,[],[f39682]) ).
fof(f41522,plain,
v3_group_1(sK95),
inference(cnf_transformation,[],[f39682]) ).
fof(f41523,plain,
v1_group_1(sK95),
inference(cnf_transformation,[],[f39682]) ).
fof(f41524,plain,
~ v3_struct_0(sK95),
inference(cnf_transformation,[],[f39682]) ).
fof(f41525,plain,
m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95)),
inference(cnf_transformation,[],[f39682]) ).
fof(f41526,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_autgroup(sK95,k2_group_1(sK95))) ),
inference(cnf_transformation,[],[f39682]) ).
fof(f41567,plain,
! [X2,X3,X0,X1,X4] :
( k5_relat_1(X3,X4) = k7_funct_2(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) ),
inference(cnf_transformation,[],[f33547]) ).
fof(f41604,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33571]) ).
fof(f41613,plain,
! [X2,X3,X0,X1,X4] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3) = k1_group_1(k5_autgroup(X0),X1,X2)
| X1 != X3
| X2 != X4
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33581]) ).
fof(f41614,plain,
! [X0,X1] :
( u1_struct_0(X1) = k4_autgroup(X0)
| k5_autgroup(X0) != X1
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f39709]) ).
fof(f41618,plain,
! [X0] :
( m2_fraenkel(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33589]) ).
fof(f41635,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f33601]) ).
fof(f41636,plain,
! [X0] :
( m1_fraenkel(k4_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,[],[f33603]) ).
fof(f41643,plain,
! [X0] :
( k6_partfun1(u1_struct_0(X0)) = k6_autgroup(X0,k2_group_1(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33615]) ).
fof(f41983,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f39783]) ).
fof(f42214,plain,
! [X0] :
( m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34093]) ).
fof(f42215,plain,
! [X0] :
( v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34093]) ).
fof(f42216,plain,
! [X0] :
( v1_group_1(k5_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34093]) ).
fof(f42337,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,[],[f39884]) ).
fof(f42340,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| m2_relset_1(X3,X0,X1)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f34183]) ).
fof(f42341,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_funct_2(X3,X0,X1)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f34183]) ).
fof(f42342,plain,
! [X2,X3,X0,X1] :
( ~ m2_fraenkel(X3,X0,X1,X2)
| v1_funct_1(X3)
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f34183]) ).
fof(f44065,plain,
! [X0] : k6_relat_1(X0) = k6_partfun1(X0),
inference(cnf_transformation,[],[f1725]) ).
fof(f44067,plain,
! [X2,X0,X1] :
( k5_relat_1(k6_relat_1(X0),X2) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f35390]) ).
fof(f44070,plain,
! [X0,X1] :
( k5_relat_1(X1,k6_relat_1(X0)) = X1
| ~ m2_relset_1(X1,X0,X0) ),
inference(cnf_transformation,[],[f35392]) ).
fof(f44443,plain,
! [X0] :
( v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f35715]) ).
fof(f44444,plain,
! [X0] :
( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f35715]) ).
fof(f46904,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f37701]) ).
fof(f46915,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f37711]) ).
fof(f50244,plain,
! [X2,X0,X1] :
( k5_relat_1(k6_partfun1(X0),X2) = X2
| ~ m2_relset_1(X2,X0,X1) ),
inference(definition_unfolding,[],[f44067,f44065]) ).
fof(f50246,plain,
! [X0,X1] :
( k5_relat_1(X1,k6_partfun1(X0)) = X1
| ~ m2_relset_1(X1,X0,X0) ),
inference(definition_unfolding,[],[f44070,f44065]) ).
fof(f50944,plain,
! [X2,X3,X0,X4] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3) = k1_group_1(k5_autgroup(X0),X3,X2)
| X2 != X4
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k5_autgroup(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f41613]) ).
fof(f50945,plain,
! [X3,X0,X4] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3) = k1_group_1(k5_autgroup(X0),X3,X4)
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X4,u1_struct_0(k5_autgroup(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k5_autgroup(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f50944]) ).
fof(f50946,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ v1_group_1(k5_autgroup(X0))
| ~ v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| ~ m1_group_2(k5_autgroup(X0),k3_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f41614]) ).
fof(f52101,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| ~ m1_group_2(k5_autgroup(X0),k3_autgroup(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,[],[f50946,f42216]) ).
fof(f52108,definition,
( spl1241_46
<=> sK96 = k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_autgroup(sK95,k2_group_1(sK95))) ),
introduced(definition,[new_symbols(definition,[spl1241_46])],[avatar_definition]) ).
fof(f52110,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_autgroup(sK95,k2_group_1(sK95)))
| spl1241_46 ),
inference(avatar_component_clause,[],[f52108]) ).
fof(f52112,definition,
( spl1241_47
<=> sK96 = k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),k6_autgroup(sK95,k2_group_1(sK95)),sK96) ),
introduced(definition,[new_symbols(definition,[spl1241_47])],[avatar_definition]) ).
fof(f52114,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| spl1241_47 ),
inference(avatar_component_clause,[],[f52112]) ).
fof(f52115,plain,
( ~ spl1241_46
| ~ spl1241_47 ),
inference(avatar_split_clause,[],[f41526,f52112,f52108]) ).
fof(f52204,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ m1_group_2(k5_autgroup(X0),k3_autgroup(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,[],[f52101,f42215]) ).
fof(f52241,plain,
! [X0] :
( k4_autgroup(X0) = u1_struct_0(k5_autgroup(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,[],[f52204,f42214]) ).
fof(f52266,definition,
( spl1241_52
<=> m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_52])],[avatar_definition]) ).
fof(f52267,plain,
( m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_52 ),
inference(avatar_component_clause,[],[f52266]) ).
fof(f52268,plain,
( ~ m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_52 ),
inference(avatar_component_clause,[],[f52266]) ).
fof(f52270,definition,
( spl1241_53
<=> v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_53])],[avatar_definition]) ).
fof(f52271,plain,
( v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_53 ),
inference(avatar_component_clause,[],[f52270]) ).
fof(f52274,definition,
( spl1241_54
<=> v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95))) ),
introduced(definition,[new_symbols(definition,[spl1241_54])],[avatar_definition]) ).
fof(f52275,plain,
( v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95)))
| ~ spl1241_54 ),
inference(avatar_component_clause,[],[f52274]) ).
fof(f52278,definition,
( spl1241_55
<=> m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_55])],[avatar_definition]) ).
fof(f52279,plain,
( m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_55 ),
inference(avatar_component_clause,[],[f52278]) ).
fof(f52282,definition,
( spl1241_56
<=> v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_56])],[avatar_definition]) ).
fof(f52283,plain,
( v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_56 ),
inference(avatar_component_clause,[],[f52282]) ).
fof(f52286,definition,
( spl1241_57
<=> v1_funct_1(sK96) ),
introduced(definition,[new_symbols(definition,[spl1241_57])],[avatar_definition]) ).
fof(f52287,plain,
( v1_funct_1(sK96)
| ~ spl1241_57 ),
inference(avatar_component_clause,[],[f52286]) ).
fof(f52290,definition,
( spl1241_58
<=> v1_xboole_0(u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_58])],[avatar_definition]) ).
fof(f52291,plain,
( ~ v1_xboole_0(u1_struct_0(sK95))
| spl1241_58 ),
inference(avatar_component_clause,[],[f52290]) ).
fof(f52292,plain,
( v1_xboole_0(u1_struct_0(sK95))
| ~ spl1241_58 ),
inference(avatar_component_clause,[],[f52290]) ).
fof(f52313,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_partfun1(u1_struct_0(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(superposition,[],[f52110,f41643]) ).
fof(f52326,plain,
( m1_subset_1(sK96,k4_autgroup(sK95))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95)) ),
inference(resolution,[],[f41525,f42337]) ).
fof(f52328,definition,
( spl1241_60
<=> m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_60])],[avatar_definition]) ).
fof(f52329,plain,
( m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_60 ),
inference(avatar_component_clause,[],[f52328]) ).
fof(f52330,plain,
( ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_60 ),
inference(avatar_component_clause,[],[f52328]) ).
fof(f52332,definition,
( spl1241_61
<=> m1_subset_1(sK96,k4_autgroup(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_61])],[avatar_definition]) ).
fof(f52335,plain,
( ~ spl1241_60
| spl1241_58
| spl1241_61 ),
inference(avatar_split_clause,[],[f52326,f52332,f52290,f52328]) ).
fof(f52341,plain,
( v1_funct_1(sK96)
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95)) ),
inference(resolution,[],[f42342,f41525]) ).
fof(f52356,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_partfun1(u1_struct_0(sK95)))
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52313,f41524]) ).
fof(f52358,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_partfun1(u1_struct_0(sK95)))
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52356,f41523]) ).
fof(f52360,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_partfun1(u1_struct_0(sK95)))
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52358,f41522]) ).
fof(f52362,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_partfun1(u1_struct_0(sK95)))
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52360,f41521]) ).
fof(f52364,plain,
( sK96 != k7_funct_2(u1_struct_0(sK95),u1_struct_0(sK95),u1_struct_0(sK95),sK96,k6_partfun1(u1_struct_0(sK95)))
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52362,f41520]) ).
fof(f52447,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m2_fraenkel(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(superposition,[],[f52364,f50945]) ).
fof(f52449,plain,
! [X2,X0,X1] :
( k5_relat_1(X2,X1) = k1_group_1(k5_autgroup(X0),X1,X2)
| v1_xboole_0(u1_struct_0(X0))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m1_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(superposition,[],[f41567,f50945]) ).
fof(f52459,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52447,f41618]) ).
fof(f52469,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52459,f41525]) ).
fof(f52474,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52469,f41524]) ).
fof(f52476,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52474,f41523]) ).
fof(f52478,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52476,f41522]) ).
fof(f52480,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| ~ l1_group_1(sK95)
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52478,f41521]) ).
fof(f52482,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| spl1241_46 ),
inference(forward_subsumption_resolution,[],[f52480,f41520]) ).
fof(f52484,definition,
( spl1241_69
<=> m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(k5_autgroup(sK95))) ),
introduced(definition,[new_symbols(definition,[spl1241_69])],[avatar_definition]) ).
fof(f52485,plain,
( m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(k5_autgroup(sK95)))
| ~ spl1241_69 ),
inference(avatar_component_clause,[],[f52484]) ).
fof(f52486,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(k5_autgroup(sK95)))
| spl1241_69 ),
inference(avatar_component_clause,[],[f52484]) ).
fof(f52488,definition,
( spl1241_70
<=> m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95))) ),
introduced(definition,[new_symbols(definition,[spl1241_70])],[avatar_definition]) ).
fof(f52489,plain,
( m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ spl1241_70 ),
inference(avatar_component_clause,[],[f52488]) ).
fof(f52490,plain,
( ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| spl1241_70 ),
inference(avatar_component_clause,[],[f52488]) ).
fof(f52492,definition,
( spl1241_71
<=> m2_fraenkel(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_71])],[avatar_definition]) ).
fof(f52493,plain,
( m2_fraenkel(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ spl1241_71 ),
inference(avatar_component_clause,[],[f52492]) ).
fof(f52494,plain,
( ~ m2_fraenkel(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| spl1241_71 ),
inference(avatar_component_clause,[],[f52492]) ).
fof(f52501,definition,
( spl1241_73
<=> m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95))) ),
introduced(definition,[new_symbols(definition,[spl1241_73])],[avatar_definition]) ).
fof(f52502,plain,
( m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| ~ spl1241_73 ),
inference(avatar_component_clause,[],[f52501]) ).
fof(f52503,plain,
( ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| spl1241_73 ),
inference(avatar_component_clause,[],[f52501]) ).
fof(f52505,definition,
( spl1241_74
<=> sK96 = k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96) ),
introduced(definition,[new_symbols(definition,[spl1241_74])],[avatar_definition]) ).
fof(f52507,plain,
( sK96 != k1_group_1(k5_autgroup(sK95),k6_partfun1(u1_struct_0(sK95)),sK96)
| spl1241_74 ),
inference(avatar_component_clause,[],[f52505]) ).
fof(f52508,plain,
( ~ spl1241_73
| ~ spl1241_70
| ~ spl1241_74
| spl1241_46 ),
inference(avatar_split_clause,[],[f52482,f52108,f52505,f52488,f52501]) ).
fof(f52577,plain,
( ~ m1_subset_1(sK96,k4_autgroup(sK95))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_70 ),
inference(superposition,[],[f52490,f52241]) ).
fof(f52595,plain,
( ~ m1_subset_1(sK96,k4_autgroup(sK95))
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_70 ),
inference(forward_subsumption_resolution,[],[f52577,f41524]) ).
fof(f52596,plain,
( ~ m1_subset_1(sK96,k4_autgroup(sK95))
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_70 ),
inference(forward_subsumption_resolution,[],[f52595,f41523]) ).
fof(f52597,plain,
( ~ m1_subset_1(sK96,k4_autgroup(sK95))
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_70 ),
inference(forward_subsumption_resolution,[],[f52596,f41522]) ).
fof(f52598,plain,
( ~ m1_subset_1(sK96,k4_autgroup(sK95))
| ~ l1_group_1(sK95)
| spl1241_70 ),
inference(forward_subsumption_resolution,[],[f52597,f41521]) ).
fof(f52599,plain,
( ~ m1_subset_1(sK96,k4_autgroup(sK95))
| spl1241_70 ),
inference(forward_subsumption_resolution,[],[f52598,f41520]) ).
fof(f52600,plain,
( ~ spl1241_61
| spl1241_70 ),
inference(avatar_split_clause,[],[f52599,f52488,f52332]) ).
fof(f52691,plain,
( v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ m1_subset_1(k2_group_1(sK95),u1_struct_0(sK95))
| spl1241_71 ),
inference(resolution,[],[f52494,f41635]) ).
fof(f52694,plain,
( v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52691,f41604]) ).
fof(f52696,plain,
( ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52694,f41524]) ).
fof(f52698,plain,
( ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52696,f41523]) ).
fof(f52700,plain,
( ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52698,f41522]) ).
fof(f52702,plain,
( ~ l1_group_1(sK95)
| spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52700,f41521]) ).
fof(f52705,plain,
( $false
| spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52702,f41520]) ).
fof(f52706,plain,
spl1241_71,
inference(avatar_contradiction_clause,[],[f52705]) ).
fof(f52708,plain,
( v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95)))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_71 ),
inference(resolution,[],[f52493,f42342]) ).
fof(f52709,plain,
( m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_71 ),
inference(resolution,[],[f52493,f42337]) ).
fof(f52734,plain,
( v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95)) ),
inference(resolution,[],[f42341,f41525]) ).
fof(f52736,plain,
( v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_71 ),
inference(resolution,[],[f42341,f52493]) ).
fof(f52740,plain,
( m2_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95)) ),
inference(resolution,[],[f42340,f41525]) ).
fof(f52742,plain,
( m2_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_71 ),
inference(resolution,[],[f42340,f52493]) ).
fof(f52779,plain,
( v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_60 ),
inference(resolution,[],[f52330,f41636]) ).
fof(f52780,plain,
( ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52779,f41524]) ).
fof(f52781,plain,
( ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52780,f41523]) ).
fof(f52782,plain,
( ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52781,f41522]) ).
fof(f52783,plain,
( ~ l1_group_1(sK95)
| spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52782,f41521]) ).
fof(f52784,plain,
( $false
| spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52783,f41520]) ).
fof(f52785,plain,
spl1241_60,
inference(avatar_contradiction_clause,[],[f52784]) ).
fof(f52846,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_69 ),
inference(superposition,[],[f52486,f52241]) ).
fof(f52847,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_69 ),
inference(forward_subsumption_resolution,[],[f52846,f41524]) ).
fof(f52849,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_69 ),
inference(forward_subsumption_resolution,[],[f52847,f41523]) ).
fof(f52851,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_69 ),
inference(forward_subsumption_resolution,[],[f52849,f41522]) ).
fof(f52853,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| ~ l1_group_1(sK95)
| spl1241_69 ),
inference(forward_subsumption_resolution,[],[f52851,f41521]) ).
fof(f52855,plain,
( ~ m1_subset_1(k6_autgroup(sK95,k2_group_1(sK95)),k4_autgroup(sK95))
| spl1241_69 ),
inference(forward_subsumption_resolution,[],[f52853,f41520]) ).
fof(f52872,plain,
( v3_struct_0(sK95)
| ~ l1_struct_0(sK95)
| ~ spl1241_58 ),
inference(resolution,[],[f52292,f46915]) ).
fof(f52873,plain,
( ~ l1_struct_0(sK95)
| ~ spl1241_58 ),
inference(forward_subsumption_resolution,[],[f52872,f41524]) ).
fof(f52880,plain,
l1_struct_0(sK95),
inference(resolution,[],[f46904,f41520]) ).
fof(f52881,plain,
( $false
| ~ spl1241_58 ),
inference(forward_subsumption_resolution,[],[f52880,f52873]) ).
fof(f52882,plain,
~ spl1241_58,
inference(avatar_contradiction_clause,[],[f52881]) ).
fof(f52884,plain,
( v1_funct_1(sK96)
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f52341,f52291]) ).
fof(f52885,plain,
( v1_xboole_0(u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_69
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52709,f52855]) ).
fof(f52886,plain,
( v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95)))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52708,f52291]) ).
fof(f52887,plain,
( v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52736,f52291]) ).
fof(f52888,plain,
( v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f52734,f52291]) ).
fof(f52889,plain,
( m2_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52742,f52291]) ).
fof(f52890,plain,
( m2_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f52740,f52291]) ).
fof(f52892,plain,
( v1_funct_1(sK96)
| spl1241_58
| ~ spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52884,f52329]) ).
fof(f52893,plain,
( ~ m1_fraenkel(k4_autgroup(sK95),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| spl1241_69
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52885,f52291]) ).
fof(f52894,plain,
( v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95)))
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52886,f52329]) ).
fof(f52895,plain,
( v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52887,f52329]) ).
fof(f52896,plain,
( v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52888,f52329]) ).
fof(f52897,plain,
( m2_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52889,f52329]) ).
fof(f52898,plain,
( m2_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_60 ),
inference(forward_subsumption_resolution,[],[f52890,f52329]) ).
fof(f52900,plain,
( spl1241_57
| spl1241_58
| ~ spl1241_60 ),
inference(avatar_split_clause,[],[f52892,f52328,f52290,f52286]) ).
fof(f52901,plain,
( $false
| spl1241_58
| ~ spl1241_60
| spl1241_69
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52893,f52329]) ).
fof(f52902,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_69
| ~ spl1241_71 ),
inference(avatar_contradiction_clause,[],[f52901]) ).
fof(f52903,plain,
( spl1241_54
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(avatar_split_clause,[],[f52894,f52492,f52328,f52290,f52274]) ).
fof(f52904,plain,
( spl1241_53
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(avatar_split_clause,[],[f52895,f52492,f52328,f52290,f52270]) ).
fof(f52905,plain,
( spl1241_56
| spl1241_58
| ~ spl1241_60 ),
inference(avatar_split_clause,[],[f52896,f52328,f52290,f52282]) ).
fof(f52955,plain,
( m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_69 ),
inference(superposition,[],[f52485,f41643]) ).
fof(f52957,plain,
( v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_69
| spl1241_73 ),
inference(forward_subsumption_resolution,[],[f52955,f52503]) ).
fof(f52958,plain,
( ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_69
| spl1241_73 ),
inference(forward_subsumption_resolution,[],[f52957,f41524]) ).
fof(f52959,plain,
( ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_69
| spl1241_73 ),
inference(forward_subsumption_resolution,[],[f52958,f41523]) ).
fof(f52960,plain,
( ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_69
| spl1241_73 ),
inference(forward_subsumption_resolution,[],[f52959,f41522]) ).
fof(f52961,plain,
( ~ l1_group_1(sK95)
| ~ spl1241_69
| spl1241_73 ),
inference(forward_subsumption_resolution,[],[f52960,f41521]) ).
fof(f52962,plain,
( $false
| ~ spl1241_69
| spl1241_73 ),
inference(forward_subsumption_resolution,[],[f52961,f41520]) ).
fof(f52963,plain,
( ~ spl1241_69
| spl1241_73 ),
inference(avatar_contradiction_clause,[],[f52962]) ).
fof(f52964,plain,
( m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_60 ),
inference(resolution,[],[f52898,f41983]) ).
fof(f52965,plain,
( spl1241_55
| spl1241_58
| ~ spl1241_60 ),
inference(avatar_split_clause,[],[f52964,f52328,f52290,f52278]) ).
fof(f52977,plain,
( m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(resolution,[],[f52897,f41983]) ).
fof(f52979,plain,
( $false
| spl1241_52
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(forward_subsumption_resolution,[],[f52977,f52268]) ).
fof(f52980,plain,
( spl1241_52
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(avatar_contradiction_clause,[],[f52979]) ).
fof(f52987,definition,
( spl1241_84
<=> m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95)) ),
introduced(definition,[new_symbols(definition,[spl1241_84])],[avatar_definition]) ).
fof(f52988,plain,
( m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ spl1241_84 ),
inference(avatar_component_clause,[],[f52987]) ).
fof(f52989,plain,
( ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_84 ),
inference(avatar_component_clause,[],[f52987]) ).
fof(f52995,definition,
( spl1241_86
<=> sK96 = k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95))) ),
introduced(definition,[new_symbols(definition,[spl1241_86])],[avatar_definition]) ).
fof(f52996,plain,
( sK96 = k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95)))
| ~ spl1241_86 ),
inference(avatar_component_clause,[],[f52995]) ).
fof(f52997,plain,
( sK96 != k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95)))
| spl1241_86 ),
inference(avatar_component_clause,[],[f52995]) ).
fof(f53006,plain,
( m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_52 ),
inference(superposition,[],[f52267,f41643]) ).
fof(f53007,plain,
( v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_52
| spl1241_84 ),
inference(forward_subsumption_resolution,[],[f53006,f52989]) ).
fof(f53008,plain,
( ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_52
| spl1241_84 ),
inference(forward_subsumption_resolution,[],[f53007,f41524]) ).
fof(f53009,plain,
( ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_52
| spl1241_84 ),
inference(forward_subsumption_resolution,[],[f53008,f41523]) ).
fof(f53010,plain,
( ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_52
| spl1241_84 ),
inference(forward_subsumption_resolution,[],[f53009,f41522]) ).
fof(f53011,plain,
( ~ l1_group_1(sK95)
| ~ spl1241_52
| spl1241_84 ),
inference(forward_subsumption_resolution,[],[f53010,f41521]) ).
fof(f53012,plain,
( $false
| ~ spl1241_52
| spl1241_84 ),
inference(forward_subsumption_resolution,[],[f53011,f41520]) ).
fof(f53013,plain,
( ~ spl1241_52
| spl1241_84 ),
inference(avatar_contradiction_clause,[],[f53012]) ).
fof(f53029,plain,
( sK96 != k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95)))
| v1_xboole_0(u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ v1_funct_1(k6_partfun1(u1_struct_0(sK95)))
| ~ v1_funct_2(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m2_fraenkel(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_74 ),
inference(superposition,[],[f52507,f52449]) ).
fof(f53148,plain,
( sK96 != sK96
| ~ m2_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_86 ),
inference(superposition,[],[f52997,f50246]) ).
fof(f53149,plain,
( ~ m2_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_86 ),
inference(trivial_inequality_removal,[],[f53148]) ).
fof(f53150,plain,
( $false
| spl1241_58
| ~ spl1241_60
| spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53149,f52898]) ).
fof(f53151,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_86 ),
inference(avatar_contradiction_clause,[],[f53150]) ).
fof(f53153,plain,
( sK96 != k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95)))
| v1_xboole_0(u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ v1_funct_2(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m2_fraenkel(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_74 ),
inference(forward_subsumption_resolution,[],[f53029,f44444]) ).
fof(f53156,plain,
( sK96 != k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95)))
| v1_xboole_0(u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m2_fraenkel(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_74 ),
inference(forward_subsumption_resolution,[],[f53153,f44443]) ).
fof(f53159,plain,
( sK96 != k5_relat_1(sK96,k6_partfun1(u1_struct_0(sK95)))
| v1_xboole_0(u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_74 ),
inference(forward_subsumption_resolution,[],[f53156,f41618]) ).
fof(f53162,plain,
( v1_xboole_0(u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_74
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53159,f52996]) ).
fof(f53165,plain,
( ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_58
| spl1241_74
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53162,f52291]) ).
fof(f53168,plain,
( ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_57
| spl1241_58
| spl1241_74
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53165,f52287]) ).
fof(f53170,plain,
( ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| spl1241_74
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53168,f52283]) ).
fof(f53172,plain,
( ~ m1_relset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| spl1241_74
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53170,f52279]) ).
fof(f53174,plain,
( ~ m2_fraenkel(sK96,u1_struct_0(sK95),u1_struct_0(sK95),k4_autgroup(sK95))
| ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53172,f52988]) ).
fof(f53176,plain,
( ~ m1_subset_1(sK96,u1_struct_0(k5_autgroup(sK95)))
| ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53174,f41525]) ).
fof(f53178,plain,
( ~ m1_subset_1(k6_partfun1(u1_struct_0(sK95)),u1_struct_0(k5_autgroup(sK95)))
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53176,f52489]) ).
fof(f53180,plain,
( v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53178,f52502]) ).
fof(f53182,plain,
( ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53180,f41524]) ).
fof(f53184,plain,
( ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53182,f41523]) ).
fof(f53186,plain,
( ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53184,f41522]) ).
fof(f53188,plain,
( ~ l1_group_1(sK95)
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53186,f41521]) ).
fof(f53190,plain,
( $false
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(forward_subsumption_resolution,[],[f53188,f41520]) ).
fof(f53191,plain,
( ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(avatar_contradiction_clause,[],[f53190]) ).
fof(f53198,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| v1_xboole_0(u1_struct_0(sK95))
| ~ v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95)))
| ~ v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47 ),
inference(superposition,[],[f52114,f41567]) ).
fof(f53199,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| ~ v1_funct_1(k6_autgroup(sK95,k2_group_1(sK95)))
| ~ v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53198,f52291]) ).
fof(f53203,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| ~ v1_funct_2(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47
| ~ spl1241_54
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53199,f52275]) ).
fof(f53207,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| ~ m1_relset_1(k6_autgroup(sK95,k2_group_1(sK95)),u1_struct_0(sK95),u1_struct_0(sK95))
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47
| ~ spl1241_53
| ~ spl1241_54
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53203,f52271]) ).
fof(f53211,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| ~ v1_funct_1(sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53207,f52267]) ).
fof(f53215,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| ~ v1_funct_2(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53211,f52287]) ).
fof(f53219,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| ~ m1_relset_1(sK96,u1_struct_0(sK95),u1_struct_0(sK95))
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53215,f52283]) ).
fof(f53222,plain,
( sK96 != k5_relat_1(k6_autgroup(sK95,k2_group_1(sK95)),sK96)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53219,f52279]) ).
fof(f53264,definition,
( spl1241_90
<=> sK96 = k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96) ),
introduced(definition,[new_symbols(definition,[spl1241_90])],[avatar_definition]) ).
fof(f53266,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| spl1241_90 ),
inference(avatar_component_clause,[],[f53264]) ).
fof(f53342,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| v3_struct_0(sK95)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(superposition,[],[f53222,f41643]) ).
fof(f53343,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ v1_group_1(sK95)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53342,f41524]) ).
fof(f53344,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ v3_group_1(sK95)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53343,f41523]) ).
fof(f53345,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ v4_group_1(sK95)
| ~ l1_group_1(sK95)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53344,f41522]) ).
fof(f53346,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| ~ l1_group_1(sK95)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53345,f41521]) ).
fof(f53347,plain,
( sK96 != k5_relat_1(k6_partfun1(u1_struct_0(sK95)),sK96)
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(forward_subsumption_resolution,[],[f53346,f41520]) ).
fof(f53348,plain,
( ~ spl1241_90
| spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58 ),
inference(avatar_split_clause,[],[f53347,f52290,f52286,f52282,f52278,f52274,f52270,f52266,f52112,f53264]) ).
fof(f53355,plain,
( ! [X0] :
( sK96 != sK96
| ~ m2_relset_1(sK96,u1_struct_0(sK95),X0) )
| spl1241_90 ),
inference(superposition,[],[f53266,f50244]) ).
fof(f53356,plain,
( ! [X0] : ~ m2_relset_1(sK96,u1_struct_0(sK95),X0)
| spl1241_90 ),
inference(trivial_inequality_removal,[],[f53355]) ).
fof(f53358,plain,
( $false
| spl1241_58
| ~ spl1241_60
| spl1241_90 ),
inference(resolution,[],[f53356,f52898]) ).
fof(f53359,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_90 ),
inference(avatar_contradiction_clause,[],[f53358]) ).
cnf(s34,plain,
( ~ spl1241_46
| ~ spl1241_47 ),
inference(sat_conversion,[],[f52115]) ).
cnf(s41,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_61 ),
inference(sat_conversion,[],[f52335]) ).
cnf(s47,plain,
( spl1241_46
| ~ spl1241_70
| ~ spl1241_73
| ~ spl1241_74 ),
inference(sat_conversion,[],[f52508]) ).
cnf(s48,plain,
( ~ spl1241_61
| spl1241_70 ),
inference(sat_conversion,[],[f52600]) ).
cnf(s51,plain,
spl1241_71,
inference(sat_conversion,[],[f52706]) ).
cnf(s52,plain,
spl1241_60,
inference(sat_conversion,[],[f52785]) ).
cnf(s55,plain,
~ spl1241_58,
inference(sat_conversion,[],[f52882]) ).
cnf(s56,plain,
( spl1241_57
| spl1241_58
| ~ spl1241_60 ),
inference(sat_conversion,[],[f52900]) ).
cnf(s57,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_69
| ~ spl1241_71 ),
inference(sat_conversion,[],[f52902]) ).
cnf(s58,plain,
( spl1241_54
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(sat_conversion,[],[f52903]) ).
cnf(s59,plain,
( spl1241_53
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(sat_conversion,[],[f52904]) ).
cnf(s60,plain,
( spl1241_56
| spl1241_58
| ~ spl1241_60 ),
inference(sat_conversion,[],[f52905]) ).
cnf(s64,plain,
( ~ spl1241_69
| spl1241_73 ),
inference(sat_conversion,[],[f52963]) ).
cnf(s65,plain,
( spl1241_55
| spl1241_58
| ~ spl1241_60 ),
inference(sat_conversion,[],[f52965]) ).
cnf(s66,plain,
( spl1241_52
| spl1241_58
| ~ spl1241_60
| ~ spl1241_71 ),
inference(sat_conversion,[],[f52980]) ).
cnf(s69,plain,
( ~ spl1241_52
| spl1241_84 ),
inference(sat_conversion,[],[f53013]) ).
cnf(s70,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_86 ),
inference(sat_conversion,[],[f53151]) ).
cnf(s71,plain,
( ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_70
| ~ spl1241_73
| spl1241_74
| ~ spl1241_84
| ~ spl1241_86 ),
inference(sat_conversion,[],[f53191]) ).
cnf(s77,plain,
( spl1241_47
| ~ spl1241_52
| ~ spl1241_53
| ~ spl1241_54
| ~ spl1241_55
| ~ spl1241_56
| ~ spl1241_57
| spl1241_58
| ~ spl1241_90 ),
inference(sat_conversion,[],[f53348]) ).
cnf(s78,plain,
( spl1241_58
| ~ spl1241_60
| spl1241_90 ),
inference(sat_conversion,[],[f53359]) ).
cnf(s79,plain,
spl1241_90,
inference(rat,[],[s78,s55,s52]) ).
cnf(s80,plain,
spl1241_86,
inference(rat,[],[s70,s55,s52]) ).
cnf(s81,plain,
spl1241_55,
inference(rat,[],[s65,s55,s52]) ).
cnf(s82,plain,
spl1241_56,
inference(rat,[],[s60,s55,s52]) ).
cnf(s83,plain,
spl1241_57,
inference(rat,[],[s56,s55,s52]) ).
cnf(s85,plain,
spl1241_69,
inference(rat,[],[s57,s52,s55,s51]) ).
cnf(s86,plain,
spl1241_52,
inference(rat,[],[s66,s52,s55,s51]) ).
cnf(s87,plain,
spl1241_53,
inference(rat,[],[s59,s52,s55,s51]) ).
cnf(s88,plain,
spl1241_54,
inference(rat,[],[s58,s52,s55,s51]) ).
cnf(s89,plain,
spl1241_73,
inference(rat,[],[s64,s85]) ).
cnf(s91,plain,
spl1241_47,
inference(rat,[],[s77,s79,s55,s83,s82,s81,s88,s87,s86]) ).
cnf(s92,plain,
spl1241_84,
inference(rat,[],[s69,s86]) ).
cnf(s94,plain,
( spl1241_46
| ~ spl1241_70
| ~ spl1241_74 ),
inference(rat,[],[s47,s89]) ).
cnf(s96,plain,
spl1241_61,
inference(rat,[],[s41,s52,s55]) ).
cnf(s97,plain,
spl1241_70,
inference(rat,[],[s48,s96]) ).
cnf(s98,plain,
spl1241_74,
inference(rat,[],[s71,s80,s92,s89,s82,s81,s55,s83,s97]) ).
cnf(s100,plain,
spl1241_46,
inference(rat,[],[s94,s98,s97]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s34,s91,s100]) ).
fof(f53360,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP632+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n020.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 10:17:12 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.21/4.85 % (3170968)Detected formulas, will run a generic FOF schedule.
% 15.21/4.85 % (3170976)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3720298008:i=109:sd=1:ins=1:gsp=on:ss=axioms_2979 on theBenchmark for (2979ds/109Mi)
% 15.21/4.85 % (3170975)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=61389938:i=141695:sd=1:nm=32:gsp=on:ss=included_2979 on theBenchmark for (2979ds/141695Mi)
% 15.21/4.85 % (3170974)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=2024877038:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2979 on theBenchmark for (2979ds/134677Mi)
% 15.21/4.85 % (3170973)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=1425324698:i=141193_2979 on theBenchmark for (2979ds/141193Mi)
% 15.21/4.85 % (3170976)Instruction limit reached!
% 15.21/4.85 % (3170976)------------------------------
% 15.21/4.85 % (3170976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/4.85 % (3170976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/4.85 % (3170976)CaDiCaL version: 2.1.3
% 15.21/4.85 % (3170976)Termination reason: Instruction limit
% 15.21/4.85 % (3170976)Termination phase: SInE selection
% 15.21/4.85 % (3170976)Time elapsed: 0.049 s
% 15.21/4.85 % (3170976)Peak memory usage: 133 MB
% 15.21/4.85 % (3170976)Instructions burned: 111 (million)
% 15.21/4.85 % (3170977)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=275308432:i=119:av=off:ss=axioms_2979 on theBenchmark for (2979ds/119Mi)
% 15.21/4.85 % (3170978)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2884749150:s2a=on:i=139:gtg=position_2979 on theBenchmark for (2979ds/139Mi)
% 15.21/4.85 % (3170979)dis-21_1_sil=8000:lcm=predicate:random_seed=2301271471:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2979 on theBenchmark for (2979ds/129Mi)
% 15.21/4.85 % (3170978)Instruction limit reached!
% 15.21/4.85 % (3170978)------------------------------
% 15.21/4.85 % (3170978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/4.85 % (3170978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/4.85 % (3170978)CaDiCaL version: 2.1.3
% 15.21/4.85 % (3170978)Termination reason: Instruction limit
% 15.21/4.85 % (3170978)Termination phase: Property scanning
% 15.21/4.85 % (3170978)Time elapsed: 0.063 s
% 15.21/4.85 % (3170978)Peak memory usage: 133 MB
% 15.21/4.85 % (3170978)Instructions burned: 141 (million)
% 15.21/4.85 % (3170977)Instruction limit reached!
% 15.21/4.85 % (3170977)------------------------------
% 15.21/4.85 % (3170977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/4.85 % (3170977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/4.85 % (3170977)CaDiCaL version: 2.1.3
% 15.21/4.85 % (3170977)Termination reason: Instruction limit
% 15.21/4.85 % (3170977)Termination phase: SInE selection
% 15.21/4.85 % (3170977)Time elapsed: 0.091 s
% 15.21/4.85 % (3170977)Peak memory usage: 133 MB
% 15.21/4.85 % (3170977)Instructions burned: 119 (million)
% 15.21/4.85 % (3170979)Instruction limit reached!
% 15.21/4.85 % (3170979)------------------------------
% 15.21/4.85 % (3170979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/4.85 % (3170979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/4.85 % (3170979)CaDiCaL version: 2.1.3
% 15.21/4.85 % (3170979)Termination reason: Instruction limit
% 15.21/4.85 % (3170979)Termination phase: SInE selection
% 15.21/4.85 % (3170979)Time elapsed: 0.094 s
% 15.21/4.85 % (3170979)Peak memory usage: 133 MB
% 15.21/4.85 % (3170979)Instructions burned: 130 (million)
% 15.21/4.85 % (3170984)lrs+10_1_sil=8000:sp=occurrence:random_seed=927904180:i=285:sd=3:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/285Mi)
% 15.21/4.85 % (3170988)lrs+10_1_sil=32000:urr=on:br=off:random_seed=788648782:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 15.21/4.85 % (3170984)Instruction limit reached!
% 15.21/4.85 % (3170984)------------------------------
% 15.21/4.85 % (3170984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.21/4.85 % (3170984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.21/4.85 % (3170984)CaDiCaL version: 2.1.3
% 15.21/4.85 % (3170984)Termination reason: Instruction limit
% 24.97/6.16 % (3170984)Termination phase: Property scanning
% 24.97/6.16 % (3170984)Time elapsed: 0.136 s
% 24.97/6.16 % (3170984)Peak memory usage: 138 MB
% 24.97/6.16 % (3170984)Instructions burned: 289 (million)
% 24.97/6.16 % (3170989)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1868787572:i=325:sd=1:ss=axioms:sgt=32_2976 on theBenchmark for (2976ds/325Mi)
% 24.97/6.16 % (3170990)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=3568934581:s2a=on:i=248:s2at=1.23:gtg=position_2976 on theBenchmark for (2976ds/248Mi)
% 24.97/6.16 % (3170988)Instruction limit reached!
% 24.97/6.16 % (3170988)------------------------------
% 24.97/6.16 % (3170988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.97/6.16 % (3170988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.97/6.16 % (3170988)CaDiCaL version: 2.1.3
% 24.97/6.16 % (3170988)Termination reason: Instruction limit
% 24.97/6.16 % (3170988)Termination phase: Property scanning
% 24.97/6.16 % (3170988)Time elapsed: 0.071 s
% 24.97/6.16 % (3170988)Peak memory usage: 133 MB
% 24.97/6.16 % (3170988)Instructions burned: 159 (million)
% 24.97/6.16 % (3170990)Instruction limit reached!
% 24.97/6.16 % (3170990)------------------------------
% 24.97/6.16 % (3170990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.97/6.16 % (3170990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.97/6.16 % (3170990)CaDiCaL version: 2.1.3
% 24.97/6.16 % (3170990)Termination reason: Instruction limit
% 24.97/6.16 % (3170990)Termination phase: Property scanning
% 24.97/6.16 % (3170990)Time elapsed: 0.107 s
% 24.97/6.16 % (3170990)Peak memory usage: 133 MB
% 24.97/6.16 % (3170990)Instructions burned: 248 (million)
% 24.97/6.16 % (3170995)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4282094909:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2974 on theBenchmark for (2974ds/294Mi)
% 24.97/6.16 % (3170996)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=438681926:i=2350_2974 on theBenchmark for (2974ds/2350Mi)
% 24.97/6.16 % (3170995)Instruction limit reached!
% 24.97/6.16 % (3170995)------------------------------
% 24.97/6.16 % (3170995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.97/6.16 % (3170995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.97/6.16 % (3170995)CaDiCaL version: 2.1.3
% 24.97/6.16 % (3170995)Termination reason: Instruction limit
% 24.97/6.16 % (3170995)Termination phase: SInE selection
% 24.97/6.16 % (3170995)Time elapsed: 0.103 s
% 24.97/6.16 % (3170995)Peak memory usage: 134 MB
% 24.97/6.16 % (3170995)Instructions burned: 295 (million)
% 24.97/6.16 % (3170989)Instruction limit reached!
% 24.97/6.16 % (3170989)------------------------------
% 24.97/6.16 % (3170989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.97/6.16 % (3170989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.97/6.16 % (3170989)CaDiCaL version: 2.1.3
% 24.97/6.16 % (3170989)Termination reason: Instruction limit
% 24.97/6.16 % (3170989)Termination phase: Saturation
% 24.97/6.16 % (3170989)Time elapsed: 0.257 s
% 24.97/6.16 % (3170989)Peak memory usage: 140 MB
% 24.97/6.16 % (3170989)Instructions burned: 326 (million)
% 24.97/6.16 % (3170997)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3419459165:cts=off:i=113:fsr=off:ss=included:sgt=4_2973 on theBenchmark for (2973ds/113Mi)
% 24.97/6.16 % (3171000)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4242561148:i=127:av=off:fsr=off:sup=off_2972 on theBenchmark for (2972ds/127Mi)
% 24.97/6.16 % (3170997)Instruction limit reached!
% 24.97/6.16 % (3170997)------------------------------
% 24.97/6.16 % (3170997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.97/6.16 % (3170997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.97/6.16 % (3170997)CaDiCaL version: 2.1.3
% 24.97/6.16 % (3170997)Termination reason: Instruction limit
% 24.97/6.16 % (3170997)Termination phase: SInE selection
% 24.97/6.16 % (3170997)Time elapsed: 0.086 s
% 24.97/6.16 % (3170997)Peak memory usage: 133 MB
% 24.97/6.16 % (3170997)Instructions burned: 114 (million)
% 24.97/6.16 % (3171000)Instruction limit reached!
% 24.97/6.16 % (3171000)------------------------------
% 24.97/6.16 % (3171000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.97/6.16 % (3171000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.97/6.16 % (3171000)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171000)Termination reason: Instruction limit
% 16.67/7.53 % (3171000)Termination phase: Preprocessing 1
% 16.67/7.53 % (3171000)Time elapsed: 0.056 s
% 16.67/7.53 % (3171000)Peak memory usage: 136 MB
% 16.67/7.53 % (3171000)Instructions burned: 129 (million)
% 16.67/7.53 % (3171001)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1398189269:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2972 on theBenchmark for (2972ds/114Mi)
% 16.67/7.53 % (3171001)Instruction limit reached!
% 16.67/7.53 % (3171001)------------------------------
% 16.67/7.53 % (3171001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171001)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171001)Termination reason: Instruction limit
% 16.67/7.53 % (3171001)Termination phase: Property scanning
% 16.67/7.53 % (3171001)Time elapsed: 0.053 s
% 16.67/7.53 % (3171001)Peak memory usage: 133 MB
% 16.67/7.53 % (3171001)Instructions burned: 115 (million)
% 16.67/7.53 % (3171004)lrs+10_1_sil=8000:sp=occurrence:random_seed=1686857721:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2971 on theBenchmark for (2971ds/907Mi)
% 16.67/7.53 % (3171005)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3988073381:i=437:sd=1:aac=none:ss=included_2970 on theBenchmark for (2970ds/437Mi)
% 16.67/7.53 % (3171007)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3083466008:i=5202:ss=axioms:sgt=16_2969 on theBenchmark for (2969ds/5202Mi)
% 16.67/7.53 % (3171005)Instruction limit reached!
% 16.67/7.53 % (3171005)------------------------------
% 16.67/7.53 % (3171005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171005)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171005)Termination reason: Instruction limit
% 16.67/7.53 % (3171005)Termination phase: Saturation
% 16.67/7.53 % (3171005)Time elapsed: 0.173 s
% 16.67/7.53 % (3171005)Peak memory usage: 141 MB
% 16.67/7.53 % (3171005)Instructions burned: 438 (million)
% 16.67/7.53 % (3171011)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3610765577:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2967 on theBenchmark for (2967ds/134Mi)
% 16.67/7.53 % (3171011)Instruction limit reached!
% 16.67/7.53 % (3171011)------------------------------
% 16.67/7.53 % (3171011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171011)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171011)Termination reason: Instruction limit
% 16.67/7.53 % (3171011)Termination phase: SInE selection
% 16.67/7.53 % (3171011)Time elapsed: 0.057 s
% 16.67/7.53 % (3171011)Peak memory usage: 133 MB
% 16.67/7.53 % (3171011)Instructions burned: 135 (million)
% 16.67/7.53 % (3171013)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=67709276:st=8:i=592:sd=3:ep=RST:ss=axioms_2965 on theBenchmark for (2965ds/592Mi)
% 16.67/7.53 % (3171004)Instruction limit reached!
% 16.67/7.53 % (3171004)------------------------------
% 16.67/7.53 % (3171004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171004)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171004)Termination reason: Instruction limit
% 16.67/7.53 % (3171004)Termination phase: Property scanning
% 16.67/7.53 % (3171004)Time elapsed: 0.591 s
% 16.67/7.53 % (3171004)Peak memory usage: 154 MB
% 16.67/7.53 % (3171004)Instructions burned: 907 (million)
% 16.67/7.53 % (3171015)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1310442034:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 16.67/7.53 % (3171013)Instruction limit reached!
% 16.67/7.53 % (3171013)------------------------------
% 16.67/7.53 % (3171013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171013)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171013)Termination reason: Instruction limit
% 16.67/7.53 % (3171013)Termination phase: Preprocessing 2
% 16.67/7.53 % (3171013)Time elapsed: 0.268 s
% 16.67/7.53 % (3171013)Peak memory usage: 141 MB
% 16.67/7.53 % (3171013)Instructions burned: 592 (million)
% 16.67/7.53 % (3171017)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=1626035203:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/125Mi)
% 16.67/7.53 % (3171017)Instruction limit reached!
% 16.67/7.53 % (3171017)------------------------------
% 16.67/7.53 % (3171017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171017)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171017)Termination reason: Instruction limit
% 16.67/7.53 % (3171017)Termination phase: Property scanning
% 16.67/7.53 % (3171017)Time elapsed: 0.031 s
% 16.67/7.53 % (3171017)Peak memory usage: 133 MB
% 16.67/7.53 % (3171017)Instructions burned: 128 (million)
% 16.67/7.53 % (3171019)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2704110543:i=134:gtgl=5:slsql=off:gtg=exists_sym_2959 on theBenchmark for (2959ds/134Mi)
% 16.67/7.53 % (3171019)Instruction limit reached!
% 16.67/7.53 % (3171019)------------------------------
% 16.67/7.53 % (3171019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171019)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171019)Termination reason: Instruction limit
% 16.67/7.53 % (3171019)Termination phase: Property scanning
% 16.67/7.53 % (3171019)Time elapsed: 0.033 s
% 16.67/7.53 % (3171019)Peak memory usage: 133 MB
% 16.67/7.53 % (3171019)Instructions burned: 137 (million)
% 16.67/7.53 % (3171021)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3542669317:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/141Mi)
% 16.67/7.53 % (3170996)Instruction limit reached!
% 16.67/7.53 % (3170996)------------------------------
% 16.67/7.53 % (3170996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3170996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3170996)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3170996)Termination reason: Instruction limit
% 16.67/7.53 % (3170996)Termination phase: Property scanning
% 16.67/7.53 % (3170996)Time elapsed: 1.572 s
% 16.67/7.53 % (3170996)Peak memory usage: 227 MB
% 16.67/7.53 % (3170996)Instructions burned: 2350 (million)
% 16.67/7.53 % (3171021)Instruction limit reached!
% 16.67/7.53 % (3171021)------------------------------
% 16.67/7.53 % (3171021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171021)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171021)Termination reason: Instruction limit
% 16.67/7.53 % (3171021)Termination phase: SInE selection
% 16.67/7.53 % (3171021)Time elapsed: 0.061 s
% 16.67/7.53 % (3171021)Peak memory usage: 133 MB
% 16.67/7.53 % (3171021)Instructions burned: 143 (million)
% 16.67/7.53 % (3171024)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=3886669801:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 16.67/7.53 % (3171023)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1438983755:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2956 on theBenchmark for (2956ds/431Mi)
% 16.67/7.53 % (3171023)Refutation not found, incomplete strategy
% 16.67/7.53 % (3171023)------------------------------
% 16.67/7.53 % (3171023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171023)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171023)Termination reason: Refutation not found, incomplete strategy
% 16.67/7.53 % (3171023)Time elapsed: 0.196 s
% 16.67/7.53 % (3171023)Peak memory usage: 139 MB
% 16.67/7.53 % (3171023)Instructions burned: 235 (million)
% 16.67/7.53 % (3171023)------------------------------
% 16.67/7.53 % (3171023)------------------------------
% 16.67/7.53 % (3171027)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=1134631750:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 16.67/7.53 % (3171027)Instruction limit reached!
% 16.67/7.53 % (3171027)------------------------------
% 16.67/7.53 % (3171027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171027)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171027)Termination reason: Instruction limit
% 16.67/7.53 % (3171027)Termination phase: SInE selection
% 16.67/7.53 % (3171027)Time elapsed: 0.117 s
% 16.67/7.53 % (3171027)Peak memory usage: 133 MB
% 16.67/7.53 % (3171027)Instructions burned: 150 (million)
% 16.67/7.53 % (3171029)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3464489084:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 16.67/7.53 % (3171007)First to succeed.
% 16.67/7.53 % (3171007)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3170968"
% 16.67/7.53 % (3171024)Instruction limit reached!
% 16.67/7.53 % (3171024)------------------------------
% 16.67/7.53 % (3171024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/7.53 % (3171024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/7.53 % (3171024)CaDiCaL version: 2.1.3
% 16.67/7.53 % (3171024)Termination reason: Instruction limit
% 16.67/7.53 % (3171024)Termination phase: Function definition elimination
% 16.67/7.53 % (3171024)Time elapsed: 2.080 s
% 16.67/7.53 % (3171024)Peak memory usage: 244 MB
% 16.67/7.53 % (3171024)Instructions burned: 6062 (million)
% 16.67/7.53 % (3171007)Refutation found. Thanks to Tanya!
% 16.67/7.53 % SZS status Theorem for theBenchmark
% 16.67/7.53 % SZS output start Proof for theBenchmark
% See solution above
% 35.01/7.77 % (3171007)------------------------------
% 35.01/7.77 % (3171007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.01/7.77 % (3171007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.01/7.77 % (3171007)CaDiCaL version: 2.1.3
% 35.01/7.77 % (3171007)Termination reason: Refutation
% 35.01/7.77 % (3171007)Time elapsed: 3.115 s
% 35.01/7.77 % (3171007)Peak memory usage: 300 MB
% 35.01/7.77 % (3171007)Instructions burned: 5039 (million)
% 35.01/7.77 % (3171007)------------------------------
% 35.01/7.77 % (3171007)------------------------------
% 35.01/7.77 % (3170968)Success in time 6.651 s
% 35.01/7.77 % Vampire exiting
%------------------------------------------------------------------------------