%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP630+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:07 AM UTC 2026
% Result : Theorem 27.84s 5.98s
% Output : Refutation 32.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 51
% Syntax : Number of formulae : 509 ( 53 unt; 22 def)
% Number of atoms : 2311 ( 225 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 3239 (1437 ~;1563 |; 149 &)
% ( 30 <=>; 60 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 23 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-5 aty)
% Number of variables : 445 ( 0 sgn 441 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2933,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(f2937,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(f6422,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(f6424,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f7377,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k3_group_1(X0,k3_group_1(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t19_group_1) ).
fof(f7378,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( k1_group_1(X0,X1,X2) = k2_group_1(X0)
| k1_group_1(X0,X2,X1) = k2_group_1(X0) )
=> ( X1 = k3_group_1(X0,X2)
& X2 = k3_group_1(X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_group_1) ).
fof(f7466,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f7471,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_group_1) ).
fof(f8697,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> v4_group_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_group_2) ).
fof(f8753,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> m1_subset_1(X2,u1_struct_0(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_group_2) ).
fof(f8759,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X2))
=> ( X3 = X1
=> k3_group_1(X2,X3) = k3_group_1(X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t57_group_2) ).
fof(f8765,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_group_2(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_group_2) ).
fof(f8898,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f12869,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k3_autgroup(X0))
& v1_group_1(k3_autgroup(X0))
& v3_group_1(k3_autgroup(X0))
& v4_group_1(k3_autgroup(X0))
& l1_group_1(k3_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_autgroup) ).
fof(f12870,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/sandbox2/benchmark/theBenchmark.p',dt_k4_autgroup) ).
fof(f12871,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/sandbox2/benchmark/theBenchmark.p',dt_k5_autgroup) ).
fof(f12872,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/sandbox2/benchmark/theBenchmark.p',dt_k6_autgroup) ).
fof(f12883,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))
=> 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(f12888,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k6_partfun1(u1_struct_0(X0)) = k2_group_1(k3_autgroup(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_autgroup) ).
fof(f12889,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))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k3_autgroup(X0)))
=> ( X1 = X2
=> k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_autgroup) ).
fof(f12892,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),k4_autgroup(X0))
=> m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_autgroup) ).
fof(f12896,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),k4_autgroup(X0))
=> m2_fraenkel(k2_funct_1(X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_autgroup) ).
fof(f12898,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/sandbox2/benchmark/theBenchmark.p',d5_autgroup) ).
fof(f12900,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/sandbox2/benchmark/theBenchmark.p',t20_autgroup) ).
fof(f12901,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k6_partfun1(u1_struct_0(X0)) = k2_group_1(k5_autgroup(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_autgroup) ).
fof(f12902,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),k4_autgroup(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
=> ( X1 = X2
=> k2_funct_1(X1) = k3_group_1(k5_autgroup(X0),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_autgroup) ).
fof(f12905,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/sandbox2/benchmark/theBenchmark.p',t24_autgroup) ).
fof(f12907,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(X0))
=> k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) = k6_autgroup(X0,k2_group_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_autgroup) ).
fof(f12909,conjecture,
! [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(X0))
=> k6_autgroup(X0,k3_group_1(X0,X1)) = k2_funct_1(k6_autgroup(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_autgroup) ).
fof(f12910,negated_conjecture,
~ ! [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(X0))
=> k6_autgroup(X0,k3_group_1(X0,X1)) = k2_funct_1(k6_autgroup(X0,X1)) ) ),
inference(negated_conjecture,[status(cth)],[f12909]) ).
fof(f12954,plain,
! [X0] :
( ( ~ v3_struct_0(k3_autgroup(X0))
& v1_group_1(k3_autgroup(X0))
& v3_group_1(k3_autgroup(X0))
& v4_group_1(k3_autgroup(X0))
& l1_group_1(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,[],[f12869]) ).
fof(f12955,plain,
! [X0] :
( ( ~ v3_struct_0(k3_autgroup(X0))
& v1_group_1(k3_autgroup(X0))
& v3_group_1(k3_autgroup(X0))
& v4_group_1(k3_autgroup(X0))
& l1_group_1(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,[],[f12954]) ).
fof(f12956,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,[],[f12870]) ).
fof(f12957,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,[],[f12956]) ).
fof(f12958,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,[],[f12871]) ).
fof(f12959,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,[],[f12958]) ).
fof(f12960,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,[],[f12872]) ).
fof(f12961,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,[],[f12960]) ).
fof(f12980,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,[],[f12883]) ).
fof(f12981,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,[],[f12980]) ).
fof(f12990,plain,
! [X0] :
( k6_partfun1(u1_struct_0(X0)) = k2_group_1(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,[],[f12888]) ).
fof(f12991,plain,
! [X0] :
( k6_partfun1(u1_struct_0(X0)) = k2_group_1(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,[],[f12990]) ).
fof(f12992,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k3_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,[],[f12889]) ).
fof(f12993,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k3_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,[],[f12992]) ).
fof(f12998,plain,
! [X0] :
( ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ 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,[],[f12892]) ).
fof(f12999,plain,
! [X0] :
( ! [X1] :
( m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ 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,[],[f12998]) ).
fof(f13006,plain,
! [X0] :
( ! [X1] :
( m2_fraenkel(k2_funct_1(X1),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)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f12896]) ).
fof(f13007,plain,
! [X0] :
( ! [X1] :
( m2_fraenkel(k2_funct_1(X1),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)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13006]) ).
fof(f13010,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,[],[f12898]) ).
fof(f13011,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,[],[f13010]) ).
fof(f13012,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,[],[f12900]) ).
fof(f13013,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,[],[f13012]) ).
fof(f13014,plain,
! [X0] :
( k6_partfun1(u1_struct_0(X0)) = k2_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(ennf_transformation,[],[f12901]) ).
fof(f13015,plain,
! [X0] :
( k6_partfun1(u1_struct_0(X0)) = k2_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(flattening,[],[f13014]) ).
fof(f13016,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_funct_1(X1) = k3_group_1(k5_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0))) )
| ~ 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,[],[f12902]) ).
fof(f13017,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_funct_1(X1) = k3_group_1(k5_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0))) )
| ~ 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,[],[f13016]) ).
fof(f13022,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,[],[f12905]) ).
fof(f13023,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,[],[f13022]) ).
fof(f13026,plain,
! [X0] :
( ! [X1] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) = k6_autgroup(X0,k2_group_1(X0))
| ~ m1_subset_1(X1,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,[],[f12907]) ).
fof(f13027,plain,
! [X0] :
( ! [X1] :
( k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1)) = k6_autgroup(X0,k2_group_1(X0))
| ~ m1_subset_1(X1,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,[],[f13026]) ).
fof(f13030,plain,
? [X0] :
( ? [X1] :
( k6_autgroup(X0,k3_group_1(X0,X1)) != k2_funct_1(k6_autgroup(X0,X1))
& m1_subset_1(X1,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,[],[f12910]) ).
fof(f13031,plain,
? [X0] :
( ? [X1] :
( k6_autgroup(X0,k3_group_1(X0,X1)) != k2_funct_1(k6_autgroup(X0,X1))
& m1_subset_1(X1,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,[],[f13030]) ).
fof(f13033,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,[],[f2937]) ).
fof(f13034,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,[],[f13033]) ).
fof(f13039,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f2933]) ).
fof(f13067,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8898]) ).
fof(f13068,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13067]) ).
fof(f13073,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8765]) ).
fof(f13074,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13073]) ).
fof(f13075,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8753]) ).
fof(f13076,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13075]) ).
fof(f13077,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8697]) ).
fof(f13078,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13077]) ).
fof(f13446,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k3_group_1(X2,X3) = k3_group_1(X0,X1)
| X1 != X3
| ~ m1_subset_1(X3,u1_struct_0(X2)) )
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8759]) ).
fof(f13447,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k3_group_1(X2,X3) = k3_group_1(X0,X1)
| X1 != X3
| ~ m1_subset_1(X3,u1_struct_0(X2)) )
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13446]) ).
fof(f13448,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f7471]) ).
fof(f13449,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f13448]) ).
fof(f13466,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k3_group_1(X0,X2)
& X2 = k3_group_1(X0,X1) )
| ( k1_group_1(X0,X1,X2) != k2_group_1(X0)
& k1_group_1(X0,X2,X1) != k2_group_1(X0) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f7378]) ).
fof(f13467,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k3_group_1(X0,X2)
& X2 = k3_group_1(X0,X1) )
| ( k1_group_1(X0,X1,X2) != k2_group_1(X0)
& k1_group_1(X0,X2,X1) != k2_group_1(X0) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13466]) ).
fof(f13468,plain,
! [X0] :
( ! [X1] :
( k3_group_1(X0,k3_group_1(X0,X1)) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f7377]) ).
fof(f13469,plain,
! [X0] :
( ! [X1] :
( k3_group_1(X0,k3_group_1(X0,X1)) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f13468]) ).
fof(f14475,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f7466]) ).
fof(f14481,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6424]) ).
fof(f14484,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6422]) ).
fof(f14485,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f14484]) ).
fof(f16189,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,[],[f13011]) ).
fof(f16193,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) != k2_funct_1(k6_autgroup(sK32,sK33))
& m1_subset_1(sK33,u1_struct_0(sK32))
& ~ v3_struct_0(sK32)
& v1_group_1(sK32)
& v3_group_1(sK32)
& v4_group_1(sK32)
& l1_group_1(sK32) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33]),skolemize(X0,sK32),skolemize(X1,sK33)],[f13031]) ).
fof(f16194,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,[],[f13034]) ).
fof(f16661,plain,
! [X0] :
( ( ( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) )
& ( v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f14481]) ).
fof(f17158,plain,
! [X0] :
( l1_group_1(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,[],[f12955]) ).
fof(f17159,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f12955]) ).
fof(f17160,plain,
! [X0] :
( v3_group_1(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,[],[f12955]) ).
fof(f17162,plain,
! [X0] :
( ~ v3_struct_0(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,[],[f12955]) ).
fof(f17163,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f12957]) ).
fof(f17164,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,[],[f12959]) ).
fof(f17165,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,[],[f12959]) ).
fof(f17166,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,[],[f12959]) ).
fof(f17167,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,[],[f12961]) ).
fof(f17212,plain,
! [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))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f12981]) ).
fof(f17220,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| k6_partfun1(u1_struct_0(X0)) = k2_group_1(k3_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f12991]) ).
fof(f17221,plain,
! [X2,X0,X1] :
( k2_funct_1(X1) = k3_group_1(k3_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k3_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(cnf_transformation,[],[f12993]) ).
fof(f17232,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ 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)
| m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f12999]) ).
fof(f17236,plain,
! [X0,X1] :
( m2_fraenkel(k2_funct_1(X1),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))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13007]) ).
fof(f17238,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,[],[f16189]) ).
fof(f17240,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,[],[f13013]) ).
fof(f17241,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| k6_partfun1(u1_struct_0(X0)) = k2_group_1(k5_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13015]) ).
fof(f17242,plain,
! [X2,X0,X1] :
( k2_funct_1(X1) = k3_group_1(k5_autgroup(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
| ~ 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(cnf_transformation,[],[f13017]) ).
fof(f17247,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| k6_partfun1(u1_struct_0(X0)) = k6_autgroup(X0,k2_group_1(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13023]) ).
fof(f17249,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| k6_autgroup(X0,k2_group_1(X0)) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,k3_group_1(X0,X1)),k6_autgroup(X0,X1))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13027]) ).
fof(f17251,plain,
l1_group_1(sK32),
inference(cnf_transformation,[],[f16193]) ).
fof(f17252,plain,
v4_group_1(sK32),
inference(cnf_transformation,[],[f16193]) ).
fof(f17253,plain,
v3_group_1(sK32),
inference(cnf_transformation,[],[f16193]) ).
fof(f17254,plain,
v1_group_1(sK32),
inference(cnf_transformation,[],[f16193]) ).
fof(f17255,plain,
~ v3_struct_0(sK32),
inference(cnf_transformation,[],[f16193]) ).
fof(f17256,plain,
m1_subset_1(sK33,u1_struct_0(sK32)),
inference(cnf_transformation,[],[f16193]) ).
fof(f17257,plain,
k6_autgroup(sK32,k3_group_1(sK32,sK33)) != k2_funct_1(k6_autgroup(sK32,sK33)),
inference(cnf_transformation,[],[f16193]) ).
fof(f17259,plain,
! [X2,X3,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| ~ m2_fraenkel(X3,X0,X1,X2)
| v1_xboole_0(X1)
| m1_subset_1(X3,X2) ),
inference(cnf_transformation,[],[f16194]) ).
fof(f17260,plain,
! [X2,X3,X0,X1] :
( ~ m1_fraenkel(X2,X0,X1)
| ~ m1_subset_1(X3,X2)
| v1_xboole_0(X1)
| m2_fraenkel(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f16194]) ).
fof(f17267,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f13039]) ).
fof(f17308,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| l1_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13068]) ).
fof(f17309,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| v3_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13068]) ).
fof(f17313,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(X0,X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13074]) ).
fof(f17314,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13076]) ).
fof(f17315,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| v4_group_1(X1)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13078]) ).
fof(f17826,plain,
! [X2,X3,X0,X1] :
( k3_group_1(X0,X1) = k3_group_1(X2,X3)
| X1 != X3
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13447]) ).
fof(f17827,plain,
! [X0,X1] :
( m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f13449]) ).
fof(f17841,plain,
! [X2,X0,X1] :
( ~ v3_group_1(X0)
| k1_group_1(X0,X2,X1) != k2_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| k3_group_1(X0,X1) = X2
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13467]) ).
fof(f17845,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k3_group_1(X0,k3_group_1(X0,X1)) = X1
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f13469]) ).
fof(f19195,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14475]) ).
fof(f19202,plain,
! [X0] :
( ~ v3_struct_0(X0)
| v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f16661]) ).
fof(f19206,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f14485]) ).
fof(f22425,plain,
! [X2,X0] :
( ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))
| ~ m1_subset_1(X2,u1_struct_0(k3_autgroup(X0)))
| k2_funct_1(X2) = k3_group_1(k3_autgroup(X0),X2)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f17221]) ).
fof(f22430,plain,
! [X0] :
( ~ v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
| ~ v1_group_1(k5_autgroup(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(equality_resolution,[],[f17238]) ).
fof(f22431,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,[],[f17240]) ).
fof(f22432,plain,
! [X3,X0,X4] :
( ~ v4_group_1(X0)
| ~ 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)
| 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)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f22431]) ).
fof(f22433,plain,
! [X2,X0] :
( ~ m2_fraenkel(X2,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
| k2_funct_1(X2) = k3_group_1(k5_autgroup(X0),X2)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f17242]) ).
fof(f22495,plain,
! [X2,X3,X0] :
( ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k3_group_1(X2,X3) = k3_group_1(X0,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f17826]) ).
fof(f23237,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| k3_group_1(sK32,k3_group_1(sK32,X0)) = X0
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17845,f17252]) ).
fof(f23238,plain,
! [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))
| ~ m1_subset_1(k6_autgroup(X0,X1),u1_struct_0(k5_autgroup(X0)))
| k2_funct_1(k6_autgroup(X0,X1)) = k3_group_1(k5_autgroup(X0),k6_autgroup(X0,X1))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f17167,f22433]) ).
fof(f23239,plain,
! [X0,X1] :
( ~ m1_subset_1(k6_autgroup(X0,X1),u1_struct_0(k5_autgroup(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))
| v3_struct_0(X0)
| k2_funct_1(k6_autgroup(X0,X1)) = k3_group_1(k5_autgroup(X0),k6_autgroup(X0,X1)) ),
inference(duplicate_literal_removal,[],[f23238]) ).
fof(f23240,plain,
! [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(k5_autgroup(X0)))
| k3_group_1(k5_autgroup(X0),X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| v3_struct_0(k3_autgroup(X0))
| ~ v3_group_1(k3_autgroup(X0))
| ~ v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0)) ),
inference(resolution,[],[f17164,f22495]) ).
fof(f23249,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| v4_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17159,f17252]) ).
fof(f23251,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(X1)))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X1)))
| v3_struct_0(k3_autgroup(X1))
| ~ v3_group_1(k3_autgroup(X1))
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(resolution,[],[f17314,f17164]) ).
fof(f23252,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17241,f17252]) ).
fof(f23255,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17220,f17252]) ).
fof(f23256,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m2_fraenkel(X1,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),X0,X1) = k1_group_1(k5_autgroup(sK32),X1,X0)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f22432,f17252]) ).
fof(f23257,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| m1_fraenkel(k4_autgroup(sK32),u1_struct_0(sK32),u1_struct_0(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17163,f17252]) ).
fof(f23258,plain,
! [X0] :
( ~ v1_group_1(k5_autgroup(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)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f22430,f17165]) ).
fof(f23259,plain,
! [X0] :
( ~ v1_group_1(k5_autgroup(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(duplicate_literal_removal,[],[f23258]) ).
fof(f23260,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17232,f17252]) ).
fof(f23261,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k6_autgroup(sK32,k2_group_1(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17247,f17252]) ).
fof(f23267,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_autgroup(sK32,k2_group_1(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)),k6_autgroup(sK32,X0))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f17249,f17252]) ).
fof(f23283,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| ~ v3_group_1(sK32)
| k3_group_1(sK32,k3_group_1(sK32,X0)) = X0
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23237,f17255]) ).
fof(f23286,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| v4_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23249,f17255]) ).
fof(f23288,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23252,f17255]) ).
fof(f23289,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23255,f17255]) ).
fof(f23290,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m2_fraenkel(X1,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),X0,X1) = k1_group_1(k5_autgroup(sK32),X1,X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23256,f17255]) ).
fof(f23291,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| m1_fraenkel(k4_autgroup(sK32),u1_struct_0(sK32),u1_struct_0(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23257,f17255]) ).
fof(f23292,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23260,f17255]) ).
fof(f23293,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k6_autgroup(sK32,k2_group_1(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23261,f17255]) ).
fof(f23295,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k6_autgroup(sK32,k2_group_1(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)),k6_autgroup(sK32,X0))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23267,f17255]) ).
fof(f23299,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| k3_group_1(sK32,k3_group_1(sK32,X0)) = X0
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23283,f17253]) ).
fof(f23302,plain,
( ~ v3_group_1(sK32)
| v4_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23286,f17254]) ).
fof(f23304,plain,
( ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23288,f17254]) ).
fof(f23305,plain,
( ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23289,f17254]) ).
fof(f23306,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m2_fraenkel(X1,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| ~ v3_group_1(sK32)
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),X0,X1) = k1_group_1(k5_autgroup(sK32),X1,X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23290,f17254]) ).
fof(f23307,plain,
( ~ v3_group_1(sK32)
| m1_fraenkel(k4_autgroup(sK32),u1_struct_0(sK32),u1_struct_0(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23291,f17254]) ).
fof(f23308,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23292,f17254]) ).
fof(f23309,plain,
( ~ v3_group_1(sK32)
| k6_partfun1(u1_struct_0(sK32)) = k6_autgroup(sK32,k2_group_1(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23293,f17254]) ).
fof(f23311,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| ~ v3_group_1(sK32)
| k6_autgroup(sK32,k2_group_1(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)),k6_autgroup(sK32,X0))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23295,f17254]) ).
fof(f23315,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| k3_group_1(sK32,k3_group_1(sK32,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f23299,f17251]) ).
fof(f23318,plain,
( v4_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23302,f17253]) ).
fof(f23320,plain,
( k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23304,f17253]) ).
fof(f23321,plain,
( k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23305,f17253]) ).
fof(f23322,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m2_fraenkel(X1,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),X0,X1) = k1_group_1(k5_autgroup(sK32),X1,X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23306,f17253]) ).
fof(f23323,plain,
( m1_fraenkel(k4_autgroup(sK32),u1_struct_0(sK32),u1_struct_0(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23307,f17253]) ).
fof(f23324,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23308,f17253]) ).
fof(f23325,plain,
( k6_partfun1(u1_struct_0(sK32)) = k6_autgroup(sK32,k2_group_1(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23309,f17253]) ).
fof(f23327,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| k6_autgroup(sK32,k2_group_1(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)),k6_autgroup(sK32,X0))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f23311,f17253]) ).
fof(f23331,plain,
v4_group_1(k3_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f23318,f17251]) ).
fof(f23332,plain,
k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k5_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f23320,f17251]) ).
fof(f23333,plain,
k6_partfun1(u1_struct_0(sK32)) = k2_group_1(k3_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f23321,f17251]) ).
fof(f23334,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m2_fraenkel(X1,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),X0,X1) = k1_group_1(k5_autgroup(sK32),X1,X0) ),
inference(forward_subsumption_resolution,[],[f23322,f17251]) ).
fof(f23335,plain,
m1_fraenkel(k4_autgroup(sK32),u1_struct_0(sK32),u1_struct_0(sK32)),
inference(forward_subsumption_resolution,[],[f23323,f17251]) ).
fof(f23336,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32)) ),
inference(forward_subsumption_resolution,[],[f23324,f17251]) ).
fof(f23337,plain,
k6_partfun1(u1_struct_0(sK32)) = k6_autgroup(sK32,k2_group_1(sK32)),
inference(forward_subsumption_resolution,[],[f23325,f17251]) ).
fof(f23339,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| k6_autgroup(sK32,k2_group_1(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)),k6_autgroup(sK32,X0)) ),
inference(forward_subsumption_resolution,[],[f23327,f17251]) ).
fof(f23343,plain,
k2_group_1(k5_autgroup(sK32)) = k6_autgroup(sK32,k2_group_1(sK32)),
inference(forward_demodulation,[],[f23337,f23332]) ).
fof(f23344,plain,
sK33 = k3_group_1(sK32,k3_group_1(sK32,sK33)),
inference(resolution,[],[f23315,f17256]) ).
fof(f23366,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| m1_subset_1(X0,k4_autgroup(sK32)) ),
inference(resolution,[],[f23335,f17259]) ).
fof(f23367,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| v1_xboole_0(u1_struct_0(sK32))
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) ),
inference(resolution,[],[f23335,f17260]) ).
fof(f23369,definition,
( spl618_24
<=> v1_xboole_0(u1_struct_0(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_24])],[avatar_definition]) ).
fof(f23370,plain,
( v1_xboole_0(u1_struct_0(sK32))
| ~ spl618_24 ),
inference(avatar_component_clause,[],[f23369]) ).
fof(f23372,definition,
( spl618_25
<=> ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) ) ),
introduced(definition,[new_symbols(definition,[spl618_25])],[avatar_definition]) ).
fof(f23373,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) )
| ~ spl618_25 ),
inference(avatar_component_clause,[],[f23372]) ).
fof(f23374,plain,
( spl618_24
| spl618_25 ),
inference(avatar_split_clause,[],[f23367,f23372,f23369]) ).
fof(f23376,definition,
( spl618_26
<=> ! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| m1_subset_1(X0,k4_autgroup(sK32)) ) ),
introduced(definition,[new_symbols(definition,[spl618_26])],[avatar_definition]) ).
fof(f23377,plain,
( ! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| m1_subset_1(X0,k4_autgroup(sK32)) )
| ~ spl618_26 ),
inference(avatar_component_clause,[],[f23376]) ).
fof(f23378,plain,
( spl618_24
| spl618_26 ),
inference(avatar_split_clause,[],[f23366,f23376,f23369]) ).
fof(f23387,plain,
( v3_struct_0(sK32)
| ~ l1_struct_0(sK32)
| ~ spl618_24 ),
inference(resolution,[],[f23370,f19206]) ).
fof(f23389,plain,
( ~ l1_struct_0(sK32)
| ~ spl618_24 ),
inference(forward_subsumption_resolution,[],[f23387,f17255]) ).
fof(f23391,plain,
( ~ l1_group_1(sK32)
| ~ spl618_24 ),
inference(resolution,[],[f23389,f19195]) ).
fof(f23393,plain,
( $false
| ~ spl618_24 ),
inference(forward_subsumption_resolution,[],[f23391,f17251]) ).
fof(f23394,plain,
~ spl618_24,
inference(avatar_contradiction_clause,[],[f23393]) ).
fof(f23426,plain,
( v3_struct_0(k3_autgroup(sK32))
| ~ v3_group_1(k3_autgroup(sK32))
| m1_group_2(k3_autgroup(sK32),k3_autgroup(sK32))
| ~ l1_group_1(k3_autgroup(sK32)) ),
inference(resolution,[],[f23331,f17313]) ).
fof(f23428,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| v3_struct_0(k3_autgroup(sK32))
| ~ v3_group_1(k3_autgroup(sK32))
| k3_group_1(k3_autgroup(sK32),k3_group_1(k3_autgroup(sK32),X0)) = X0
| ~ l1_group_1(k3_autgroup(sK32)) ),
inference(resolution,[],[f23331,f17845]) ).
fof(f23433,definition,
( spl618_33
<=> l1_group_1(k3_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_33])],[avatar_definition]) ).
fof(f23434,plain,
( ~ l1_group_1(k3_autgroup(sK32))
| spl618_33 ),
inference(avatar_component_clause,[],[f23433]) ).
fof(f23436,definition,
( spl618_34
<=> v3_group_1(k3_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_34])],[avatar_definition]) ).
fof(f23437,plain,
( ~ v3_group_1(k3_autgroup(sK32))
| spl618_34 ),
inference(avatar_component_clause,[],[f23436]) ).
fof(f23442,definition,
( spl618_36
<=> v3_struct_0(k3_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_36])],[avatar_definition]) ).
fof(f23443,plain,
( v3_struct_0(k3_autgroup(sK32))
| ~ spl618_36 ),
inference(avatar_component_clause,[],[f23442]) ).
fof(f23453,definition,
( spl618_39
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),k3_group_1(k3_autgroup(sK32),X0)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl618_39])],[avatar_definition]) ).
fof(f23454,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),k3_group_1(k3_autgroup(sK32),X0)) = X0 )
| ~ spl618_39 ),
inference(avatar_component_clause,[],[f23453]) ).
fof(f23455,plain,
( ~ spl618_33
| ~ spl618_34
| spl618_36
| spl618_39 ),
inference(avatar_split_clause,[],[f23428,f23453,f23442,f23436,f23433]) ).
fof(f23461,definition,
( spl618_41
<=> m1_group_2(k3_autgroup(sK32),k3_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_41])],[avatar_definition]) ).
fof(f23462,plain,
( m1_group_2(k3_autgroup(sK32),k3_autgroup(sK32))
| ~ spl618_41 ),
inference(avatar_component_clause,[],[f23461]) ).
fof(f23463,plain,
( ~ spl618_33
| spl618_41
| ~ spl618_34
| spl618_36 ),
inference(avatar_split_clause,[],[f23426,f23442,f23436,f23461,f23433]) ).
fof(f23508,plain,
( $false
| spl618_33 ),
inference(unit_resulting_resolution,[],[f17158,f17251,f17252,f17253,f17254,f17255,f23434]) ).
fof(f23510,plain,
spl618_33,
inference(avatar_contradiction_clause,[],[f23508]) ).
fof(f23511,plain,
( $false
| spl618_34 ),
inference(unit_resulting_resolution,[],[f17160,f17251,f17252,f17253,f17254,f17255,f23437]) ).
fof(f23513,plain,
spl618_34,
inference(avatar_contradiction_clause,[],[f23511]) ).
fof(f23514,plain,
( $false
| ~ spl618_36 ),
inference(unit_resulting_resolution,[],[f17162,f17251,f17252,f17253,f17254,f17255,f23443]) ).
fof(f23517,plain,
~ spl618_36,
inference(avatar_contradiction_clause,[],[f23514]) ).
fof(f23524,plain,
k2_group_1(k5_autgroup(sK32)) = k2_group_1(k3_autgroup(sK32)),
inference(superposition,[],[f23332,f23333]) ).
fof(f23537,plain,
k6_autgroup(sK32,k2_group_1(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),k6_autgroup(sK32,sK33)),
inference(resolution,[],[f23339,f17256]) ).
fof(f23541,plain,
k2_group_1(k5_autgroup(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),k6_autgroup(sK32,sK33)),
inference(forward_demodulation,[],[f23537,f23343]) ).
fof(f23543,plain,
k2_group_1(k3_autgroup(sK32)) = k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),k6_autgroup(sK32,sK33)),
inference(forward_demodulation,[],[f23541,f23524]) ).
fof(f23557,definition,
( spl618_54
<=> l1_group_1(k5_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_54])],[avatar_definition]) ).
fof(f23558,plain,
( ~ l1_group_1(k5_autgroup(sK32))
| spl618_54 ),
inference(avatar_component_clause,[],[f23557]) ).
fof(f23560,definition,
( spl618_55
<=> v3_struct_0(k5_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_55])],[avatar_definition]) ).
fof(f23561,plain,
( v3_struct_0(k5_autgroup(sK32))
| ~ spl618_55 ),
inference(avatar_component_clause,[],[f23560]) ).
fof(f23566,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(resolution,[],[f23336,f17167]) ).
fof(f23609,plain,
( ! [X0] :
( m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(resolution,[],[f23377,f17167]) ).
fof(f23610,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(X0),k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) )
| ~ spl618_26 ),
inference(resolution,[],[f23377,f17236]) ).
fof(f23654,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(X1)))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X1)))
| ~ v3_group_1(k3_autgroup(X1))
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f23251,f17162]) ).
fof(f23670,plain,
! [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(k5_autgroup(X0)))
| k3_group_1(k5_autgroup(X0),X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| ~ v3_group_1(k3_autgroup(X0))
| ~ v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0)) ),
inference(forward_subsumption_resolution,[],[f23240,f17162]) ).
fof(f23671,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,[],[f23259,f17166]) ).
fof(f23678,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23566,f17255]) ).
fof(f23684,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(X0),k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23610,f17255]) ).
fof(f23685,plain,
( ! [X0] :
( m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23609,f17255]) ).
fof(f23687,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(X1)))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X1)))
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f23654,f17160]) ).
fof(f23705,plain,
! [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(k5_autgroup(X0)))
| k3_group_1(k5_autgroup(X0),X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| ~ v4_group_1(k3_autgroup(X0))
| ~ l1_group_1(k3_autgroup(X0)) ),
inference(forward_subsumption_resolution,[],[f23670,f17160]) ).
fof(f23706,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| k4_autgroup(X0) = u1_struct_0(k5_autgroup(X0))
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f23671,f17164]) ).
fof(f23712,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23678,f17254]) ).
fof(f23718,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(X0),k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23684,f17254]) ).
fof(f23719,plain,
( ! [X0] :
( m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23685,f17254]) ).
fof(f23721,plain,
! [X0,X1] :
( ~ v3_group_1(X1)
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X1)))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(X1)))
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f23687,f17158]) ).
fof(f23731,plain,
! [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(k5_autgroup(X0)))
| k3_group_1(k5_autgroup(X0),X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))
| ~ l1_group_1(k3_autgroup(X0)) ),
inference(forward_subsumption_resolution,[],[f23705,f17159]) ).
fof(f23737,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23712,f17253]) ).
fof(f23743,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(X0),k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23718,f17253]) ).
fof(f23744,plain,
( ! [X0] :
( m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23719,f17253]) ).
fof(f23754,plain,
! [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(k5_autgroup(X0)))
| k3_group_1(k5_autgroup(X0),X1) = k3_group_1(k3_autgroup(X0),X1)
| ~ l1_group_1(k3_autgroup(X0)) ),
inference(forward_subsumption_resolution,[],[f23731,f23721]) ).
fof(f23760,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23737,f17252]) ).
fof(f23766,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(X0),k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ l1_group_1(sK32) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23743,f17252]) ).
fof(f23767,plain,
( ! [X0] :
( m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23744,f17252]) ).
fof(f23790,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
| k3_group_1(k5_autgroup(X0),X1) = k3_group_1(k3_autgroup(X0),X1) ),
inference(forward_subsumption_resolution,[],[f23754,f17158]) ).
fof(f23796,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32)) ),
inference(forward_subsumption_resolution,[],[f23760,f17251]) ).
fof(f23802,plain,
( ! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| m1_subset_1(k2_funct_1(X0),k4_autgroup(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23766,f17251]) ).
fof(f23803,plain,
( ! [X0] :
( m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f23767,f17251]) ).
fof(f23825,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m2_fraenkel(k6_autgroup(sK32,X0),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f23803,f23373]) ).
fof(f23924,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(resolution,[],[f23796,f17827]) ).
fof(f23927,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23924,f17255]) ).
fof(f23929,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23927,f17253]) ).
fof(f23931,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) ),
inference(forward_subsumption_resolution,[],[f23929,f17252]) ).
fof(f23933,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32)) ),
inference(forward_subsumption_resolution,[],[f23931,f17251]) ).
fof(f24054,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k4_autgroup(sK32) = u1_struct_0(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f23706,f17252]) ).
fof(f24060,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| k4_autgroup(sK32) = u1_struct_0(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f24054,f17255]) ).
fof(f24061,plain,
( ~ v3_group_1(sK32)
| k4_autgroup(sK32) = u1_struct_0(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f24060,f17254]) ).
fof(f24062,plain,
( k4_autgroup(sK32) = u1_struct_0(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f24061,f17253]) ).
fof(f24063,plain,
k4_autgroup(sK32) = u1_struct_0(k5_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f24062,f17251]) ).
fof(f24065,plain,
! [X0] :
( ~ m1_subset_1(k6_autgroup(sK32,X0),k4_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) ),
inference(superposition,[],[f23239,f24063]) ).
fof(f24093,definition,
( spl618_100
<=> l1_struct_0(k5_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_100])],[avatar_definition]) ).
fof(f24094,plain,
( ~ l1_struct_0(k5_autgroup(sK32))
| spl618_100 ),
inference(avatar_component_clause,[],[f24093]) ).
fof(f24096,definition,
( spl618_101
<=> v1_xboole_0(k4_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_101])],[avatar_definition]) ).
fof(f24097,plain,
( ~ v1_xboole_0(k4_autgroup(sK32))
| spl618_101 ),
inference(avatar_component_clause,[],[f24096]) ).
fof(f24110,plain,
( ! [X0] :
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24065,f23803]) ).
fof(f24113,plain,
( ! [X0] :
( ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24110,f17254]) ).
fof(f24114,plain,
( ! [X0] :
( ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24113,f17253]) ).
fof(f24115,plain,
( ! [X0] :
( ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24114,f17252]) ).
fof(f24116,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| v3_struct_0(sK32)
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24115,f17251]) ).
fof(f24117,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| k2_funct_1(k6_autgroup(sK32,X0)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,X0)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24116,f17255]) ).
fof(f24119,plain,
( k2_funct_1(k6_autgroup(sK32,sK33)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,sK33))
| ~ spl618_26 ),
inference(resolution,[],[f24117,f17256]) ).
fof(f24120,plain,
( ! [X0] :
( k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(resolution,[],[f24117,f17827]) ).
fof(f24123,plain,
( ! [X0] :
( k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24120,f17255]) ).
fof(f24125,plain,
( ! [X0] :
( k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24123,f17253]) ).
fof(f24127,plain,
( ! [X0] :
( k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0)))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24125,f17252]) ).
fof(f24129,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,X0))) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24127,f17251]) ).
fof(f24146,plain,
( ~ l1_group_1(k5_autgroup(sK32))
| spl618_100 ),
inference(resolution,[],[f24094,f19195]) ).
fof(f24248,plain,
( k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_26 ),
inference(resolution,[],[f24129,f17256]) ).
fof(f24509,definition,
( spl618_150
<=> m1_subset_1(k6_autgroup(sK32,sK33),k4_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_150])],[avatar_definition]) ).
fof(f24510,plain,
( m1_subset_1(k6_autgroup(sK32,sK33),k4_autgroup(sK32))
| ~ spl618_150 ),
inference(avatar_component_clause,[],[f24509]) ).
fof(f24521,definition,
( spl618_151
<=> m2_fraenkel(k6_autgroup(sK32,sK33),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_151])],[avatar_definition]) ).
fof(f24522,plain,
( m2_fraenkel(k6_autgroup(sK32,sK33),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ spl618_151 ),
inference(avatar_component_clause,[],[f24521]) ).
fof(f24527,plain,
( ~ m2_fraenkel(k6_autgroup(sK32,sK33),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| spl618_151 ),
inference(avatar_component_clause,[],[f24521]) ).
fof(f24597,plain,
( m1_subset_1(k6_autgroup(sK32,sK33),k4_autgroup(sK32))
| ~ spl618_26
| ~ spl618_151 ),
inference(resolution,[],[f24522,f23377]) ).
fof(f24658,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f23825,f17827]) ).
fof(f24660,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24658,f17255]) ).
fof(f24662,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24660,f17253]) ).
fof(f24664,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24662,f17252]) ).
fof(f24666,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,X0)),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24664,f17251]) ).
fof(f24793,plain,
m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32)),
inference(resolution,[],[f23933,f17256]) ).
fof(f24816,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,X0)),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(resolution,[],[f23802,f17167]) ).
fof(f24820,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,X0)),k4_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24816,f17255]) ).
fof(f24822,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,X0)),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24820,f17254]) ).
fof(f24824,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,X0)),k4_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24822,f17253]) ).
fof(f24826,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,X0)),k4_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24824,f17252]) ).
fof(f24828,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m1_subset_1(k2_funct_1(k6_autgroup(sK32,X0)),k4_autgroup(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24826,f17251]) ).
fof(f24830,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(resolution,[],[f24828,f17827]) ).
fof(f24832,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24830,f17255]) ).
fof(f24834,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))),k4_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24832,f17253]) ).
fof(f24836,plain,
( ! [X0] :
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))),k4_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24834,f17252]) ).
fof(f24838,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,X0))),k4_autgroup(sK32)) )
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f24836,f17251]) ).
fof(f24889,plain,
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),k4_autgroup(sK32))
| ~ spl618_26 ),
inference(resolution,[],[f24838,f17256]) ).
fof(f25058,plain,
( m2_fraenkel(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f24793,f17212]) ).
fof(f25060,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f24793,f22425]) ).
fof(f25061,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25060,f17255]) ).
fof(f25063,plain,
( m2_fraenkel(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25058,f17255]) ).
fof(f25069,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25061,f17254]) ).
fof(f25071,plain,
( m2_fraenkel(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25063,f17254]) ).
fof(f25077,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25069,f17253]) ).
fof(f25079,plain,
( m2_fraenkel(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25071,f17253]) ).
fof(f25085,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25077,f17252]) ).
fof(f25087,plain,
( m2_fraenkel(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25079,f17252]) ).
fof(f25093,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33))) ),
inference(forward_subsumption_resolution,[],[f25085,f17251]) ).
fof(f25095,plain,
m2_fraenkel(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k1_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f25087,f17251]) ).
fof(f25102,definition,
( spl618_194
<=> k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33))) ),
introduced(definition,[new_symbols(definition,[spl618_194])],[avatar_definition]) ).
fof(f25103,plain,
( k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) = k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_194 ),
inference(avatar_component_clause,[],[f25102]) ).
fof(f25105,definition,
( spl618_195
<=> m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32))) ),
introduced(definition,[new_symbols(definition,[spl618_195])],[avatar_definition]) ).
fof(f25106,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| spl618_195 ),
inference(avatar_component_clause,[],[f25105]) ).
fof(f25107,plain,
( spl618_194
| ~ spl618_195 ),
inference(avatar_split_clause,[],[f25093,f25105,f25102]) ).
fof(f25230,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f25095,f22425]) ).
fof(f25231,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25230,f17255]) ).
fof(f25239,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25231,f17254]) ).
fof(f25247,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25239,f17253]) ).
fof(f25255,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25247,f17252]) ).
fof(f25263,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) ),
inference(forward_subsumption_resolution,[],[f25255,f17251]) ).
fof(f25272,definition,
( spl618_207
<=> k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) ),
introduced(definition,[new_symbols(definition,[spl618_207])],[avatar_definition]) ).
fof(f25273,plain,
( k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_207 ),
inference(avatar_component_clause,[],[f25272]) ).
fof(f25275,definition,
( spl618_208
<=> m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32))) ),
introduced(definition,[new_symbols(definition,[spl618_208])],[avatar_definition]) ).
fof(f25276,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| spl618_208 ),
inference(avatar_component_clause,[],[f25275]) ).
fof(f25277,plain,
( spl618_207
| ~ spl618_208 ),
inference(avatar_split_clause,[],[f25263,f25275,f25272]) ).
fof(f25412,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,k3_group_1(sK32,X0))),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f24666,f17827]) ).
fof(f25414,plain,
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f24666,f17256]) ).
fof(f25415,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,k3_group_1(sK32,X0))),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f25412,f17255]) ).
fof(f25417,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,k3_group_1(sK32,X0))),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f25415,f17253]) ).
fof(f25419,plain,
( ! [X0] :
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,k3_group_1(sK32,X0))),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f25417,f17252]) ).
fof(f25421,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK32))
| m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,k3_group_1(sK32,X0))),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32)) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f25419,f17251]) ).
fof(f25423,plain,
( ! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),X0) = k1_group_1(k5_autgroup(sK32),X0,k6_autgroup(sK32,k3_group_1(sK32,sK33))) )
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f25414,f23334]) ).
fof(f25426,plain,
( m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),k4_autgroup(sK32))
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f25414,f23377]) ).
fof(f25435,definition,
( spl618_222
<=> k6_autgroup(sK32,sK33) = k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))) ),
introduced(definition,[new_symbols(definition,[spl618_222])],[avatar_definition]) ).
fof(f25436,plain,
( k6_autgroup(sK32,sK33) = k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_222 ),
inference(avatar_component_clause,[],[f25435]) ).
fof(f25438,plain,
( ! [X0] :
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),X0) = k1_group_1(k5_autgroup(sK32),X0,k6_autgroup(sK32,k3_group_1(sK32,sK33))) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_demodulation,[],[f25423,f24063]) ).
fof(f25439,plain,
( ! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),X0) = k1_group_1(k5_autgroup(sK32),X0,k6_autgroup(sK32,k3_group_1(sK32,sK33))) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f25438,f25426]) ).
fof(f25440,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| ~ m2_fraenkel(X0,u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),X0) = k1_group_1(k5_autgroup(sK32),X0,k6_autgroup(sK32,k3_group_1(sK32,sK33))) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_demodulation,[],[f25439,f24063]) ).
fof(f25441,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),X0) = k1_group_1(k5_autgroup(sK32),X0,k6_autgroup(sK32,k3_group_1(sK32,sK33))) )
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_subsumption_resolution,[],[f25440,f23373]) ).
fof(f25941,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f23721,f17253]) ).
fof(f25944,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| ~ v1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25941,f17255]) ).
fof(f25946,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25944,f17254]) ).
fof(f25948,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f25946,f17252]) ).
fof(f25950,plain,
! [X0] :
( m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32))) ),
inference(forward_subsumption_resolution,[],[f25948,f17251]) ).
fof(f25951,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(sK32))) ),
inference(forward_demodulation,[],[f25950,f24063]) ).
fof(f25958,plain,
( m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),u1_struct_0(k3_autgroup(sK32)))
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f25951,f25426]) ).
fof(f25961,plain,
( m1_subset_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))),u1_struct_0(k3_autgroup(sK32)))
| ~ spl618_26 ),
inference(resolution,[],[f25951,f24889]) ).
fof(f25966,plain,
( $false
| ~ spl618_26
| spl618_208 ),
inference(forward_subsumption_resolution,[],[f25961,f25276]) ).
fof(f25967,plain,
( ~ spl618_26
| spl618_208 ),
inference(avatar_contradiction_clause,[],[f25966]) ).
fof(f25970,plain,
( $false
| ~ spl618_25
| ~ spl618_26
| spl618_195 ),
inference(forward_subsumption_resolution,[],[f25958,f25106]) ).
fof(f25971,plain,
( ~ spl618_25
| ~ spl618_26
| spl618_195 ),
inference(avatar_contradiction_clause,[],[f25970]) ).
fof(f25976,plain,
( spl618_150
| ~ spl618_26
| ~ spl618_151 ),
inference(avatar_split_clause,[],[f24597,f24521,f23376,f24509]) ).
fof(f25998,plain,
( k7_funct_2(u1_struct_0(sK32),u1_struct_0(sK32),u1_struct_0(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)),k6_autgroup(sK32,sK33)) = k1_group_1(k5_autgroup(sK32),k6_autgroup(sK32,sK33),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150 ),
inference(resolution,[],[f24510,f25441]) ).
fof(f26020,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) = k3_group_1(k3_autgroup(sK32),k3_group_1(k3_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39 ),
inference(resolution,[],[f25958,f23454]) ).
fof(f26033,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) = k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194 ),
inference(forward_demodulation,[],[f26020,f25103]) ).
fof(f26155,plain,
( k6_autgroup(sK32,sK33) != k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| spl618_222 ),
inference(avatar_component_clause,[],[f25435]) ).
fof(f26224,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) = k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207 ),
inference(superposition,[],[f25273,f26033]) ).
fof(f26418,plain,
! [X0] :
( ~ v1_group_1(sK32)
| v3_struct_0(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),X0) = k3_group_1(k5_autgroup(sK32),X0) ),
inference(resolution,[],[f23790,f17253]) ).
fof(f26421,plain,
! [X0] :
( v3_struct_0(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),X0) = k3_group_1(k5_autgroup(sK32),X0) ),
inference(forward_subsumption_resolution,[],[f26418,f17254]) ).
fof(f26423,plain,
! [X0] :
( ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),X0) = k3_group_1(k5_autgroup(sK32),X0) ),
inference(forward_subsumption_resolution,[],[f26421,f17255]) ).
fof(f26425,plain,
! [X0] :
( ~ l1_group_1(sK32)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),X0) = k3_group_1(k5_autgroup(sK32),X0) ),
inference(forward_subsumption_resolution,[],[f26423,f17252]) ).
fof(f26427,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| k3_group_1(k3_autgroup(sK32),X0) = k3_group_1(k5_autgroup(sK32),X0) ),
inference(forward_subsumption_resolution,[],[f26425,f17251]) ).
fof(f26428,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| k3_group_1(k3_autgroup(sK32),X0) = k3_group_1(k5_autgroup(sK32),X0) ),
inference(forward_demodulation,[],[f26427,f24063]) ).
fof(f26434,plain,
( k3_group_1(k3_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k5_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_26 ),
inference(resolution,[],[f26428,f24889]) ).
fof(f26435,plain,
( k2_funct_1(k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))) = k3_group_1(k5_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_26
| ~ spl618_207 ),
inference(forward_demodulation,[],[f26434,f25273]) ).
fof(f26440,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) = k3_group_1(k5_autgroup(sK32),k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33))))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207 ),
inference(forward_demodulation,[],[f26435,f26224]) ).
fof(f27413,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(X1))
| v3_struct_0(k3_autgroup(X1))
| v3_group_1(X0)
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(resolution,[],[f17309,f17160]) ).
fof(f27414,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(X1))
| v3_group_1(X0)
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f27413,f17162]) ).
fof(f27416,plain,
! [X0,X1] :
( ~ v3_group_1(X1)
| v3_group_1(X0)
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ m1_group_2(X0,k3_autgroup(X1))
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f27414,f17158]) ).
fof(f27840,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(X1))
| v3_struct_0(k3_autgroup(X1))
| l1_group_1(X0)
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(resolution,[],[f17308,f17160]) ).
fof(f27841,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(X1))
| l1_group_1(X0)
| ~ l1_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ v1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f27840,f17162]) ).
fof(f27843,plain,
! [X0,X1] :
( ~ v1_group_1(X1)
| l1_group_1(X0)
| v3_struct_0(X1)
| ~ m1_group_2(X0,k3_autgroup(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f27841,f17158]) ).
fof(f30397,plain,
( v1_xboole_0(k4_autgroup(sK32))
| ~ spl618_101 ),
inference(avatar_component_clause,[],[f24096]) ).
fof(f30713,plain,
( $false
| ~ spl618_101 ),
inference(unit_resulting_resolution,[],[f17267,f23335,f30397]) ).
fof(f30715,plain,
~ spl618_101,
inference(avatar_contradiction_clause,[],[f30713]) ).
fof(f31723,plain,
( m2_fraenkel(k6_autgroup(sK32,k3_group_1(sK32,k3_group_1(sK32,sK33))),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ spl618_25
| ~ spl618_26 ),
inference(resolution,[],[f25421,f17256]) ).
fof(f31724,plain,
( m2_fraenkel(k6_autgroup(sK32,sK33),u1_struct_0(sK32),u1_struct_0(sK32),k4_autgroup(sK32))
| ~ spl618_25
| ~ spl618_26 ),
inference(forward_demodulation,[],[f31723,f23344]) ).
fof(f38011,plain,
! [X0] :
( l1_group_1(X0)
| v3_struct_0(sK32)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f27843,f17254]) ).
fof(f38015,plain,
! [X0] :
( l1_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38011,f17255]) ).
fof(f38017,plain,
! [X0] :
( l1_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38015,f17253]) ).
fof(f38019,plain,
! [X0] :
( l1_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38017,f17252]) ).
fof(f38021,plain,
! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f38019,f17251]) ).
fof(f38022,plain,
( l1_group_1(k3_autgroup(sK32))
| ~ spl618_41 ),
inference(resolution,[],[f38021,f23462]) ).
fof(f38023,plain,
( l1_group_1(k5_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f38021,f17164]) ).
fof(f38024,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_54 ),
inference(forward_subsumption_resolution,[],[f38023,f23558]) ).
fof(f38025,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_54 ),
inference(forward_subsumption_resolution,[],[f38024,f17255]) ).
fof(f38026,plain,
( ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_54 ),
inference(forward_subsumption_resolution,[],[f38025,f17254]) ).
fof(f38027,plain,
( ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_54 ),
inference(forward_subsumption_resolution,[],[f38026,f17253]) ).
fof(f38028,plain,
( ~ l1_group_1(sK32)
| spl618_54 ),
inference(forward_subsumption_resolution,[],[f38027,f17252]) ).
fof(f38029,plain,
( $false
| spl618_54 ),
inference(forward_subsumption_resolution,[],[f38028,f17251]) ).
fof(f38030,plain,
spl618_54,
inference(avatar_contradiction_clause,[],[f38029]) ).
fof(f38034,definition,
( spl618_770
<=> v4_group_1(k5_autgroup(sK32)) ),
introduced(definition,[new_symbols(definition,[spl618_770])],[avatar_definition]) ).
fof(f38035,plain,
( ~ v4_group_1(k5_autgroup(sK32))
| spl618_770 ),
inference(avatar_component_clause,[],[f38034]) ).
fof(f38127,plain,
( ~ spl618_54
| spl618_100 ),
inference(avatar_split_clause,[],[f24146,f24093,f23557]) ).
fof(f38165,plain,
( l1_group_1(k5_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38023,f17255]) ).
fof(f38202,plain,
( l1_group_1(k5_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38165,f17254]) ).
fof(f38236,plain,
( l1_group_1(k5_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38202,f17253]) ).
fof(f38269,plain,
( l1_group_1(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f38236,f17252]) ).
fof(f38289,plain,
l1_group_1(k5_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f38269,f17251]) ).
fof(f38365,plain,
( v1_xboole_0(u1_struct_0(k5_autgroup(sK32)))
| ~ l1_struct_0(k5_autgroup(sK32))
| ~ spl618_55 ),
inference(resolution,[],[f23561,f19202]) ).
fof(f38367,plain,
( v1_xboole_0(k4_autgroup(sK32))
| ~ l1_struct_0(k5_autgroup(sK32))
| ~ spl618_55 ),
inference(forward_demodulation,[],[f38365,f24063]) ).
fof(f38368,plain,
( ~ l1_struct_0(k5_autgroup(sK32))
| ~ spl618_55
| spl618_101 ),
inference(forward_subsumption_resolution,[],[f38367,f24097]) ).
fof(f38369,plain,
( ~ spl618_100
| ~ spl618_55
| spl618_101 ),
inference(avatar_split_clause,[],[f38368,f24096,f23560,f24093]) ).
fof(f39924,plain,
! [X0] :
( v3_group_1(X0)
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f27416,f17253]) ).
fof(f39925,plain,
! [X0] :
( v3_group_1(X0)
| ~ v1_group_1(sK32)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39924,f17255]) ).
fof(f39928,plain,
! [X0] :
( v3_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39925,f17254]) ).
fof(f39931,plain,
! [X0] :
( v3_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39928,f17252]) ).
fof(f39934,plain,
! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| v3_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f39931,f17251]) ).
fof(f39940,plain,
( v3_group_1(k3_autgroup(sK32))
| ~ spl618_41 ),
inference(resolution,[],[f39934,f23462]) ).
fof(f39941,plain,
( v3_group_1(k5_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f39934,f17164]) ).
fof(f39942,plain,
( v3_group_1(k5_autgroup(sK32))
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39941,f17255]) ).
fof(f39943,plain,
( v3_group_1(k5_autgroup(sK32))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39942,f17254]) ).
fof(f39944,plain,
( v3_group_1(k5_autgroup(sK32))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39943,f17253]) ).
fof(f39945,plain,
( v3_group_1(k5_autgroup(sK32))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f39944,f17252]) ).
fof(f39946,plain,
v3_group_1(k5_autgroup(sK32)),
inference(forward_subsumption_resolution,[],[f39945,f17251]) ).
fof(f39963,plain,
! [X0,X1] :
( k2_group_1(k5_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| v3_struct_0(k5_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ v4_group_1(k5_autgroup(sK32))
| ~ l1_group_1(k5_autgroup(sK32)) ),
inference(resolution,[],[f39946,f17841]) ).
fof(f40051,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| v3_struct_0(k3_autgroup(sK32))
| v4_group_1(X0)
| ~ v4_group_1(k3_autgroup(sK32))
| ~ l1_group_1(k3_autgroup(sK32)) )
| ~ spl618_41 ),
inference(resolution,[],[f39940,f17315]) ).
fof(f40150,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| v3_struct_0(k3_autgroup(sK32))
| v4_group_1(X0)
| ~ l1_group_1(k3_autgroup(sK32)) )
| ~ spl618_41 ),
inference(forward_subsumption_resolution,[],[f40051,f23331]) ).
fof(f40220,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| v3_struct_0(k3_autgroup(sK32))
| v4_group_1(X0) )
| ~ spl618_41 ),
inference(forward_subsumption_resolution,[],[f40150,f38022]) ).
fof(f40391,definition,
( spl618_999
<=> ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| v4_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl618_999])],[avatar_definition]) ).
fof(f40392,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK32))
| v4_group_1(X0) )
| ~ spl618_999 ),
inference(avatar_component_clause,[],[f40391]) ).
fof(f40393,plain,
( spl618_36
| spl618_999
| ~ spl618_41 ),
inference(avatar_split_clause,[],[f40220,f23461,f40391,f23442]) ).
fof(f40455,plain,
( v4_group_1(k5_autgroup(sK32))
| v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ spl618_999 ),
inference(resolution,[],[f40392,f17164]) ).
fof(f40456,plain,
( v3_struct_0(sK32)
| ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_770
| ~ spl618_999 ),
inference(forward_subsumption_resolution,[],[f40455,f38035]) ).
fof(f40457,plain,
( ~ v1_group_1(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_770
| ~ spl618_999 ),
inference(forward_subsumption_resolution,[],[f40456,f17255]) ).
fof(f40458,plain,
( ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_770
| ~ spl618_999 ),
inference(forward_subsumption_resolution,[],[f40457,f17254]) ).
fof(f40459,plain,
( ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| spl618_770
| ~ spl618_999 ),
inference(forward_subsumption_resolution,[],[f40458,f17253]) ).
fof(f40460,plain,
( ~ l1_group_1(sK32)
| spl618_770
| ~ spl618_999 ),
inference(forward_subsumption_resolution,[],[f40459,f17252]) ).
fof(f40461,plain,
( $false
| spl618_770
| ~ spl618_999 ),
inference(forward_subsumption_resolution,[],[f40460,f17251]) ).
fof(f40462,plain,
( spl618_770
| ~ spl618_999 ),
inference(avatar_contradiction_clause,[],[f40461]) ).
fof(f40504,plain,
! [X0,X1] :
( k2_group_1(k5_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| v3_struct_0(k5_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ v4_group_1(k5_autgroup(sK32)) ),
inference(forward_subsumption_resolution,[],[f39963,f38289]) ).
fof(f40582,plain,
! [X0,X1] :
( k2_group_1(k3_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK32)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| v3_struct_0(k5_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ v4_group_1(k5_autgroup(sK32)) ),
inference(forward_demodulation,[],[f40504,f23524]) ).
fof(f40648,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| k2_group_1(k3_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK32)))
| v3_struct_0(k5_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ v4_group_1(k5_autgroup(sK32)) ),
inference(forward_demodulation,[],[f40582,f24063]) ).
fof(f40711,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK32))
| ~ m1_subset_1(X0,k4_autgroup(sK32))
| k2_group_1(k3_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1)
| v3_struct_0(k5_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ v4_group_1(k5_autgroup(sK32)) ),
inference(forward_demodulation,[],[f40648,f24063]) ).
fof(f40766,definition,
( spl618_1045
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ m1_subset_1(X0,k4_autgroup(sK32))
| k2_group_1(k3_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl618_1045])],[avatar_definition]) ).
fof(f40767,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK32))
| k3_group_1(k5_autgroup(sK32),X1) = X0
| ~ m1_subset_1(X1,k4_autgroup(sK32))
| k2_group_1(k3_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),X0,X1) )
| ~ spl618_1045 ),
inference(avatar_component_clause,[],[f40766]) ).
fof(f40768,plain,
( ~ spl618_770
| spl618_55
| spl618_1045 ),
inference(avatar_split_clause,[],[f40711,f40766,f23560,f38034]) ).
fof(f41256,plain,
( ! [X0] :
( k2_group_1(k3_autgroup(sK32)) != k1_group_1(k5_autgroup(sK32),k6_autgroup(sK32,sK33),X0)
| ~ m1_subset_1(X0,k4_autgroup(sK32))
| k6_autgroup(sK32,sK33) = k3_group_1(k5_autgroup(sK32),X0) )
| ~ spl618_150
| ~ spl618_1045 ),
inference(resolution,[],[f40767,f24510]) ).
fof(f41350,plain,
( k2_group_1(k3_autgroup(sK32)) = k1_group_1(k5_autgroup(sK32),k6_autgroup(sK32,sK33),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150 ),
inference(forward_demodulation,[],[f25998,f23543]) ).
fof(f41367,plain,
( $false
| ~ spl618_25
| ~ spl618_26
| spl618_151 ),
inference(forward_subsumption_resolution,[],[f31724,f24527]) ).
fof(f41368,plain,
( ~ spl618_25
| ~ spl618_26
| spl618_151 ),
inference(avatar_contradiction_clause,[],[f41367]) ).
fof(f41916,plain,
( k2_group_1(k3_autgroup(sK32)) != k2_group_1(k3_autgroup(sK32))
| ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),k4_autgroup(sK32))
| k6_autgroup(sK32,sK33) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| ~ spl618_1045 ),
inference(superposition,[],[f41256,f41350]) ).
fof(f41917,plain,
( ~ m1_subset_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)),k4_autgroup(sK32))
| k6_autgroup(sK32,sK33) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| ~ spl618_1045 ),
inference(trivial_inequality_removal,[],[f41916]) ).
fof(f41918,plain,
( k6_autgroup(sK32,sK33) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| ~ spl618_1045 ),
inference(forward_subsumption_resolution,[],[f41917,f25426]) ).
fof(f41920,plain,
( k6_autgroup(sK32,sK33) = k2_funct_1(k6_autgroup(sK32,k3_group_1(sK32,sK33)))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| ~ spl618_1045 ),
inference(superposition,[],[f41918,f24248]) ).
fof(f41946,plain,
( $false
| ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| spl618_222
| ~ spl618_1045 ),
inference(forward_subsumption_resolution,[],[f41920,f26155]) ).
fof(f41947,plain,
( ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| spl618_222
| ~ spl618_1045 ),
inference(avatar_contradiction_clause,[],[f41946]) ).
fof(f42123,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) = k3_group_1(k5_autgroup(sK32),k6_autgroup(sK32,sK33))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207
| ~ spl618_222 ),
inference(superposition,[],[f26440,f25436]) ).
fof(f42146,plain,
( k6_autgroup(sK32,k3_group_1(sK32,sK33)) = k2_funct_1(k6_autgroup(sK32,sK33))
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207
| ~ spl618_222 ),
inference(forward_demodulation,[],[f42123,f24119]) ).
fof(f42155,plain,
( $false
| ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207
| ~ spl618_222 ),
inference(forward_subsumption_resolution,[],[f42146,f17257]) ).
fof(f42156,plain,
( ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207
| ~ spl618_222 ),
inference(avatar_contradiction_clause,[],[f42155]) ).
cnf(s19,plain,
( spl618_24
| spl618_25 ),
inference(sat_conversion,[],[f23374]) ).
cnf(s20,plain,
( spl618_24
| spl618_26 ),
inference(sat_conversion,[],[f23378]) ).
cnf(s24,plain,
~ spl618_24,
inference(sat_conversion,[],[f23394]) ).
cnf(s31,plain,
( ~ spl618_33
| ~ spl618_34
| spl618_36
| spl618_39 ),
inference(sat_conversion,[],[f23455]) ).
cnf(s33,plain,
( ~ spl618_33
| ~ spl618_34
| spl618_36
| spl618_41 ),
inference(sat_conversion,[],[f23463]) ).
cnf(s45,plain,
spl618_33,
inference(sat_conversion,[],[f23510]) ).
cnf(s46,plain,
spl618_34,
inference(sat_conversion,[],[f23513]) ).
cnf(s47,plain,
~ spl618_36,
inference(sat_conversion,[],[f23517]) ).
cnf(s165,plain,
( spl618_194
| ~ spl618_195 ),
inference(sat_conversion,[],[f25107]) ).
cnf(s175,plain,
( spl618_207
| ~ spl618_208 ),
inference(sat_conversion,[],[f25277]) ).
cnf(s234,plain,
( ~ spl618_26
| spl618_208 ),
inference(sat_conversion,[],[f25967]) ).
cnf(s236,plain,
( ~ spl618_25
| ~ spl618_26
| spl618_195 ),
inference(sat_conversion,[],[f25971]) ).
cnf(s238,plain,
( ~ spl618_26
| spl618_150
| ~ spl618_151 ),
inference(sat_conversion,[],[f25976]) ).
cnf(s375,plain,
~ spl618_101,
inference(sat_conversion,[],[f30715]) ).
cnf(s759,plain,
spl618_54,
inference(sat_conversion,[],[f38030]) ).
cnf(s780,plain,
( ~ spl618_54
| spl618_100 ),
inference(sat_conversion,[],[f38127]) ).
cnf(s805,plain,
( ~ spl618_55
| ~ spl618_100
| spl618_101 ),
inference(sat_conversion,[],[f38369]) ).
cnf(s975,plain,
( spl618_36
| ~ spl618_41
| spl618_999 ),
inference(sat_conversion,[],[f40393]) ).
cnf(s985,plain,
( spl618_770
| ~ spl618_999 ),
inference(sat_conversion,[],[f40462]) ).
cnf(s1024,plain,
( spl618_55
| ~ spl618_770
| spl618_1045 ),
inference(sat_conversion,[],[f40768]) ).
cnf(s1095,plain,
( ~ spl618_25
| ~ spl618_26
| spl618_151 ),
inference(sat_conversion,[],[f41368]) ).
cnf(s1144,plain,
( ~ spl618_25
| ~ spl618_26
| ~ spl618_150
| spl618_222
| ~ spl618_1045 ),
inference(sat_conversion,[],[f41947]) ).
cnf(s1167,plain,
( ~ spl618_25
| ~ spl618_26
| ~ spl618_39
| ~ spl618_194
| ~ spl618_207
| ~ spl618_222 ),
inference(sat_conversion,[],[f42156]) ).
cnf(s1215,plain,
spl618_100,
inference(rat,[],[s780,s759]) ).
cnf(s1377,plain,
~ spl618_55,
inference(rat,[],[s805,s1215,s375]) ).
cnf(s1500,plain,
spl618_41,
inference(rat,[],[s33,s47,s46,s45]) ).
cnf(s1503,plain,
spl618_999,
inference(rat,[],[s975,s47,s1500]) ).
cnf(s1559,plain,
spl618_770,
inference(rat,[],[s985,s1503]) ).
cnf(s1579,plain,
spl618_1045,
inference(rat,[],[s1024,s1377,s1559]) ).
cnf(s1646,plain,
spl618_39,
inference(rat,[],[s31,s47,s46,s45]) ).
cnf(s1679,plain,
spl618_26,
inference(rat,[],[s20,s24]) ).
cnf(s1684,plain,
spl618_208,
inference(rat,[],[s234,s1679]) ).
cnf(s1689,plain,
spl618_207,
inference(rat,[],[s175,s1684]) ).
cnf(s1704,plain,
spl618_25,
inference(rat,[],[s19,s24]) ).
cnf(s1706,plain,
spl618_151,
inference(rat,[],[s1095,s1679,s1704]) ).
cnf(s1712,plain,
spl618_195,
inference(rat,[],[s236,s1679,s1704]) ).
cnf(s1716,plain,
spl618_150,
inference(rat,[],[s238,s1679,s1706]) ).
cnf(s1721,plain,
spl618_194,
inference(rat,[],[s165,s1712]) ).
cnf(s1729,plain,
spl618_222,
inference(rat,[],[s1144,s1579,s1704,s1679,s1716]) ).
cnf(s1733,plain,
$false,
inference(rat,[],[s1167,s1704,s1689,s1679,s1646,s1729,s1721]) ).
fof(f42161,plain,
$false,
inference(avatar_sat_refutation,[],[s1733]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP630+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n016.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 10:20:34 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.59/3.19 % (2413478)Detected formulas, will run a generic FOF schedule.
% 12.59/3.19 % (2413498)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1355893790:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 12.59/3.19 % (2413493)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=3686716999:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 12.59/3.19 % (2413495)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=529870443:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 12.59/3.19 % (2413491)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=3727567860:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 12.59/3.19 % (2413501)dis-21_1_sil=8000:lcm=predicate:random_seed=1004716370:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 12.59/3.19 % (2413496)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=894275867:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 12.59/3.19 % (2413500)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2575719393:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 12.59/3.19 % (2413498)Instruction limit reached!
% 12.59/3.19 % (2413498)------------------------------
% 12.59/3.19 % (2413498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/3.19 % (2413498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/3.19 % (2413498)CaDiCaL version: 2.1.3
% 12.59/3.19 % (2413498)Termination reason: Instruction limit
% 12.59/3.19 % (2413498)Termination phase: Preprocessing 3
% 12.59/3.19 % (2413498)Time elapsed: 0.061 s
% 12.59/3.19 % (2413498)Peak memory usage: 105 MB
% 12.59/3.19 % (2413498)Instructions burned: 121 (million)
% 12.59/3.19 % (2413500)Instruction limit reached!
% 12.59/3.19 % (2413500)------------------------------
% 12.59/3.19 % (2413500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/3.19 % (2413500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/3.19 % (2413500)CaDiCaL version: 2.1.3
% 12.59/3.19 % (2413500)Termination reason: Instruction limit
% 12.59/3.19 % (2413500)Termination phase: Property scanning
% 12.59/3.19 % (2413500)Time elapsed: 0.061 s
% 12.59/3.19 % (2413500)Peak memory usage: 101 MB
% 12.59/3.19 % (2413500)Instructions burned: 141 (million)
% 12.59/3.19 % (2413496)Instruction limit reached!
% 12.59/3.19 % (2413496)------------------------------
% 12.59/3.19 % (2413496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/3.19 % (2413496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/3.19 % (2413496)CaDiCaL version: 2.1.3
% 12.59/3.19 % (2413496)Termination reason: Instruction limit
% 12.59/3.19 % (2413496)Termination phase: Saturation
% 12.59/3.19 % (2413496)Time elapsed: 0.081 s
% 12.59/3.19 % (2413496)Peak memory usage: 105 MB
% 12.59/3.19 % (2413496)Instructions burned: 110 (million)
% 12.59/3.19 % (2413501)Instruction limit reached!
% 12.59/3.19 % (2413501)------------------------------
% 12.59/3.19 % (2413501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/3.19 % (2413501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/3.19 % (2413501)CaDiCaL version: 2.1.3
% 12.59/3.19 % (2413501)Termination reason: Instruction limit
% 12.59/3.19 % (2413501)Termination phase: Preprocessing 1
% 12.59/3.19 % (2413501)Time elapsed: 0.099 s
% 12.59/3.19 % (2413501)Peak memory usage: 102 MB
% 12.59/3.19 % (2413501)Instructions burned: 129 (million)
% 12.59/3.19 % (2413558)lrs+10_1_sil=8000:sp=occurrence:random_seed=3288004386:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 12.59/3.19 % (2413572)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2868800117:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 12.59/3.19 % (2413578)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2283740991:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 12.59/3.19 % (2413558)Instruction limit reached!
% 12.59/3.19 % (2413558)------------------------------
% 12.59/3.19 % (2413558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/3.19 % (2413558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/4.09 % (2413558)CaDiCaL version: 2.1.3
% 19.00/4.09 % (2413558)Termination reason: Instruction limit
% 19.00/4.09 % (2413558)Termination phase: Saturation
% 19.00/4.09 % (2413558)Time elapsed: 0.109 s
% 19.00/4.09 % (2413558)Peak memory usage: 110 MB
% 19.00/4.09 % (2413558)Instructions burned: 286 (million)
% 19.00/4.09 % (2413584)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=408377998:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 19.00/4.09 % (2413572)Instruction limit reached!
% 19.00/4.09 % (2413572)------------------------------
% 19.00/4.09 % (2413572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.00/4.09 % (2413572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/4.09 % (2413572)CaDiCaL version: 2.1.3
% 19.00/4.09 % (2413572)Termination reason: Instruction limit
% 19.00/4.09 % (2413572)Termination phase: Property scanning
% 19.00/4.09 % (2413572)Time elapsed: 0.069 s
% 19.00/4.09 % (2413572)Peak memory usage: 101 MB
% 19.00/4.09 % (2413572)Instructions burned: 159 (million)
% 19.00/4.09 % (2413624)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2742686827:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 19.00/4.09 % (2413584)Instruction limit reached!
% 19.00/4.09 % (2413584)------------------------------
% 19.00/4.09 % (2413584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.00/4.09 % (2413584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/4.09 % (2413584)CaDiCaL version: 2.1.3
% 19.00/4.09 % (2413584)Termination reason: Instruction limit
% 19.00/4.09 % (2413584)Termination phase: SInE selection
% 19.00/4.09 % (2413584)Time elapsed: 0.129 s
% 19.00/4.09 % (2413584)Peak memory usage: 102 MB
% 19.00/4.09 % (2413584)Instructions burned: 249 (million)
% 19.00/4.09 % (2413626)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2344171705:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 19.00/4.09 % (2413578)Instruction limit reached!
% 19.00/4.09 % (2413578)------------------------------
% 19.00/4.09 % (2413578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.00/4.09 % (2413578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/4.09 % (2413578)CaDiCaL version: 2.1.3
% 19.00/4.09 % (2413578)Termination reason: Instruction limit
% 19.00/4.09 % (2413578)Termination phase: Saturation
% 19.00/4.09 % (2413578)Time elapsed: 0.225 s
% 19.00/4.09 % (2413578)Peak memory usage: 108 MB
% 19.00/4.09 % (2413578)Instructions burned: 325 (million)
% 19.00/4.09 % (2413624)Instruction limit reached!
% 19.00/4.09 % (2413624)------------------------------
% 19.00/4.09 % (2413624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.00/4.09 % (2413624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/4.09 % (2413624)CaDiCaL version: 2.1.3
% 19.00/4.09 % (2413624)Termination reason: Instruction limit
% 19.00/4.09 % (2413624)Termination phase: Saturation
% 19.00/4.09 % (2413624)Time elapsed: 0.107 s
% 19.00/4.09 % (2413624)Peak memory usage: 110 MB
% 19.00/4.09 % (2413624)Instructions burned: 296 (million)
% 19.00/4.09 % (2413628)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1622388827:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 19.00/4.09 % (2413631)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3861868262:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 19.00/4.09 % (2413631)Instruction limit reached!
% 19.00/4.09 % (2413631)------------------------------
% 19.00/4.09 % (2413631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.00/4.09 % (2413631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/4.09 % (2413631)CaDiCaL version: 2.1.3
% 19.00/4.09 % (2413631)Termination reason: Instruction limit
% 19.00/4.09 % (2413631)Termination phase: Property scanning
% 19.00/4.09 % (2413631)Time elapsed: 0.027 s
% 19.00/4.09 % (2413631)Peak memory usage: 101 MB
% 19.00/4.09 % (2413631)Instructions burned: 119 (million)
% 19.00/4.09 % (2413630)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2836435353:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 19.00/4.09 % (2413628)Instruction limit reached!
% 19.00/4.09 % (2413628)------------------------------
% 19.00/4.09 % (2413628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413628)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413628)Termination reason: Instruction limit
% 27.84/5.98 % (2413628)Termination phase: Preprocessing 3
% 27.84/5.98 % (2413628)Time elapsed: 0.096 s
% 27.84/5.98 % (2413628)Peak memory usage: 105 MB
% 27.84/5.98 % (2413628)Instructions burned: 113 (million)
% 27.84/5.98 % (2413630)Instruction limit reached!
% 27.84/5.98 % (2413630)------------------------------
% 27.84/5.98 % (2413630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413630)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413630)Termination reason: Instruction limit
% 27.84/5.98 % (2413630)Termination phase: Preprocessing 2
% 27.84/5.98 % (2413630)Time elapsed: 0.104 s
% 27.84/5.98 % (2413630)Peak memory usage: 107 MB
% 27.84/5.98 % (2413630)Instructions burned: 127 (million)
% 27.84/5.98 % (2413634)lrs+10_1_sil=8000:sp=occurrence:random_seed=2285343348:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 27.84/5.98 % (2413636)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1363659344:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 27.84/5.98 % (2413638)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2666938849:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 27.84/5.98 % (2413634)Instruction limit reached!
% 27.84/5.98 % (2413634)------------------------------
% 27.84/5.98 % (2413634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413634)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413634)Termination reason: Instruction limit
% 27.84/5.98 % (2413634)Termination phase: Saturation
% 27.84/5.98 % (2413634)Time elapsed: 0.297 s
% 27.84/5.98 % (2413634)Peak memory usage: 120 MB
% 27.84/5.98 % (2413634)Instructions burned: 907 (million)
% 27.84/5.98 % (2413636)Instruction limit reached!
% 27.84/5.98 % (2413636)------------------------------
% 27.84/5.98 % (2413636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413636)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413636)Termination reason: Instruction limit
% 27.84/5.98 % (2413636)Termination phase: Saturation
% 27.84/5.98 % (2413636)Time elapsed: 0.226 s
% 27.84/5.98 % (2413636)Peak memory usage: 107 MB
% 27.84/5.98 % (2413636)Instructions burned: 438 (million)
% 27.84/5.98 % (2413642)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2446494331:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 27.84/5.98 % (2413641)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4087958090:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 27.84/5.98 % (2413641)Instruction limit reached!
% 27.84/5.98 % (2413641)------------------------------
% 27.84/5.98 % (2413641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413641)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413641)Termination reason: Instruction limit
% 27.84/5.98 % (2413641)Termination phase: Property scanning
% 27.84/5.98 % (2413641)Time elapsed: 0.103 s
% 27.84/5.98 % (2413641)Peak memory usage: 105 MB
% 27.84/5.98 % (2413641)Instructions burned: 134 (million)
% 27.84/5.98 % (2413642)Instruction limit reached!
% 27.84/5.98 % (2413642)------------------------------
% 27.84/5.98 % (2413642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413642)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413642)Termination reason: Instruction limit
% 27.84/5.98 % (2413642)Termination phase: Property scanning
% 27.84/5.98 % (2413642)Time elapsed: 0.231 s
% 27.84/5.98 % (2413642)Peak memory usage: 122 MB
% 27.84/5.98 % (2413642)Instructions burned: 593 (million)
% 27.84/5.98 % (2413645)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1211561327:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 27.84/5.98 % (2413646)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=4105838788:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 27.84/5.98 % (2413646)Instruction limit reached!
% 27.84/5.98 % (2413646)------------------------------
% 27.84/5.98 % (2413646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413646)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413646)Termination reason: Instruction limit
% 27.84/5.98 % (2413646)Termination phase: Property scanning
% 27.84/5.98 % (2413646)Time elapsed: 0.030 s
% 27.84/5.98 % (2413646)Peak memory usage: 101 MB
% 27.84/5.98 % (2413646)Instructions burned: 129 (million)
% 27.84/5.98 % (2413649)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3547427332:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 27.84/5.98 % (2413649)Instruction limit reached!
% 27.84/5.98 % (2413649)------------------------------
% 27.84/5.98 % (2413649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413649)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413649)Termination reason: Instruction limit
% 27.84/5.98 % (2413649)Termination phase: Property scanning
% 27.84/5.98 % (2413649)Time elapsed: 0.032 s
% 27.84/5.98 % (2413649)Peak memory usage: 101 MB
% 27.84/5.98 % (2413649)Instructions burned: 136 (million)
% 27.84/5.98 % (2413651)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4006390459:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 27.84/5.98 % (2413626)Instruction limit reached!
% 27.84/5.98 % (2413626)------------------------------
% 27.84/5.98 % (2413626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413626)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413626)Termination reason: Instruction limit
% 27.84/5.98 % (2413626)Termination phase: Saturation
% 27.84/5.98 % (2413626)Time elapsed: 1.448 s
% 27.84/5.98 % (2413626)Peak memory usage: 228 MB
% 27.84/5.98 % (2413626)Instructions burned: 2350 (million)
% 27.84/5.98 % (2413651)Instruction limit reached!
% 27.84/5.98 % (2413651)------------------------------
% 27.84/5.98 % (2413651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413651)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413651)Termination reason: Instruction limit
% 27.84/5.98 % (2413651)Termination phase: Saturation
% 27.84/5.98 % (2413651)Time elapsed: 0.056 s
% 27.84/5.98 % (2413651)Peak memory usage: 106 MB
% 27.84/5.98 % (2413651)Instructions burned: 144 (million)
% 27.84/5.98 % (2413653)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3540722174:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 27.84/5.98 % (2413654)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=3217568391:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 27.84/5.98 % (2413653)Refutation not found, incomplete strategy
% 27.84/5.98 % (2413653)------------------------------
% 27.84/5.98 % (2413653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413653)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413653)Termination reason: Refutation not found, incomplete strategy
% 27.84/5.98 % (2413653)Time elapsed: 0.041 s
% 27.84/5.98 % (2413653)Peak memory usage: 106 MB
% 27.84/5.98 % (2413653)Instructions burned: 82 (million)
% 27.84/5.98 % (2413653)------------------------------
% 27.84/5.98 % (2413653)------------------------------
% 27.84/5.98 % (2413657)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=1183871035:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 27.84/5.98 % (2413657)Instruction limit reached!
% 27.84/5.98 % (2413657)------------------------------
% 27.84/5.98 % (2413657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.84/5.98 % (2413657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/5.98 % (2413657)CaDiCaL version: 2.1.3
% 27.84/5.98 % (2413657)Termination reason: Instruction limit
% 27.84/5.98 % (2413657)Termination phase: Preprocessing 1
% 27.84/5.98 % (2413657)Time elapsed: 0.067 s
% 27.84/5.98 % (2413657)Peak memory usage: 102 MB
% 27.84/5.98 % (2413657)Instructions burned: 152 (million)
% 27.84/5.98 % (2413659)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1246529565:i=14155:bd=all_2967 on theBenchmark for (2967ds/14155Mi)
% 27.84/5.98 % (2413493)First to succeed.
% 27.84/5.98 % (2413493)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2413478"
% 27.84/5.98 % (2413493)Refutation found. Thanks to Tanya!
% 27.84/5.98 % SZS status Theorem for theBenchmark
% 27.84/5.98 % SZS output start Proof for theBenchmark
% See solution above
% 32.89/6.18 % (2413493)------------------------------
% 32.89/6.18 % (2413493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.89/6.18 % (2413493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.89/6.18 % (2413493)CaDiCaL version: 2.1.3
% 32.89/6.18 % (2413493)Termination reason: Refutation
% 32.89/6.18 % (2413493)Time elapsed: 3.987 s
% 32.89/6.18 % (2413493)Peak memory usage: 209 MB
% 32.89/6.18 % (2413493)Instructions burned: 6001 (million)
% 32.89/6.18 % (2413493)------------------------------
% 32.89/6.18 % (2413493)------------------------------
% 32.89/6.18 % (2413478)Success in time 5.12 s
% 32.89/6.18 % Vampire exiting
%------------------------------------------------------------------------------