%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP620+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:18:15 AM UTC 2026
% Result : Theorem 0.18s 0.48s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 28
% Syntax : Number of formulae : 228 ( 33 unt; 15 def)
% Number of atoms : 1189 ( 18 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 1673 ( 712 ~; 761 |; 139 &)
% ( 31 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 15 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 179 ( 0 sgn 172 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> m2_fraenkel(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_autgroup) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> m2_fraenkel(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) ) )
& ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X2,X1)
<=> ( v2_funct_1(X2)
& v3_group_6(X2,X0,X0) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_autgroup) ).
fof(f17,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_autgroup) ).
fof(f22,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f24,axiom,
! [X0,X1,X2] :
( m1_fraenkel(X2,X0,X1)
=> ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
fof(f27,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/sandbox2/benchmark/theBenchmark.p',dt_m2_fraenkel) ).
fof(f39,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f57,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f60,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f61,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f64,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X1,X0,X0)
& m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_autgroup) ).
fof(f66,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
=> ( v1_funct_1(k2_funct_1(X1))
& v1_funct_2(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k2_funct_1(X1),X0,X0)
& m2_relset_1(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_autgroup) ).
fof(f68,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
& v1_group_6(X2,X1,X0)
& m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( ( v4_group_6(X2,X1,X0)
& X3 = k2_funct_1(X2) )
=> v4_group_6(X3,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t73_group_6) ).
fof(f71,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
=> ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1)
=> ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) ) )
& ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
=> ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) ) ) ) ) ) ),
inference(rectify,[],[f15]) ).
fof(f76,plain,
? [X0] :
( ? [X1] :
( ~ m2_fraenkel(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f77,plain,
? [X0] :
( ? [X1] :
( ~ m2_fraenkel(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
& m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
& ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f76]) ).
fof(f98,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f99,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f98]) ).
fof(f102,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f103,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f102]) ).
fof(f106,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f108,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,[],[f27]) ).
fof(f109,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,[],[f108]) ).
fof(f116,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f117,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f116]) ).
fof(f124,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,[],[f57]) ).
fof(f125,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,[],[f124]) ).
fof(f126,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f127,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f61]) ).
fof(f128,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f127]) ).
fof(f132,plain,
! [X0] :
( ! [X1] :
( ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f133,plain,
! [X0] :
( ! [X1] :
( ( r2_hidden(X1,k1_autgroup(X0))
<=> v4_group_6(X1,X0,X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f132]) ).
fof(f135,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(k2_funct_1(X1))
& v1_funct_2(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k2_funct_1(X1),X0,X0)
& m2_relset_1(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f66]) ).
fof(f136,plain,
! [X0] :
( ! [X1] :
( ( v1_funct_1(k2_funct_1(X1))
& v1_funct_2(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k2_funct_1(X1),X0,X0)
& m2_relset_1(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f135]) ).
fof(f138,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v4_group_6(X3,X0,X1)
| ~ v4_group_6(X2,X1,X0)
| k2_funct_1(X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_group_6(X2,X1,X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f139,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( v4_group_6(X3,X0,X1)
| ~ v4_group_6(X2,X1,X0)
| k2_funct_1(X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_group_6(X2,X1,X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f138]) ).
fof(f142,definition,
! [X0,X1] :
( sP0(X0,X1)
<=> ! [X3] :
( ( r2_hidden(X3,X1)
<=> ( v2_funct_1(X3)
& v3_group_6(X3,X0,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X3,X0,X0)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f143,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_autgroup(X0)
<=> ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP0(X0,X1) ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(definition_folding,[],[f99,f142]) ).
fof(f144,plain,
( ~ m2_fraenkel(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1),k1_autgroup(sK1))
& m2_fraenkel(sK2,u1_struct_0(sK1),u1_struct_0(sK1),k1_autgroup(sK1))
& ~ v3_struct_0(sK1)
& v1_group_1(sK1)
& v3_group_1(sK1)
& v4_group_1(sK1)
& l1_group_1(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f77]) ).
fof(f152,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP0(X0,X1) )
& ( ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP0(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f143]) ).
fof(f153,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP0(X0,X1) )
& ( ( ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X2,X0,X0)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP0(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f152]) ).
fof(f154,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ? [X2] :
( ( ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X0)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP0(X0,X1) )
& ( ( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP0(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f153]) ).
fof(f155,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k1_autgroup(X0)
| ( ( ~ v1_funct_1(sK4(X0,X1))
| ~ v1_funct_2(sK4(X0,X1),u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(sK4(X0,X1),X0,X0)
| ~ m2_relset_1(sK4(X0,X1),u1_struct_0(X0),u1_struct_0(X0)) )
& m2_fraenkel(sK4(X0,X1),u1_struct_0(X0),u1_struct_0(X0),X1) )
| ~ sP0(X0,X1) )
& ( ( ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(X3,X0,X0)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1) )
& sP0(X0,X1) )
| k1_autgroup(X0) != X1 ) )
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f154]) ).
fof(f178,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,[],[f125]) ).
fof(f180,plain,
! [X0] :
( ! [X1] :
( ( ( r2_hidden(X1,k1_autgroup(X0))
| ~ v4_group_6(X1,X0,X0) )
& ( v4_group_6(X1,X0,X0)
| ~ r2_hidden(X1,k1_autgroup(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f133]) ).
fof(f181,plain,
l1_group_1(sK1),
inference(cnf_transformation,[],[f144]) ).
fof(f182,plain,
v4_group_1(sK1),
inference(cnf_transformation,[],[f144]) ).
fof(f183,plain,
v3_group_1(sK1),
inference(cnf_transformation,[],[f144]) ).
fof(f184,plain,
v1_group_1(sK1),
inference(cnf_transformation,[],[f144]) ).
fof(f185,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f144]) ).
fof(f186,plain,
m2_fraenkel(sK2,u1_struct_0(sK1),u1_struct_0(sK1),k1_autgroup(sK1)),
inference(cnf_transformation,[],[f144]) ).
fof(f187,plain,
~ m2_fraenkel(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1),k1_autgroup(sK1)),
inference(cnf_transformation,[],[f144]) ).
fof(f224,plain,
! [X3,X0,X1] :
( v1_group_6(X3,X0,X0)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),X1)
| k1_autgroup(X0) != X1
| ~ m1_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f231,plain,
! [X0] :
( m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f234,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f106]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f237,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,[],[f109]) ).
fof(f238,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,[],[f109]) ).
fof(f239,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,[],[f109]) ).
fof(f253,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f301,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,[],[f178]) ).
fof(f302,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,[],[f178]) ).
fof(f306,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f307,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f128]) ).
fof(f310,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ r2_hidden(X1,k1_autgroup(X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| v4_group_6(X1,X0,X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f311,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v4_group_6(X1,X0,X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(X0))
| ~ v1_group_6(X1,X0,X0)
| r2_hidden(X1,k1_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,[],[f180]) ).
fof(f313,plain,
! [X0,X1] :
( ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| m2_relset_1(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f314,plain,
! [X0,X1] :
( ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_group_6(k2_funct_1(X1),X0,X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f315,plain,
! [X0,X1] :
( ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_funct_2(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f316,plain,
! [X0,X1] :
( ~ m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_funct_1(k2_funct_1(X1))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f318,plain,
! [X2,X3,X0,X1] :
( v4_group_6(X3,X0,X1)
| ~ v4_group_6(X2,X1,X0)
| k2_funct_1(X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_group_6(X2,X1,X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f323,plain,
! [X3,X0] :
( v1_group_6(X3,X0,X0)
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f224]) ).
fof(f326,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(k2_funct_1(X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v4_group_6(X2,X1,X0)
| ~ v1_funct_1(k2_funct_1(X2))
| ~ v1_funct_2(k2_funct_1(X2),u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(k2_funct_1(X2),X0,X1)
| v4_group_6(k2_funct_1(X2),X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ v1_group_6(X2,X1,X0)
| ~ m2_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f318]) ).
fof(f331,plain,
l1_struct_0(sK1),
inference(resolution,[],[f234,f181]) ).
fof(f432,plain,
( v1_funct_1(sK2)
| v1_xboole_0(u1_struct_0(sK1))
| ~ m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(resolution,[],[f239,f186]) ).
fof(f434,definition,
( spl27_3
<=> m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition]) ).
fof(f435,plain,
( m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ spl27_3 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( ~ m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1))
| spl27_3 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl27_4
<=> v1_xboole_0(u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
fof(f440,plain,
( v1_xboole_0(u1_struct_0(sK1))
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f442,definition,
( spl27_5
<=> v1_funct_1(sK2) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
fof(f444,plain,
( v1_funct_1(sK2)
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f445,plain,
( ~ spl27_3
| spl27_4
| spl27_5 ),
inference(avatar_split_clause,[],[f432,f442,f438,f434]) ).
fof(f458,plain,
( m1_subset_1(sK2,k1_autgroup(sK1))
| v1_xboole_0(u1_struct_0(sK1))
| ~ m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(resolution,[],[f301,f186]) ).
fof(f461,plain,
( ~ m1_subset_1(k2_funct_1(sK2),k1_autgroup(sK1))
| v1_xboole_0(u1_struct_0(sK1))
| ~ m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(resolution,[],[f302,f187]) ).
fof(f466,plain,
( m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v1_xboole_0(u1_struct_0(sK1))
| ~ m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(resolution,[],[f237,f186]) ).
fof(f471,plain,
( v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v1_xboole_0(u1_struct_0(sK1))
| ~ m1_fraenkel(k1_autgroup(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(resolution,[],[f238,f186]) ).
fof(f519,plain,
( v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| spl27_3 ),
inference(resolution,[],[f231,f436]) ).
fof(f522,plain,
( ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f519,f185]) ).
fof(f523,plain,
( ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f522,f184]) ).
fof(f524,plain,
( ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f523,f183]) ).
fof(f525,plain,
( ~ l1_group_1(sK1)
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f524,f182]) ).
fof(f526,plain,
( $false
| spl27_3 ),
inference(forward_subsumption_resolution,[],[f525,f181]) ).
fof(f527,plain,
spl27_3,
inference(avatar_contradiction_clause,[],[f526]) ).
fof(f529,definition,
( spl27_9
<=> m1_subset_1(sK2,k1_autgroup(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
fof(f531,plain,
( m1_subset_1(sK2,k1_autgroup(sK1))
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f532,plain,
( ~ spl27_3
| spl27_4
| spl27_9 ),
inference(avatar_split_clause,[],[f458,f529,f438,f434]) ).
fof(f534,definition,
( spl27_10
<=> m1_subset_1(k2_funct_1(sK2),k1_autgroup(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
fof(f536,plain,
( ~ m1_subset_1(k2_funct_1(sK2),k1_autgroup(sK1))
| spl27_10 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f537,plain,
( ~ spl27_3
| spl27_4
| ~ spl27_10 ),
inference(avatar_split_clause,[],[f461,f534,f438,f434]) ).
fof(f539,definition,
( spl27_11
<=> m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
fof(f541,plain,
( m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f542,plain,
( ~ spl27_3
| spl27_4
| spl27_11 ),
inference(avatar_split_clause,[],[f466,f539,f438,f434]) ).
fof(f544,definition,
( spl27_12
<=> v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition]) ).
fof(f546,plain,
( v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ spl27_12 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( ~ spl27_3
| spl27_4
| spl27_12 ),
inference(avatar_split_clause,[],[f471,f544,f438,f434]) ).
fof(f548,plain,
( v3_struct_0(sK1)
| ~ l1_struct_0(sK1)
| ~ spl27_4 ),
inference(resolution,[],[f440,f253]) ).
fof(f563,plain,
( ~ l1_struct_0(sK1)
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f548,f185]) ).
fof(f564,plain,
( $false
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f563,f331]) ).
fof(f565,plain,
~ spl27_4,
inference(avatar_contradiction_clause,[],[f564]) ).
fof(f573,plain,
( r2_hidden(sK2,k1_autgroup(sK1))
| v1_xboole_0(k1_autgroup(sK1))
| ~ spl27_9 ),
inference(resolution,[],[f531,f307]) ).
fof(f586,definition,
( spl27_17
<=> v1_xboole_0(k1_autgroup(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_17])],[avatar_definition]) ).
fof(f590,definition,
( spl27_18
<=> r2_hidden(sK2,k1_autgroup(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_18])],[avatar_definition]) ).
fof(f593,plain,
( spl27_17
| spl27_18
| ~ spl27_9 ),
inference(avatar_split_clause,[],[f573,f529,f590,f586]) ).
fof(f633,plain,
( v1_funct_1(k2_funct_1(sK2))
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f316,f186]) ).
fof(f638,plain,
( v1_funct_1(k2_funct_1(sK2))
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f633,f185]) ).
fof(f639,plain,
( v1_funct_1(k2_funct_1(sK2))
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f638,f184]) ).
fof(f640,plain,
( v1_funct_1(k2_funct_1(sK2))
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f639,f183]) ).
fof(f641,plain,
( v1_funct_1(k2_funct_1(sK2))
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f640,f182]) ).
fof(f642,plain,
v1_funct_1(k2_funct_1(sK2)),
inference(forward_subsumption_resolution,[],[f641,f181]) ).
fof(f647,plain,
( v1_group_6(k2_funct_1(sK2),sK1,sK1)
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f314,f186]) ).
fof(f652,plain,
( v1_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f647,f185]) ).
fof(f653,plain,
( v1_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f652,f184]) ).
fof(f654,plain,
( v1_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f653,f183]) ).
fof(f655,plain,
( v1_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f654,f182]) ).
fof(f656,plain,
v1_group_6(k2_funct_1(sK2),sK1,sK1),
inference(forward_subsumption_resolution,[],[f655,f181]) ).
fof(f786,plain,
( m2_relset_1(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f313,f186]) ).
fof(f791,plain,
( m2_relset_1(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f786,f185]) ).
fof(f792,plain,
( m2_relset_1(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f791,f184]) ).
fof(f793,plain,
( m2_relset_1(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f792,f183]) ).
fof(f794,plain,
( m2_relset_1(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f793,f182]) ).
fof(f795,plain,
m2_relset_1(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1)),
inference(forward_subsumption_resolution,[],[f794,f181]) ).
fof(f797,plain,
( v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f315,f186]) ).
fof(f802,plain,
( v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f797,f185]) ).
fof(f803,plain,
( v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f802,f184]) ).
fof(f804,plain,
( v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f803,f183]) ).
fof(f805,plain,
( v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f804,f182]) ).
fof(f806,plain,
v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1)),
inference(forward_subsumption_resolution,[],[f805,f181]) ).
fof(f825,definition,
( spl27_45
<=> v1_group_6(sK2,sK1,sK1) ),
introduced(definition,[new_symbols(definition,[spl27_45])],[avatar_definition]) ).
fof(f826,plain,
( v1_group_6(sK2,sK1,sK1)
| ~ spl27_45 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f853,plain,
( ~ v1_xboole_0(k1_autgroup(sK1))
| ~ spl27_3 ),
inference(resolution,[],[f435,f236]) ).
fof(f858,plain,
! [X3,X0] :
( ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| v1_group_6(X3,X0,X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f323,f231]) ).
fof(f859,plain,
( v1_group_6(sK2,sK1,sK1)
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f858,f186]) ).
fof(f872,plain,
( v1_group_6(sK2,sK1,sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f859,f185]) ).
fof(f874,plain,
( v1_group_6(sK2,sK1,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f872,f184]) ).
fof(f880,plain,
( v1_group_6(sK2,sK1,sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f874,f183]) ).
fof(f881,plain,
( v1_group_6(sK2,sK1,sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f880,f182]) ).
fof(f882,plain,
v1_group_6(sK2,sK1,sK1),
inference(forward_subsumption_resolution,[],[f881,f181]) ).
fof(f883,plain,
spl27_45,
inference(avatar_split_clause,[],[f882,f825]) ).
fof(f918,plain,
( ~ spl27_17
| ~ spl27_3 ),
inference(avatar_split_clause,[],[f853,f434,f586]) ).
fof(f956,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| v4_group_6(sK2,sK1,sK1)
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_11 ),
inference(resolution,[],[f310,f541]) ).
fof(f963,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| v4_group_6(sK2,sK1,sK1)
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f956,f444]) ).
fof(f966,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| v4_group_6(sK2,sK1,sK1)
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12 ),
inference(forward_subsumption_resolution,[],[f963,f546]) ).
fof(f968,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| v4_group_6(sK2,sK1,sK1)
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f966,f826]) ).
fof(f970,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| v4_group_6(sK2,sK1,sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f968,f185]) ).
fof(f971,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| v4_group_6(sK2,sK1,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f970,f184]) ).
fof(f972,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| v4_group_6(sK2,sK1,sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f971,f183]) ).
fof(f973,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| v4_group_6(sK2,sK1,sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f972,f182]) ).
fof(f974,plain,
( ~ r2_hidden(sK2,k1_autgroup(sK1))
| v4_group_6(sK2,sK1,sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f973,f181]) ).
fof(f976,definition,
( spl27_49
<=> v4_group_6(sK2,sK1,sK1) ),
introduced(definition,[new_symbols(definition,[spl27_49])],[avatar_definition]) ).
fof(f978,plain,
( v4_group_6(sK2,sK1,sK1)
| ~ spl27_49 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f979,plain,
( spl27_49
| ~ spl27_18
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45 ),
inference(avatar_split_clause,[],[f974,f825,f544,f539,f442,f590,f976]) ).
fof(f1074,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_1(k2_funct_1(sK2))
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(k2_funct_1(sK2),sK1,sK1)
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f795,f311]) ).
fof(f1100,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(k2_funct_1(sK2),sK1,sK1)
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f1074,f642]) ).
fof(f1110,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| v3_struct_0(sK1)
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f1100,f656]) ).
fof(f1121,definition,
( spl27_51
<=> v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_51])],[avatar_definition]) ).
fof(f1138,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| ~ v1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f1110,f185]) ).
fof(f1145,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f1138,f184]) ).
fof(f1152,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f1145,f183]) ).
fof(f1159,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| ~ l1_group_1(sK1) ),
inference(forward_subsumption_resolution,[],[f1152,f182]) ).
fof(f1167,definition,
( spl27_56
<=> v4_group_6(k2_funct_1(sK2),sK1,sK1) ),
introduced(definition,[new_symbols(definition,[spl27_56])],[avatar_definition]) ).
fof(f1174,plain,
( ~ v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1)) ),
inference(forward_subsumption_resolution,[],[f1159,f181]) ).
fof(f1176,definition,
( spl27_57
<=> r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_57])],[avatar_definition]) ).
fof(f1177,plain,
( r2_hidden(k2_funct_1(sK2),k1_autgroup(sK1))
| ~ spl27_57 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1180,plain,
( spl27_57
| ~ spl27_51
| ~ spl27_56 ),
inference(avatar_split_clause,[],[f1174,f1167,f1121,f1176]) ).
fof(f1181,plain,
( ~ v4_group_6(sK2,sK1,sK1)
| ~ v1_funct_1(k2_funct_1(sK2))
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(k2_funct_1(sK2),sK1,sK1)
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(resolution,[],[f326,f795]) ).
fof(f1182,plain,
( ~ v4_group_6(sK2,sK1,sK1)
| ~ v1_funct_1(k2_funct_1(sK2))
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(k2_funct_1(sK2),sK1,sK1)
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1) ),
inference(duplicate_literal_removal,[],[f1181]) ).
fof(f1183,plain,
( ~ v1_funct_1(k2_funct_1(sK2))
| ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(k2_funct_1(sK2),sK1,sK1)
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1182,f978]) ).
fof(f1184,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(k2_funct_1(sK2),sK1,sK1)
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1183,f642]) ).
fof(f1185,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_1(sK2)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1184,f656]) ).
fof(f1186,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_funct_2(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1185,f444]) ).
fof(f1187,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v1_group_6(sK2,sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_12
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1186,f546]) ).
fof(f1188,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ m2_relset_1(sK2,u1_struct_0(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1187,f826]) ).
fof(f1189,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| v3_struct_0(sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1188,f541]) ).
fof(f1190,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v3_group_1(sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1189,f185]) ).
fof(f1191,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ v4_group_1(sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1190,f183]) ).
fof(f1192,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ l1_group_1(sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1191,f182]) ).
fof(f1193,plain,
( ~ v1_funct_2(k2_funct_1(sK2),u1_struct_0(sK1),u1_struct_0(sK1))
| v4_group_6(k2_funct_1(sK2),sK1,sK1)
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(forward_subsumption_resolution,[],[f1192,f181]) ).
fof(f1194,plain,
( spl27_56
| ~ spl27_51
| ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49 ),
inference(avatar_split_clause,[],[f1193,f976,f825,f544,f539,f442,f1121,f1167]) ).
fof(f1195,plain,
spl27_51,
inference(avatar_split_clause,[],[f806,f1121]) ).
fof(f1203,plain,
( m1_subset_1(k2_funct_1(sK2),k1_autgroup(sK1))
| ~ spl27_57 ),
inference(resolution,[],[f1177,f306]) ).
fof(f1206,plain,
( $false
| spl27_10
| ~ spl27_57 ),
inference(forward_subsumption_resolution,[],[f1203,f536]) ).
fof(f1207,plain,
( spl27_10
| ~ spl27_57 ),
inference(avatar_contradiction_clause,[],[f1206]) ).
cnf(s2,plain,
( ~ spl27_3
| spl27_4
| spl27_5 ),
inference(sat_conversion,[],[f445]) ).
cnf(s5,plain,
spl27_3,
inference(sat_conversion,[],[f527]) ).
cnf(s6,plain,
( ~ spl27_3
| spl27_4
| spl27_9 ),
inference(sat_conversion,[],[f532]) ).
cnf(s7,plain,
( ~ spl27_3
| spl27_4
| ~ spl27_10 ),
inference(sat_conversion,[],[f537]) ).
cnf(s8,plain,
( ~ spl27_3
| spl27_4
| spl27_11 ),
inference(sat_conversion,[],[f542]) ).
cnf(s9,plain,
( ~ spl27_3
| spl27_4
| spl27_12 ),
inference(sat_conversion,[],[f547]) ).
cnf(s11,plain,
~ spl27_4,
inference(sat_conversion,[],[f565]) ).
cnf(s13,plain,
( ~ spl27_9
| spl27_17
| spl27_18 ),
inference(sat_conversion,[],[f593]) ).
cnf(s34,plain,
spl27_45,
inference(sat_conversion,[],[f883]) ).
cnf(s37,plain,
( ~ spl27_3
| ~ spl27_17 ),
inference(sat_conversion,[],[f918]) ).
cnf(s40,plain,
( ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_18
| ~ spl27_45
| spl27_49 ),
inference(sat_conversion,[],[f979]) ).
cnf(s50,plain,
( ~ spl27_51
| ~ spl27_56
| spl27_57 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s51,plain,
( ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49
| ~ spl27_51
| spl27_56 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s52,plain,
spl27_51,
inference(sat_conversion,[],[f1195]) ).
cnf(s53,plain,
( spl27_10
| ~ spl27_57 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s54,plain,
( ~ spl27_5
| ~ spl27_11
| ~ spl27_12
| ~ spl27_45
| ~ spl27_49
| spl27_56 ),
inference(rat,[],[s51,s52]) ).
cnf(s55,plain,
( ~ spl27_56
| spl27_57 ),
inference(rat,[],[s50,s52]) ).
cnf(s68,plain,
( ~ spl27_3
| spl27_12 ),
inference(rat,[],[s9,s11]) ).
cnf(s69,plain,
( ~ spl27_3
| spl27_11 ),
inference(rat,[],[s8,s11]) ).
cnf(s70,plain,
( ~ spl27_3
| ~ spl27_10 ),
inference(rat,[],[s7,s11]) ).
cnf(s71,plain,
( ~ spl27_3
| spl27_9 ),
inference(rat,[],[s6,s11]) ).
cnf(s72,plain,
~ spl27_17,
inference(rat,[],[s37,s5]) ).
cnf(s74,plain,
spl27_12,
inference(rat,[],[s68,s5]) ).
cnf(s75,plain,
spl27_11,
inference(rat,[],[s69,s5]) ).
cnf(s76,plain,
~ spl27_10,
inference(rat,[],[s70,s5]) ).
cnf(s77,plain,
spl27_9,
inference(rat,[],[s71,s5]) ).
cnf(s80,plain,
~ spl27_57,
inference(rat,[],[s53,s76]) ).
cnf(s81,plain,
spl27_18,
inference(rat,[],[s13,s72,s77]) ).
cnf(s83,plain,
~ spl27_56,
inference(rat,[],[s55,s80]) ).
cnf(s85,plain,
spl27_5,
inference(rat,[],[s2,s11,s5]) ).
cnf(s86,plain,
~ spl27_49,
inference(rat,[],[s54,s83,s75,s34,s74,s85]) ).
cnf(s87,plain,
$false,
inference(rat,[],[s40,s81,s34,s75,s74,s86,s85]) ).
fof(f1208,plain,
$false,
inference(avatar_sat_refutation,[],[s87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP620+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n026.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:12:01 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.48 % (2605102)Will run a generic schedule for satisfiability detection.
% 0.18/0.48 % (2605113)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2113521656:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.48 % (2605108)% WARNING: option uhcvi not known.
% 0.18/0.48 % (2605107)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1830518672_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.48 % (2605110)dis+10_1_sil=32000:sp=arity:random_seed=3313687259:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.48 % (2605108)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3513250065:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.48 % (2605109)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1261161372:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.48 % (2605112)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=793129887:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.48 % (2605111)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2983990001:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.48 % TRYING [1]
% 0.18/0.48 % TRYING [2]
% 0.18/0.48 % TRYING [3]
% 0.18/0.48 % (2605110) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2605102-2605110"...
% 0.18/0.48 % (2605110)...printing done.
% 0.18/0.48 % (2605110)Refutation found. Thanks to Tanya!
% 0.18/0.48 % SZS status Theorem for theBenchmark
% 0.18/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.49 % (2605110)------------------------------
% 0.18/0.49 % (2605110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.49 % (2605110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.49 % (2605110)CaDiCaL version: 2.1.3
% 0.18/0.49 % (2605110)Termination reason: Refutation
% 0.18/0.49 % (2605110)Time elapsed: 0.027 s
% 0.18/0.49 % (2605110)Peak memory usage: 13 MB
% 0.18/0.49 % (2605110)Instructions burned: 40 (million)
% 0.18/0.49 % (2605102)Success in time 0.061 s
% 0.18/0.49 % Vampire exiting
%------------------------------------------------------------------------------