%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP630+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 25.82s 10.14s
% Output : Refutation 53.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 62
% Syntax : Number of formulae : 603 ( 65 unt; 28 def)
% Number of atoms : 2891 ( 342 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 4099 (1811 ~;1999 |; 172 &)
% ( 39 <=>; 78 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 29 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-5 aty)
% Number of variables : 625 ( 0 sgn 621 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f3367,axiom,
! [X0,X1,X2] :
( m1_fraenkel(X2,X0,X1)
=> ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_fraenkel) ).
fof(f3371,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X1)
& m1_fraenkel(X2,X0,X1) )
=> ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_fraenkel) ).
fof(f17598,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18264,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r2_hidden(X1,k2_pre_topc(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_pre_topc) ).
fof(f18891,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))
=> ( 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) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_group_1) ).
fof(f18898,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))
=> ( k3_group_1(X0,X1) = k3_group_1(X0,X2)
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_group_1) ).
fof(f18900,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/sandbox/benchmark/theBenchmark.p',t19_group_1) ).
fof(f18901,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/sandbox/benchmark/theBenchmark.p',t20_group_1) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f18994,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/sandbox/benchmark/theBenchmark.p',dt_k3_group_1) ).
fof(f21806,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/sandbox/benchmark/theBenchmark.p',cc1_group_2) ).
fof(f21862,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/sandbox/benchmark/theBenchmark.p',t51_group_2) ).
fof(f21863,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_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))
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X3))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X3))
=> ( ( X4 = X1
& X5 = X2 )
=> k1_group_1(X3,X4,X5) = k1_group_1(X0,X1,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_group_2) ).
fof(f21868,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/sandbox/benchmark/theBenchmark.p',t57_group_2) ).
fof(f21874,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/sandbox/benchmark/theBenchmark.p',t63_group_2) ).
fof(f21876,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v3_group_1(X2)
& v4_group_1(X2)
& l1_group_1(X2) )
=> ( ( m1_group_2(X0,X1)
& m1_group_2(X1,X2) )
=> m1_group_2(X0,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_group_2) ).
fof(f22007,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/sandbox/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f33387,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/sandbox/benchmark/theBenchmark.p',dt_k3_autgroup) ).
fof(f33388,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_autgroup) ).
fof(f33389,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_autgroup) ).
fof(f33390,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_autgroup) ).
fof(f33406,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/sandbox/benchmark/theBenchmark.p',t10_autgroup) ).
fof(f33407,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/sandbox/benchmark/theBenchmark.p',t11_autgroup) ).
fof(f33410,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/sandbox/benchmark/theBenchmark.p',t13_autgroup) ).
fof(f33414,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/sandbox/benchmark/theBenchmark.p',t17_autgroup) ).
fof(f33416,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& v1_group_3(X1,k3_autgroup(X0))
& m1_group_2(X1,k3_autgroup(X0)) )
=> ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_autgroup) ).
fof(f33418,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k5_autgroup(X0)))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k5_autgroup(X0)))
=> ! [X3] :
( m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ! [X4] :
( m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
=> ( ( X1 = X3
& X2 = X4 )
=> k1_group_1(k5_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_autgroup) ).
fof(f33419,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/sandbox/benchmark/theBenchmark.p',t21_autgroup) ).
fof(f33420,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/sandbox/benchmark/theBenchmark.p',t22_autgroup) ).
fof(f33423,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_group_1(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_autgroup) ).
fof(f33425,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/sandbox/benchmark/theBenchmark.p',t26_autgroup) ).
fof(f33427,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/sandbox/benchmark/theBenchmark.p',t28_autgroup) ).
fof(f33428,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)],[f33427]) ).
fof(f33517,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,[],[f33387]) ).
fof(f33518,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,[],[f33517]) ).
fof(f33519,plain,
! [X0] :
( m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33388]) ).
fof(f33520,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,[],[f33519]) ).
fof(f33521,plain,
! [X0] :
( ( v1_group_1(k5_autgroup(X0))
& v1_group_3(k5_autgroup(X0),k3_autgroup(X0))
& m1_group_2(k5_autgroup(X0),k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33389]) ).
fof(f33522,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,[],[f33521]) ).
fof(f33523,plain,
! [X0,X1] :
( m2_fraenkel(k6_autgroup(X0,X1),u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f33390]) ).
fof(f33524,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,[],[f33523]) ).
fof(f33553,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,[],[f33406]) ).
fof(f33554,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,[],[f33553]) ).
fof(f33555,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,[],[f33407]) ).
fof(f33556,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,[],[f33555]) ).
fof(f33561,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,[],[f33410]) ).
fof(f33562,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,[],[f33561]) ).
fof(f33569,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,[],[f33414]) ).
fof(f33570,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,[],[f33569]) ).
fof(f33573,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_autgroup(X0)
<=> u1_struct_0(X1) = k4_autgroup(X0) )
| ~ v1_group_1(X1)
| ~ v1_group_3(X1,k3_autgroup(X0))
| ~ m1_group_2(X1,k3_autgroup(X0)) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33416]) ).
fof(f33574,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,[],[f33573]) ).
fof(f33575,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( k1_group_1(k5_autgroup(X0),X1,X2) = k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),X4,X3)
| X1 != X3
| X2 != X4
| ~ m2_fraenkel(X4,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m2_fraenkel(X3,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(k5_autgroup(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(X0))) )
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33418]) ).
fof(f33576,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,[],[f33575]) ).
fof(f33577,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,[],[f33419]) ).
fof(f33578,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,[],[f33577]) ).
fof(f33579,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,[],[f33420]) ).
fof(f33580,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,[],[f33579]) ).
fof(f33585,plain,
! [X0] :
( k6_autgroup(X0,k2_group_1(X0)) = k6_partfun1(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f33423]) ).
fof(f33586,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,[],[f33585]) ).
fof(f33589,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,[],[f33425]) ).
fof(f33590,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,[],[f33589]) ).
fof(f33593,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,[],[f33428]) ).
fof(f33594,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,[],[f33593]) ).
fof(f33597,plain,
! [X0,X1,X2] :
( ! [X3] :
( m2_fraenkel(X3,X0,X1,X2)
<=> m1_subset_1(X3,X2) )
| v1_xboole_0(X1)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3371]) ).
fof(f33598,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,[],[f33597]) ).
fof(f33603,plain,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X2)
& v1_fraenkel(X2) )
| ~ m1_fraenkel(X2,X0,X1) ),
inference(ennf_transformation,[],[f3367]) ).
fof(f33622,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,[],[f22007]) ).
fof(f33623,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,[],[f33622]) ).
fof(f33626,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21876]) ).
fof(f33627,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f33626]) ).
fof(f33628,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,[],[f21874]) ).
fof(f33629,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,[],[f33628]) ).
fof(f33632,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,[],[f21862]) ).
fof(f33633,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,[],[f33632]) ).
fof(f33636,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,[],[f21806]) ).
fof(f33637,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,[],[f33636]) ).
fof(f33702,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f34028,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k1_group_1(X3,X4,X5) = k1_group_1(X0,X1,X2)
| X1 != X4
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3)) )
| ~ m1_subset_1(X4,u1_struct_0(X3)) )
| ~ m1_group_2(X3,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)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21863]) ).
fof(f34029,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k1_group_1(X3,X4,X5) = k1_group_1(X0,X1,X2)
| X1 != X4
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3)) )
| ~ m1_subset_1(X4,u1_struct_0(X3)) )
| ~ m1_group_2(X3,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)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f34028]) ).
fof(f34080,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,[],[f21868]) ).
fof(f34081,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,[],[f34080]) ).
fof(f34082,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,[],[f18994]) ).
fof(f34083,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,[],[f34082]) ).
fof(f34104,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,[],[f18901]) ).
fof(f34105,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,[],[f34104]) ).
fof(f34106,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,[],[f18900]) ).
fof(f34107,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,[],[f34106]) ).
fof(f34110,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| k3_group_1(X0,X1) != k3_group_1(X0,X2)
| ~ 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,[],[f18898]) ).
fof(f34111,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| k3_group_1(X0,X1) != k3_group_1(X0,X2)
| ~ 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,[],[f34110]) ).
fof(f34116,plain,
! [X0] :
( ! [X1] :
( ! [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,[],[f18891]) ).
fof(f34117,plain,
! [X0] :
( ! [X1] :
( ! [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,[],[f34116]) ).
fof(f36676,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f36682,plain,
! [X0] :
( ( v3_struct_0(X0)
<=> v1_xboole_0(u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f17598]) ).
fof(f37981,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18264]) ).
fof(f37982,plain,
! [X0] :
( ! [X1] :
( r2_hidden(X1,k2_pre_topc(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f37981]) ).
fof(f37984,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f39577,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,[],[f33574]) ).
fof(f39581,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) != k2_funct_1(k6_autgroup(sK45,sK46))
& m1_subset_1(sK46,u1_struct_0(sK45))
& ~ v3_struct_0(sK45)
& v1_group_1(sK45)
& v3_group_1(sK45)
& v4_group_1(sK45)
& l1_group_1(sK45) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45,sK46]),skolemize(X0,sK45),skolemize(X1,sK46)],[f33594]) ).
fof(f39582,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,[],[f33598]) ).
fof(f39750,plain,
! [X0] :
( ! [X1] :
( ! [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) )
& ( ( k1_group_1(X0,X1,X2) = k2_group_1(X0)
& k1_group_1(X0,X2,X1) = k2_group_1(X0) )
| k3_group_1(X0,X1) != X2 ) )
| ~ 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(nnf_transformation,[],[f34117]) ).
fof(f39751,plain,
! [X0] :
( ! [X1] :
( ! [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) )
& ( ( k1_group_1(X0,X1,X2) = k2_group_1(X0)
& k1_group_1(X0,X2,X1) = k2_group_1(X0) )
| k3_group_1(X0,X1) != X2 ) )
| ~ 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,[],[f39750]) ).
fof(f40461,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,[],[f36682]) ).
fof(f41286,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,[],[f33518]) ).
fof(f41287,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,[],[f33518]) ).
fof(f41288,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,[],[f33518]) ).
fof(f41290,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,[],[f33518]) ).
fof(f41291,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,[],[f33520]) ).
fof(f41292,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,[],[f33522]) ).
fof(f41293,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,[],[f33522]) ).
fof(f41294,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,[],[f33522]) ).
fof(f41295,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,[],[f33524]) ).
fof(f41348,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,[],[f33554]) ).
fof(f41349,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,[],[f33556]) ).
fof(f41360,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,[],[f33562]) ).
fof(f41364,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,[],[f33570]) ).
fof(f41366,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,[],[f39577]) ).
fof(f41368,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,[],[f33576]) ).
fof(f41369,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,[],[f33578]) ).
fof(f41370,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,[],[f33580]) ).
fof(f41375,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,[],[f33586]) ).
fof(f41377,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v1_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))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33590]) ).
fof(f41379,plain,
l1_group_1(sK45),
inference(cnf_transformation,[],[f39581]) ).
fof(f41380,plain,
v4_group_1(sK45),
inference(cnf_transformation,[],[f39581]) ).
fof(f41381,plain,
v3_group_1(sK45),
inference(cnf_transformation,[],[f39581]) ).
fof(f41382,plain,
v1_group_1(sK45),
inference(cnf_transformation,[],[f39581]) ).
fof(f41383,plain,
~ v3_struct_0(sK45),
inference(cnf_transformation,[],[f39581]) ).
fof(f41384,plain,
m1_subset_1(sK46,u1_struct_0(sK45)),
inference(cnf_transformation,[],[f39581]) ).
fof(f41385,plain,
k6_autgroup(sK45,k3_group_1(sK45,sK46)) != k2_funct_1(k6_autgroup(sK45,sK46)),
inference(cnf_transformation,[],[f39581]) ).
fof(f41388,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,[],[f39582]) ).
fof(f41389,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,[],[f39582]) ).
fof(f41396,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_fraenkel(X2,X0,X1) ),
inference(cnf_transformation,[],[f33603]) ).
fof(f41424,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,[],[f33623]) ).
fof(f41425,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,[],[f33623]) ).
fof(f41426,plain,
! [X0,X1] :
( ~ v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33623]) ).
fof(f41428,plain,
! [X2,X0,X1] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33627]) ).
fof(f41429,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,[],[f33629]) ).
fof(f41431,plain,
! [X2,X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(X2,u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f33633]) ).
fof(f41434,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,[],[f33637]) ).
fof(f41515,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f33702]) ).
fof(f42044,plain,
! [X2,X3,X0,X1,X4,X5] :
( k1_group_1(X0,X1,X2) = k1_group_1(X3,X4,X5)
| X1 != X4
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3))
| ~ m1_subset_1(X4,u1_struct_0(X3))
| ~ m1_group_2(X3,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)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34029]) ).
fof(f42146,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,[],[f34081]) ).
fof(f42147,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,[],[f34083]) ).
fof(f42164,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,[],[f34105]) ).
fof(f42165,plain,
! [X2,X0,X1] :
( ~ v3_group_1(X0)
| k1_group_1(X0,X1,X2) != 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,[],[f34105]) ).
fof(f42168,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,[],[f34107]) ).
fof(f42170,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| k3_group_1(X0,X1) != k3_group_1(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| X1 = X2
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f34111]) ).
fof(f42173,plain,
! [X2,X0,X1] :
( k1_group_1(X0,X2,X1) = k2_group_1(X0)
| k3_group_1(X0,X1) != X2
| ~ 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(cnf_transformation,[],[f39751]) ).
fof(f45487,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36676]) ).
fof(f45494,plain,
! [X0] :
( ~ v3_struct_0(X0)
| v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f40461]) ).
fof(f47288,plain,
! [X0,X1] :
( ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| r2_hidden(X1,k2_pre_topc(X0)) ),
inference(cnf_transformation,[],[f37982]) ).
fof(f47290,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f37984]) ).
fof(f50890,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,[],[f41349]) ).
fof(f50895,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,[],[f41366]) ).
fof(f50896,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,[],[f41368]) ).
fof(f50897,plain,
! [X3,X0,X4] :
( ~ m1_subset_1(X3,u1_struct_0(k5_autgroup(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)))
| 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)
| v3_struct_0(X0)
| ~ v1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f50896]) ).
fof(f50898,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,[],[f41370]) ).
fof(f50973,plain,
! [X2,X3,X0,X4,X5] :
( k1_group_1(X3,X4,X5) = k1_group_1(X0,X4,X2)
| X2 != X5
| ~ m1_subset_1(X5,u1_struct_0(X3))
| ~ m1_subset_1(X4,u1_struct_0(X3))
| ~ m1_group_2(X3,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f42044]) ).
fof(f50974,plain,
! [X3,X0,X4,X5] :
( ~ v3_group_1(X0)
| ~ m1_subset_1(X5,u1_struct_0(X3))
| ~ m1_subset_1(X4,u1_struct_0(X3))
| ~ m1_group_2(X3,X0)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| v3_struct_0(X0)
| k1_group_1(X3,X4,X5) = k1_group_1(X0,X4,X5)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f50973]) ).
fof(f50977,plain,
! [X2,X3,X0] :
( ~ v4_group_1(X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k3_group_1(X2,X3) = k3_group_1(X0,X3)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f42146]) ).
fof(f50983,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k2_group_1(X0) = k1_group_1(X0,k3_group_1(X0,X1),X1)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f42173]) ).
fof(f52128,plain,
! [X2,X0,X1] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f41428,f41434]) ).
fof(f52223,plain,
! [X2,X0,X1] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v3_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f52128,f41426]) ).
fof(f52255,plain,
! [X2,X0,X1] :
( m1_group_2(X0,X2)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f52223,f41425]) ).
fof(f52263,plain,
! [X2,X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X0)
| m1_group_2(X0,X2)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f52255,f41424]) ).
fof(f52287,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f47290,f45487]) ).
fof(f52288,plain,
u1_struct_0(sK45) = k2_pre_topc(sK45),
inference(resolution,[],[f52287,f41379]) ).
fof(f52290,plain,
m1_subset_1(sK46,k2_pre_topc(sK45)),
inference(superposition,[],[f41384,f52288]) ).
fof(f52292,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(superposition,[],[f41295,f52288]) ).
fof(f52293,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k3_autgroup(sK45),X0)
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(superposition,[],[f50890,f52288]) ).
fof(f52294,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k5_autgroup(sK45),X0)
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(superposition,[],[f50898,f52288]) ).
fof(f52295,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK45,X0),k2_pre_topc(sK45))
| v3_struct_0(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(superposition,[],[f42147,f52288]) ).
fof(f52297,plain,
! [X0] :
( ~ v3_group_1(X0)
| ~ v1_group_1(X0)
| v3_struct_0(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| u1_struct_0(k3_autgroup(X0)) = k2_pre_topc(k3_autgroup(X0)) ),
inference(resolution,[],[f41286,f52287]) ).
fof(f52318,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| v4_group_1(k3_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41287,f41380]) ).
fof(f52319,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| v4_group_1(k3_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52318,f41383]) ).
fof(f52320,plain,
( ~ v3_group_1(sK45)
| v4_group_1(k3_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52319,f41382]) ).
fof(f52321,plain,
( v4_group_1(k3_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52320,f41381]) ).
fof(f52322,plain,
v4_group_1(k3_autgroup(sK45)),
inference(forward_subsumption_resolution,[],[f52321,f41379]) ).
fof(f52327,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| k3_group_1(X1,X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ l1_group_1(k3_autgroup(sK45)) ),
inference(resolution,[],[f52322,f50977]) ).
fof(f52328,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| k3_group_1(k3_autgroup(sK45),k3_group_1(k3_autgroup(sK45),X0)) = X0
| ~ l1_group_1(k3_autgroup(sK45)) ),
inference(resolution,[],[f52322,f42168]) ).
fof(f52330,definition,
( spl1179_50
<=> l1_group_1(k3_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_50])],[avatar_definition]) ).
fof(f52331,plain,
( ~ l1_group_1(k3_autgroup(sK45))
| spl1179_50 ),
inference(avatar_component_clause,[],[f52330]) ).
fof(f52333,definition,
( spl1179_51
<=> v3_group_1(k3_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_51])],[avatar_definition]) ).
fof(f52334,plain,
( ~ v3_group_1(k3_autgroup(sK45))
| spl1179_51 ),
inference(avatar_component_clause,[],[f52333]) ).
fof(f52336,definition,
( spl1179_52
<=> v3_struct_0(k3_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_52])],[avatar_definition]) ).
fof(f52337,plain,
( v3_struct_0(k3_autgroup(sK45))
| ~ spl1179_52 ),
inference(avatar_component_clause,[],[f52336]) ).
fof(f52339,definition,
( spl1179_53
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k3_group_1(k3_autgroup(sK45),k3_group_1(k3_autgroup(sK45),X0)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl1179_53])],[avatar_definition]) ).
fof(f52340,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k3_group_1(k3_autgroup(sK45),k3_group_1(k3_autgroup(sK45),X0)) = X0 )
| ~ spl1179_53 ),
inference(avatar_component_clause,[],[f52339]) ).
fof(f52341,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_53 ),
inference(avatar_split_clause,[],[f52328,f52339,f52336,f52333,f52330]) ).
fof(f52342,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| k3_group_1(X1,X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ l1_group_1(k3_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f52327,f41431]) ).
fof(f52363,definition,
( spl1179_59
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| k3_group_1(X1,X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ m1_group_2(X1,k3_autgroup(sK45)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_59])],[avatar_definition]) ).
fof(f52364,plain,
( ! [X0,X1] :
( ~ m1_group_2(X1,k3_autgroup(sK45))
| k3_group_1(X1,X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ m1_subset_1(X0,u1_struct_0(X1)) )
| ~ spl1179_59 ),
inference(avatar_component_clause,[],[f52363]) ).
fof(f52365,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_59 ),
inference(avatar_split_clause,[],[f52342,f52363,f52336,f52333,f52330]) ).
fof(f52366,plain,
( $false
| spl1179_50 ),
inference(unit_resulting_resolution,[],[f41286,f41379,f41380,f41381,f41382,f41383,f52331]) ).
fof(f52368,plain,
spl1179_50,
inference(avatar_contradiction_clause,[],[f52366]) ).
fof(f52369,plain,
( $false
| spl1179_51 ),
inference(unit_resulting_resolution,[],[f41288,f41379,f41380,f41381,f41382,f41383,f52334]) ).
fof(f52371,plain,
spl1179_51,
inference(avatar_contradiction_clause,[],[f52369]) ).
fof(f52372,plain,
( $false
| ~ spl1179_52 ),
inference(unit_resulting_resolution,[],[f41290,f41379,f41380,f41381,f41382,f41383,f52337]) ).
fof(f52374,plain,
~ spl1179_52,
inference(avatar_contradiction_clause,[],[f52372]) ).
fof(f52376,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_59 ),
inference(resolution,[],[f52364,f41292]) ).
fof(f52378,plain,
( v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| m1_group_2(k3_autgroup(sK45),k3_autgroup(sK45))
| ~ l1_group_1(k3_autgroup(sK45)) ),
inference(resolution,[],[f41429,f52322]) ).
fof(f52380,definition,
( spl1179_60
<=> m1_group_2(k3_autgroup(sK45),k3_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_60])],[avatar_definition]) ).
fof(f52381,plain,
( m1_group_2(k3_autgroup(sK45),k3_autgroup(sK45))
| ~ spl1179_60 ),
inference(avatar_component_clause,[],[f52380]) ).
fof(f52382,plain,
( ~ spl1179_50
| spl1179_60
| ~ spl1179_51
| spl1179_52 ),
inference(avatar_split_clause,[],[f52378,f52336,f52333,f52380,f52330]) ).
fof(f52442,plain,
! [X0,X1] :
( k3_group_1(k3_autgroup(sK45),X0) != k3_group_1(k3_autgroup(sK45),X1)
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| X0 = X1
| ~ l1_group_1(k3_autgroup(sK45)) ),
inference(resolution,[],[f42170,f52322]) ).
fof(f52444,definition,
( spl1179_66
<=> ! [X0,X1] :
( k3_group_1(k3_autgroup(sK45),X0) != k3_group_1(k3_autgroup(sK45),X1)
| X0 = X1
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45))) ) ),
introduced(definition,[new_symbols(definition,[spl1179_66])],[avatar_definition]) ).
fof(f52445,plain,
( ! [X0,X1] :
( k3_group_1(k3_autgroup(sK45),X0) != k3_group_1(k3_autgroup(sK45),X1)
| X0 = X1
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45))) )
| ~ spl1179_66 ),
inference(avatar_component_clause,[],[f52444]) ).
fof(f52446,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_66 ),
inference(avatar_split_clause,[],[f52442,f52444,f52336,f52333,f52330]) ).
fof(f52455,plain,
! [X0] :
( m2_fraenkel(k2_funct_1(X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(superposition,[],[f41364,f52288]) ).
fof(f52462,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(X2))
| v3_struct_0(k3_autgroup(X2))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X2)))
| ~ l1_group_1(k3_autgroup(X2))
| v3_struct_0(X2)
| ~ v1_group_1(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) ),
inference(resolution,[],[f41431,f41288]) ).
fof(f52469,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k1_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41360,f41380]) ).
fof(f52475,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k1_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52469,f41383]) ).
fof(f52476,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ v3_group_1(sK45)
| m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k1_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52475,f41382]) ).
fof(f52477,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k1_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52476,f41381]) ).
fof(f52478,plain,
! [X0] :
( ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k1_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f52477,f41379]) ).
fof(f52479,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k1_autgroup(sK45)) ),
inference(forward_demodulation,[],[f52478,f52288]) ).
fof(f52480,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45)) ),
inference(forward_demodulation,[],[f52479,f52288]) ).
fof(f52482,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,[],[f50895,f41293]) ).
fof(f52483,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,[],[f52482]) ).
fof(f52484,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| m1_fraenkel(k4_autgroup(sK45),u1_struct_0(sK45),u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41291,f41380]) ).
fof(f52490,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| m1_fraenkel(k4_autgroup(sK45),u1_struct_0(sK45),u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52484,f41383]) ).
fof(f52491,plain,
( ~ v3_group_1(sK45)
| m1_fraenkel(k4_autgroup(sK45),u1_struct_0(sK45),u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52490,f41382]) ).
fof(f52492,plain,
( m1_fraenkel(k4_autgroup(sK45),u1_struct_0(sK45),u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52491,f41381]) ).
fof(f52493,plain,
m1_fraenkel(k4_autgroup(sK45),u1_struct_0(sK45),u1_struct_0(sK45)),
inference(forward_subsumption_resolution,[],[f52492,f41379]) ).
fof(f52494,plain,
m1_fraenkel(k4_autgroup(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45)),
inference(forward_demodulation,[],[f52493,f52288]) ).
fof(f52496,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| v1_xboole_0(k2_pre_topc(sK45))
| m1_subset_1(X0,k4_autgroup(sK45)) ),
inference(resolution,[],[f52494,f41388]) ).
fof(f52498,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| v1_xboole_0(k2_pre_topc(sK45))
| m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)) ),
inference(resolution,[],[f52494,f41389]) ).
fof(f52500,definition,
( spl1179_69
<=> v1_xboole_0(k2_pre_topc(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_69])],[avatar_definition]) ).
fof(f52501,plain,
( v1_xboole_0(k2_pre_topc(sK45))
| ~ spl1179_69 ),
inference(avatar_component_clause,[],[f52500]) ).
fof(f52503,definition,
( spl1179_70
<=> ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_70])],[avatar_definition]) ).
fof(f52504,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)) )
| ~ spl1179_70 ),
inference(avatar_component_clause,[],[f52503]) ).
fof(f52505,plain,
( spl1179_69
| spl1179_70 ),
inference(avatar_split_clause,[],[f52498,f52503,f52500]) ).
fof(f52511,definition,
( spl1179_72
<=> ! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| m1_subset_1(X0,k4_autgroup(sK45)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_72])],[avatar_definition]) ).
fof(f52512,plain,
( ! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| m1_subset_1(X0,k4_autgroup(sK45)) )
| ~ spl1179_72 ),
inference(avatar_component_clause,[],[f52511]) ).
fof(f52513,plain,
( spl1179_69
| spl1179_72 ),
inference(avatar_split_clause,[],[f52496,f52511,f52500]) ).
fof(f52548,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k6_partfun1(u1_struct_0(sK45)) = k2_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41369,f41380]) ).
fof(f52554,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k6_partfun1(u1_struct_0(sK45)) = k2_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52548,f41383]) ).
fof(f52555,plain,
( ~ v3_group_1(sK45)
| k6_partfun1(u1_struct_0(sK45)) = k2_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52554,f41382]) ).
fof(f52556,plain,
( k6_partfun1(u1_struct_0(sK45)) = k2_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52555,f41381]) ).
fof(f52557,plain,
k6_partfun1(u1_struct_0(sK45)) = k2_group_1(k5_autgroup(sK45)),
inference(forward_subsumption_resolution,[],[f52556,f41379]) ).
fof(f52558,plain,
k2_group_1(k5_autgroup(sK45)) = k6_partfun1(k2_pre_topc(sK45)),
inference(forward_demodulation,[],[f52557,f52288]) ).
fof(f52561,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k2_group_1(k3_autgroup(sK45)) = k6_partfun1(u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41348,f41380]) ).
fof(f52564,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k2_group_1(k3_autgroup(sK45)) = k6_partfun1(u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52561,f41383]) ).
fof(f52569,plain,
( ~ v3_group_1(sK45)
| k2_group_1(k3_autgroup(sK45)) = k6_partfun1(u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52564,f41382]) ).
fof(f52570,plain,
( k2_group_1(k3_autgroup(sK45)) = k6_partfun1(u1_struct_0(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52569,f41381]) ).
fof(f52571,plain,
k2_group_1(k3_autgroup(sK45)) = k6_partfun1(u1_struct_0(sK45)),
inference(forward_subsumption_resolution,[],[f52570,f41379]) ).
fof(f52572,plain,
k2_group_1(k3_autgroup(sK45)) = k6_partfun1(k2_pre_topc(sK45)),
inference(forward_demodulation,[],[f52571,f52288]) ).
fof(f52574,plain,
k2_group_1(k3_autgroup(sK45)) = k2_group_1(k5_autgroup(sK45)),
inference(superposition,[],[f52558,f52572]) ).
fof(f52621,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK45,X0),k2_pre_topc(sK45))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52295,f41383]) ).
fof(f52625,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(X2))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X2)))
| ~ l1_group_1(k3_autgroup(X2))
| v3_struct_0(X2)
| ~ v1_group_1(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) ),
inference(forward_subsumption_resolution,[],[f52462,f41290]) ).
fof(f52627,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52294,f41383]) ).
fof(f52628,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52293,f41383]) ).
fof(f52629,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52292,f41383]) ).
fof(f52630,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_59 ),
inference(forward_subsumption_resolution,[],[f52376,f41383]) ).
fof(f52633,plain,
! [X0] :
( m2_fraenkel(k2_funct_1(X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52455,f41383]) ).
fof(f52637,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,[],[f52483,f41294]) ).
fof(f52642,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK45,X0),k2_pre_topc(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52621,f41381]) ).
fof(f52655,plain,
! [X2,X0,X1] :
( ~ v3_group_1(X2)
| ~ m1_group_2(X1,k3_autgroup(X2))
| m1_subset_1(X0,u1_struct_0(k3_autgroup(X2)))
| v3_struct_0(X2)
| ~ v1_group_1(X2)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ v4_group_1(X2)
| ~ l1_group_1(X2) ),
inference(forward_subsumption_resolution,[],[f52625,f41286]) ).
fof(f52660,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52627,f41382]) ).
fof(f52661,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52628,f41382]) ).
fof(f52662,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52629,f41382]) ).
fof(f52663,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_59 ),
inference(forward_subsumption_resolution,[],[f52630,f41382]) ).
fof(f52666,plain,
! [X0] :
( m2_fraenkel(k2_funct_1(X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52633,f41382]) ).
fof(f52669,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,[],[f52637,f41292]) ).
fof(f52673,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK45,X0),k2_pre_topc(sK45))
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52642,f41380]) ).
fof(f52674,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52660,f41381]) ).
fof(f52675,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52661,f41381]) ).
fof(f52676,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52662,f41381]) ).
fof(f52677,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_59 ),
inference(forward_subsumption_resolution,[],[f52663,f41381]) ).
fof(f52680,plain,
! [X0] :
( m2_fraenkel(k2_funct_1(X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52666,f41381]) ).
fof(f52686,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK45))
| m1_subset_1(k3_group_1(sK45,X0),k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52673,f41379]) ).
fof(f52687,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52674,f41380]) ).
fof(f52688,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k3_autgroup(sK45),X0)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52675,f41380]) ).
fof(f52689,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ l1_group_1(sK45)
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52676,f41380]) ).
fof(f52690,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ l1_group_1(sK45) )
| ~ spl1179_59 ),
inference(forward_subsumption_resolution,[],[f52677,f41380]) ).
fof(f52693,plain,
! [X0] :
( m2_fraenkel(k2_funct_1(X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52680,f41380]) ).
fof(f52699,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k5_autgroup(sK45),X0) ),
inference(forward_subsumption_resolution,[],[f52687,f41379]) ).
fof(f52700,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| k2_funct_1(X0) = k3_group_1(k3_autgroup(sK45),X0) ),
inference(forward_subsumption_resolution,[],[f52688,f41379]) ).
fof(f52701,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_subsumption_resolution,[],[f52689,f41379]) ).
fof(f52702,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0) )
| ~ spl1179_59 ),
inference(forward_subsumption_resolution,[],[f52690,f41379]) ).
fof(f52705,plain,
! [X0] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| m2_fraenkel(k2_funct_1(X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f52693,f41379]) ).
fof(f52724,plain,
m1_subset_1(k3_group_1(sK45,sK46),k2_pre_topc(sK45)),
inference(resolution,[],[f52686,f52290]) ).
fof(f52743,plain,
! [X0] :
( m2_fraenkel(k6_autgroup(sK45,X0),k2_pre_topc(sK45),k2_pre_topc(sK45),k1_autgroup(sK45))
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(resolution,[],[f52701,f52480]) ).
fof(f52748,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k4_autgroup(sK45) = u1_struct_0(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f52669,f41380]) ).
fof(f52754,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k4_autgroup(sK45) = u1_struct_0(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52748,f41383]) ).
fof(f52755,plain,
( ~ v3_group_1(sK45)
| k4_autgroup(sK45) = u1_struct_0(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52754,f41382]) ).
fof(f52756,plain,
( k4_autgroup(sK45) = u1_struct_0(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52755,f41381]) ).
fof(f52757,plain,
k4_autgroup(sK45) = u1_struct_0(k5_autgroup(sK45)),
inference(forward_subsumption_resolution,[],[f52756,f41379]) ).
fof(f52759,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X1,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1)
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(superposition,[],[f50897,f52757]) ).
fof(f52766,plain,
! [X0] :
( m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),k4_autgroup(sK45))
| v3_struct_0(k5_autgroup(sK45))
| ~ v3_group_1(k5_autgroup(sK45))
| ~ v4_group_1(k5_autgroup(sK45))
| ~ l1_group_1(k5_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45)) ),
inference(superposition,[],[f42147,f52757]) ).
fof(f52773,definition,
( spl1179_92
<=> l1_group_1(k5_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_92])],[avatar_definition]) ).
fof(f52774,plain,
( ~ l1_group_1(k5_autgroup(sK45))
| spl1179_92 ),
inference(avatar_component_clause,[],[f52773]) ).
fof(f52776,definition,
( spl1179_93
<=> v4_group_1(k5_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_93])],[avatar_definition]) ).
fof(f52777,plain,
( ~ v4_group_1(k5_autgroup(sK45))
| spl1179_93 ),
inference(avatar_component_clause,[],[f52776]) ).
fof(f52779,definition,
( spl1179_94
<=> v3_group_1(k5_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_94])],[avatar_definition]) ).
fof(f52780,plain,
( ~ v3_group_1(k5_autgroup(sK45))
| spl1179_94 ),
inference(avatar_component_clause,[],[f52779]) ).
fof(f52785,definition,
( spl1179_96
<=> v3_struct_0(k5_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_96])],[avatar_definition]) ).
fof(f52786,plain,
( v3_struct_0(k5_autgroup(sK45))
| ~ spl1179_96 ),
inference(avatar_component_clause,[],[f52785]) ).
fof(f52804,definition,
( spl1179_101
<=> l1_struct_0(k5_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_101])],[avatar_definition]) ).
fof(f52805,plain,
( ~ l1_struct_0(k5_autgroup(sK45))
| spl1179_101 ),
inference(avatar_component_clause,[],[f52804]) ).
fof(f52807,definition,
( spl1179_102
<=> v1_xboole_0(k4_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_102])],[avatar_definition]) ).
fof(f52808,plain,
( ~ v1_xboole_0(k4_autgroup(sK45))
| spl1179_102 ),
inference(avatar_component_clause,[],[f52807]) ).
fof(f52811,definition,
( spl1179_103
<=> ! [X0] :
( m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_103])],[avatar_definition]) ).
fof(f52812,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),k4_autgroup(sK45)) )
| ~ spl1179_103 ),
inference(avatar_component_clause,[],[f52811]) ).
fof(f52813,plain,
( ~ spl1179_92
| ~ spl1179_93
| ~ spl1179_94
| spl1179_96
| spl1179_103 ),
inference(avatar_split_clause,[],[f52766,f52811,f52785,f52779,f52776,f52773]) ).
fof(f52838,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X1,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52759,f41383]) ).
fof(f52840,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X1,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52838,f41382]) ).
fof(f52842,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X1,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52840,f41381]) ).
fof(f52844,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X1,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f52842,f41380]) ).
fof(f52846,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X1,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1) ),
inference(forward_subsumption_resolution,[],[f52844,f41379]) ).
fof(f52848,plain,
! [X0,X1] :
( ~ m2_fraenkel(X1,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m2_fraenkel(X0,u1_struct_0(sK45),u1_struct_0(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1) ),
inference(forward_demodulation,[],[f52846,f52288]) ).
fof(f52850,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m2_fraenkel(X1,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),X1,X0) = k1_group_1(k5_autgroup(sK45),X0,X1) ),
inference(forward_demodulation,[],[f52848,f52288]) ).
fof(f52851,plain,
! [X0,X1] :
( ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| k1_group_1(k5_autgroup(sK45),X0,X1) = k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),X1,X0)
| ~ m2_fraenkel(X1,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45)) ),
inference(forward_demodulation,[],[f52850,f52288]) ).
fof(f52861,plain,
( ~ l1_group_1(k5_autgroup(sK45))
| spl1179_101 ),
inference(resolution,[],[f52805,f45487]) ).
fof(f52863,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| k3_group_1(k3_autgroup(sK45),X0) = k3_group_1(k5_autgroup(sK45),X0) )
| ~ spl1179_59 ),
inference(superposition,[],[f52702,f52757]) ).
fof(f52971,plain,
! [X0] :
( ~ m1_subset_1(k6_autgroup(sK45,X0),u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,k2_pre_topc(sK45))
| k2_funct_1(k6_autgroup(sK45,X0)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,X0)) ),
inference(resolution,[],[f52743,f52700]) ).
fof(f53027,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k6_partfun1(u1_struct_0(sK45)) = k6_autgroup(sK45,k2_group_1(sK45))
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41375,f41380]) ).
fof(f53030,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| k6_partfun1(u1_struct_0(sK45)) = k6_autgroup(sK45,k2_group_1(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f53027,f41383]) ).
fof(f53032,plain,
( ~ v3_group_1(sK45)
| k6_partfun1(u1_struct_0(sK45)) = k6_autgroup(sK45,k2_group_1(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f53030,f41382]) ).
fof(f53037,plain,
( k6_partfun1(u1_struct_0(sK45)) = k6_autgroup(sK45,k2_group_1(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f53032,f41381]) ).
fof(f53038,plain,
k6_partfun1(u1_struct_0(sK45)) = k6_autgroup(sK45,k2_group_1(sK45)),
inference(forward_subsumption_resolution,[],[f53037,f41379]) ).
fof(f53039,plain,
k6_partfun1(k2_pre_topc(sK45)) = k6_autgroup(sK45,k2_group_1(sK45)),
inference(forward_demodulation,[],[f53038,f52288]) ).
fof(f53040,plain,
k2_group_1(k5_autgroup(sK45)) = k6_autgroup(sK45,k2_group_1(sK45)),
inference(forward_demodulation,[],[f53039,f52558]) ).
fof(f53041,plain,
k2_group_1(k3_autgroup(sK45)) = k6_autgroup(sK45,k2_group_1(sK45)),
inference(forward_demodulation,[],[f53040,f52574]) ).
fof(f53269,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f41377,f41381]) ).
fof(f53272,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK45))
| ~ v1_group_1(sK45)
| k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f53269,f41383]) ).
fof(f53274,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK45))
| k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f53272,f41382]) ).
fof(f53276,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK45))
| k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f53274,f41380]) ).
fof(f53278,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK45))
| k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0)) ),
inference(forward_subsumption_resolution,[],[f53276,f41379]) ).
fof(f53279,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK45))
| k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(u1_struct_0(sK45),u1_struct_0(sK45),u1_struct_0(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0)) ),
inference(forward_demodulation,[],[f53278,f52288]) ).
fof(f53280,plain,
! [X0] :
( k6_autgroup(sK45,k2_group_1(sK45)) = k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK45)) ),
inference(forward_demodulation,[],[f53279,f52288]) ).
fof(f53281,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK45))
| k2_group_1(k3_autgroup(sK45)) = k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),k6_autgroup(sK45,k3_group_1(sK45,X0)),k6_autgroup(sK45,X0)) ),
inference(forward_demodulation,[],[f53280,f53041]) ).
fof(f53282,plain,
k2_group_1(k3_autgroup(sK45)) = k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)),k6_autgroup(sK45,sK46)),
inference(resolution,[],[f53281,f52290]) ).
fof(f53359,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK45))
| m2_fraenkel(k2_funct_1(k6_autgroup(sK45,X0)),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)) ),
inference(resolution,[],[f52705,f52701]) ).
fof(f53372,plain,
( ~ v1_group_1(sK45)
| v3_struct_0(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| u1_struct_0(k3_autgroup(sK45)) = k2_pre_topc(k3_autgroup(sK45)) ),
inference(resolution,[],[f52297,f41381]) ).
fof(f53375,plain,
( v3_struct_0(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| u1_struct_0(k3_autgroup(sK45)) = k2_pre_topc(k3_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f53372,f41382]) ).
fof(f53377,plain,
( ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| u1_struct_0(k3_autgroup(sK45)) = k2_pre_topc(k3_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f53375,f41383]) ).
fof(f53379,plain,
( ~ l1_group_1(sK45)
| u1_struct_0(k3_autgroup(sK45)) = k2_pre_topc(k3_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f53377,f41380]) ).
fof(f53381,plain,
u1_struct_0(k3_autgroup(sK45)) = k2_pre_topc(k3_autgroup(sK45)),
inference(forward_subsumption_resolution,[],[f53379,f41379]) ).
fof(f53382,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| k3_group_1(k3_autgroup(sK45),k3_group_1(k3_autgroup(sK45),X0)) = X0 )
| ~ spl1179_53 ),
inference(superposition,[],[f52340,f53381]) ).
fof(f53394,plain,
! [X0] :
( ~ m1_subset_1(k6_autgroup(sK45,X0),k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,k2_pre_topc(sK45))
| k2_funct_1(k6_autgroup(sK45,X0)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,X0)) ),
inference(superposition,[],[f52971,f53381]) ).
fof(f53402,plain,
! [X0] :
( m1_subset_1(k3_group_1(k3_autgroup(sK45),X0),k2_pre_topc(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| ~ v4_group_1(k3_autgroup(sK45))
| ~ l1_group_1(k3_autgroup(sK45))
| ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45))) ),
inference(superposition,[],[f42147,f53381]) ).
fof(f53412,plain,
! [X0] :
( m1_subset_1(k3_group_1(k3_autgroup(sK45),X0),k2_pre_topc(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| ~ l1_group_1(k3_autgroup(sK45))
| ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45))) ),
inference(forward_subsumption_resolution,[],[f53402,f52322]) ).
fof(f53437,definition,
( spl1179_177
<=> ! [X0] :
( m1_subset_1(k3_group_1(k3_autgroup(sK45),X0),k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45))) ) ),
introduced(definition,[new_symbols(definition,[spl1179_177])],[avatar_definition]) ).
fof(f53438,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| m1_subset_1(k3_group_1(k3_autgroup(sK45),X0),k2_pre_topc(k3_autgroup(sK45))) )
| ~ spl1179_177 ),
inference(avatar_component_clause,[],[f53437]) ).
fof(f53439,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_177 ),
inference(avatar_split_clause,[],[f53412,f53437,f52336,f52333,f52330]) ).
fof(f53781,definition,
( spl1179_202
<=> k2_funct_1(k6_autgroup(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46)) ),
introduced(definition,[new_symbols(definition,[spl1179_202])],[avatar_definition]) ).
fof(f53782,plain,
( k2_funct_1(k6_autgroup(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46))
| ~ spl1179_202 ),
inference(avatar_component_clause,[],[f53781]) ).
fof(f54036,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,[],[f41424,f41288]) ).
fof(f54037,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,[],[f54036,f41290]) ).
fof(f54039,plain,
! [X0,X1] :
( ~ v3_group_1(X1)
| l1_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,[],[f54037,f41286]) ).
fof(f54043,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,[],[f41425,f41288]) ).
fof(f54044,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,[],[f54043,f41290]) ).
fof(f54046,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,[],[f54044,f41286]) ).
fof(f54052,plain,
m2_fraenkel(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)),
inference(resolution,[],[f53359,f52724]) ).
fof(f54449,plain,
( ! [X0] : ~ r2_hidden(X0,k2_pre_topc(sK45))
| ~ spl1179_69 ),
inference(resolution,[],[f52501,f41515]) ).
fof(f54456,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK45))
| m1_subset_1(k6_autgroup(sK45,X0),k4_autgroup(sK45)) )
| ~ spl1179_72 ),
inference(resolution,[],[f52512,f52701]) ).
fof(f54482,plain,
( m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k4_autgroup(sK45))
| ~ spl1179_72 ),
inference(resolution,[],[f54456,f52724]) ).
fof(f54484,plain,
( m1_subset_1(k6_autgroup(sK45,sK46),k4_autgroup(sK45))
| ~ spl1179_72 ),
inference(resolution,[],[f54456,f52290]) ).
fof(f54533,plain,
( v1_xboole_0(k4_autgroup(sK45))
| ~ spl1179_102 ),
inference(avatar_component_clause,[],[f52807]) ).
fof(f54537,plain,
( $false
| ~ spl1179_102 ),
inference(unit_resulting_resolution,[],[f41396,f52494,f54533]) ).
fof(f54540,plain,
~ spl1179_102,
inference(avatar_contradiction_clause,[],[f54537]) ).
fof(f54979,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| v3_struct_0(X1)
| r2_hidden(X0,k2_pre_topc(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(resolution,[],[f47288,f45487]) ).
fof(f54980,plain,
( $false
| ~ spl1179_69 ),
inference(unit_resulting_resolution,[],[f54979,f41383,f41379,f41384,f54449]) ).
fof(f54983,plain,
~ spl1179_69,
inference(avatar_contradiction_clause,[],[f54980]) ).
fof(f55167,plain,
( k3_group_1(k5_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46))) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_72 ),
inference(resolution,[],[f54482,f52863]) ).
fof(f57195,plain,
( m2_fraenkel(k6_autgroup(sK45,sK46),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ spl1179_70
| ~ spl1179_72 ),
inference(resolution,[],[f54484,f52504]) ).
fof(f58668,plain,
( m1_subset_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),k4_autgroup(sK45))
| ~ spl1179_72 ),
inference(resolution,[],[f54052,f52512]) ).
fof(f58670,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),u1_struct_0(k5_autgroup(sK45)))
| k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))) ),
inference(resolution,[],[f54052,f52699]) ).
fof(f58680,plain,
( ~ m1_subset_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),k4_autgroup(sK45))
| k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))) ),
inference(forward_demodulation,[],[f58670,f52757]) ).
fof(f59838,plain,
! [X0] :
( l1_group_1(X0)
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f54039,f41381]) ).
fof(f59841,plain,
! [X0] :
( l1_group_1(X0)
| ~ v1_group_1(sK45)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59838,f41383]) ).
fof(f59843,plain,
! [X0] :
( l1_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59841,f41382]) ).
fof(f59845,plain,
! [X0] :
( l1_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59843,f41380]) ).
fof(f59847,plain,
! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f59845,f41379]) ).
fof(f59848,plain,
( l1_group_1(k3_autgroup(sK45))
| ~ spl1179_60 ),
inference(resolution,[],[f59847,f52381]) ).
fof(f59849,plain,
( l1_group_1(k5_autgroup(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f59847,f41292]) ).
fof(f59850,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_92 ),
inference(forward_subsumption_resolution,[],[f59849,f52774]) ).
fof(f59851,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_92 ),
inference(forward_subsumption_resolution,[],[f59850,f41383]) ).
fof(f59852,plain,
( ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_92 ),
inference(forward_subsumption_resolution,[],[f59851,f41382]) ).
fof(f59853,plain,
( ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_92 ),
inference(forward_subsumption_resolution,[],[f59852,f41381]) ).
fof(f59854,plain,
( ~ l1_group_1(sK45)
| spl1179_92 ),
inference(forward_subsumption_resolution,[],[f59853,f41380]) ).
fof(f59855,plain,
( $false
| spl1179_92 ),
inference(forward_subsumption_resolution,[],[f59854,f41379]) ).
fof(f59856,plain,
spl1179_92,
inference(avatar_contradiction_clause,[],[f59855]) ).
fof(f59857,plain,
( ~ spl1179_92
| spl1179_101 ),
inference(avatar_split_clause,[],[f52861,f52804,f52773]) ).
fof(f59858,plain,
( l1_group_1(k5_autgroup(sK45))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59849,f41383]) ).
fof(f59859,plain,
( l1_group_1(k5_autgroup(sK45))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59858,f41382]) ).
fof(f59860,plain,
( l1_group_1(k5_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59859,f41381]) ).
fof(f59861,plain,
( l1_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f59860,f41380]) ).
fof(f59862,plain,
l1_group_1(k5_autgroup(sK45)),
inference(forward_subsumption_resolution,[],[f59861,f41379]) ).
fof(f60967,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f52655,f41381]) ).
fof(f60971,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45)))
| ~ v1_group_1(sK45)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60967,f41383]) ).
fof(f60973,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60971,f41382]) ).
fof(f60975,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60973,f41380]) ).
fof(f60977,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| m1_subset_1(X1,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f60975,f41379]) ).
fof(f60978,plain,
! [X0,X1] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| m1_subset_1(X1,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(forward_demodulation,[],[f60977,f53381]) ).
fof(f60980,plain,
! [X0] :
( m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f60978,f41292]) ).
fof(f60981,plain,
! [X0] :
( m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60980,f41383]) ).
fof(f60983,plain,
! [X0] :
( m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60981,f41382]) ).
fof(f60984,plain,
! [X0] :
( m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60983,f41381]) ).
fof(f60985,plain,
! [X0] :
( m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f60984,f41380]) ).
fof(f60986,plain,
! [X0] :
( m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45))) ),
inference(forward_subsumption_resolution,[],[f60985,f41379]) ).
fof(f60987,plain,
! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45))) ),
inference(forward_demodulation,[],[f60986,f52757]) ).
fof(f60988,plain,
( m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k2_pre_topc(k3_autgroup(sK45)))
| ~ spl1179_72 ),
inference(resolution,[],[f60987,f54482]) ).
fof(f60989,plain,
( m1_subset_1(k6_autgroup(sK45,sK46),k2_pre_topc(k3_autgroup(sK45)))
| ~ spl1179_72 ),
inference(resolution,[],[f60987,f54484]) ).
fof(f61141,plain,
! [X0] :
( v3_group_1(X0)
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f54046,f41381]) ).
fof(f61145,plain,
! [X0] :
( v3_group_1(X0)
| ~ v1_group_1(sK45)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61141,f41383]) ).
fof(f61147,plain,
! [X0] :
( v3_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61145,f41382]) ).
fof(f61149,plain,
! [X0] :
( v3_group_1(X0)
| ~ m1_group_2(X0,k3_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61147,f41380]) ).
fof(f61151,plain,
! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| v3_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f61149,f41379]) ).
fof(f61152,plain,
( v3_group_1(k3_autgroup(sK45))
| ~ spl1179_60 ),
inference(resolution,[],[f61151,f52381]) ).
fof(f61153,plain,
( v3_group_1(k5_autgroup(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(resolution,[],[f61151,f41292]) ).
fof(f61154,plain,
( v3_group_1(k5_autgroup(sK45))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61153,f41383]) ).
fof(f61155,plain,
( v3_group_1(k5_autgroup(sK45))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61154,f41382]) ).
fof(f61156,plain,
( v3_group_1(k5_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61155,f41381]) ).
fof(f61157,plain,
( v3_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45) ),
inference(forward_subsumption_resolution,[],[f61156,f41380]) ).
fof(f61158,plain,
v3_group_1(k5_autgroup(sK45)),
inference(forward_subsumption_resolution,[],[f61157,f41379]) ).
fof(f61179,plain,
! [X0,X1] :
( k2_group_1(k5_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ v4_group_1(k5_autgroup(sK45))
| ~ l1_group_1(k5_autgroup(sK45)) ),
inference(resolution,[],[f61158,f42164]) ).
fof(f61180,plain,
! [X0,X1] :
( k2_group_1(k5_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X0) = X1
| ~ v4_group_1(k5_autgroup(sK45))
| ~ l1_group_1(k5_autgroup(sK45)) ),
inference(resolution,[],[f61158,f42165]) ).
fof(f61191,plain,
! [X0,X1] :
( ~ m1_group_2(k5_autgroup(sK45),X0)
| ~ m1_group_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(k5_autgroup(sK45))
| m1_group_2(k5_autgroup(sK45),X1)
| ~ v4_group_1(k5_autgroup(sK45))
| ~ l1_group_1(k5_autgroup(sK45)) ),
inference(resolution,[],[f61158,f52263]) ).
fof(f61241,plain,
( v1_xboole_0(u1_struct_0(k5_autgroup(sK45)))
| ~ l1_struct_0(k5_autgroup(sK45))
| ~ spl1179_96 ),
inference(resolution,[],[f52786,f45494]) ).
fof(f61243,plain,
( v1_xboole_0(k4_autgroup(sK45))
| ~ l1_struct_0(k5_autgroup(sK45))
| ~ spl1179_96 ),
inference(forward_demodulation,[],[f61241,f52757]) ).
fof(f61244,plain,
( ~ l1_struct_0(k5_autgroup(sK45))
| ~ spl1179_96
| spl1179_102 ),
inference(forward_subsumption_resolution,[],[f61243,f52808]) ).
fof(f61245,plain,
( ~ spl1179_101
| ~ spl1179_96
| spl1179_102 ),
inference(avatar_split_clause,[],[f61244,f52807,f52785,f52804]) ).
fof(f61260,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| v4_group_1(X0)
| ~ v4_group_1(k3_autgroup(sK45))
| ~ l1_group_1(k3_autgroup(sK45)) )
| ~ spl1179_60 ),
inference(resolution,[],[f61152,f41434]) ).
fof(f61317,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| v4_group_1(X0)
| ~ l1_group_1(k3_autgroup(sK45)) )
| ~ spl1179_60 ),
inference(forward_subsumption_resolution,[],[f61260,f52322]) ).
fof(f61361,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| v4_group_1(X0) )
| ~ spl1179_60 ),
inference(forward_subsumption_resolution,[],[f61317,f59848]) ).
fof(f61438,definition,
( spl1179_540
<=> ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| v4_group_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl1179_540])],[avatar_definition]) ).
fof(f61439,plain,
( ! [X0] :
( ~ m1_group_2(X0,k3_autgroup(sK45))
| v4_group_1(X0) )
| ~ spl1179_540 ),
inference(avatar_component_clause,[],[f61438]) ).
fof(f61440,plain,
( spl1179_52
| spl1179_540
| ~ spl1179_60 ),
inference(avatar_split_clause,[],[f61361,f52380,f61438,f52336]) ).
fof(f61637,plain,
( k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))))
| ~ spl1179_72 ),
inference(forward_subsumption_resolution,[],[f58680,f58668]) ).
fof(f61795,definition,
( spl1179_588
<=> m2_fraenkel(k6_autgroup(sK45,sK46),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_588])],[avatar_definition]) ).
fof(f61796,plain,
( m2_fraenkel(k6_autgroup(sK45,sK46),k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ spl1179_588 ),
inference(avatar_component_clause,[],[f61795]) ).
fof(f61808,plain,
( spl1179_588
| ~ spl1179_70
| ~ spl1179_72 ),
inference(avatar_split_clause,[],[f57195,f52511,f52503,f61795]) ).
fof(f62214,plain,
( ~ m1_subset_1(sK46,k2_pre_topc(sK45))
| k2_funct_1(k6_autgroup(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46))
| ~ spl1179_72 ),
inference(resolution,[],[f60989,f53394]) ).
fof(f62215,plain,
( k6_autgroup(sK45,sK46) = k3_group_1(k3_autgroup(sK45),k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46)))
| ~ spl1179_53
| ~ spl1179_72 ),
inference(resolution,[],[f60989,f53382]) ).
fof(f62222,plain,
( m1_subset_1(k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46)),k2_pre_topc(k3_autgroup(sK45)))
| ~ spl1179_72
| ~ spl1179_177 ),
inference(resolution,[],[f60989,f53438]) ).
fof(f62240,plain,
( k2_funct_1(k6_autgroup(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46))
| ~ spl1179_72 ),
inference(forward_subsumption_resolution,[],[f62214,f52290]) ).
fof(f62282,plain,
( spl1179_202
| ~ spl1179_72 ),
inference(avatar_split_clause,[],[f62240,f52511,f53781]) ).
fof(f62492,plain,
( ~ m1_subset_1(k3_group_1(sK45,sK46),k2_pre_topc(sK45))
| k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_72 ),
inference(resolution,[],[f60988,f53394]) ).
fof(f62510,plain,
( k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_72 ),
inference(forward_subsumption_resolution,[],[f62492,f52724]) ).
fof(f62976,definition,
( spl1179_639
<=> k6_autgroup(sK45,sK46) = k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))) ),
introduced(definition,[new_symbols(definition,[spl1179_639])],[avatar_definition]) ).
fof(f62977,plain,
( k6_autgroup(sK45,sK46) = k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_639 ),
inference(avatar_component_clause,[],[f62976]) ).
fof(f63065,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) != k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = X0
| ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45))) )
| ~ spl1179_66
| ~ spl1179_72 ),
inference(superposition,[],[f52445,f62510]) ).
fof(f63073,plain,
( ! [X0] :
( ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k2_pre_topc(k3_autgroup(sK45)))
| k3_group_1(k3_autgroup(sK45),X0) != k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45))) )
| ~ spl1179_66
| ~ spl1179_72 ),
inference(forward_demodulation,[],[f63065,f53381]) ).
fof(f63080,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) != k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45))) )
| ~ spl1179_66
| ~ spl1179_72 ),
inference(forward_subsumption_resolution,[],[f63073,f60988]) ).
fof(f63083,plain,
( k6_autgroup(sK45,sK46) != k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| spl1179_639 ),
inference(avatar_component_clause,[],[f62976]) ).
fof(f63088,plain,
( ! [X0] :
( k3_group_1(k3_autgroup(sK45),X0) != k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = X0 )
| ~ spl1179_66
| ~ spl1179_72 ),
inference(forward_demodulation,[],[f63080,f53381]) ).
fof(f63311,plain,
( k6_autgroup(sK45,sK46) != k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ m1_subset_1(k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46)),k2_pre_topc(k3_autgroup(sK45)))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46))
| ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72 ),
inference(superposition,[],[f63088,f62215]) ).
fof(f63975,plain,
( v4_group_1(k5_autgroup(sK45))
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ spl1179_540 ),
inference(resolution,[],[f61439,f41292]) ).
fof(f63976,plain,
( v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_93
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63975,f52777]) ).
fof(f63977,plain,
( ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_93
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63976,f41383]) ).
fof(f63978,plain,
( ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_93
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63977,f41382]) ).
fof(f63979,plain,
( ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| spl1179_93
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63978,f41381]) ).
fof(f63980,plain,
( ~ l1_group_1(sK45)
| spl1179_93
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63979,f41380]) ).
fof(f63981,plain,
( $false
| spl1179_93
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63980,f41379]) ).
fof(f63982,plain,
( spl1179_93
| ~ spl1179_540 ),
inference(avatar_contradiction_clause,[],[f63981]) ).
fof(f63983,plain,
( $false
| spl1179_94 ),
inference(forward_subsumption_resolution,[],[f52780,f61158]) ).
fof(f63984,plain,
spl1179_94,
inference(avatar_contradiction_clause,[],[f63983]) ).
fof(f63999,plain,
! [X0,X1] :
( ~ m1_group_2(k5_autgroup(sK45),X0)
| ~ m1_group_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(k5_autgroup(sK45))
| m1_group_2(k5_autgroup(sK45),X1)
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f61191,f59862]) ).
fof(f64010,plain,
! [X0,X1] :
( k2_group_1(k5_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X0) = X1
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f61180,f59862]) ).
fof(f64011,plain,
! [X0,X1] :
( k2_group_1(k5_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_subsumption_resolution,[],[f61179,f59862]) ).
fof(f64031,plain,
( v4_group_1(k5_autgroup(sK45))
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f63975,f41383]) ).
fof(f64065,definition,
( spl1179_667
<=> ! [X0,X1] :
( ~ m1_group_2(k5_autgroup(sK45),X0)
| m1_group_2(k5_autgroup(sK45),X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ m1_group_2(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl1179_667])],[avatar_definition]) ).
fof(f64066,plain,
( ! [X0,X1] :
( ~ m1_group_2(k5_autgroup(sK45),X0)
| m1_group_2(k5_autgroup(sK45),X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ m1_group_2(X0,X1) )
| ~ spl1179_667 ),
inference(avatar_component_clause,[],[f64065]) ).
fof(f64067,plain,
( ~ spl1179_93
| spl1179_96
| spl1179_667 ),
inference(avatar_split_clause,[],[f63999,f64065,f52785,f52776]) ).
fof(f64084,plain,
! [X0,X1] :
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X0) = X1
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_demodulation,[],[f64010,f52574]) ).
fof(f64085,plain,
! [X0,X1] :
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_demodulation,[],[f64011,f52574]) ).
fof(f64117,plain,
( v4_group_1(k5_autgroup(sK45))
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64031,f41382]) ).
fof(f64149,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK45))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X0) = X1
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_demodulation,[],[f64084,f52757]) ).
fof(f64150,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_demodulation,[],[f64085,f52757]) ).
fof(f64169,plain,
( v4_group_1(k5_autgroup(sK45))
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45)
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64117,f41381]) ).
fof(f64188,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X0) = X1
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_demodulation,[],[f64149,f52757]) ).
fof(f64189,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| v3_struct_0(k5_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ v4_group_1(k5_autgroup(sK45)) ),
inference(forward_demodulation,[],[f64150,f52757]) ).
fof(f64206,plain,
( v4_group_1(k5_autgroup(sK45))
| ~ l1_group_1(sK45)
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64169,f41380]) ).
fof(f64215,definition,
( spl1179_686
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X0) = X1
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X1,k4_autgroup(sK45)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_686])],[avatar_definition]) ).
fof(f64216,plain,
( ! [X0,X1] :
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| k3_group_1(k5_autgroup(sK45),X0) = X1
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45)) )
| ~ spl1179_686 ),
inference(avatar_component_clause,[],[f64215]) ).
fof(f64217,plain,
( ~ spl1179_93
| spl1179_96
| spl1179_686 ),
inference(avatar_split_clause,[],[f64188,f64215,f52785,f52776]) ).
fof(f64219,definition,
( spl1179_687
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK45))
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl1179_687])],[avatar_definition]) ).
fof(f64220,plain,
( ! [X0,X1] :
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k5_autgroup(sK45),X0,X1)
| k3_group_1(k5_autgroup(sK45),X1) = X0
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m1_subset_1(X1,k4_autgroup(sK45)) )
| ~ spl1179_687 ),
inference(avatar_component_clause,[],[f64219]) ).
fof(f64221,plain,
( ~ spl1179_93
| spl1179_96
| spl1179_687 ),
inference(avatar_split_clause,[],[f64189,f64219,f52785,f52776]) ).
fof(f64246,plain,
( v4_group_1(k5_autgroup(sK45))
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64206,f41379]) ).
fof(f64280,plain,
( ! [X0] :
( ~ m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| ~ v3_group_1(k5_autgroup(sK45))
| k2_group_1(k5_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0)
| ~ l1_group_1(k5_autgroup(sK45)) )
| ~ spl1179_540 ),
inference(resolution,[],[f64246,f50983]) ).
fof(f64283,plain,
( ! [X0] :
( ~ m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k2_group_1(k5_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0)
| ~ l1_group_1(k5_autgroup(sK45)) )
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64280,f61158]) ).
fof(f64303,plain,
( ! [X0] :
( ~ m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k2_group_1(k5_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0) )
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64283,f59862]) ).
fof(f64326,plain,
( ! [X0] :
( ~ m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),k4_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45)))
| v3_struct_0(k5_autgroup(sK45))
| k2_group_1(k5_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0) )
| ~ spl1179_540 ),
inference(forward_demodulation,[],[f64303,f52757]) ).
fof(f64354,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| ~ m1_subset_1(k3_group_1(k5_autgroup(sK45),X0),k4_autgroup(sK45))
| v3_struct_0(k5_autgroup(sK45))
| k2_group_1(k5_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0) )
| ~ spl1179_540 ),
inference(forward_demodulation,[],[f64326,f52757]) ).
fof(f64391,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| v3_struct_0(k5_autgroup(sK45))
| k2_group_1(k5_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0) )
| ~ spl1179_103
| ~ spl1179_540 ),
inference(forward_subsumption_resolution,[],[f64354,f52812]) ).
fof(f64415,plain,
( ! [X0] :
( k2_group_1(k3_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0)
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| v3_struct_0(k5_autgroup(sK45)) )
| ~ spl1179_103
| ~ spl1179_540 ),
inference(forward_demodulation,[],[f64391,f52574]) ).
fof(f64419,definition,
( spl1179_714
<=> ! [X0] :
( k2_group_1(k3_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0)
| ~ m1_subset_1(X0,k4_autgroup(sK45)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_714])],[avatar_definition]) ).
fof(f64420,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| k2_group_1(k3_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),X0),X0) )
| ~ spl1179_714 ),
inference(avatar_component_clause,[],[f64419]) ).
fof(f64421,plain,
( spl1179_96
| spl1179_714
| ~ spl1179_103
| ~ spl1179_540 ),
inference(avatar_split_clause,[],[f64415,f61438,f52811,f64419,f52785]) ).
fof(f64440,plain,
( m1_subset_1(k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))),k4_autgroup(sK45))
| ~ spl1179_72
| ~ spl1179_103 ),
inference(resolution,[],[f52812,f58668]) ).
fof(f64450,plain,
( m1_subset_1(k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))),k4_autgroup(sK45))
| ~ spl1179_72
| ~ spl1179_103 ),
inference(forward_demodulation,[],[f64440,f61637]) ).
fof(f64602,plain,
( k2_group_1(k3_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k5_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46))),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_72
| ~ spl1179_714 ),
inference(resolution,[],[f64420,f54482]) ).
fof(f64608,plain,
( k2_group_1(k3_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46))),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_714 ),
inference(forward_demodulation,[],[f64602,f55167]) ).
fof(f64613,plain,
( k2_group_1(k3_autgroup(sK45)) = k1_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_714 ),
inference(forward_demodulation,[],[f64608,f62510]) ).
fof(f66108,plain,
( k2_group_1(k3_autgroup(sK45)) != k2_group_1(k3_autgroup(sK45))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))))
| ~ m1_subset_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),k4_autgroup(sK45))
| ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k4_autgroup(sK45))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_686
| ~ spl1179_714 ),
inference(superposition,[],[f64216,f64613]) ).
fof(f66111,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))))
| ~ m1_subset_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))),k4_autgroup(sK45))
| ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k4_autgroup(sK45))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_686
| ~ spl1179_714 ),
inference(trivial_inequality_removal,[],[f66108]) ).
fof(f66112,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))))
| ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k4_autgroup(sK45))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_686
| ~ spl1179_714 ),
inference(forward_subsumption_resolution,[],[f66111,f58668]) ).
fof(f66113,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k5_autgroup(sK45),k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_686
| ~ spl1179_714 ),
inference(forward_subsumption_resolution,[],[f66112,f54482]) ).
fof(f66115,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46))))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_686
| ~ spl1179_714 ),
inference(superposition,[],[f61637,f66113]) ).
fof(f68288,plain,
( ! [X0] :
( m1_group_2(k5_autgroup(sK45),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(k3_autgroup(sK45),X0)
| v3_struct_0(sK45)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_667 ),
inference(resolution,[],[f64066,f41292]) ).
fof(f68290,plain,
( ! [X0] :
( m1_group_2(k5_autgroup(sK45),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(k3_autgroup(sK45),X0)
| ~ v1_group_1(sK45)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68288,f41383]) ).
fof(f68291,plain,
( ! [X0] :
( m1_group_2(k5_autgroup(sK45),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(k3_autgroup(sK45),X0)
| ~ v3_group_1(sK45)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68290,f41382]) ).
fof(f68292,plain,
( ! [X0] :
( m1_group_2(k5_autgroup(sK45),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(k3_autgroup(sK45),X0)
| ~ v4_group_1(sK45)
| ~ l1_group_1(sK45) )
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68291,f41381]) ).
fof(f68293,plain,
( ! [X0] :
( m1_group_2(k5_autgroup(sK45),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(k3_autgroup(sK45),X0)
| ~ l1_group_1(sK45) )
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68292,f41380]) ).
fof(f68294,plain,
( ! [X0] :
( ~ m1_group_2(k3_autgroup(sK45),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(k5_autgroup(sK45),X0) )
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68293,f41379]) ).
fof(f68295,plain,
( ~ l1_group_1(k3_autgroup(sK45))
| ~ v4_group_1(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| m1_group_2(k5_autgroup(sK45),k3_autgroup(sK45))
| ~ spl1179_60
| ~ spl1179_667 ),
inference(resolution,[],[f68294,f52381]) ).
fof(f68296,plain,
( ~ v4_group_1(k3_autgroup(sK45))
| ~ v3_group_1(k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| m1_group_2(k5_autgroup(sK45),k3_autgroup(sK45))
| ~ spl1179_60
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68295,f59848]) ).
fof(f68297,plain,
( ~ v3_group_1(k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| m1_group_2(k5_autgroup(sK45),k3_autgroup(sK45))
| ~ spl1179_60
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68296,f52322]) ).
fof(f68298,plain,
( v3_struct_0(k3_autgroup(sK45))
| m1_group_2(k5_autgroup(sK45),k3_autgroup(sK45))
| ~ spl1179_60
| ~ spl1179_667 ),
inference(forward_subsumption_resolution,[],[f68297,f61152]) ).
fof(f68300,definition,
( spl1179_926
<=> m1_group_2(k5_autgroup(sK45),k3_autgroup(sK45)) ),
introduced(definition,[new_symbols(definition,[spl1179_926])],[avatar_definition]) ).
fof(f68301,plain,
( m1_group_2(k5_autgroup(sK45),k3_autgroup(sK45))
| ~ spl1179_926 ),
inference(avatar_component_clause,[],[f68300]) ).
fof(f68302,plain,
( spl1179_926
| spl1179_52
| ~ spl1179_60
| ~ spl1179_667 ),
inference(avatar_split_clause,[],[f68298,f64065,f52380,f52336,f68300]) ).
fof(f71177,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X2,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0)
| ~ l1_group_1(k3_autgroup(sK45)) )
| ~ spl1179_60 ),
inference(resolution,[],[f50974,f61152]) ).
fof(f71184,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| ~ m1_subset_1(X0,u1_struct_0(k3_autgroup(sK45)))
| ~ m1_subset_1(X2,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0) )
| ~ spl1179_60 ),
inference(forward_subsumption_resolution,[],[f71177,f59848]) ).
fof(f71191,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| ~ m1_subset_1(X2,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0) )
| ~ spl1179_60 ),
inference(forward_demodulation,[],[f71184,f53381]) ).
fof(f71198,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| ~ m1_subset_1(X2,u1_struct_0(k3_autgroup(sK45)))
| v3_struct_0(k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0) )
| ~ spl1179_60 ),
inference(forward_subsumption_resolution,[],[f71191,f60978]) ).
fof(f71205,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X2,k2_pre_topc(k3_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0) )
| ~ spl1179_60 ),
inference(forward_demodulation,[],[f71198,f53381]) ).
fof(f71212,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_group_2(X1,k3_autgroup(sK45))
| v3_struct_0(k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0) )
| ~ spl1179_60 ),
inference(forward_subsumption_resolution,[],[f71205,f60978]) ).
fof(f71225,definition,
( spl1179_1159
<=> ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0)
| ~ m1_group_2(X1,k3_autgroup(sK45))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl1179_1159])],[avatar_definition]) ).
fof(f71226,plain,
( ! [X2,X0,X1] :
( ~ m1_group_2(X1,k3_autgroup(sK45))
| k1_group_1(X1,X2,X0) = k1_group_1(k3_autgroup(sK45),X2,X0)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ spl1179_1159 ),
inference(avatar_component_clause,[],[f71225]) ).
fof(f71227,plain,
( spl1179_52
| spl1179_1159
| ~ spl1179_60 ),
inference(avatar_split_clause,[],[f71212,f52380,f71225,f52336]) ).
fof(f71248,plain,
( ! [X0,X1] :
( k1_group_1(k5_autgroup(sK45),X0,X1) = k1_group_1(k3_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(sK45)))
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45))) )
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(resolution,[],[f71226,f68301]) ).
fof(f71249,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK45))
| k1_group_1(k5_autgroup(sK45),X0,X1) = k1_group_1(k3_autgroup(sK45),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k5_autgroup(sK45))) )
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_demodulation,[],[f71248,f52757]) ).
fof(f71251,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45))
| k1_group_1(k5_autgroup(sK45),X0,X1) = k1_group_1(k3_autgroup(sK45),X0,X1) )
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_demodulation,[],[f71249,f52757]) ).
fof(f71262,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| k1_group_1(k5_autgroup(sK45),X0,k6_autgroup(sK45,k3_group_1(sK45,sK46))) = k1_group_1(k3_autgroup(sK45),X0,k6_autgroup(sK45,k3_group_1(sK45,sK46))) )
| ~ spl1179_72
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(resolution,[],[f71251,f54482]) ).
fof(f75882,plain,
( k1_group_1(k5_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46))) = k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_72
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(resolution,[],[f71262,f54484]) ).
fof(f75891,plain,
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k6_autgroup(sK45,sK46) = k3_group_1(k5_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ m1_subset_1(k6_autgroup(sK45,sK46),k4_autgroup(sK45))
| ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k4_autgroup(sK45))
| ~ spl1179_72
| ~ spl1179_687
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(superposition,[],[f64220,f75882]) ).
fof(f75892,plain,
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k6_autgroup(sK45,sK46) = k3_group_1(k5_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ m1_subset_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)),k4_autgroup(sK45))
| ~ spl1179_72
| ~ spl1179_687
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_subsumption_resolution,[],[f75891,f54484]) ).
fof(f75894,plain,
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k6_autgroup(sK45,sK46) = k3_group_1(k5_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_72
| ~ spl1179_687
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_subsumption_resolution,[],[f75892,f54482]) ).
fof(f75896,plain,
( k6_autgroup(sK45,sK46) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_687
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_demodulation,[],[f75894,f55167]) ).
fof(f75898,plain,
( k6_autgroup(sK45,sK46) = k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| k2_group_1(k3_autgroup(sK45)) != k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_72
| ~ spl1179_687
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_demodulation,[],[f75896,f62510]) ).
fof(f75900,plain,
( k2_group_1(k3_autgroup(sK45)) != k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_72
| spl1179_639
| ~ spl1179_687
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_subsumption_resolution,[],[f75898,f63083]) ).
fof(f135797,plain,
( ! [X0] :
( k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),X0,k6_autgroup(sK45,sK46)) = k1_group_1(k5_autgroup(sK45),k6_autgroup(sK45,sK46),X0)
| ~ m2_fraenkel(X0,k2_pre_topc(sK45),k2_pre_topc(sK45),k4_autgroup(sK45))
| ~ m1_subset_1(k6_autgroup(sK45,sK46),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45)) )
| ~ spl1179_588 ),
inference(resolution,[],[f52851,f61796]) ).
fof(f135806,plain,
( ! [X0] :
( k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),X0,k6_autgroup(sK45,sK46)) = k1_group_1(k5_autgroup(sK45),k6_autgroup(sK45,sK46),X0)
| ~ m1_subset_1(k6_autgroup(sK45,sK46),k4_autgroup(sK45))
| ~ m1_subset_1(X0,k4_autgroup(sK45)) )
| ~ spl1179_70
| ~ spl1179_588 ),
inference(forward_subsumption_resolution,[],[f135797,f52504]) ).
fof(f135819,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_autgroup(sK45))
| k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),X0,k6_autgroup(sK45,sK46)) = k1_group_1(k5_autgroup(sK45),k6_autgroup(sK45,sK46),X0) )
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_588 ),
inference(forward_subsumption_resolution,[],[f135806,f54484]) ).
fof(f135842,plain,
( k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))),k6_autgroup(sK45,sK46)) = k1_group_1(k5_autgroup(sK45),k6_autgroup(sK45,sK46),k2_funct_1(k2_funct_1(k6_autgroup(sK45,k3_group_1(sK45,sK46)))))
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588 ),
inference(resolution,[],[f135819,f64450]) ).
fof(f135871,plain,
( k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)),k6_autgroup(sK45,sK46)) = k1_group_1(k5_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588
| ~ spl1179_686
| ~ spl1179_714 ),
inference(forward_demodulation,[],[f135842,f66115]) ).
fof(f135886,plain,
( k7_funct_2(k2_pre_topc(sK45),k2_pre_topc(sK45),k2_pre_topc(sK45),k6_autgroup(sK45,k3_group_1(sK45,sK46)),k6_autgroup(sK45,sK46)) = k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588
| ~ spl1179_686
| ~ spl1179_714
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_demodulation,[],[f135871,f75882]) ).
fof(f135898,plain,
( k2_group_1(k3_autgroup(sK45)) = k1_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46),k6_autgroup(sK45,k3_group_1(sK45,sK46)))
| ~ spl1179_59
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588
| ~ spl1179_686
| ~ spl1179_714
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_demodulation,[],[f135886,f53282]) ).
fof(f135904,plain,
( $false
| ~ spl1179_59
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588
| spl1179_639
| ~ spl1179_686
| ~ spl1179_687
| ~ spl1179_714
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(forward_subsumption_resolution,[],[f135898,f75900]) ).
fof(f135905,plain,
( ~ spl1179_59
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588
| spl1179_639
| ~ spl1179_686
| ~ spl1179_687
| ~ spl1179_714
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(avatar_contradiction_clause,[],[f135904]) ).
fof(f135912,plain,
( ~ m1_subset_1(k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46)),k2_pre_topc(k3_autgroup(sK45)))
| k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46))
| ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72
| ~ spl1179_639 ),
inference(forward_subsumption_resolution,[],[f63311,f62977]) ).
fof(f136595,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k3_group_1(k3_autgroup(sK45),k6_autgroup(sK45,sK46))
| ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72
| ~ spl1179_177
| ~ spl1179_639 ),
inference(forward_subsumption_resolution,[],[f135912,f62222]) ).
fof(f136966,plain,
( k6_autgroup(sK45,k3_group_1(sK45,sK46)) = k2_funct_1(k6_autgroup(sK45,sK46))
| ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72
| ~ spl1179_177
| ~ spl1179_202
| ~ spl1179_639 ),
inference(forward_demodulation,[],[f136595,f53782]) ).
fof(f137132,plain,
( $false
| ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72
| ~ spl1179_177
| ~ spl1179_202
| ~ spl1179_639 ),
inference(forward_subsumption_resolution,[],[f136966,f41385]) ).
fof(f137133,plain,
( ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72
| ~ spl1179_177
| ~ spl1179_202
| ~ spl1179_639 ),
inference(avatar_contradiction_clause,[],[f137132]) ).
cnf(s38,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_53 ),
inference(sat_conversion,[],[f52341]) ).
cnf(s43,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_59 ),
inference(sat_conversion,[],[f52365]) ).
cnf(s44,plain,
spl1179_50,
inference(sat_conversion,[],[f52368]) ).
cnf(s45,plain,
spl1179_51,
inference(sat_conversion,[],[f52371]) ).
cnf(s46,plain,
~ spl1179_52,
inference(sat_conversion,[],[f52374]) ).
cnf(s47,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_60 ),
inference(sat_conversion,[],[f52382]) ).
cnf(s53,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_66 ),
inference(sat_conversion,[],[f52446]) ).
cnf(s56,plain,
( spl1179_69
| spl1179_70 ),
inference(sat_conversion,[],[f52505]) ).
cnf(s58,plain,
( spl1179_69
| spl1179_72 ),
inference(sat_conversion,[],[f52513]) ).
cnf(s90,plain,
( ~ spl1179_92
| ~ spl1179_93
| ~ spl1179_94
| spl1179_96
| spl1179_103 ),
inference(sat_conversion,[],[f52813]) ).
cnf(s155,plain,
( ~ spl1179_50
| ~ spl1179_51
| spl1179_52
| spl1179_177 ),
inference(sat_conversion,[],[f53439]) ).
cnf(s218,plain,
~ spl1179_102,
inference(sat_conversion,[],[f54540]) ).
cnf(s230,plain,
~ spl1179_69,
inference(sat_conversion,[],[f54983]) ).
cnf(s478,plain,
spl1179_92,
inference(sat_conversion,[],[f59856]) ).
cnf(s479,plain,
( ~ spl1179_92
| spl1179_101 ),
inference(sat_conversion,[],[f59857]) ).
cnf(s576,plain,
( ~ spl1179_96
| ~ spl1179_101
| spl1179_102 ),
inference(sat_conversion,[],[f61245]) ).
cnf(s590,plain,
( spl1179_52
| ~ spl1179_60
| spl1179_540 ),
inference(sat_conversion,[],[f61440]) ).
cnf(s650,plain,
( ~ spl1179_70
| ~ spl1179_72
| spl1179_588 ),
inference(sat_conversion,[],[f61808]) ).
cnf(s737,plain,
( ~ spl1179_72
| spl1179_202 ),
inference(sat_conversion,[],[f62282]) ).
cnf(s805,plain,
( spl1179_93
| ~ spl1179_540 ),
inference(sat_conversion,[],[f63982]) ).
cnf(s806,plain,
spl1179_94,
inference(sat_conversion,[],[f63984]) ).
cnf(s813,plain,
( ~ spl1179_93
| spl1179_96
| spl1179_667 ),
inference(sat_conversion,[],[f64067]) ).
cnf(s832,plain,
( ~ spl1179_93
| spl1179_96
| spl1179_686 ),
inference(sat_conversion,[],[f64217]) ).
cnf(s833,plain,
( ~ spl1179_93
| spl1179_96
| spl1179_687 ),
inference(sat_conversion,[],[f64221]) ).
cnf(s860,plain,
( spl1179_96
| ~ spl1179_103
| ~ spl1179_540
| spl1179_714 ),
inference(sat_conversion,[],[f64421]) ).
cnf(s1051,plain,
( spl1179_52
| ~ spl1179_60
| ~ spl1179_667
| spl1179_926 ),
inference(sat_conversion,[],[f68302]) ).
cnf(s1255,plain,
( spl1179_52
| ~ spl1179_60
| spl1179_1159 ),
inference(sat_conversion,[],[f71227]) ).
cnf(s4015,plain,
( ~ spl1179_59
| ~ spl1179_70
| ~ spl1179_72
| ~ spl1179_103
| ~ spl1179_588
| spl1179_639
| ~ spl1179_686
| ~ spl1179_687
| ~ spl1179_714
| ~ spl1179_926
| ~ spl1179_1159 ),
inference(sat_conversion,[],[f135905]) ).
cnf(s4094,plain,
( ~ spl1179_53
| ~ spl1179_66
| ~ spl1179_72
| ~ spl1179_177
| ~ spl1179_202
| ~ spl1179_639 ),
inference(sat_conversion,[],[f137133]) ).
cnf(s4363,plain,
spl1179_101,
inference(rat,[],[s479,s478]) ).
cnf(s4595,plain,
~ spl1179_96,
inference(rat,[],[s576,s4363,s218]) ).
cnf(s4664,plain,
( ~ spl1179_93
| spl1179_103 ),
inference(rat,[],[s90,s4595,s806,s478]) ).
cnf(s4670,plain,
spl1179_72,
inference(rat,[],[s58,s230]) ).
cnf(s4688,plain,
spl1179_202,
inference(rat,[],[s737,s4670]) ).
cnf(s4702,plain,
spl1179_70,
inference(rat,[],[s56,s230]) ).
cnf(s4706,plain,
spl1179_588,
inference(rat,[],[s650,s4670,s4702]) ).
cnf(s4731,plain,
spl1179_177,
inference(rat,[],[s155,s45,s46,s44]) ).
cnf(s4742,plain,
spl1179_66,
inference(rat,[],[s53,s45,s46,s44]) ).
cnf(s4746,plain,
spl1179_60,
inference(rat,[],[s47,s45,s46,s44]) ).
cnf(s4794,plain,
spl1179_1159,
inference(rat,[],[s1255,s46,s4746]) ).
cnf(s4812,plain,
spl1179_540,
inference(rat,[],[s590,s46,s4746]) ).
cnf(s4916,plain,
spl1179_93,
inference(rat,[],[s805,s4812]) ).
cnf(s5022,plain,
spl1179_687,
inference(rat,[],[s833,s4595,s4916]) ).
cnf(s5023,plain,
spl1179_686,
inference(rat,[],[s832,s4595,s4916]) ).
cnf(s5041,plain,
spl1179_667,
inference(rat,[],[s813,s4595,s4916]) ).
cnf(s5053,plain,
spl1179_103,
inference(rat,[],[s4664,s4916]) ).
cnf(s5104,plain,
spl1179_926,
inference(rat,[],[s1051,s4746,s46,s5041]) ).
cnf(s5193,plain,
spl1179_714,
inference(rat,[],[s860,s4812,s4595,s5053]) ).
cnf(s5266,plain,
spl1179_59,
inference(rat,[],[s43,s46,s45,s44]) ).
cnf(s5268,plain,
spl1179_639,
inference(rat,[],[s4015,s4794,s5104,s5193,s5022,s5023,s5053,s4706,s4702,s4670,s5266]) ).
cnf(s5283,plain,
~ spl1179_53,
inference(rat,[],[s4094,s4742,s4688,s4731,s4670,s5268]) ).
cnf(s5574,plain,
$false,
inference(rat,[],[s38,s5283,s46,s45,s44]) ).
fof(f137342,plain,
$false,
inference(avatar_sat_refutation,[],[s5574]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP630+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n003.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 10:17:32 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.91/4.61 % (289978)Detected formulas, will run a generic FOF schedule.
% 13.91/4.61 % (289988)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=658704057:s2a=on:i=139:gtg=position_2979 on theBenchmark for (2979ds/139Mi)
% 13.91/4.61 % (289983)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=851606886:i=141193_2979 on theBenchmark for (2979ds/141193Mi)
% 13.91/4.61 % (289984)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=1111372094:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2979 on theBenchmark for (2979ds/134677Mi)
% 13.91/4.61 % (289985)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=2092829843:i=141695:sd=1:nm=32:gsp=on:ss=included_2979 on theBenchmark for (2979ds/141695Mi)
% 13.91/4.61 % (289987)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3280118017:i=119:av=off:ss=axioms_2979 on theBenchmark for (2979ds/119Mi)
% 13.91/4.61 % (289986)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=180905226:i=109:sd=1:ins=1:gsp=on:ss=axioms_2979 on theBenchmark for (2979ds/109Mi)
% 13.91/4.61 % (289988)Instruction limit reached!
% 13.91/4.61 % (289988)------------------------------
% 13.91/4.61 % (289988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/4.61 % (289988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/4.61 % (289988)CaDiCaL version: 2.1.3
% 13.91/4.61 % (289988)Termination reason: Instruction limit
% 13.91/4.61 % (289988)Termination phase: Property scanning
% 13.91/4.61 % (289988)Time elapsed: 0.036 s
% 13.91/4.61 % (289988)Peak memory usage: 133 MB
% 13.91/4.61 % (289988)Instructions burned: 142 (million)
% 13.91/4.61 % (289989)dis-21_1_sil=8000:lcm=predicate:random_seed=3896426747:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2979 on theBenchmark for (2979ds/129Mi)
% 13.91/4.61 % (289986)Instruction limit reached!
% 13.91/4.61 % (289986)------------------------------
% 13.91/4.61 % (289986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/4.61 % (289986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/4.61 % (289986)CaDiCaL version: 2.1.3
% 13.91/4.61 % (289986)Termination reason: Instruction limit
% 13.91/4.61 % (289986)Termination phase: SInE selection
% 13.91/4.61 % (289986)Time elapsed: 0.080 s
% 13.91/4.61 % (289986)Peak memory usage: 133 MB
% 13.91/4.61 % (289986)Instructions burned: 109 (million)
% 13.91/4.61 % (289987)Instruction limit reached!
% 13.91/4.61 % (289987)------------------------------
% 13.91/4.61 % (289987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/4.61 % (289987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/4.61 % (289987)CaDiCaL version: 2.1.3
% 13.91/4.61 % (289987)Termination reason: Instruction limit
% 13.91/4.61 % (289987)Termination phase: SInE selection
% 13.91/4.61 % (289987)Time elapsed: 0.086 s
% 13.91/4.61 % (289987)Peak memory usage: 133 MB
% 13.91/4.61 % (289987)Instructions burned: 119 (million)
% 13.91/4.61 % (289997)lrs+10_1_sil=8000:sp=occurrence:random_seed=2368900242:i=285:sd=3:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/285Mi)
% 13.91/4.61 % (289989)Instruction limit reached!
% 13.91/4.61 % (289989)------------------------------
% 13.91/4.61 % (289989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/4.61 % (289989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/4.61 % (289989)CaDiCaL version: 2.1.3
% 13.91/4.61 % (289989)Termination reason: Instruction limit
% 13.91/4.61 % (289989)Termination phase: SInE selection
% 13.91/4.61 % (289989)Time elapsed: 0.095 s
% 13.91/4.61 % (289989)Peak memory usage: 133 MB
% 13.91/4.61 % (289989)Instructions burned: 129 (million)
% 13.91/4.61 % (289998)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1796136980:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 13.91/4.61 % (290000)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1998143:i=325:sd=1:ss=axioms:sgt=32_2976 on theBenchmark for (2976ds/325Mi)
% 13.91/4.61 % (289997)Instruction limit reached!
% 13.91/4.61 % (289997)------------------------------
% 13.91/4.61 % (289997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/4.61 % (289997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (289997)CaDiCaL version: 2.1.3
% 22.41/5.92 % (289997)Termination reason: Instruction limit
% 22.41/5.92 % (289997)Termination phase: Preprocessing 3
% 22.41/5.92 % (289997)Time elapsed: 0.140 s
% 22.41/5.92 % (289997)Peak memory usage: 138 MB
% 22.41/5.92 % (289997)Instructions burned: 287 (million)
% 22.41/5.92 % (290001)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=1702795377:s2a=on:i=248:s2at=1.23:gtg=position_2976 on theBenchmark for (2976ds/248Mi)
% 22.41/5.92 % (289998)Instruction limit reached!
% 22.41/5.92 % (289998)------------------------------
% 22.41/5.92 % (289998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/5.92 % (289998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (289998)CaDiCaL version: 2.1.3
% 22.41/5.92 % (289998)Termination reason: Instruction limit
% 22.41/5.92 % (289998)Termination phase: Property scanning
% 22.41/5.92 % (289998)Time elapsed: 0.070 s
% 22.41/5.92 % (289998)Peak memory usage: 133 MB
% 22.41/5.92 % (289998)Instructions burned: 157 (million)
% 22.41/5.92 % (290004)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2640230321:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2975 on theBenchmark for (2975ds/294Mi)
% 22.41/5.92 % (290001)Instruction limit reached!
% 22.41/5.92 % (290001)------------------------------
% 22.41/5.92 % (290001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/5.92 % (290001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (290001)CaDiCaL version: 2.1.3
% 22.41/5.92 % (290001)Termination reason: Instruction limit
% 22.41/5.92 % (290001)Termination phase: Property scanning
% 22.41/5.92 % (290001)Time elapsed: 0.108 s
% 22.41/5.92 % (290001)Peak memory usage: 133 MB
% 22.41/5.92 % (290001)Instructions burned: 249 (million)
% 22.41/5.92 % (290006)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1001889648:i=2350_2974 on theBenchmark for (2974ds/2350Mi)
% 22.41/5.92 % (290004)Instruction limit reached!
% 22.41/5.92 % (290004)------------------------------
% 22.41/5.92 % (290004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/5.92 % (290004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (290004)CaDiCaL version: 2.1.3
% 22.41/5.92 % (290004)Termination reason: Instruction limit
% 22.41/5.92 % (290004)Termination phase: SInE selection
% 22.41/5.92 % (290004)Time elapsed: 0.104 s
% 22.41/5.92 % (290004)Peak memory usage: 134 MB
% 22.41/5.92 % (290004)Instructions burned: 297 (million)
% 22.41/5.92 % (290000)Instruction limit reached!
% 22.41/5.92 % (290000)------------------------------
% 22.41/5.92 % (290000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/5.92 % (290000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (290000)CaDiCaL version: 2.1.3
% 22.41/5.92 % (290000)Termination reason: Instruction limit
% 22.41/5.92 % (290000)Termination phase: Saturation
% 22.41/5.92 % (290000)Time elapsed: 0.253 s
% 22.41/5.92 % (290000)Peak memory usage: 141 MB
% 22.41/5.92 % (290000)Instructions burned: 325 (million)
% 22.41/5.92 % (290008)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3342759396:cts=off:i=113:fsr=off:ss=included:sgt=4_2973 on theBenchmark for (2973ds/113Mi)
% 22.41/5.92 % (290010)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=848732792:i=127:av=off:fsr=off:sup=off_2973 on theBenchmark for (2973ds/127Mi)
% 22.41/5.92 % (290010)Instruction limit reached!
% 22.41/5.92 % (290010)------------------------------
% 22.41/5.92 % (290010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/5.92 % (290010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (290010)CaDiCaL version: 2.1.3
% 22.41/5.92 % (290010)Termination reason: Instruction limit
% 22.41/5.92 % (290010)Termination phase: Preprocessing 1
% 22.41/5.92 % (290010)Time elapsed: 0.057 s
% 22.41/5.92 % (290010)Peak memory usage: 136 MB
% 22.41/5.92 % (290010)Instructions burned: 129 (million)
% 22.41/5.92 % (290008)Instruction limit reached!
% 22.41/5.92 % (290008)------------------------------
% 22.41/5.92 % (290008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/5.92 % (290008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/5.92 % (290008)CaDiCaL version: 2.1.3
% 22.41/5.92 % (290008)Termination reason: Instruction limit
% 22.41/5.92 % (290008)Termination phase: SInE selection
% 22.41/5.92 % (290008)Time elapsed: 0.090 s
% 25.82/10.14 % (290008)Peak memory usage: 133 MB
% 25.82/10.14 % (290008)Instructions burned: 114 (million)
% 25.82/10.14 % (290011)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=906235707:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2972 on theBenchmark for (2972ds/114Mi)
% 25.82/10.14 % (290011)Instruction limit reached!
% 25.82/10.14 % (290011)------------------------------
% 25.82/10.14 % (290011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290011)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290011)Termination reason: Instruction limit
% 25.82/10.14 % (290011)Termination phase: Property scanning
% 25.82/10.14 % (290011)Time elapsed: 0.052 s
% 25.82/10.14 % (290011)Peak memory usage: 133 MB
% 25.82/10.14 % (290011)Instructions burned: 116 (million)
% 25.82/10.14 % (290014)lrs+10_1_sil=8000:sp=occurrence:random_seed=1561464730:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2971 on theBenchmark for (2971ds/907Mi)
% 25.82/10.14 % (290015)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3644850057:i=437:sd=1:aac=none:ss=included_2971 on theBenchmark for (2971ds/437Mi)
% 25.82/10.14 % (290017)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=701844627:i=5202:ss=axioms:sgt=16_2970 on theBenchmark for (2970ds/5202Mi)
% 25.82/10.14 % (290015)Instruction limit reached!
% 25.82/10.14 % (290015)------------------------------
% 25.82/10.14 % (290015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290015)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290015)Termination reason: Instruction limit
% 25.82/10.14 % (290015)Termination phase: Saturation
% 25.82/10.14 % (290015)Time elapsed: 0.284 s
% 25.82/10.14 % (290015)Peak memory usage: 141 MB
% 25.82/10.14 % (290015)Instructions burned: 437 (million)
% 25.82/10.14 % (290014)Instruction limit reached!
% 25.82/10.14 % (290014)------------------------------
% 25.82/10.14 % (290014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290014)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290014)Termination reason: Instruction limit
% 25.82/10.14 % (290014)Termination phase: Property scanning
% 25.82/10.14 % (290014)Time elapsed: 0.334 s
% 25.82/10.14 % (290014)Peak memory usage: 154 MB
% 25.82/10.14 % (290014)Instructions burned: 909 (million)
% 25.82/10.14 % (290022)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=896739807:st=8:i=592:sd=3:ep=RST:ss=axioms_2967 on theBenchmark for (2967ds/592Mi)
% 25.82/10.14 % (290021)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4035044833:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2967 on theBenchmark for (2967ds/134Mi)
% 25.82/10.14 % (290021)Instruction limit reached!
% 25.82/10.14 % (290021)------------------------------
% 25.82/10.14 % (290021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290021)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290021)Termination reason: Instruction limit
% 25.82/10.14 % (290021)Termination phase: SInE selection
% 25.82/10.14 % (290021)Time elapsed: 0.103 s
% 25.82/10.14 % (290021)Peak memory usage: 133 MB
% 25.82/10.14 % (290021)Instructions burned: 134 (million)
% 25.82/10.14 % (290025)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=651923307:st=3:i=13193:sd=3:ss=axioms_2964 on theBenchmark for (2964ds/13193Mi)
% 25.82/10.14 % (290022)Instruction limit reached!
% 25.82/10.14 % (290022)------------------------------
% 25.82/10.14 % (290022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290022)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290022)Termination reason: Instruction limit
% 25.82/10.14 % (290022)Termination phase: Preprocessing 2
% 25.82/10.14 % (290022)Time elapsed: 0.270 s
% 25.82/10.14 % (290022)Peak memory usage: 145 MB
% 25.82/10.14 % (290022)Instructions burned: 592 (million)
% 25.82/10.14 % (290027)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=3611605858:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/125Mi)
% 25.82/10.14 % (290027)Instruction limit reached!
% 25.82/10.14 % (290027)------------------------------
% 25.82/10.14 % (290027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290027)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290027)Termination reason: Instruction limit
% 25.82/10.14 % (290027)Termination phase: Property scanning
% 25.82/10.14 % (290027)Time elapsed: 0.030 s
% 25.82/10.14 % (290027)Peak memory usage: 133 MB
% 25.82/10.14 % (290027)Instructions burned: 126 (million)
% 25.82/10.14 % (290029)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4280243175:i=134:gtgl=5:slsql=off:gtg=exists_sym_2962 on theBenchmark for (2962ds/134Mi)
% 25.82/10.14 % (290029)Instruction limit reached!
% 25.82/10.14 % (290029)------------------------------
% 25.82/10.14 % (290029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290029)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290029)Termination reason: Instruction limit
% 25.82/10.14 % (290029)Termination phase: Property scanning
% 25.82/10.14 % (290029)Time elapsed: 0.062 s
% 25.82/10.14 % (290029)Peak memory usage: 134 MB
% 25.82/10.14 % (290029)Instructions burned: 136 (million)
% 25.82/10.14 % (290031)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2301473267:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/141Mi)
% 25.82/10.14 % (290031)Instruction limit reached!
% 25.82/10.14 % (290031)------------------------------
% 25.82/10.14 % (290031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290031)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290031)Termination reason: Instruction limit
% 25.82/10.14 % (290031)Termination phase: SInE selection
% 25.82/10.14 % (290031)Time elapsed: 0.104 s
% 25.82/10.14 % (290031)Peak memory usage: 133 MB
% 25.82/10.14 % (290031)Instructions burned: 142 (million)
% 25.82/10.14 % (290006)Instruction limit reached!
% 25.82/10.14 % (290006)------------------------------
% 25.82/10.14 % (290006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290006)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290006)Termination reason: Instruction limit
% 25.82/10.14 % (290006)Termination phase: Property scanning
% 25.82/10.14 % (290006)Time elapsed: 1.535 s
% 25.82/10.14 % (290006)Peak memory usage: 227 MB
% 25.82/10.14 % (290006)Instructions burned: 2352 (million)
% 25.82/10.14 % (290033)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1472123244:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2957 on theBenchmark for (2957ds/431Mi)
% 25.82/10.14 % (290034)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=2089609296:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi)
% 25.82/10.14 % (290033)Refutation not found, incomplete strategy
% 25.82/10.14 % (290033)------------------------------
% 25.82/10.14 % (290033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290033)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290033)Termination reason: Refutation not found, incomplete strategy
% 25.82/10.14 % (290033)Time elapsed: 0.190 s
% 25.82/10.14 % (290033)Peak memory usage: 139 MB
% 25.82/10.14 % (290033)Instructions burned: 242 (million)
% 25.82/10.14 % (290033)------------------------------
% 25.82/10.14 % (290033)------------------------------
% 25.82/10.14 % (290037)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=3988442479:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2951 on theBenchmark for (2951ds/150Mi)
% 25.82/10.14 % (290037)Instruction limit reached!
% 25.82/10.14 % (290037)------------------------------
% 25.82/10.14 % (290037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290037)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290037)Termination reason: Instruction limit
% 25.82/10.14 % (290037)Termination phase: SInE selection
% 25.82/10.14 % (290037)Time elapsed: 0.119 s
% 25.82/10.14 % (290037)Peak memory usage: 133 MB
% 25.82/10.14 % (290037)Instructions burned: 151 (million)
% 25.82/10.14 % (290039)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=462326769:i=14155:bd=all_2949 on theBenchmark for (2949ds/14155Mi)
% 25.82/10.14 % (290017)Instruction limit reached!
% 25.82/10.14 % (290017)------------------------------
% 25.82/10.14 % (290017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290017)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290017)Termination reason: Instruction limit
% 25.82/10.14 % (290017)Termination phase: Saturation
% 25.82/10.14 % (290017)Time elapsed: 3.119 s
% 25.82/10.14 % (290017)Peak memory usage: 258 MB
% 25.82/10.14 % (290017)Instructions burned: 5202 (million)
% 25.82/10.14 % (290041)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1538600393:i=667:av=off:fsr=off_2938 on theBenchmark for (2938ds/667Mi)
% 25.82/10.14 % (290041)Instruction limit reached!
% 25.82/10.14 % (290041)------------------------------
% 25.82/10.14 % (290041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290041)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290041)Termination reason: Instruction limit
% 25.82/10.14 % (290041)Termination phase: NewCNF
% 25.82/10.14 % (290041)Time elapsed: 0.529 s
% 25.82/10.14 % (290041)Peak memory usage: 183 MB
% 25.82/10.14 % (290041)Instructions burned: 668 (million)
% 25.82/10.14 % (290065)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2173604309:s2a=on:i=185:s2at=1.8:fdi=4_2931 on theBenchmark for (2931ds/185Mi)
% 25.82/10.14 % (290065)Instruction limit reached!
% 25.82/10.14 % (290065)------------------------------
% 25.82/10.14 % (290065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290065)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290065)Termination reason: Instruction limit
% 25.82/10.14 % (290065)Termination phase: SInE selection
% 25.82/10.14 % (290065)Time elapsed: 0.128 s
% 25.82/10.14 % (290065)Peak memory usage: 133 MB
% 25.82/10.14 % (290065)Instructions burned: 187 (million)
% 25.82/10.14 % (290167)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=53531988:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2928 on theBenchmark for (2928ds/193Mi)
% 25.82/10.14 % (290167)Instruction limit reached!
% 25.82/10.14 % (290167)------------------------------
% 25.82/10.14 % (290167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290167)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290167)Termination reason: Instruction limit
% 25.82/10.14 % (290167)Termination phase: SInE selection
% 25.82/10.14 % (290167)Time elapsed: 0.147 s
% 25.82/10.14 % (290167)Peak memory usage: 134 MB
% 25.82/10.14 % (290167)Instructions burned: 193 (million)
% 25.82/10.14 % (290285)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1247965451:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2926 on theBenchmark for (2926ds/4850Mi)
% 25.82/10.14 % (290034)Instruction limit reached!
% 25.82/10.14 % (290034)------------------------------
% 25.82/10.14 % (290034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.82/10.14 % (290034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.82/10.14 % (290034)CaDiCaL version: 2.1.3
% 25.82/10.14 % (290034)Termination reason: Instruction limit
% 25.82/10.14 % (290034)Termination phase: Function definition elimination
% 25.82/10.14 % (290034)Time elapsed: 3.798 s
% 25.82/10.14 % (290034)Peak memory usage: 244 MB
% 25.82/10.14 % (290034)Instructions burned: 6062 (million)
% 25.82/10.14 % (290639)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1818228261:i=12111:sd=1:ss=included_2917 on theBenchmark for (2917ds/12111Mi)
% 25.82/10.14 % (289984)First to succeed.
% 25.82/10.14 % (289984)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-289978"
% 25.82/10.14 % (289984)Refutation found. Thanks to Tanya!
% 25.82/10.14 % SZS status Theorem for theBenchmark
% 25.82/10.14 % SZS output start Proof for theBenchmark
% See solution above
% 53.07/10.27 % (289984)------------------------------
% 53.07/10.27 % (289984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.07/10.27 % (289984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.07/10.27 % (289984)CaDiCaL version: 2.1.3
% 53.07/10.27 % (289984)Termination reason: Refutation
% 53.07/10.27 % (289984)Time elapsed: 6.698 s
% 53.07/10.27 % (289984)Peak memory usage: 331 MB
% 53.07/10.27 % (289984)Instructions burned: 16911 (million)
% 53.07/10.27 % (289984)------------------------------
% 53.07/10.27 % (289984)------------------------------
% 53.07/10.27 % (289978)Success in time 9.292 s
% 53.07/10.27 % Vampire exiting
%------------------------------------------------------------------------------