%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP635+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:10 AM UTC 2026
% Result : Theorem 27.28s 5.33s
% Output : Refutation 32.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 67
% Syntax : Number of formulae : 597 ( 61 unt; 38 def)
% Number of atoms : 2919 ( 249 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 3944 (1622 ~;1968 |; 234 &)
% ( 50 <=>; 70 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 33 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 9 con; 0-4 aty)
% Number of variables : 684 ( 0 sgn 639 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ? [X4] :
( v1_group_1(X4)
& m1_group_2(X4,X1)
& u1_struct_0(X4) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_latsubgr) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ? [X4] :
( v1_group_1(X4)
& m1_group_2(X4,X1)
& u1_struct_0(X4) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f6,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f9,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(X4,k1_relat_1(X0))
& r2_hidden(X4,X1)
& X3 = k1_funct_1(X0,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_funct_1) ).
fof(f10,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( ( ( X1 = k1_xboole_0
=> X0 = k1_xboole_0 )
=> ( v1_funct_2(X2,X0,X1)
<=> X0 = k4_relset_1(X0,X1,X2) ) )
& ( X1 = k1_xboole_0
=> ( X0 = k1_xboole_0
| ( v1_funct_2(X2,X0,X1)
<=> X2 = k1_xboole_0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_funct_2) ).
fof(f11,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( r1_rlvect_1(X0,X1)
<=> r2_hidden(X1,u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_rlvect_1) ).
fof(f12,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_group_6(X2,X0,X1)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X3,X4)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_group_6) ).
fof(f15,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_group_1) ).
fof(f19,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_funct_2) ).
fof(f20,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_group_1) ).
fof(f22,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(f26,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f28,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(f31,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f40,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f42,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f53,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f54,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k4_relset_1(X0,X1,X2) = k1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f55,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f56,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f58,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ! [X4] :
~ ( r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
& ! [X5] :
( m1_subset_1(X5,X0)
=> ~ ( r2_hidden(X5,X2)
& X4 = k1_funct_1(X3,X5) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t116_funct_2) ).
fof(f59,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f60,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f62,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] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X3,X0,X1)
& m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
=> k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,k3_group_1(X0,X2)) = k3_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_group_6) ).
fof(f63,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ( X1 != k1_xboole_0
=> ! [X4] :
( ? [X5] :
( r2_hidden(X5,X0)
& r2_hidden(X5,X2)
& X4 = k1_funct_1(X3,X5) )
=> r2_hidden(X4,k9_relat_1(X3,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_funct_2) ).
fof(f65,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> r1_rlvect_1(X1,k2_group_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t55_group_2) ).
fof(f66,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))
=> ! [X3] :
( m1_group_2(X3,X0)
=> ( ( r1_rlvect_1(X3,X1)
& r1_rlvect_1(X3,X2) )
=> r1_rlvect_1(X3,k1_group_1(X0,X1,X2)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t59_group_2) ).
fof(f68,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)
=> ( r1_rlvect_1(X2,X1)
=> r1_rlvect_1(X2,k3_group_1(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_group_2) ).
fof(f69,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( X1 != k1_xboole_0
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
=> r2_hidden(k1_group_1(X0,X2,X3),X1) ) ) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
=> r2_hidden(k3_group_1(X0,X2),X1) ) )
& ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
=> u1_struct_0(X2) != X1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t61_group_2) ).
fof(f71,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f74,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( X1 != k1_xboole_0
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
=> r2_hidden(k1_group_1(X0,X2,X3),X1) ) ) )
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ( r2_hidden(X4,X1)
=> r2_hidden(k3_group_1(X0,X4),X1) ) )
& ! [X5] :
( ( v1_group_1(X5)
& m1_group_2(X5,X0) )
=> u1_struct_0(X5) != X1 ) ) ) ),
inference(rectify,[],[f69]) ).
fof(f76,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ! [X4] :
( ~ v1_group_1(X4)
| ~ m1_group_2(X4,X1)
| u1_struct_0(X4) != k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
& m1_group_2(X3,X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ 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,[],[f2]) ).
fof(f77,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ! [X4] :
( ~ v1_group_1(X4)
| ~ m1_group_2(X4,X1)
| u1_struct_0(X4) != k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
& m1_group_2(X3,X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ 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,[],[f76]) ).
fof(f83,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f6]) ).
fof(f88,plain,
! [X0] :
( ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(X4,k1_relat_1(X0))
& r2_hidden(X4,X1)
& X3 = k1_funct_1(X0,X4) ) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f89,plain,
! [X0] :
( ! [X1,X2] :
( X2 = k9_relat_1(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ? [X4] :
( r2_hidden(X4,k1_relat_1(X0))
& r2_hidden(X4,X1)
& X3 = k1_funct_1(X0,X4) ) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f88]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ( ( ( v1_funct_2(X2,X0,X1)
<=> X0 = k4_relset_1(X0,X1,X2) )
| ( k1_xboole_0 != X0
& X1 = k1_xboole_0 ) )
& ( X0 = k1_xboole_0
| ( v1_funct_2(X2,X0,X1)
<=> X2 = k1_xboole_0 )
| k1_xboole_0 != X1 ) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f91,plain,
! [X0,X1,X2] :
( ( ( ( v1_funct_2(X2,X0,X1)
<=> X0 = k4_relset_1(X0,X1,X2) )
| ( k1_xboole_0 != X0
& X1 = k1_xboole_0 ) )
& ( X0 = k1_xboole_0
| ( v1_funct_2(X2,X0,X1)
<=> X2 = k1_xboole_0 )
| k1_xboole_0 != X1 ) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0] :
( ! [X1] :
( r1_rlvect_1(X0,X1)
<=> r2_hidden(X1,u1_struct_0(X0)) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f93,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_group_6(X2,X0,X1)
<=> ! [X3] :
( ! [X4] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X3,X4)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f94,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_group_6(X2,X0,X1)
<=> ! [X3] :
( ! [X4] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X3,X4)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f93]) ).
fof(f97,plain,
! [X0,X1,X2] :
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f15]) ).
fof(f98,plain,
! [X0,X1,X2] :
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f97]) ).
fof(f99,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f102,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f101]) ).
fof(f103,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,[],[f22]) ).
fof(f104,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,[],[f103]) ).
fof(f108,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f109,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,[],[f28]) ).
fof(f110,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,[],[f109]) ).
fof(f111,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f115,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f116,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f115]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f53]) ).
fof(f125,plain,
! [X0,X1,X2,X3] :
( k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0,X1,X2] :
( k4_relset_1(X0,X1,X2) = k1_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f54]) ).
fof(f127,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ~ r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
| ? [X5] :
( r2_hidden(X5,X2)
& X4 = k1_funct_1(X3,X5)
& m1_subset_1(X5,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f58]) ).
fof(f130,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ~ r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
| ? [X5] :
( r2_hidden(X5,X2)
& X4 = k1_funct_1(X3,X5)
& m1_subset_1(X5,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f59]) ).
fof(f132,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f133,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f132]) ).
fof(f135,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,k3_group_1(X0,X2)) = k3_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,X2))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f136,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,k3_group_1(X0,X2)) = k3_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,X2))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( r2_hidden(X4,k9_relat_1(X3,X2))
| ! [X5] :
( ~ r2_hidden(X5,X0)
| ~ r2_hidden(X5,X2)
| k1_funct_1(X3,X5) != X4 ) )
| k1_xboole_0 = X1
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f63]) ).
fof(f138,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( r2_hidden(X4,k9_relat_1(X3,X2))
| ! [X5] :
( ~ r2_hidden(X5,X0)
| ~ r2_hidden(X5,X2)
| k1_funct_1(X3,X5) != X4 ) )
| k1_xboole_0 = X1
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f137]) ).
fof(f141,plain,
! [X0] :
( ! [X1] :
( r1_rlvect_1(X1,k2_group_1(X0))
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f65]) ).
fof(f142,plain,
! [X0] :
( ! [X1] :
( r1_rlvect_1(X1,k2_group_1(X0))
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f141]) ).
fof(f143,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( r1_rlvect_1(X3,k1_group_1(X0,X1,X2))
| ~ r1_rlvect_1(X3,X1)
| ~ r1_rlvect_1(X3,X2)
| ~ 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)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f66]) ).
fof(f144,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( r1_rlvect_1(X3,k1_group_1(X0,X1,X2))
| ~ r1_rlvect_1(X3,X1)
| ~ r1_rlvect_1(X3,X2)
| ~ 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)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f143]) ).
fof(f146,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_rlvect_1(X2,k3_group_1(X0,X1))
| ~ r1_rlvect_1(X2,X1)
| ~ 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,[],[f68]) ).
fof(f147,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_rlvect_1(X2,k3_group_1(X0,X1))
| ~ r1_rlvect_1(X2,X1)
| ~ 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,[],[f146]) ).
fof(f148,plain,
! [X0] :
( ! [X1] :
( k1_xboole_0 = X1
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k1_group_1(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ? [X4] :
( ~ r2_hidden(k3_group_1(X0,X4),X1)
& r2_hidden(X4,X1)
& m1_subset_1(X4,u1_struct_0(X0)) )
| ? [X5] :
( u1_struct_0(X5) = X1
& v1_group_1(X5)
& m1_group_2(X5,X0) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f149,plain,
! [X0] :
( ! [X1] :
( k1_xboole_0 = X1
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k1_group_1(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ? [X4] :
( ~ r2_hidden(k3_group_1(X0,X4),X1)
& r2_hidden(X4,X1)
& m1_subset_1(X4,u1_struct_0(X0)) )
| ? [X5] :
( u1_struct_0(X5) = X1
& v1_group_1(X5)
& m1_group_2(X5,X0) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f148]) ).
fof(f151,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f71]) ).
fof(f153,definition,
! [X1,X0] :
( ? [X2] :
( ? [X3] :
( ~ r2_hidden(k1_group_1(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ sP0(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f154,definition,
! [X1,X0] :
( ? [X5] :
( u1_struct_0(X5) = X1
& v1_group_1(X5)
& m1_group_2(X5,X0) )
| ~ sP1(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f155,plain,
! [X0] :
( ! [X1] :
( k1_xboole_0 = X1
| sP0(X1,X0)
| ? [X4] :
( ~ r2_hidden(k3_group_1(X0,X4),X1)
& r2_hidden(X4,X1)
& m1_subset_1(X4,u1_struct_0(X0)) )
| sP1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(definition_folding,[],[f149,f154,f153]) ).
fof(f156,plain,
( ! [X4] :
( ~ v1_group_1(X4)
| ~ m1_group_2(X4,sK3)
| u1_struct_0(X4) != k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),sK4,u1_struct_0(sK5)) )
& m1_group_2(sK5,sK2)
& v1_funct_1(sK4)
& v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
& v1_group_6(sK4,sK2,sK3)
& m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3))
& ~ v3_struct_0(sK3)
& v3_group_1(sK3)
& v4_group_1(sK3)
& l1_group_1(sK3)
& ~ v3_struct_0(sK2)
& v3_group_1(sK2)
& v4_group_1(sK2)
& l1_group_1(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f77]) ).
fof(f157,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ r2_hidden(X4,k1_relat_1(X0))
| ~ r2_hidden(X4,X1)
| k1_funct_1(X0,X4) != X3 )
| ~ r2_hidden(X3,X2) )
& ( ? [X4] :
( r2_hidden(X4,k1_relat_1(X0))
& r2_hidden(X4,X1)
& X3 = k1_funct_1(X0,X4) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ! [X4] :
( ~ r2_hidden(X4,k1_relat_1(X0))
| ~ r2_hidden(X4,X1)
| k1_funct_1(X0,X4) != X3 ) )
& ( ? [X4] :
( r2_hidden(X4,k1_relat_1(X0))
& r2_hidden(X4,X1)
& X3 = k1_funct_1(X0,X4) )
| ~ r2_hidden(X3,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(nnf_transformation,[],[f89]) ).
fof(f158,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ? [X3] :
( ( ! [X4] :
( ~ r2_hidden(X4,k1_relat_1(X0))
| ~ r2_hidden(X4,X1)
| k1_funct_1(X0,X4) != X3 )
| ~ r2_hidden(X3,X2) )
& ( ? [X5] :
( r2_hidden(X5,k1_relat_1(X0))
& r2_hidden(X5,X1)
& k1_funct_1(X0,X5) = X3 )
| r2_hidden(X3,X2) ) ) )
& ( ! [X6] :
( ( r2_hidden(X6,X2)
| ! [X7] :
( ~ r2_hidden(X7,k1_relat_1(X0))
| ~ r2_hidden(X7,X1)
| k1_funct_1(X0,X7) != X6 ) )
& ( ? [X8] :
( r2_hidden(X8,k1_relat_1(X0))
& r2_hidden(X8,X1)
& k1_funct_1(X0,X8) = X6 )
| ~ r2_hidden(X6,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(rectify,[],[f157]) ).
fof(f159,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = k9_relat_1(X0,X1)
| ( ( ! [X4] :
( ~ r2_hidden(X4,k1_relat_1(X0))
| ~ r2_hidden(X4,X1)
| k1_funct_1(X0,X4) != sK6(X0,X1,X2) )
| ~ r2_hidden(sK6(X0,X1,X2),X2) )
& ( ( r2_hidden(sK7(X0,X1,X2),k1_relat_1(X0))
& r2_hidden(sK7(X0,X1,X2),X1)
& sK6(X0,X1,X2) = k1_funct_1(X0,sK7(X0,X1,X2)) )
| r2_hidden(sK6(X0,X1,X2),X2) ) ) )
& ( ! [X6] :
( ( r2_hidden(X6,X2)
| ! [X7] :
( ~ r2_hidden(X7,k1_relat_1(X0))
| ~ r2_hidden(X7,X1)
| k1_funct_1(X0,X7) != X6 ) )
& ( ( r2_hidden(sK8(X0,X1,X6),k1_relat_1(X0))
& r2_hidden(sK8(X0,X1,X6),X1)
& k1_funct_1(X0,sK8(X0,X1,X6)) = X6 )
| ~ r2_hidden(X6,X2) ) )
| k9_relat_1(X0,X1) != X2 ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X3,sK6(X0,X1,X2)),skolemize(X5,sK7(X0,X1,X2)),skolemize(X8,sK8(X0,X1,X6))],[f158]) ).
fof(f160,plain,
! [X0,X1,X2] :
( ( ( ( ( v1_funct_2(X2,X0,X1)
| k4_relset_1(X0,X1,X2) != X0 )
& ( X0 = k4_relset_1(X0,X1,X2)
| ~ v1_funct_2(X2,X0,X1) ) )
| ( k1_xboole_0 != X0
& X1 = k1_xboole_0 ) )
& ( X0 = k1_xboole_0
| ( ( v1_funct_2(X2,X0,X1)
| k1_xboole_0 != X2 )
& ( X2 = k1_xboole_0
| ~ v1_funct_2(X2,X0,X1) ) )
| k1_xboole_0 != X1 ) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(nnf_transformation,[],[f91]) ).
fof(f161,plain,
! [X0] :
( ! [X1] :
( ( r1_rlvect_1(X0,X1)
| ~ r2_hidden(X1,u1_struct_0(X0)) )
& ( r2_hidden(X1,u1_struct_0(X0))
| ~ r1_rlvect_1(X0,X1) ) )
| ~ l1_struct_0(X0) ),
inference(nnf_transformation,[],[f92]) ).
fof(f162,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_group_6(X2,X0,X1)
| ? [X3] :
( ? [X4] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X3,X4)) != k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X3] :
( ! [X4] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X3,X4)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ v1_group_6(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f94]) ).
fof(f163,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_group_6(X2,X0,X1)
| ? [X3] :
( ? [X4] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X3,X4)) != k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X3),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X4))
& m1_subset_1(X4,u1_struct_0(X0)) )
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X5] :
( ! [X6] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X5,X6)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X5),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X6))
| ~ m1_subset_1(X6,u1_struct_0(X0)) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ v1_group_6(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f162]) ).
fof(f164,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( v1_group_6(X2,X0,X1)
| ( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,sK9(X0,X1,X2),sK10(X0,X1,X2))) != k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK9(X0,X1,X2)),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,sK10(X0,X1,X2)))
& m1_subset_1(sK10(X0,X1,X2),u1_struct_0(X0))
& m1_subset_1(sK9(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ! [X5] :
( ! [X6] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X5,X6)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X5),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X6))
| ~ m1_subset_1(X6,u1_struct_0(X0)) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ v1_group_6(X2,X0,X1) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X3,sK9(X0,X1,X2)),skolemize(X4,sK10(X0,X1,X2))],[f163]) ).
fof(f179,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f56]) ).
fof(f180,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ~ r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
| ( r2_hidden(sK25(X0,X2,X3,X4),X2)
& k1_funct_1(X3,sK25(X0,X2,X3,X4)) = X4
& m1_subset_1(sK25(X0,X2,X3,X4),X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X5,sK25(X0,X2,X3,X4))],[f130]) ).
fof(f181,plain,
! [X1,X0] :
( ? [X5] :
( u1_struct_0(X5) = X1
& v1_group_1(X5)
& m1_group_2(X5,X0) )
| ~ sP1(X1,X0) ),
inference(nnf_transformation,[],[f154]) ).
fof(f182,plain,
! [X0,X1] :
( ? [X2] :
( u1_struct_0(X2) = X0
& v1_group_1(X2)
& m1_group_2(X2,X1) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( ( u1_struct_0(sK26(X0,X1)) = X0
& v1_group_1(sK26(X0,X1))
& m1_group_2(sK26(X0,X1),X1) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X2,sK26(X0,X1))],[f182]) ).
fof(f184,plain,
! [X1,X0] :
( ? [X2] :
( ? [X3] :
( ~ r2_hidden(k1_group_1(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ sP0(X1,X0) ),
inference(nnf_transformation,[],[f153]) ).
fof(f185,plain,
! [X0,X1] :
( ? [X2] :
( ? [X3] :
( ~ r2_hidden(k1_group_1(X1,X2,X3),X0)
& r2_hidden(X2,X0)
& r2_hidden(X3,X0)
& m1_subset_1(X3,u1_struct_0(X1)) )
& m1_subset_1(X2,u1_struct_0(X1)) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f184]) ).
fof(f186,plain,
! [X0,X1] :
( ( ~ r2_hidden(k1_group_1(X1,sK27(X0,X1),sK28(X0,X1)),X0)
& r2_hidden(sK27(X0,X1),X0)
& r2_hidden(sK28(X0,X1),X0)
& m1_subset_1(sK28(X0,X1),u1_struct_0(X1))
& m1_subset_1(sK27(X0,X1),u1_struct_0(X1)) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28]),skolemize(X2,sK27(X0,X1)),skolemize(X3,sK28(X0,X1))],[f185]) ).
fof(f187,plain,
! [X0] :
( ! [X1] :
( k1_xboole_0 = X1
| sP0(X1,X0)
| ? [X2] :
( ~ r2_hidden(k3_group_1(X0,X2),X1)
& r2_hidden(X2,X1)
& m1_subset_1(X2,u1_struct_0(X0)) )
| sP1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f155]) ).
fof(f188,plain,
! [X0] :
( ! [X1] :
( k1_xboole_0 = X1
| sP0(X1,X0)
| ( ~ r2_hidden(k3_group_1(X0,sK29(X0,X1)),X1)
& r2_hidden(sK29(X0,X1),X1)
& m1_subset_1(sK29(X0,X1),u1_struct_0(X0)) )
| sP1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(X2,sK29(X0,X1))],[f187]) ).
fof(f189,plain,
l1_group_1(sK2),
inference(cnf_transformation,[],[f156]) ).
fof(f190,plain,
v4_group_1(sK2),
inference(cnf_transformation,[],[f156]) ).
fof(f191,plain,
v3_group_1(sK2),
inference(cnf_transformation,[],[f156]) ).
fof(f192,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f156]) ).
fof(f193,plain,
l1_group_1(sK3),
inference(cnf_transformation,[],[f156]) ).
fof(f194,plain,
v4_group_1(sK3),
inference(cnf_transformation,[],[f156]) ).
fof(f195,plain,
v3_group_1(sK3),
inference(cnf_transformation,[],[f156]) ).
fof(f196,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f156]) ).
fof(f197,plain,
m2_relset_1(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(cnf_transformation,[],[f156]) ).
fof(f198,plain,
v1_group_6(sK4,sK2,sK3),
inference(cnf_transformation,[],[f156]) ).
fof(f199,plain,
v1_funct_2(sK4,u1_struct_0(sK2),u1_struct_0(sK3)),
inference(cnf_transformation,[],[f156]) ).
fof(f200,plain,
v1_funct_1(sK4),
inference(cnf_transformation,[],[f156]) ).
fof(f201,plain,
m1_group_2(sK5,sK2),
inference(cnf_transformation,[],[f156]) ).
fof(f202,plain,
! [X4] :
( ~ v1_group_1(X4)
| ~ m1_group_2(X4,sK3)
| u1_struct_0(X4) != k2_funct_2(u1_struct_0(sK2),u1_struct_0(sK3),sK4,u1_struct_0(sK5)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f207,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f83]) ).
fof(f218,plain,
! [X2,X0,X1,X6,X7] :
( r2_hidden(X6,X2)
| ~ r2_hidden(X7,k1_relat_1(X0))
| ~ r2_hidden(X7,X1)
| k1_funct_1(X0,X7) != X6
| k9_relat_1(X0,X1) != X2
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f225,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| k1_xboole_0 = X1
| k4_relset_1(X0,X1,X2) = X0 ),
inference(cnf_transformation,[],[f160]) ).
fof(f229,plain,
! [X0,X1] :
( r2_hidden(X1,u1_struct_0(X0))
| ~ r1_rlvect_1(X0,X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f230,plain,
! [X0,X1] :
( ~ r2_hidden(X1,u1_struct_0(X0))
| r1_rlvect_1(X0,X1)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f231,plain,
! [X2,X0,X1,X6,X5] :
( ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X6,u1_struct_0(X0))
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ v1_group_6(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k1_group_1(X0,X5,X6)) = k1_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X5),k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,X6))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f237,plain,
! [X2,X0,X1] :
( m1_subset_1(k1_group_1(X0,X1,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f98]) ).
fof(f238,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f239,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f240,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,[],[f104]) ).
fof(f243,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f244,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f247,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f257,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f259,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f42]) ).
fof(f280,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f125]) ).
fof(f281,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k4_relset_1(X0,X1,X2) = k1_relat_1(X2) ),
inference(cnf_transformation,[],[f126]) ).
fof(f282,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f283,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f179]) ).
fof(f286,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
| m1_subset_1(sK25(X0,X2,X3,X4),X0)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
| k1_funct_1(X3,sK25(X0,X2,X3,X4)) = X4
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f288,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X4,k2_funct_2(X0,X1,X3,X2))
| r2_hidden(sK25(X0,X2,X3,X4),X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f289,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f290,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X3,X0,X1)
| k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,k3_group_1(X0,X2)) = k3_group_1(X1,k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X3,X2))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f293,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X4,k9_relat_1(X3,X2))
| ~ r2_hidden(X5,X0)
| ~ r2_hidden(X5,X2)
| k1_funct_1(X3,X5) != X4
| k1_xboole_0 = X1
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
fof(f295,plain,
! [X0,X1] :
( r1_rlvect_1(X1,k2_group_1(X0))
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f296,plain,
! [X2,X3,X0,X1] :
( r1_rlvect_1(X3,k1_group_1(X0,X1,X2))
| ~ r1_rlvect_1(X3,X1)
| ~ r1_rlvect_1(X3,X2)
| ~ 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)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f298,plain,
! [X2,X0,X1] :
( r1_rlvect_1(X2,k3_group_1(X0,X1))
| ~ r1_rlvect_1(X2,X1)
| ~ 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,[],[f147]) ).
fof(f299,plain,
! [X0,X1] :
( m1_group_2(sK26(X0,X1),X1)
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f183]) ).
fof(f300,plain,
! [X0,X1] :
( v1_group_1(sK26(X0,X1))
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f183]) ).
fof(f301,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| u1_struct_0(sK26(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f183]) ).
fof(f304,plain,
! [X0,X1] :
( r2_hidden(sK28(X0,X1),X0)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
fof(f305,plain,
! [X0,X1] :
( r2_hidden(sK27(X0,X1),X0)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
fof(f306,plain,
! [X0,X1] :
( ~ r2_hidden(k1_group_1(X1,sK27(X0,X1),sK28(X0,X1)),X0)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
fof(f308,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| sP0(X1,X0)
| r2_hidden(sK29(X0,X1),X1)
| sP1(X1,X0)
| k1_xboole_0 = X1
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f309,plain,
! [X0,X1] :
( ~ r2_hidden(k3_group_1(X0,sK29(X0,X1)),X1)
| sP0(X1,X0)
| k1_xboole_0 = X1
| sP1(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f311,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f151]) ).
fof(f313,plain,
! [X2,X0,X1,X7] :
( r2_hidden(k1_funct_1(X0,X7),X2)
| ~ r2_hidden(X7,k1_relat_1(X0))
| ~ r2_hidden(X7,X1)
| k9_relat_1(X0,X1) != X2
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(equality_resolution,[],[f218]) ).
fof(f314,plain,
! [X0,X1,X7] :
( r2_hidden(k1_funct_1(X0,X7),k9_relat_1(X0,X1))
| ~ r2_hidden(X7,k1_relat_1(X0))
| ~ r2_hidden(X7,X1)
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(equality_resolution,[],[f313]) ).
fof(f323,plain,
! [X2,X3,X0,X1,X5] :
( ~ m2_relset_1(X3,X0,X1)
| ~ r2_hidden(X5,X0)
| ~ r2_hidden(X5,X2)
| k1_xboole_0 = X1
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| r2_hidden(k1_funct_1(X3,X5),k9_relat_1(X3,X2)) ),
inference(equality_resolution,[],[f293]) ).
fof(f324,definition,
sF30 = u1_struct_0(sK2),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f325,plain,
u1_struct_0(sK2) = sF30,
inference(reorient_equations,[],[f324]) ).
fof(f326,definition,
sF31 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f327,plain,
u1_struct_0(sK3) = sF31,
inference(reorient_equations,[],[f326]) ).
fof(f328,definition,
sF32 = u1_struct_0(sK5),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f329,plain,
u1_struct_0(sK5) = sF32,
inference(reorient_equations,[],[f328]) ).
fof(f330,definition,
sF33 = k2_funct_2(sF30,sF31,sK4,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f331,plain,
k2_funct_2(sF30,sF31,sK4,sF32) = sF33,
inference(reorient_equations,[],[f330]) ).
fof(f332,plain,
! [X4] :
( u1_struct_0(X4) != sF33
| ~ m1_group_2(X4,sK3)
| ~ v1_group_1(X4) ),
inference(definition_folding,[],[f202,f331,f329,f327,f325]) ).
fof(f333,plain,
v1_funct_2(sK4,sF30,sF31),
inference(definition_folding,[],[f199,f327,f325]) ).
fof(f334,plain,
m2_relset_1(sK4,sF30,sF31),
inference(definition_folding,[],[f197,f327,f325]) ).
fof(f377,plain,
( m1_subset_1(sF33,k1_zfmisc_1(sF31))
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31) ),
inference(superposition,[],[f238,f331]) ).
fof(f378,plain,
( m1_subset_1(sF33,k1_zfmisc_1(sF31))
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31) ),
inference(forward_subsumption_resolution,[],[f377,f200]) ).
fof(f379,plain,
( m1_subset_1(sF33,k1_zfmisc_1(sF31))
| ~ m1_relset_1(sK4,sF30,sF31) ),
inference(forward_subsumption_resolution,[],[f378,f333]) ).
fof(f381,definition,
( spl34_10
<=> m1_relset_1(sK4,sF30,sF31) ),
introduced(definition,[new_symbols(definition,[spl34_10])],[avatar_definition]) ).
fof(f382,plain,
( m1_relset_1(sK4,sF30,sF31)
| ~ spl34_10 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f383,plain,
( ~ m1_relset_1(sK4,sF30,sF31)
| spl34_10 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f385,definition,
( spl34_11
<=> m1_subset_1(sF33,k1_zfmisc_1(sF31)) ),
introduced(definition,[new_symbols(definition,[spl34_11])],[avatar_definition]) ).
fof(f387,plain,
( m1_subset_1(sF33,k1_zfmisc_1(sF31))
| ~ spl34_11 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,plain,
( ~ spl34_10
| spl34_11 ),
inference(avatar_split_clause,[],[f379,f385,f381]) ).
fof(f389,plain,
l1_struct_0(sK3),
inference(resolution,[],[f243,f193]) ).
fof(f390,plain,
l1_struct_0(sK2),
inference(resolution,[],[f243,f189]) ).
fof(f391,plain,
m1_relset_1(sK4,sF30,sF31),
inference(resolution,[],[f283,f334]) ).
fof(f392,plain,
( $false
| spl34_10 ),
inference(forward_subsumption_resolution,[],[f391,f383]) ).
fof(f393,plain,
spl34_10,
inference(avatar_contradiction_clause,[],[f392]) ).
fof(f394,plain,
( ! [X0] :
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| k2_funct_2(sF30,sF31,sK4,X0) = k9_relat_1(sK4,X0) )
| ~ spl34_10 ),
inference(resolution,[],[f280,f382]) ).
fof(f395,plain,
( ! [X0] :
( ~ v1_funct_2(sK4,sF30,sF31)
| k2_funct_2(sF30,sF31,sK4,X0) = k9_relat_1(sK4,X0) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f394,f200]) ).
fof(f396,plain,
( ! [X0] : k2_funct_2(sF30,sF31,sK4,X0) = k9_relat_1(sK4,X0)
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f395,f333]) ).
fof(f398,plain,
( sF33 = k9_relat_1(sK4,sF32)
| ~ spl34_10 ),
inference(superposition,[],[f331,f396]) ).
fof(f403,plain,
! [X0] :
( r2_hidden(X0,sF32)
| ~ r1_rlvect_1(sK5,X0)
| ~ l1_struct_0(sK5) ),
inference(superposition,[],[f229,f329]) ).
fof(f409,definition,
( spl34_12
<=> l1_struct_0(sK5) ),
introduced(definition,[new_symbols(definition,[spl34_12])],[avatar_definition]) ).
fof(f410,plain,
( l1_struct_0(sK5)
| ~ spl34_12 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f411,plain,
( ~ l1_struct_0(sK5)
| spl34_12 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f413,definition,
( spl34_13
<=> ! [X0] :
( r2_hidden(X0,sF32)
| ~ r1_rlvect_1(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_13])],[avatar_definition]) ).
fof(f414,plain,
( ! [X0] :
( ~ r1_rlvect_1(sK5,X0)
| r2_hidden(X0,sF32) )
| ~ spl34_13 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f415,plain,
( ~ spl34_12
| spl34_13 ),
inference(avatar_split_clause,[],[f403,f413,f409]) ).
fof(f421,plain,
! [X0] :
( ~ r2_hidden(X0,sF32)
| r1_rlvect_1(sK5,X0)
| ~ l1_struct_0(sK5) ),
inference(superposition,[],[f230,f329]) ).
fof(f428,plain,
( ! [X0] :
( v1_xboole_0(sF30)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| k8_funct_2(sF30,sF31,sK4,X0) = k1_funct_1(sK4,X0)
| ~ m1_subset_1(X0,sF30) )
| ~ spl34_10 ),
inference(resolution,[],[f282,f382]) ).
fof(f429,plain,
( ! [X0] :
( v1_xboole_0(sF30)
| ~ v1_funct_2(sK4,sF30,sF31)
| k8_funct_2(sF30,sF31,sK4,X0) = k1_funct_1(sK4,X0)
| ~ m1_subset_1(X0,sF30) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f428,f200]) ).
fof(f430,plain,
( ! [X0] :
( v1_xboole_0(sF30)
| k8_funct_2(sF30,sF31,sK4,X0) = k1_funct_1(sK4,X0)
| ~ m1_subset_1(X0,sF30) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f429,f333]) ).
fof(f432,definition,
( spl34_14
<=> ! [X0] :
( k8_funct_2(sF30,sF31,sK4,X0) = k1_funct_1(sK4,X0)
| ~ m1_subset_1(X0,sF30) ) ),
introduced(definition,[new_symbols(definition,[spl34_14])],[avatar_definition]) ).
fof(f433,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF30)
| k8_funct_2(sF30,sF31,sK4,X0) = k1_funct_1(sK4,X0) )
| ~ spl34_14 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,definition,
( spl34_15
<=> v1_xboole_0(sF30) ),
introduced(definition,[new_symbols(definition,[spl34_15])],[avatar_definition]) ).
fof(f436,plain,
( ~ v1_xboole_0(sF30)
| spl34_15 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f438,plain,
( spl34_14
| spl34_15
| ~ spl34_10 ),
inference(avatar_split_clause,[],[f430,f381,f435,f432]) ).
fof(f441,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK2,X0),sF30)
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ m1_subset_1(X0,sF30) ),
inference(superposition,[],[f240,f325]) ).
fof(f442,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK2,X0),sF30)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ m1_subset_1(X0,sF30) ),
inference(forward_subsumption_resolution,[],[f441,f192]) ).
fof(f445,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK2,X0),sF30)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ m1_subset_1(X0,sF30) ),
inference(forward_subsumption_resolution,[],[f442,f191]) ).
fof(f448,definition,
( spl34_16
<=> l1_group_1(sK5) ),
introduced(definition,[new_symbols(definition,[spl34_16])],[avatar_definition]) ).
fof(f449,plain,
( l1_group_1(sK5)
| ~ spl34_16 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( ~ l1_group_1(sK5)
| spl34_16 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f463,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK2,X0),sF30)
| ~ l1_group_1(sK2)
| ~ m1_subset_1(X0,sF30) ),
inference(forward_subsumption_resolution,[],[f445,f190]) ).
fof(f465,plain,
! [X0] :
( m1_subset_1(k3_group_1(sK2,X0),sF30)
| ~ m1_subset_1(X0,sF30) ),
inference(forward_subsumption_resolution,[],[f463,f189]) ).
fof(f467,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| k1_funct_1(sK4,sK25(sF30,sF32,sK4,X0)) = X0
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(superposition,[],[f287,f331]) ).
fof(f470,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| k1_funct_1(sK4,sK25(sF30,sF32,sK4,X0)) = X0
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(forward_subsumption_resolution,[],[f467,f200]) ).
fof(f472,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| k1_funct_1(sK4,sK25(sF30,sF32,sK4,X0)) = X0
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(forward_subsumption_resolution,[],[f470,f333]) ).
fof(f474,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| k1_funct_1(sK4,sK25(sF30,sF32,sK4,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f472,f334]) ).
fof(f479,definition,
( spl34_20
<=> v1_relat_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl34_20])],[avatar_definition]) ).
fof(f480,plain,
( v1_relat_1(sK4)
| ~ spl34_20 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f481,plain,
( ~ v1_relat_1(sK4)
| spl34_20 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f486,plain,
( l1_group_1(sK5)
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ l1_group_1(sK2) ),
inference(resolution,[],[f244,f201]) ).
fof(f487,plain,
( v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ l1_group_1(sK2)
| spl34_16 ),
inference(forward_subsumption_resolution,[],[f486,f450]) ).
fof(f488,plain,
( ~ v3_group_1(sK2)
| ~ l1_group_1(sK2)
| spl34_16 ),
inference(forward_subsumption_resolution,[],[f487,f192]) ).
fof(f489,plain,
( ~ l1_group_1(sK2)
| spl34_16 ),
inference(forward_subsumption_resolution,[],[f488,f191]) ).
fof(f490,plain,
( $false
| spl34_16 ),
inference(forward_subsumption_resolution,[],[f489,f189]) ).
fof(f491,plain,
spl34_16,
inference(avatar_contradiction_clause,[],[f490]) ).
fof(f492,plain,
( l1_struct_0(sK5)
| ~ spl34_16 ),
inference(resolution,[],[f449,f243]) ).
fof(f493,plain,
( $false
| spl34_12
| ~ spl34_16 ),
inference(forward_subsumption_resolution,[],[f492,f411]) ).
fof(f494,plain,
( spl34_12
| ~ spl34_16 ),
inference(avatar_contradiction_clause,[],[f493]) ).
fof(f495,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF32)
| r1_rlvect_1(sK5,X0) )
| ~ spl34_12 ),
inference(forward_subsumption_resolution,[],[f421,f410]) ).
fof(f496,plain,
( ! [X0,X1] :
( r2_hidden(k3_group_1(X0,X1),sF32)
| ~ r1_rlvect_1(sK5,X1)
| ~ m1_group_2(sK5,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) )
| ~ spl34_13 ),
inference(resolution,[],[f414,f298]) ).
fof(f497,plain,
( ! [X0] :
( r2_hidden(k2_group_1(X0),sF32)
| ~ m1_group_2(sK5,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl34_13 ),
inference(resolution,[],[f414,f295]) ).
fof(f498,plain,
( ! [X2,X0,X1] :
( r2_hidden(k1_group_1(X0,X1,X2),sF32)
| ~ r1_rlvect_1(sK5,X1)
| ~ r1_rlvect_1(sK5,X2)
| ~ m1_group_2(sK5,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) )
| ~ spl34_13 ),
inference(resolution,[],[f414,f296]) ).
fof(f500,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF30)
| k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,X0)) = k1_funct_1(sK4,k3_group_1(sK2,X0)) )
| ~ spl34_14 ),
inference(resolution,[],[f465,f433]) ).
fof(f505,plain,
( ~ v1_xboole_0(sF31)
| v3_struct_0(sK3)
| ~ l1_struct_0(sK3) ),
inference(superposition,[],[f257,f327]) ).
fof(f506,plain,
( ~ v1_xboole_0(sF30)
| v3_struct_0(sK2)
| ~ l1_struct_0(sK2) ),
inference(superposition,[],[f257,f325]) ).
fof(f507,plain,
( ~ v1_xboole_0(sF30)
| ~ l1_struct_0(sK2) ),
inference(forward_subsumption_resolution,[],[f506,f192]) ).
fof(f508,plain,
( ~ v1_xboole_0(sF31)
| ~ l1_struct_0(sK3) ),
inference(forward_subsumption_resolution,[],[f505,f196]) ).
fof(f510,plain,
~ v1_xboole_0(sF30),
inference(forward_subsumption_resolution,[],[f507,f390]) ).
fof(f511,plain,
~ v1_xboole_0(sF31),
inference(forward_subsumption_resolution,[],[f508,f389]) ).
fof(f517,plain,
~ spl34_15,
inference(avatar_split_clause,[],[f510,f435]) ).
fof(f523,plain,
! [X0] :
( r2_hidden(k3_group_1(sK2,X0),sF30)
| v1_xboole_0(sF30)
| ~ m1_subset_1(X0,sF30) ),
inference(resolution,[],[f290,f465]) ).
fof(f526,plain,
( ! [X0] :
( r2_hidden(k3_group_1(sK2,X0),sF30)
| ~ m1_subset_1(X0,sF30) )
| spl34_15 ),
inference(forward_subsumption_resolution,[],[f523,f436]) ).
fof(f534,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f207,f247]) ).
fof(f536,plain,
v1_relat_1(sK4),
inference(resolution,[],[f534,f334]) ).
fof(f537,plain,
( $false
| spl34_20 ),
inference(forward_subsumption_resolution,[],[f536,f481]) ).
fof(f538,plain,
spl34_20,
inference(avatar_contradiction_clause,[],[f537]) ).
fof(f544,plain,
( k4_relset_1(sF30,sF31,sK4) = k1_relat_1(sK4)
| ~ spl34_10 ),
inference(resolution,[],[f281,f382]) ).
fof(f567,plain,
( ~ v1_funct_2(sK4,sF30,sF31)
| k1_xboole_0 = sF31
| sF30 = k4_relset_1(sF30,sF31,sK4) ),
inference(resolution,[],[f225,f334]) ).
fof(f568,plain,
( k1_xboole_0 = sF31
| sF30 = k4_relset_1(sF30,sF31,sK4) ),
inference(forward_subsumption_resolution,[],[f567,f333]) ).
fof(f569,plain,
( sF30 = k1_relat_1(sK4)
| k1_xboole_0 = sF31
| ~ spl34_10 ),
inference(forward_demodulation,[],[f568,f544]) ).
fof(f571,definition,
( spl34_23
<=> k1_xboole_0 = sF31 ),
introduced(definition,[new_symbols(definition,[spl34_23])],[avatar_definition]) ).
fof(f572,plain,
( k1_xboole_0 != sF31
| spl34_23 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f573,plain,
( k1_xboole_0 = sF31
| ~ spl34_23 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl34_24
<=> sF30 = k1_relat_1(sK4) ),
introduced(definition,[new_symbols(definition,[spl34_24])],[avatar_definition]) ).
fof(f577,plain,
( sF30 = k1_relat_1(sK4)
| ~ spl34_24 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,plain,
( spl34_23
| spl34_24
| ~ spl34_10 ),
inference(avatar_split_clause,[],[f569,f381,f575,f571]) ).
fof(f588,plain,
( ~ v1_xboole_0(k1_xboole_0)
| ~ spl34_23 ),
inference(superposition,[],[f511,f573]) ).
fof(f590,plain,
( $false
| ~ spl34_23 ),
inference(forward_subsumption_resolution,[],[f588,f259]) ).
fof(f591,plain,
~ spl34_23,
inference(avatar_contradiction_clause,[],[f590]) ).
fof(f596,plain,
( m1_subset_1(k2_group_1(sK2),sF30)
| v3_struct_0(sK2)
| ~ l1_group_1(sK2) ),
inference(superposition,[],[f239,f325]) ).
fof(f597,plain,
( m1_subset_1(k2_group_1(sK2),sF30)
| ~ l1_group_1(sK2) ),
inference(forward_subsumption_resolution,[],[f596,f192]) ).
fof(f600,plain,
m1_subset_1(k2_group_1(sK2),sF30),
inference(forward_subsumption_resolution,[],[f597,f189]) ).
fof(f604,plain,
( r2_hidden(k2_group_1(sK2),sF30)
| v1_xboole_0(sF30) ),
inference(resolution,[],[f600,f290]) ).
fof(f605,plain,
( r2_hidden(k2_group_1(sK2),sF30)
| spl34_15 ),
inference(forward_subsumption_resolution,[],[f604,f436]) ).
fof(f618,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sK4,X0),sF33)
| ~ r2_hidden(X0,k1_relat_1(sK4))
| ~ r2_hidden(X0,sF32)
| ~ v1_relat_1(sK4)
| ~ v1_funct_1(sK4) )
| ~ spl34_10 ),
inference(superposition,[],[f314,f398]) ).
fof(f620,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sK4,X0),sF33)
| ~ r2_hidden(X0,k1_relat_1(sK4))
| ~ r2_hidden(X0,sF32)
| ~ v1_funct_1(sK4) )
| ~ spl34_10
| ~ spl34_20 ),
inference(forward_subsumption_resolution,[],[f618,f480]) ).
fof(f622,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sK4,X0),sF33)
| ~ r2_hidden(X0,k1_relat_1(sK4))
| ~ r2_hidden(X0,sF32) )
| ~ spl34_10
| ~ spl34_20 ),
inference(forward_subsumption_resolution,[],[f620,f200]) ).
fof(f624,plain,
( ! [X0] :
( r2_hidden(k1_funct_1(sK4,X0),sF33)
| ~ r2_hidden(X0,sF30)
| ~ r2_hidden(X0,sF32) )
| ~ spl34_10
| ~ spl34_20
| ~ spl34_24 ),
inference(forward_demodulation,[],[f622,f577]) ).
fof(f643,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK29(X1,k2_funct_2(X0,u1_struct_0(X1),X2,X3)),k2_funct_2(X0,u1_struct_0(X1),X2,X3))
| sP0(k2_funct_2(X0,u1_struct_0(X1),X2,X3),X1)
| sP1(k2_funct_2(X0,u1_struct_0(X1),X2,X3),X1)
| k1_xboole_0 = k2_funct_2(X0,u1_struct_0(X1),X2,X3)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,u1_struct_0(X1))
| ~ m1_relset_1(X2,X0,u1_struct_0(X1)) ),
inference(resolution,[],[f308,f238]) ).
fof(f645,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF31))
| sP0(X0,sK3)
| r2_hidden(sK29(sK3,X0),X0)
| sP1(X0,sK3)
| k1_xboole_0 = X0
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3) ),
inference(superposition,[],[f308,f327]) ).
fof(f648,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF31))
| sP0(X0,sK3)
| r2_hidden(sK29(sK3,X0),X0)
| sP1(X0,sK3)
| k1_xboole_0 = X0
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f645,f196]) ).
fof(f650,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF31))
| sP0(X0,sK3)
| r2_hidden(sK29(sK3,X0),X0)
| sP1(X0,sK3)
| k1_xboole_0 = X0
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f648,f195]) ).
fof(f652,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF31))
| sP0(X0,sK3)
| r2_hidden(sK29(sK3,X0),X0)
| sP1(X0,sK3)
| k1_xboole_0 = X0
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f650,f194]) ).
fof(f654,plain,
! [X0] :
( r2_hidden(sK29(sK3,X0),X0)
| sP0(X0,sK3)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF31))
| sP1(X0,sK3)
| k1_xboole_0 = X0 ),
inference(forward_subsumption_resolution,[],[f652,f193]) ).
fof(f664,plain,
( sP0(sF33,sK3)
| ~ m1_subset_1(sF33,k1_zfmisc_1(sF31))
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| sK29(sK3,sF33) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) ),
inference(resolution,[],[f654,f474]) ).
fof(f665,plain,
( sP0(sF33,sK3)
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| sK29(sK3,sF33) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ spl34_11 ),
inference(forward_subsumption_resolution,[],[f664,f387]) ).
fof(f691,definition,
( spl34_30
<=> sK29(sK3,sF33) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) ),
introduced(definition,[new_symbols(definition,[spl34_30])],[avatar_definition]) ).
fof(f693,plain,
( sK29(sK3,sF33) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ spl34_30 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f695,definition,
( spl34_31
<=> k1_xboole_0 = sF33 ),
introduced(definition,[new_symbols(definition,[spl34_31])],[avatar_definition]) ).
fof(f696,plain,
( k1_xboole_0 != sF33
| spl34_31 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f697,plain,
( k1_xboole_0 = sF33
| ~ spl34_31 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f699,definition,
( spl34_32
<=> sP1(sF33,sK3) ),
introduced(definition,[new_symbols(definition,[spl34_32])],[avatar_definition]) ).
fof(f700,plain,
( ~ sP1(sF33,sK3)
| spl34_32 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f701,plain,
( sP1(sF33,sK3)
| ~ spl34_32 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f703,definition,
( spl34_33
<=> sP0(sF33,sK3) ),
introduced(definition,[new_symbols(definition,[spl34_33])],[avatar_definition]) ).
fof(f704,plain,
( ~ sP0(sF33,sK3)
| spl34_33 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f705,plain,
( sP0(sF33,sK3)
| ~ spl34_33 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f706,plain,
( spl34_30
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_11 ),
inference(avatar_split_clause,[],[f665,f385,f703,f699,f695,f691]) ).
fof(f779,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| ~ v1_group_6(X0,sK2,X1)
| k8_funct_2(sF30,u1_struct_0(X1),X0,k3_group_1(sK2,X2)) = k3_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| ~ m1_subset_1(X2,sF30)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2) ),
inference(superposition,[],[f292,f325]) ).
fof(f785,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| ~ v1_group_6(X0,sK2,X1)
| k8_funct_2(sF30,u1_struct_0(X1),X0,k3_group_1(sK2,X2)) = k3_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| ~ m1_subset_1(X2,sF30)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2) ),
inference(forward_subsumption_resolution,[],[f779,f192]) ).
fof(f789,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| ~ v1_group_6(X0,sK2,X1)
| k8_funct_2(sF30,u1_struct_0(X1),X0,k3_group_1(sK2,X2)) = k3_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| ~ m1_subset_1(X2,sF30)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2) ),
inference(forward_subsumption_resolution,[],[f785,f191]) ).
fof(f793,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| ~ v1_group_6(X0,sK2,X1)
| k8_funct_2(sF30,u1_struct_0(X1),X0,k3_group_1(sK2,X2)) = k3_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| ~ m1_subset_1(X2,sF30)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ l1_group_1(sK2) ),
inference(forward_subsumption_resolution,[],[f789,f190]) ).
fof(f797,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| ~ v1_group_6(X0,sK2,X1)
| k8_funct_2(sF30,u1_struct_0(X1),X0,k3_group_1(sK2,X2)) = k3_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| ~ m1_subset_1(X2,sF30)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f793,f189]) ).
fof(f802,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF30)
| ~ r2_hidden(X0,sF32)
| ~ v1_xboole_0(sF33) )
| ~ spl34_10
| ~ spl34_20
| ~ spl34_24 ),
inference(resolution,[],[f624,f311]) ).
fof(f867,plain,
! [X0,X1] :
( ~ r2_hidden(X0,sF30)
| ~ r2_hidden(X0,X1)
| k1_xboole_0 = sF31
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| r2_hidden(k1_funct_1(sK4,X0),k9_relat_1(sK4,X1)) ),
inference(resolution,[],[f323,f334]) ).
fof(f868,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF30)
| ~ r2_hidden(X0,X1)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| r2_hidden(k1_funct_1(sK4,X0),k9_relat_1(sK4,X1)) )
| spl34_23 ),
inference(forward_subsumption_resolution,[],[f867,f572]) ).
fof(f869,plain,
( ! [X0,X1] :
( ~ r2_hidden(X0,sF30)
| ~ r2_hidden(X0,X1)
| ~ v1_funct_2(sK4,sF30,sF31)
| r2_hidden(k1_funct_1(sK4,X0),k9_relat_1(sK4,X1)) )
| spl34_23 ),
inference(forward_subsumption_resolution,[],[f868,f200]) ).
fof(f870,plain,
( ! [X0,X1] :
( r2_hidden(k1_funct_1(sK4,X0),k9_relat_1(sK4,X1))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,sF30) )
| spl34_23 ),
inference(forward_subsumption_resolution,[],[f869,f333]) ).
fof(f923,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| ~ v1_group_6(X0,sK2,sK3)
| k8_funct_2(sF30,sF31,X0,k3_group_1(sK2,X1)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,X0,X1))
| ~ m1_subset_1(X1,sF30)
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3) ),
inference(superposition,[],[f797,f327]) ).
fof(f926,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| ~ v1_group_6(X0,sK2,sK3)
| k8_funct_2(sF30,sF31,X0,k3_group_1(sK2,X1)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,X0,X1))
| ~ m1_subset_1(X1,sF30)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f923,f196]) ).
fof(f928,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| ~ v1_group_6(X0,sK2,sK3)
| k8_funct_2(sF30,sF31,X0,k3_group_1(sK2,X1)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,X0,X1))
| ~ m1_subset_1(X1,sF30)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f926,f195]) ).
fof(f930,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| ~ v1_group_6(X0,sK2,sK3)
| k8_funct_2(sF30,sF31,X0,k3_group_1(sK2,X1)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,X0,X1))
| ~ m1_subset_1(X1,sF30)
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f928,f194]) ).
fof(f932,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| ~ v1_group_6(X0,sK2,sK3)
| k8_funct_2(sF30,sF31,X0,k3_group_1(sK2,X1)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,X0,X1))
| ~ m1_subset_1(X1,sF30) ),
inference(forward_subsumption_resolution,[],[f930,f193]) ).
fof(f933,plain,
! [X0] :
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ v1_group_6(sK4,sK2,sK3)
| k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,X0)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X0))
| ~ m1_subset_1(X0,sF30) ),
inference(resolution,[],[f932,f334]) ).
fof(f934,plain,
! [X0] :
( ~ v1_funct_2(sK4,sF30,sF31)
| ~ v1_group_6(sK4,sK2,sK3)
| k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,X0)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X0))
| ~ m1_subset_1(X0,sF30) ),
inference(forward_subsumption_resolution,[],[f933,f200]) ).
fof(f935,plain,
! [X0] :
( ~ v1_group_6(sK4,sK2,sK3)
| k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,X0)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X0))
| ~ m1_subset_1(X0,sF30) ),
inference(forward_subsumption_resolution,[],[f934,f333]) ).
fof(f936,plain,
! [X0] :
( ~ m1_subset_1(X0,sF30)
| k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,X0)) = k3_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X0)) ),
inference(forward_subsumption_resolution,[],[f935,f198]) ).
fof(f1004,plain,
! [X0,X1] :
( m1_subset_1(k1_group_1(sK2,X0,X1),sF30)
| v3_struct_0(sK2)
| ~ l1_group_1(sK2)
| ~ m1_subset_1(X0,sF30)
| ~ m1_subset_1(X1,sF30) ),
inference(superposition,[],[f237,f325]) ).
fof(f1005,plain,
! [X0,X1] :
( m1_subset_1(k1_group_1(sK2,X0,X1),sF30)
| ~ l1_group_1(sK2)
| ~ m1_subset_1(X0,sF30)
| ~ m1_subset_1(X1,sF30) ),
inference(forward_subsumption_resolution,[],[f1004,f192]) ).
fof(f1008,plain,
! [X0,X1] :
( m1_subset_1(k1_group_1(sK2,X0,X1),sF30)
| ~ m1_subset_1(X0,sF30)
| ~ m1_subset_1(X1,sF30) ),
inference(forward_subsumption_resolution,[],[f1005,f189]) ).
fof(f1125,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK25(X0,X3,X2,sK28(k2_funct_2(X0,X1,X2,X3),X4)),X3)
| ~ sP0(k2_funct_2(X0,X1,X2,X3),X4)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(resolution,[],[f304,f288]) ).
fof(f1133,plain,
! [X0] :
( ~ sP0(sF33,X0)
| sK28(sF33,X0) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK28(sF33,X0))) ),
inference(resolution,[],[f304,f474]) ).
fof(f1141,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK25(X0,X3,X2,sK27(k2_funct_2(X0,X1,X2,X3),X4)),X3)
| ~ sP0(k2_funct_2(X0,X1,X2,X3),X4)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(resolution,[],[f305,f288]) ).
fof(f1149,plain,
! [X0] :
( ~ sP0(sF33,X0)
| sK27(sF33,X0) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK27(sF33,X0))) ),
inference(resolution,[],[f305,f474]) ).
fof(f1166,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| m1_subset_1(sK25(sF30,sF32,sK4,X0),sF30)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(superposition,[],[f286,f331]) ).
fof(f1169,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| m1_subset_1(sK25(sF30,sF32,sK4,X0),sF30)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(forward_subsumption_resolution,[],[f1166,f200]) ).
fof(f1171,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| m1_subset_1(sK25(sF30,sF32,sK4,X0),sF30)
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(forward_subsumption_resolution,[],[f1169,f333]) ).
fof(f1173,plain,
! [X0] :
( m1_subset_1(sK25(sF30,sF32,sK4,X0),sF30)
| ~ r2_hidden(X0,sF33) ),
inference(forward_subsumption_resolution,[],[f1171,f334]) ).
fof(f1217,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ m1_subset_1(X2,sF30)
| ~ m1_subset_1(X3,sF30)
| ~ v1_group_6(X0,sK2,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| k8_funct_2(sF30,u1_struct_0(X1),X0,k1_group_1(sK2,X3,X2)) = k1_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X3),k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK2)
| ~ l1_group_1(sK2) ),
inference(superposition,[],[f231,f325]) ).
fof(f1224,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ m1_subset_1(X2,sF30)
| ~ m1_subset_1(X3,sF30)
| ~ v1_group_6(X0,sK2,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| k8_funct_2(sF30,u1_struct_0(X1),X0,k1_group_1(sK2,X3,X2)) = k1_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X3),k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ l1_group_1(sK2) ),
inference(forward_subsumption_resolution,[],[f1217,f192]) ).
fof(f1230,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X0,sF30,u1_struct_0(X1))
| ~ m1_subset_1(X2,sF30)
| ~ m1_subset_1(X3,sF30)
| ~ v1_group_6(X0,sK2,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,u1_struct_0(X1))
| k8_funct_2(sF30,u1_struct_0(X1),X0,k1_group_1(sK2,X3,X2)) = k1_group_1(X1,k8_funct_2(sF30,u1_struct_0(X1),X0,X3),k8_funct_2(sF30,u1_struct_0(X1),X0,X2))
| v3_struct_0(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f1224,f189]) ).
fof(f1446,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ m1_subset_1(X1,sF30)
| ~ m1_subset_1(X2,sF30)
| ~ v1_group_6(X0,sK2,sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| k8_funct_2(sF30,sF31,X0,k1_group_1(sK2,X2,X1)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,X0,X2),k8_funct_2(sF30,sF31,X0,X1))
| v3_struct_0(sK3)
| ~ l1_group_1(sK3) ),
inference(superposition,[],[f1230,f327]) ).
fof(f1450,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ m1_subset_1(X1,sF30)
| ~ m1_subset_1(X2,sF30)
| ~ v1_group_6(X0,sK2,sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| k8_funct_2(sF30,sF31,X0,k1_group_1(sK2,X2,X1)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,X0,X2),k8_funct_2(sF30,sF31,X0,X1))
| ~ l1_group_1(sK3) ),
inference(forward_subsumption_resolution,[],[f1446,f196]) ).
fof(f1453,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF30,sF31)
| ~ m1_subset_1(X1,sF30)
| ~ m1_subset_1(X2,sF30)
| ~ v1_group_6(X0,sK2,sK3)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF30,sF31)
| k8_funct_2(sF30,sF31,X0,k1_group_1(sK2,X2,X1)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,X0,X2),k8_funct_2(sF30,sF31,X0,X1)) ),
inference(forward_subsumption_resolution,[],[f1450,f193]) ).
fof(f1455,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF30)
| ~ m1_subset_1(X1,sF30)
| ~ v1_group_6(sK4,sK2,sK3)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,X1,X0)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X1),k8_funct_2(sF30,sF31,sK4,X0)) ),
inference(resolution,[],[f1453,f334]) ).
fof(f1456,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF30)
| ~ m1_subset_1(X1,sF30)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,X1,X0)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X1),k8_funct_2(sF30,sF31,sK4,X0)) ),
inference(forward_subsumption_resolution,[],[f1455,f198]) ).
fof(f1457,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF30)
| ~ m1_subset_1(X1,sF30)
| ~ v1_funct_2(sK4,sF30,sF31)
| k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,X1,X0)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X1),k8_funct_2(sF30,sF31,sK4,X0)) ),
inference(forward_subsumption_resolution,[],[f1456,f200]) ).
fof(f1458,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF30)
| ~ m1_subset_1(X0,sF30)
| k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,X1,X0)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,sK4,X1),k8_funct_2(sF30,sF31,sK4,X0)) ),
inference(forward_subsumption_resolution,[],[f1457,f333]) ).
fof(f1752,definition,
( spl34_96
<=> v1_xboole_0(sF33) ),
introduced(definition,[new_symbols(definition,[spl34_96])],[avatar_definition]) ).
fof(f1754,plain,
( ~ v1_xboole_0(sF33)
| spl34_96 ),
inference(avatar_component_clause,[],[f1752]) ).
fof(f1756,definition,
( spl34_97
<=> ! [X0] :
( ~ r2_hidden(X0,sF30)
| ~ r2_hidden(X0,sF32) ) ),
introduced(definition,[new_symbols(definition,[spl34_97])],[avatar_definition]) ).
fof(f1757,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF32)
| ~ r2_hidden(X0,sF30) )
| ~ spl34_97 ),
inference(avatar_component_clause,[],[f1756]) ).
fof(f1758,plain,
( ~ spl34_96
| spl34_97
| ~ spl34_10
| ~ spl34_20
| ~ spl34_24 ),
inference(avatar_split_clause,[],[f802,f575,f479,f381,f1756,f1752]) ).
fof(f1845,plain,
( sF33 = u1_struct_0(sK26(sF33,sK3))
| ~ spl34_32 ),
inference(resolution,[],[f701,f301]) ).
fof(f1864,plain,
( sF33 != sF33
| ~ m1_group_2(sK26(sF33,sK3),sK3)
| ~ v1_group_1(sK26(sF33,sK3))
| ~ spl34_32 ),
inference(superposition,[],[f332,f1845]) ).
fof(f1878,plain,
( ~ m1_group_2(sK26(sF33,sK3),sK3)
| ~ v1_group_1(sK26(sF33,sK3))
| ~ spl34_32 ),
inference(trivial_inequality_removal,[],[f1864]) ).
fof(f1966,definition,
( spl34_138
<=> v1_group_1(sK26(sF33,sK3)) ),
introduced(definition,[new_symbols(definition,[spl34_138])],[avatar_definition]) ).
fof(f1968,plain,
( ~ v1_group_1(sK26(sF33,sK3))
| spl34_138 ),
inference(avatar_component_clause,[],[f1966]) ).
fof(f1970,definition,
( spl34_139
<=> m1_group_2(sK26(sF33,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl34_139])],[avatar_definition]) ).
fof(f1972,plain,
( ~ m1_group_2(sK26(sF33,sK3),sK3)
| spl34_139 ),
inference(avatar_component_clause,[],[f1970]) ).
fof(f1973,plain,
( ~ spl34_138
| ~ spl34_139
| ~ spl34_32 ),
inference(avatar_split_clause,[],[f1878,f699,f1970,f1966]) ).
fof(f2041,plain,
( ~ sP1(sF33,sK3)
| spl34_139 ),
inference(resolution,[],[f1972,f299]) ).
fof(f2042,plain,
( $false
| ~ spl34_32
| spl34_139 ),
inference(forward_subsumption_resolution,[],[f2041,f701]) ).
fof(f2043,plain,
( ~ spl34_32
| spl34_139 ),
inference(avatar_contradiction_clause,[],[f2042]) ).
fof(f2086,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF33)
| k1_funct_1(sK4,sK25(sF30,sF32,sK4,X0)) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,X0)) )
| ~ spl34_14 ),
inference(resolution,[],[f1173,f433]) ).
fof(f2087,plain,
! [X0] :
( ~ r2_hidden(X0,sF33)
| r2_hidden(sK25(sF30,sF32,sK4,X0),sF30)
| v1_xboole_0(sF30) ),
inference(resolution,[],[f1173,f290]) ).
fof(f2088,plain,
( ! [X0] :
( r2_hidden(sK25(sF30,sF32,sK4,X0),sF30)
| ~ r2_hidden(X0,sF33) )
| spl34_15 ),
inference(forward_subsumption_resolution,[],[f2087,f436]) ).
fof(f2357,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK28(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(superposition,[],[f1125,f396]) ).
fof(f2358,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK28(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f2357,f200]) ).
fof(f2366,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK28(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f2358,f333]) ).
fof(f2374,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK28(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f2366,f334]) ).
fof(f2402,plain,
( ! [X0] :
( ~ sP0(k9_relat_1(sK4,sF32),X0)
| r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(k9_relat_1(sK4,sF32),X0))) )
| ~ spl34_10
| ~ spl34_12 ),
inference(resolution,[],[f2374,f495]) ).
fof(f2416,plain,
( ! [X0] :
( ~ sP0(sF33,X0)
| r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(k9_relat_1(sK4,sF32),X0))) )
| ~ spl34_10
| ~ spl34_12 ),
inference(forward_demodulation,[],[f2402,f398]) ).
fof(f2507,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK27(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(superposition,[],[f1141,f396]) ).
fof(f2508,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK27(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f2507,f200]) ).
fof(f2516,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK27(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f2508,f333]) ).
fof(f2524,plain,
( ! [X0,X1] :
( r2_hidden(sK25(sF30,X0,sK4,sK27(k9_relat_1(sK4,X0),X1)),X0)
| ~ sP0(k9_relat_1(sK4,X0),X1) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f2516,f334]) ).
fof(f2549,plain,
( ! [X0] :
( ~ sP0(k9_relat_1(sK4,sF32),X0)
| r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(k9_relat_1(sK4,sF32),X0))) )
| ~ spl34_10
| ~ spl34_12 ),
inference(resolution,[],[f2524,f495]) ).
fof(f2561,plain,
( ! [X0] :
( ~ sP0(sF33,X0)
| r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(k9_relat_1(sK4,sF32),X0))) )
| ~ spl34_10
| ~ spl34_12 ),
inference(forward_demodulation,[],[f2549,f398]) ).
fof(f2846,plain,
! [X2,X0,X1] :
( r2_hidden(sK29(sK3,k2_funct_2(X0,sF31,X1,X2)),k2_funct_2(X0,sF31,X1,X2))
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31) ),
inference(superposition,[],[f643,f327]) ).
fof(f2854,plain,
! [X2,X0,X1] :
( r2_hidden(sK29(sK3,k2_funct_2(X0,sF31,X1,X2)),k2_funct_2(X0,sF31,X1,X2))
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31) ),
inference(forward_subsumption_resolution,[],[f2846,f196]) ).
fof(f2860,plain,
! [X2,X0,X1] :
( r2_hidden(sK29(sK3,k2_funct_2(X0,sF31,X1,X2)),k2_funct_2(X0,sF31,X1,X2))
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31) ),
inference(forward_subsumption_resolution,[],[f2854,f195]) ).
fof(f2862,plain,
! [X2,X0,X1] :
( r2_hidden(sK29(sK3,k2_funct_2(X0,sF31,X1,X2)),k2_funct_2(X0,sF31,X1,X2))
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ l1_group_1(sK3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31) ),
inference(forward_subsumption_resolution,[],[f2860,f194]) ).
fof(f2864,plain,
! [X2,X0,X1] :
( r2_hidden(sK29(sK3,k2_funct_2(X0,sF31,X1,X2)),k2_funct_2(X0,sF31,X1,X2))
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31) ),
inference(forward_subsumption_resolution,[],[f2862,f193]) ).
fof(f2868,plain,
! [X2,X0,X1] :
( sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31)
| m1_subset_1(sK25(X0,X2,X1,sK29(sK3,k2_funct_2(X0,sF31,X1,X2))),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m2_relset_1(X1,X0,sF31) ),
inference(resolution,[],[f2864,f286]) ).
fof(f2869,plain,
! [X2,X0,X1] :
( sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31)
| r2_hidden(sK25(X0,X2,X1,sK29(sK3,k2_funct_2(X0,sF31,X1,X2))),X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m2_relset_1(X1,X0,sF31) ),
inference(resolution,[],[f2864,f288]) ).
fof(f2873,plain,
( r2_hidden(sK29(sK3,sF33),sF33)
| sP0(sF33,sK3)
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31) ),
inference(superposition,[],[f2864,f331]) ).
fof(f2876,plain,
! [X2,X0,X1] :
( sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31)
| r2_hidden(sK25(X0,X2,X1,sK29(sK3,k2_funct_2(X0,sF31,X1,X2))),X2)
| ~ m2_relset_1(X1,X0,sF31) ),
inference(duplicate_literal_removal,[],[f2869]) ).
fof(f2877,plain,
! [X2,X0,X1] :
( sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| ~ m1_relset_1(X1,X0,sF31)
| m1_subset_1(sK25(X0,X2,X1,sK29(sK3,k2_funct_2(X0,sF31,X1,X2))),X0)
| ~ m2_relset_1(X1,X0,sF31) ),
inference(duplicate_literal_removal,[],[f2868]) ).
fof(f2882,plain,
! [X2,X0,X1] :
( r2_hidden(sK25(X0,X2,X1,sK29(sK3,k2_funct_2(X0,sF31,X1,X2))),X2)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| ~ m2_relset_1(X1,X0,sF31) ),
inference(forward_subsumption_resolution,[],[f2876,f283]) ).
fof(f2883,plain,
! [X2,X0,X1] :
( m1_subset_1(sK25(X0,X2,X1,sK29(sK3,k2_funct_2(X0,sF31,X1,X2))),X0)
| sP1(k2_funct_2(X0,sF31,X1,X2),sK3)
| k1_xboole_0 = k2_funct_2(X0,sF31,X1,X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,X0,sF31)
| sP0(k2_funct_2(X0,sF31,X1,X2),sK3)
| ~ m2_relset_1(X1,X0,sF31) ),
inference(forward_subsumption_resolution,[],[f2877,f283]) ).
fof(f3086,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| sP0(sF33,sK3)
| ~ m2_relset_1(sK4,sF30,sF31) ),
inference(superposition,[],[f2882,f331]) ).
fof(f3407,plain,
( ~ v1_xboole_0(k1_xboole_0)
| ~ spl34_31
| spl34_96 ),
inference(forward_demodulation,[],[f1754,f697]) ).
fof(f3442,plain,
( $false
| ~ spl34_31
| spl34_96 ),
inference(forward_subsumption_resolution,[],[f3407,f259]) ).
fof(f3443,plain,
( ~ spl34_31
| spl34_96 ),
inference(avatar_contradiction_clause,[],[f3442]) ).
fof(f3458,plain,
( ! [X0] :
( r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(sF33,X0)))
| ~ sP0(sF33,X0) )
| ~ spl34_10
| ~ spl34_12 ),
inference(forward_demodulation,[],[f2416,f398]) ).
fof(f3461,plain,
( ! [X0] :
( r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(sF33,X0)))
| ~ sP0(sF33,X0) )
| ~ spl34_10
| ~ spl34_12 ),
inference(forward_demodulation,[],[f2561,f398]) ).
fof(f3475,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| k1_xboole_0 = sF33
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| sP0(sF33,sK3)
| ~ m2_relset_1(sK4,sF30,sF31)
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f3086,f700]) ).
fof(f3496,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| sP0(sF33,sK3)
| ~ m2_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f3475,f696]) ).
fof(f3506,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| ~ v1_funct_2(sK4,sF30,sF31)
| sP0(sF33,sK3)
| ~ m2_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f3496,f200]) ).
fof(f3514,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| sP0(sF33,sK3)
| ~ m2_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f3506,f333]) ).
fof(f3573,definition,
( spl34_220
<=> r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32) ),
introduced(definition,[new_symbols(definition,[spl34_220])],[avatar_definition]) ).
fof(f3574,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| ~ spl34_220 ),
inference(avatar_component_clause,[],[f3573]) ).
fof(f3577,definition,
( spl34_221
<=> r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30) ),
introduced(definition,[new_symbols(definition,[spl34_221])],[avatar_definition]) ).
fof(f3578,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| ~ spl34_221 ),
inference(avatar_component_clause,[],[f3577]) ).
fof(f3579,plain,
( ~ r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| spl34_221 ),
inference(avatar_component_clause,[],[f3577]) ).
fof(f3581,definition,
( spl34_222
<=> r2_hidden(sK29(sK3,sF33),sF33) ),
introduced(definition,[new_symbols(definition,[spl34_222])],[avatar_definition]) ).
fof(f3582,plain,
( ~ r2_hidden(sK29(sK3,sF33),sF33)
| spl34_222 ),
inference(avatar_component_clause,[],[f3581]) ).
fof(f3691,definition,
( spl34_231
<=> r2_hidden(sK28(sF33,sK3),sF33) ),
introduced(definition,[new_symbols(definition,[spl34_231])],[avatar_definition]) ).
fof(f3692,plain,
( ~ r2_hidden(sK28(sF33,sK3),sF33)
| spl34_231 ),
inference(avatar_component_clause,[],[f3691]) ).
fof(f3693,plain,
( r2_hidden(sK28(sF33,sK3),sF33)
| ~ spl34_231 ),
inference(avatar_component_clause,[],[f3691]) ).
fof(f3725,definition,
( spl34_236
<=> r2_hidden(sK27(sF33,sK3),sF33) ),
introduced(definition,[new_symbols(definition,[spl34_236])],[avatar_definition]) ).
fof(f3726,plain,
( ~ r2_hidden(sK27(sF33,sK3),sF33)
| spl34_236 ),
inference(avatar_component_clause,[],[f3725]) ).
fof(f3727,plain,
( r2_hidden(sK27(sF33,sK3),sF33)
| ~ spl34_236 ),
inference(avatar_component_clause,[],[f3725]) ).
fof(f4026,definition,
( spl34_296
<=> r2_hidden(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30) ),
introduced(definition,[new_symbols(definition,[spl34_296])],[avatar_definition]) ).
fof(f4027,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30)
| ~ spl34_296 ),
inference(avatar_component_clause,[],[f4026]) ).
fof(f4028,plain,
( ~ r2_hidden(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30)
| spl34_296 ),
inference(avatar_component_clause,[],[f4026]) ).
fof(f4073,definition,
( spl34_300
<=> r2_hidden(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sF30) ),
introduced(definition,[new_symbols(definition,[spl34_300])],[avatar_definition]) ).
fof(f4074,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sF30)
| ~ spl34_300 ),
inference(avatar_component_clause,[],[f4073]) ).
fof(f4075,plain,
( ~ r2_hidden(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sF30)
| spl34_300 ),
inference(avatar_component_clause,[],[f4073]) ).
fof(f4091,plain,
( ~ sP0(sF33,sK3)
| spl34_231 ),
inference(resolution,[],[f3692,f304]) ).
fof(f4092,plain,
( $false
| ~ spl34_33
| spl34_231 ),
inference(forward_subsumption_resolution,[],[f4091,f705]) ).
fof(f4093,plain,
( ~ spl34_33
| spl34_231 ),
inference(avatar_contradiction_clause,[],[f4092]) ).
fof(f4097,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| ~ m2_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f3514,f704]) ).
fof(f4098,plain,
( sP0(sF33,sK3)
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31)
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f2873,f3582]) ).
fof(f4104,plain,
( r2_hidden(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF32)
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f4097,f334]) ).
fof(f4105,plain,
( sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31)
| spl34_33
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f4098,f704]) ).
fof(f4108,plain,
( spl34_220
| spl34_31
| spl34_32
| spl34_33 ),
inference(avatar_split_clause,[],[f4104,f703,f699,f695,f3573]) ).
fof(f4109,plain,
( k1_xboole_0 = sF33
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31)
| spl34_32
| spl34_33
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f4105,f700]) ).
fof(f4112,plain,
( ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32
| spl34_33
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f4109,f696]) ).
fof(f4117,plain,
( ~ v1_funct_2(sK4,sF30,sF31)
| ~ m1_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32
| spl34_33
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f4112,f200]) ).
fof(f4118,plain,
( ~ m1_relset_1(sK4,sF30,sF31)
| spl34_31
| spl34_32
| spl34_33
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f4117,f333]) ).
fof(f4119,plain,
( $false
| ~ spl34_10
| spl34_31
| spl34_32
| spl34_33
| spl34_222 ),
inference(forward_subsumption_resolution,[],[f4118,f382]) ).
fof(f4120,plain,
( ~ spl34_10
| spl34_31
| spl34_32
| spl34_33
| spl34_222 ),
inference(avatar_contradiction_clause,[],[f4119]) ).
fof(f4229,plain,
( ~ r2_hidden(sK28(sF33,sK3),sF33)
| spl34_15
| spl34_296 ),
inference(resolution,[],[f2088,f4028]) ).
fof(f4231,plain,
( ~ r2_hidden(sK27(sF33,sK3),sF33)
| spl34_15
| spl34_300 ),
inference(resolution,[],[f2088,f4075]) ).
fof(f4232,plain,
( ~ r2_hidden(sK29(sK3,sF33),sF33)
| spl34_15
| spl34_221 ),
inference(resolution,[],[f2088,f3579]) ).
fof(f4697,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| sP0(sF33,sK3)
| ~ m1_subset_1(sF33,k1_zfmisc_1(sF31))
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ spl34_14 ),
inference(resolution,[],[f2086,f654]) ).
fof(f4973,plain,
( ! [X0] :
( m1_subset_1(sK25(sF30,X0,sK4,sK29(sK3,k9_relat_1(sK4,X0))),sF30)
| sP1(k9_relat_1(sK4,X0),sK3)
| k1_xboole_0 = k9_relat_1(sK4,X0)
| ~ v1_funct_1(sK4)
| ~ v1_funct_2(sK4,sF30,sF31)
| sP0(k9_relat_1(sK4,X0),sK3)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(superposition,[],[f2883,f396]) ).
fof(f4974,plain,
( ! [X0] :
( m1_subset_1(sK25(sF30,X0,sK4,sK29(sK3,k9_relat_1(sK4,X0))),sF30)
| sP1(k9_relat_1(sK4,X0),sK3)
| k1_xboole_0 = k9_relat_1(sK4,X0)
| ~ v1_funct_2(sK4,sF30,sF31)
| sP0(k9_relat_1(sK4,X0),sK3)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f4973,f200]) ).
fof(f4975,plain,
( ! [X0] :
( m1_subset_1(sK25(sF30,X0,sK4,sK29(sK3,k9_relat_1(sK4,X0))),sF30)
| sP1(k9_relat_1(sK4,X0),sK3)
| k1_xboole_0 = k9_relat_1(sK4,X0)
| sP0(k9_relat_1(sK4,X0),sK3)
| ~ m2_relset_1(sK4,sF30,sF31) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f4974,f333]) ).
fof(f4976,plain,
( ! [X0] :
( m1_subset_1(sK25(sF30,X0,sK4,sK29(sK3,k9_relat_1(sK4,X0))),sF30)
| sP1(k9_relat_1(sK4,X0),sK3)
| k1_xboole_0 = k9_relat_1(sK4,X0)
| sP0(k9_relat_1(sK4,X0),sK3) )
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f4975,f334]) ).
fof(f4983,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| sP0(sF33,sK3)
| ~ spl34_10 ),
inference(superposition,[],[f4976,f398]) ).
fof(f6321,plain,
( ~ spl34_236
| spl34_15
| spl34_300 ),
inference(avatar_split_clause,[],[f4231,f4073,f435,f3725]) ).
fof(f6403,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ m1_subset_1(sF33,k1_zfmisc_1(sF31))
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ spl34_14
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f4697,f704]) ).
fof(f6405,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| k1_xboole_0 = sF33
| sP0(sF33,sK3)
| ~ spl34_10
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f4983,f700]) ).
fof(f6409,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| sP1(sF33,sK3)
| k1_xboole_0 = sF33
| ~ spl34_11
| ~ spl34_14
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f6403,f387]) ).
fof(f6411,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| sP0(sF33,sK3)
| ~ spl34_10
| spl34_31
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f6405,f696]) ).
fof(f6415,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| k1_xboole_0 = sF33
| ~ spl34_11
| ~ spl34_14
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f6409,f700]) ).
fof(f6417,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| ~ spl34_10
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f6411,f704]) ).
fof(f6421,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ spl34_11
| ~ spl34_14
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f6415,f696]) ).
fof(f6425,plain,
( sK29(sK3,sF33) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ spl34_11
| ~ spl34_14
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_demodulation,[],[f6421,f693]) ).
fof(f6433,plain,
( ~ sP1(sF33,sK3)
| spl34_138 ),
inference(resolution,[],[f1968,f300]) ).
fof(f6468,plain,
( ~ sP0(sF33,sK3)
| spl34_236 ),
inference(resolution,[],[f3726,f305]) ).
fof(f6471,plain,
( r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ spl34_12
| ~ spl34_220 ),
inference(resolution,[],[f3574,f495]) ).
fof(f6556,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| ~ spl34_221 ),
inference(resolution,[],[f3578,f289]) ).
fof(f6613,plain,
( k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))) = k1_funct_1(sK4,k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))))
| ~ spl34_10
| ~ spl34_14
| spl34_31
| spl34_32
| spl34_33 ),
inference(resolution,[],[f6417,f500]) ).
fof(f6615,plain,
( k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))) = k3_group_1(sK3,k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK29(sK3,sF33))))
| ~ spl34_10
| spl34_31
| spl34_32
| spl34_33 ),
inference(resolution,[],[f6417,f936]) ).
fof(f6619,plain,
( k8_funct_2(sF30,sF31,sK4,k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))) = k3_group_1(sK3,sK29(sK3,sF33))
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_demodulation,[],[f6615,f6425]) ).
fof(f6622,plain,
( k1_funct_1(sK4,k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))) = k3_group_1(sK3,sK29(sK3,sF33))
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_demodulation,[],[f6619,f6613]) ).
fof(f6711,plain,
( ! [X0] :
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,X0))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),k1_relat_1(sK4))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),X0)
| ~ v1_relat_1(sK4)
| ~ v1_funct_1(sK4) )
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(superposition,[],[f314,f6622]) ).
fof(f6712,plain,
( ! [X0] :
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,X0))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),k1_relat_1(sK4))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),X0)
| ~ v1_funct_1(sK4) )
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_20
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f6711,f480]) ).
fof(f6720,definition,
( spl34_400
<=> r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),sF30) ),
introduced(definition,[new_symbols(definition,[spl34_400])],[avatar_definition]) ).
fof(f6722,plain,
( ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),sF30)
| spl34_400 ),
inference(avatar_component_clause,[],[f6720]) ).
fof(f6724,definition,
( spl34_401
<=> r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),sF33) ),
introduced(definition,[new_symbols(definition,[spl34_401])],[avatar_definition]) ).
fof(f6726,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),sF33)
| ~ spl34_401 ),
inference(avatar_component_clause,[],[f6724]) ).
fof(f6729,definition,
( spl34_402
<=> ! [X0] :
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,X0))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_402])],[avatar_definition]) ).
fof(f6730,plain,
( ! [X0] :
( ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),X0)
| r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,X0)) )
| ~ spl34_402 ),
inference(avatar_component_clause,[],[f6729]) ).
fof(f6736,plain,
( ! [X0] :
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,X0))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),k1_relat_1(sK4))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),X0) )
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_20
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_subsumption_resolution,[],[f6712,f200]) ).
fof(f6739,plain,
( ! [X0] :
( ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),sF30)
| r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,X0))
| ~ r2_hidden(k3_group_1(sK2,sK25(sF30,sF32,sK4,sK29(sK3,sF33))),X0) )
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_20
| ~ spl34_24
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(forward_demodulation,[],[f6736,f577]) ).
fof(f6742,plain,
( spl34_402
| ~ spl34_400
| ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_20
| ~ spl34_24
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(avatar_split_clause,[],[f6739,f703,f699,f695,f691,f575,f479,f432,f385,f381,f6720,f6729]) ).
fof(f6773,plain,
( ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| spl34_15
| spl34_400 ),
inference(resolution,[],[f6722,f526]) ).
fof(f6775,plain,
( $false
| ~ spl34_10
| spl34_15
| spl34_31
| spl34_32
| spl34_33
| spl34_400 ),
inference(forward_subsumption_resolution,[],[f6773,f6417]) ).
fof(f6776,plain,
( ~ spl34_10
| spl34_15
| spl34_31
| spl34_32
| spl34_33
| spl34_400 ),
inference(avatar_contradiction_clause,[],[f6775]) ).
fof(f6779,plain,
( $false
| spl34_15
| ~ spl34_231
| spl34_296 ),
inference(forward_subsumption_resolution,[],[f4229,f3693]) ).
fof(f6780,plain,
( spl34_15
| ~ spl34_231
| spl34_296 ),
inference(avatar_contradiction_clause,[],[f6779]) ).
fof(f6782,plain,
( $false
| ~ spl34_33
| spl34_236 ),
inference(forward_subsumption_resolution,[],[f6468,f705]) ).
fof(f6783,plain,
( ~ spl34_33
| spl34_236 ),
inference(avatar_contradiction_clause,[],[f6782]) ).
fof(f6788,plain,
( ~ spl34_222
| spl34_15
| spl34_221 ),
inference(avatar_split_clause,[],[f4232,f3577,f435,f3581]) ).
fof(f6958,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30)
| ~ spl34_296 ),
inference(resolution,[],[f4027,f289]) ).
fof(f6981,plain,
( m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sF30)
| ~ spl34_300 ),
inference(resolution,[],[f4074,f289]) ).
fof(f7237,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK29(sK3,sF33)))
| ~ m1_group_2(sK5,sK2)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_402 ),
inference(resolution,[],[f6730,f496]) ).
fof(f7244,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ m1_group_2(sK5,sK2)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7237,f6471]) ).
fof(f7246,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7244,f201]) ).
fof(f7248,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7246,f192]) ).
fof(f7250,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7248,f191]) ).
fof(f7252,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| ~ l1_group_1(sK2)
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7250,f190]) ).
fof(f7254,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7252,f189]) ).
fof(f7268,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),sF33)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),u1_struct_0(sK2))
| ~ spl34_10
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_demodulation,[],[f7254,f398]) ).
fof(f7269,plain,
( ~ m1_subset_1(sK25(sF30,sF32,sK4,sK29(sK3,sF33)),sF30)
| r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),sF33)
| ~ spl34_10
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_402 ),
inference(forward_demodulation,[],[f7268,f325]) ).
fof(f7270,plain,
( r2_hidden(k3_group_1(sK3,sK29(sK3,sF33)),sF33)
| ~ spl34_10
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_221
| ~ spl34_402 ),
inference(forward_subsumption_resolution,[],[f7269,f6556]) ).
fof(f7271,plain,
( spl34_401
| ~ spl34_10
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_221
| ~ spl34_402 ),
inference(avatar_split_clause,[],[f7270,f6729,f3577,f3573,f413,f409,f381,f6724]) ).
fof(f7272,plain,
( sP0(sF33,sK3)
| k1_xboole_0 = sF33
| sP1(sF33,sK3)
| ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| ~ spl34_401 ),
inference(resolution,[],[f6726,f309]) ).
fof(f7282,plain,
( k1_xboole_0 = sF33
| sP1(sF33,sK3)
| ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7272,f704]) ).
fof(f7283,plain,
( sP1(sF33,sK3)
| ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| spl34_31
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7282,f696]) ).
fof(f7284,plain,
( ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| v3_struct_0(sK3)
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7283,f700]) ).
fof(f7285,plain,
( ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v3_group_1(sK3)
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7284,f196]) ).
fof(f7286,plain,
( ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ v4_group_1(sK3)
| ~ l1_group_1(sK3)
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7285,f195]) ).
fof(f7287,plain,
( ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| ~ l1_group_1(sK3)
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7286,f194]) ).
fof(f7288,plain,
( ~ m1_subset_1(sF33,k1_zfmisc_1(u1_struct_0(sK3)))
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7287,f193]) ).
fof(f7289,plain,
( ~ m1_subset_1(sF33,k1_zfmisc_1(sF31))
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_demodulation,[],[f7288,f327]) ).
fof(f7290,plain,
( $false
| ~ spl34_11
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(forward_subsumption_resolution,[],[f7289,f387]) ).
fof(f7291,plain,
( ~ spl34_11
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(avatar_contradiction_clause,[],[f7290]) ).
fof(f7498,plain,
( ! [X0] :
( ~ r2_hidden(k2_group_1(X0),sF30)
| ~ m1_group_2(sK5,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl34_13
| ~ spl34_97 ),
inference(resolution,[],[f1757,f497]) ).
fof(f10199,plain,
( ~ m1_group_2(sK5,sK2)
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(resolution,[],[f7498,f605]) ).
fof(f10202,plain,
( v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f10199,f201]) ).
fof(f10203,plain,
( ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f10202,f192]) ).
fof(f10204,plain,
( ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f10203,f191]) ).
fof(f10205,plain,
( ~ l1_group_1(sK2)
| ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f10204,f190]) ).
fof(f10206,plain,
( $false
| ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f10205,f189]) ).
fof(f10207,plain,
( ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(avatar_contradiction_clause,[],[f10206]) ).
fof(f10222,plain,
( $false
| ~ spl34_32
| spl34_138 ),
inference(forward_subsumption_resolution,[],[f6433,f701]) ).
fof(f10223,plain,
( ~ spl34_32
| spl34_138 ),
inference(avatar_contradiction_clause,[],[f10222]) ).
fof(f10516,plain,
( sK27(sF33,sK3) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK27(sF33,sK3)))
| ~ spl34_33 ),
inference(resolution,[],[f705,f1149]) ).
fof(f10517,plain,
( sK28(sF33,sK3) = k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| ~ spl34_33 ),
inference(resolution,[],[f705,f1133]) ).
fof(f10521,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK28(sF33,sK3))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| ~ spl34_14
| ~ spl34_231 ),
inference(resolution,[],[f3693,f2086]) ).
fof(f10528,plain,
( sK28(sF33,sK3) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| ~ spl34_14
| ~ spl34_33
| ~ spl34_231 ),
inference(forward_demodulation,[],[f10521,f10517]) ).
fof(f10529,plain,
( k1_funct_1(sK4,sK25(sF30,sF32,sK4,sK27(sF33,sK3))) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK27(sF33,sK3)))
| ~ spl34_14
| ~ spl34_236 ),
inference(resolution,[],[f3727,f2086]) ).
fof(f10536,plain,
( sK27(sF33,sK3) = k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK27(sF33,sK3)))
| ~ spl34_14
| ~ spl34_33
| ~ spl34_236 ),
inference(forward_demodulation,[],[f10529,f10516]) ).
fof(f13291,definition,
( spl34_699
<=> r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(sF33,sK3))) ),
introduced(definition,[new_symbols(definition,[spl34_699])],[avatar_definition]) ).
fof(f13292,plain,
( r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| ~ spl34_699 ),
inference(avatar_component_clause,[],[f13291]) ).
fof(f13293,plain,
( ~ r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| spl34_699 ),
inference(avatar_component_clause,[],[f13291]) ).
fof(f13295,plain,
( ~ sP0(sF33,sK3)
| ~ spl34_10
| ~ spl34_12
| spl34_699 ),
inference(resolution,[],[f13293,f3458]) ).
fof(f13299,plain,
( $false
| ~ spl34_10
| ~ spl34_12
| ~ spl34_33
| spl34_699 ),
inference(forward_subsumption_resolution,[],[f13295,f705]) ).
fof(f13300,plain,
( ~ spl34_10
| ~ spl34_12
| ~ spl34_33
| spl34_699 ),
inference(avatar_contradiction_clause,[],[f13299]) ).
fof(f13667,definition,
( spl34_721
<=> r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(sF33,sK3))) ),
introduced(definition,[new_symbols(definition,[spl34_721])],[avatar_definition]) ).
fof(f13668,plain,
( r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(sF33,sK3)))
| ~ spl34_721 ),
inference(avatar_component_clause,[],[f13667]) ).
fof(f13669,plain,
( ~ r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(sF33,sK3)))
| spl34_721 ),
inference(avatar_component_clause,[],[f13667]) ).
fof(f13671,plain,
( ~ sP0(sF33,sK3)
| ~ spl34_10
| ~ spl34_12
| spl34_721 ),
inference(resolution,[],[f13669,f3461]) ).
fof(f13675,plain,
( $false
| ~ spl34_10
| ~ spl34_12
| ~ spl34_33
| spl34_721 ),
inference(forward_subsumption_resolution,[],[f13671,f705]) ).
fof(f13676,plain,
( ~ spl34_10
| ~ spl34_12
| ~ spl34_33
| spl34_721 ),
inference(avatar_contradiction_clause,[],[f13675]) ).
fof(f18627,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF30)
| k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),X0)) = k1_group_1(sK3,k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK27(sF33,sK3))),k8_funct_2(sF30,sF31,sK4,X0)) )
| ~ spl34_300 ),
inference(resolution,[],[f6981,f1458]) ).
fof(f18642,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF30)
| k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),X0)) = k1_group_1(sK3,sK27(sF33,sK3),k8_funct_2(sF30,sF31,sK4,X0)) )
| ~ spl34_14
| ~ spl34_33
| ~ spl34_236
| ~ spl34_300 ),
inference(forward_demodulation,[],[f18627,f10536]) ).
fof(f18669,plain,
( k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3)))) = k1_group_1(sK3,sK27(sF33,sK3),k8_funct_2(sF30,sF31,sK4,sK25(sF30,sF32,sK4,sK28(sF33,sK3))))
| ~ spl34_14
| ~ spl34_33
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300 ),
inference(resolution,[],[f18642,f6958]) ).
fof(f18685,plain,
( k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3)))) = k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3))
| ~ spl34_14
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300 ),
inference(forward_demodulation,[],[f18669,f10528]) ).
fof(f18713,definition,
( spl34_951
<=> m1_subset_1(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),sF30) ),
introduced(definition,[new_symbols(definition,[spl34_951])],[avatar_definition]) ).
fof(f18714,plain,
( m1_subset_1(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),sF30)
| ~ spl34_951 ),
inference(avatar_component_clause,[],[f18713]) ).
fof(f18715,plain,
( ~ m1_subset_1(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),sF30)
| spl34_951 ),
inference(avatar_component_clause,[],[f18713]) ).
fof(f18727,plain,
( ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sF30)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30)
| spl34_951 ),
inference(resolution,[],[f18715,f1008]) ).
fof(f18728,plain,
( ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30)
| ~ spl34_300
| spl34_951 ),
inference(forward_subsumption_resolution,[],[f18727,f6981]) ).
fof(f18729,plain,
( $false
| ~ spl34_296
| ~ spl34_300
| spl34_951 ),
inference(forward_subsumption_resolution,[],[f18728,f6958]) ).
fof(f18730,plain,
( ~ spl34_296
| ~ spl34_300
| spl34_951 ),
inference(avatar_contradiction_clause,[],[f18729]) ).
fof(f29003,plain,
( k8_funct_2(sF30,sF31,sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3)))) = k1_funct_1(sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))))
| ~ spl34_14
| ~ spl34_951 ),
inference(resolution,[],[f18714,f433]) ).
fof(f29022,plain,
( r2_hidden(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),sF30)
| v1_xboole_0(sF30)
| ~ spl34_951 ),
inference(resolution,[],[f18714,f290]) ).
fof(f29023,plain,
( r2_hidden(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),sF30)
| spl34_15
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29022,f436]) ).
fof(f29036,plain,
( k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)) = k1_funct_1(sK4,k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))))
| ~ spl34_14
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_951 ),
inference(forward_demodulation,[],[f29003,f18685]) ).
fof(f29040,plain,
( ! [X0] :
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,X0))
| ~ r2_hidden(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),X0)
| ~ r2_hidden(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),sF30) )
| ~ spl34_14
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_951 ),
inference(superposition,[],[f870,f29036]) ).
fof(f29049,plain,
( ! [X0] :
( ~ r2_hidden(k1_group_1(sK2,sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sK25(sF30,sF32,sK4,sK28(sF33,sK3))),X0)
| r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,X0)) )
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29040,f29023]) ).
fof(f29060,definition,
( spl34_1639
<=> r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33) ),
introduced(definition,[new_symbols(definition,[spl34_1639])],[avatar_definition]) ).
fof(f29062,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33)
| ~ spl34_1639 ),
inference(avatar_component_clause,[],[f29060]) ).
fof(f29075,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK27(sF33,sK3)))
| ~ r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| ~ m1_group_2(sK5,sK2)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_951 ),
inference(resolution,[],[f29049,f498]) ).
fof(f29088,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ r1_rlvect_1(sK5,sK25(sF30,sF32,sK4,sK28(sF33,sK3)))
| ~ m1_group_2(sK5,sK2)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29075,f13668]) ).
fof(f29091,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ m1_group_2(sK5,sK2)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29088,f13292]) ).
fof(f29094,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29091,f201]) ).
fof(f29096,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ v3_group_1(sK2)
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29094,f192]) ).
fof(f29097,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ v4_group_1(sK2)
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29096,f191]) ).
fof(f29098,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ l1_group_1(sK2)
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29097,f190]) ).
fof(f29099,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),k9_relat_1(sK4,sF32))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29098,f189]) ).
fof(f29100,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),u1_struct_0(sK2))
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_demodulation,[],[f29099,f398]) ).
fof(f29101,plain,
( ~ m1_subset_1(sK25(sF30,sF32,sK4,sK28(sF33,sK3)),sF30)
| r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_demodulation,[],[f29100,f325]) ).
fof(f29102,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33)
| ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),u1_struct_0(sK2))
| ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29101,f6958]) ).
fof(f29103,plain,
( ~ m1_subset_1(sK25(sF30,sF32,sK4,sK27(sF33,sK3)),sF30)
| r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33)
| ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_demodulation,[],[f29102,f325]) ).
fof(f29104,plain,
( r2_hidden(k1_group_1(sK3,sK27(sF33,sK3),sK28(sF33,sK3)),sF33)
| ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(forward_subsumption_resolution,[],[f29103,f6981]) ).
fof(f29105,plain,
( spl34_1639
| ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951 ),
inference(avatar_split_clause,[],[f29104,f18713,f13667,f13291,f4073,f4026,f3725,f3691,f703,f571,f435,f432,f413,f381,f29060]) ).
fof(f29106,plain,
( ~ sP0(sF33,sK3)
| ~ spl34_1639 ),
inference(resolution,[],[f29062,f306]) ).
fof(f29145,plain,
( $false
| ~ spl34_33
| ~ spl34_1639 ),
inference(forward_subsumption_resolution,[],[f29106,f705]) ).
fof(f29146,plain,
( ~ spl34_33
| ~ spl34_1639 ),
inference(avatar_contradiction_clause,[],[f29145]) ).
cnf(s4,plain,
( ~ spl34_10
| spl34_11 ),
inference(sat_conversion,[],[f388]) ).
cnf(s5,plain,
spl34_10,
inference(sat_conversion,[],[f393]) ).
cnf(s6,plain,
( ~ spl34_12
| spl34_13 ),
inference(sat_conversion,[],[f415]) ).
cnf(s7,plain,
( ~ spl34_10
| spl34_14
| spl34_15 ),
inference(sat_conversion,[],[f438]) ).
cnf(s10,plain,
spl34_16,
inference(sat_conversion,[],[f491]) ).
cnf(s11,plain,
( spl34_12
| ~ spl34_16 ),
inference(sat_conversion,[],[f494]) ).
cnf(s13,plain,
~ spl34_15,
inference(sat_conversion,[],[f517]) ).
cnf(s14,plain,
spl34_20,
inference(sat_conversion,[],[f538]) ).
cnf(s16,plain,
( ~ spl34_10
| spl34_23
| spl34_24 ),
inference(sat_conversion,[],[f578]) ).
cnf(s17,plain,
~ spl34_23,
inference(sat_conversion,[],[f591]) ).
cnf(s19,plain,
( ~ spl34_11
| spl34_30
| spl34_31
| spl34_32
| spl34_33 ),
inference(sat_conversion,[],[f706]) ).
cnf(s58,plain,
( ~ spl34_10
| ~ spl34_20
| ~ spl34_24
| ~ spl34_96
| spl34_97 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s79,plain,
( ~ spl34_32
| ~ spl34_138
| ~ spl34_139 ),
inference(sat_conversion,[],[f1973]) ).
cnf(s97,plain,
( ~ spl34_32
| spl34_139 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s153,plain,
( ~ spl34_31
| spl34_96 ),
inference(sat_conversion,[],[f3443]) ).
cnf(s230,plain,
( ~ spl34_33
| spl34_231 ),
inference(sat_conversion,[],[f4093]) ).
cnf(s232,plain,
( spl34_31
| spl34_32
| spl34_33
| spl34_220 ),
inference(sat_conversion,[],[f4108]) ).
cnf(s235,plain,
( ~ spl34_10
| spl34_31
| spl34_32
| spl34_33
| spl34_222 ),
inference(sat_conversion,[],[f4120]) ).
cnf(s277,plain,
( spl34_15
| ~ spl34_236
| spl34_300 ),
inference(sat_conversion,[],[f6321]) ).
cnf(s301,plain,
( ~ spl34_10
| ~ spl34_11
| ~ spl34_14
| ~ spl34_20
| ~ spl34_24
| ~ spl34_30
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_400
| spl34_402 ),
inference(sat_conversion,[],[f6742]) ).
cnf(s304,plain,
( ~ spl34_10
| spl34_15
| spl34_31
| spl34_32
| spl34_33
| spl34_400 ),
inference(sat_conversion,[],[f6776]) ).
cnf(s306,plain,
( spl34_15
| ~ spl34_231
| spl34_296 ),
inference(sat_conversion,[],[f6780]) ).
cnf(s307,plain,
( ~ spl34_33
| spl34_236 ),
inference(sat_conversion,[],[f6783]) ).
cnf(s310,plain,
( spl34_15
| spl34_221
| ~ spl34_222 ),
inference(sat_conversion,[],[f6788]) ).
cnf(s338,plain,
( ~ spl34_10
| ~ spl34_12
| ~ spl34_13
| ~ spl34_220
| ~ spl34_221
| spl34_401
| ~ spl34_402 ),
inference(sat_conversion,[],[f7271]) ).
cnf(s339,plain,
( ~ spl34_11
| spl34_31
| spl34_32
| spl34_33
| ~ spl34_401 ),
inference(sat_conversion,[],[f7291]) ).
cnf(s411,plain,
( ~ spl34_13
| spl34_15
| ~ spl34_97 ),
inference(sat_conversion,[],[f10207]) ).
cnf(s414,plain,
( ~ spl34_32
| spl34_138 ),
inference(sat_conversion,[],[f10223]) ).
cnf(s661,plain,
( ~ spl34_10
| ~ spl34_12
| ~ spl34_33
| spl34_699 ),
inference(sat_conversion,[],[f13300]) ).
cnf(s697,plain,
( ~ spl34_10
| ~ spl34_12
| ~ spl34_33
| spl34_721 ),
inference(sat_conversion,[],[f13676]) ).
cnf(s955,plain,
( ~ spl34_296
| ~ spl34_300
| spl34_951 ),
inference(sat_conversion,[],[f18730]) ).
cnf(s1657,plain,
( ~ spl34_10
| ~ spl34_13
| ~ spl34_14
| spl34_15
| spl34_23
| ~ spl34_33
| ~ spl34_231
| ~ spl34_236
| ~ spl34_296
| ~ spl34_300
| ~ spl34_699
| ~ spl34_721
| ~ spl34_951
| spl34_1639 ),
inference(sat_conversion,[],[f29105]) ).
cnf(s1663,plain,
( ~ spl34_33
| ~ spl34_1639 ),
inference(sat_conversion,[],[f29146]) ).
cnf(s1681,plain,
( ~ spl34_10
| spl34_24 ),
inference(rat,[],[s16,s17]) ).
cnf(s1690,plain,
spl34_12,
inference(rat,[],[s11,s10]) ).
cnf(s1700,plain,
( ~ spl34_10
| spl34_14 ),
inference(rat,[],[s7,s13]) ).
cnf(s1701,plain,
spl34_13,
inference(rat,[],[s6,s1690]) ).
cnf(s1702,plain,
~ spl34_97,
inference(rat,[],[s411,s13,s1701]) ).
cnf(s1706,plain,
spl34_24,
inference(rat,[],[s1681,s5]) ).
cnf(s1708,plain,
spl34_14,
inference(rat,[],[s1700,s5]) ).
cnf(s1711,plain,
~ spl34_96,
inference(rat,[],[s58,s1702,s5,s14,s1706]) ).
cnf(s1719,plain,
~ spl34_31,
inference(rat,[],[s153,s1711]) ).
cnf(s1741,plain,
spl34_11,
inference(rat,[],[s4,s5]) ).
cnf(s1742,plain,
~ spl34_33,
inference(rat,[],[s1657,s955,s306,s277,s661,s697,s230,s307,s1663,s1701,s13,s17,s5,s1708,s1690]) ).
cnf(s1743,plain,
~ spl34_32,
inference(rat,[],[s79,s97,s414]) ).
cnf(s1744,plain,
spl34_30,
inference(rat,[],[s19,s1742,s1741,s1719,s1743]) ).
cnf(s1745,plain,
spl34_222,
inference(rat,[],[s235,s1742,s1719,s5,s1743]) ).
cnf(s1746,plain,
spl34_220,
inference(rat,[],[s232,s1742,s1719,s1743]) ).
cnf(s1747,plain,
spl34_400,
inference(rat,[],[s304,s1742,s1719,s5,s13,s1743]) ).
cnf(s1748,plain,
~ spl34_401,
inference(rat,[],[s339,s1742,s1741,s1719,s1743]) ).
cnf(s1752,plain,
spl34_221,
inference(rat,[],[s310,s13,s1745]) ).
cnf(s1758,plain,
spl34_402,
inference(rat,[],[s301,s1744,s1743,s1742,s1741,s1719,s1708,s1706,s14,s5,s1747]) ).
cnf(s1761,plain,
$false,
inference(rat,[],[s338,s1746,s1748,s5,s1701,s1690,s1758,s1752]) ).
fof(f29148,plain,
$false,
inference(avatar_sat_refutation,[],[s1761]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP635+1 : 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.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:20:35 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 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
% 12.02/2.63 % (3173487)Detected formulas, will run a generic FOF schedule.
% 12.02/2.63 % (3173496)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1301589183:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.02/2.63 % (3173496)Instruction limit reached!
% 12.02/2.63 % (3173496)------------------------------
% 12.02/2.63 % (3173496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.63 % (3173496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.63 % (3173496)CaDiCaL version: 2.1.3
% 12.02/2.63 % (3173496)Termination reason: Instruction limit
% 12.02/2.63 % (3173496)Termination phase: Saturation
% 12.02/2.63 % (3173496)Time elapsed: 0.039 s
% 12.02/2.63 % (3173496)Peak memory usage: 89 MB
% 12.02/2.63 % (3173496)Instructions burned: 120 (million)
% 12.02/2.63 % (3173497)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1051436731:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.02/2.63 % (3173495)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2032119846:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.02/2.63 % (3173498)dis-21_1_sil=8000:lcm=predicate:random_seed=3262025762:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.02/2.63 % (3173492)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=1539275466:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.02/2.63 % (3173493)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=3885387256:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.02/2.63 % (3173494)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=2853741474:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.02/2.63 % (3173495)Refutation not found, incomplete strategy
% 12.02/2.63 % (3173495)------------------------------
% 12.02/2.63 % (3173495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.63 % (3173495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.63 % (3173495)CaDiCaL version: 2.1.3
% 12.02/2.63 % (3173495)Termination reason: Refutation not found, incomplete strategy
% 12.02/2.63 % (3173495)Time elapsed: 0.005 s
% 12.02/2.63 % (3173495)Peak memory usage: 88 MB
% 12.02/2.63 % (3173495)Instructions burned: 6 (million)
% 12.02/2.63 % (3173497)Instruction limit reached!
% 12.02/2.63 % (3173497)------------------------------
% 12.02/2.63 % (3173497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.63 % (3173497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.63 % (3173497)CaDiCaL version: 2.1.3
% 12.02/2.63 % (3173497)Termination reason: Instruction limit
% 12.02/2.63 % (3173497)Termination phase: Saturation
% 12.02/2.63 % (3173497)Time elapsed: 0.055 s
% 12.02/2.63 % (3173497)Peak memory usage: 90 MB
% 12.02/2.63 % (3173497)Instructions burned: 140 (million)
% 12.02/2.63 % (3173498)Instruction limit reached!
% 12.02/2.63 % (3173498)------------------------------
% 12.02/2.63 % (3173498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.63 % (3173498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.63 % (3173498)CaDiCaL version: 2.1.3
% 12.02/2.63 % (3173498)Termination reason: Instruction limit
% 12.02/2.63 % (3173498)Termination phase: Saturation
% 12.02/2.63 % (3173498)Time elapsed: 0.073 s
% 12.02/2.63 % (3173498)Peak memory usage: 91 MB
% 12.02/2.63 % (3173498)Instructions burned: 129 (million)
% 12.02/2.63 % (3173501)lrs+10_1_sil=8000:sp=occurrence:random_seed=3067189374:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.02/2.63 % (3173507)lrs+10_1_sil=32000:urr=on:br=off:random_seed=95830193:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.02/2.63 % (3173507)Instruction limit reached!
% 12.02/2.63 % (3173507)------------------------------
% 12.02/2.63 % (3173507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/2.63 % (3173507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/2.63 % (3173507)CaDiCaL version: 2.1.3
% 12.02/2.63 % (3173507)Termination reason: Instruction limit
% 12.02/2.63 % (3173507)Termination phase: Saturation
% 19.24/3.65 % (3173507)Time elapsed: 0.043 s
% 19.24/3.65 % (3173507)Peak memory usage: 89 MB
% 19.24/3.65 % (3173507)Instructions burned: 158 (million)
% 19.24/3.65 % (3173508)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3899598497:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.24/3.65 % (3173495)------------------------------
% 19.24/3.65 % (3173495)------------------------------
% 19.24/3.65 % (3173511)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=3781594040:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.24/3.65 % (3173501)Instruction limit reached!
% 19.24/3.65 % (3173501)------------------------------
% 19.24/3.65 % (3173501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.24/3.65 % (3173501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.65 % (3173501)CaDiCaL version: 2.1.3
% 19.24/3.65 % (3173501)Termination reason: Instruction limit
% 19.24/3.65 % (3173501)Termination phase: Saturation
% 19.24/3.65 % (3173501)Time elapsed: 0.175 s
% 19.24/3.65 % (3173501)Peak memory usage: 93 MB
% 19.24/3.65 % (3173501)Instructions burned: 286 (million)
% 19.24/3.65 % (3173511)Instruction limit reached!
% 19.24/3.65 % (3173511)------------------------------
% 19.24/3.65 % (3173511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.24/3.65 % (3173511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.65 % (3173511)CaDiCaL version: 2.1.3
% 19.24/3.65 % (3173511)Termination reason: Instruction limit
% 19.24/3.65 % (3173511)Termination phase: Saturation
% 19.24/3.65 % (3173511)Time elapsed: 0.075 s
% 19.24/3.65 % (3173511)Peak memory usage: 92 MB
% 19.24/3.65 % (3173511)Instructions burned: 252 (million)
% 19.24/3.65 % (3173513)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=800920969:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.24/3.65 % (3173513)Refutation not found, incomplete strategy
% 19.24/3.65 % (3173513)------------------------------
% 19.24/3.65 % (3173513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.24/3.65 % (3173513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.65 % (3173513)CaDiCaL version: 2.1.3
% 19.24/3.65 % (3173513)Termination reason: Refutation not found, incomplete strategy
% 19.24/3.65 % (3173513)Time elapsed: 0.005 s
% 19.24/3.65 % (3173513)Peak memory usage: 88 MB
% 19.24/3.65 % (3173513)Instructions burned: 7 (million)
% 19.24/3.65 % (3173516)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1116674348:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 19.24/3.65 % (3173508)Instruction limit reached!
% 19.24/3.65 % (3173508)------------------------------
% 19.24/3.65 % (3173508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.24/3.65 % (3173508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.65 % (3173508)CaDiCaL version: 2.1.3
% 19.24/3.65 % (3173508)Termination reason: Instruction limit
% 19.24/3.65 % (3173508)Termination phase: Saturation
% 19.24/3.65 % (3173508)Time elapsed: 0.218 s
% 19.24/3.65 % (3173508)Peak memory usage: 92 MB
% 19.24/3.65 % (3173508)Instructions burned: 327 (million)
% 19.24/3.65 % (3173515)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2763922506:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.24/3.65 % (3173516)Instruction limit reached!
% 19.24/3.65 % (3173516)------------------------------
% 19.24/3.65 % (3173516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.24/3.65 % (3173516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.65 % (3173516)CaDiCaL version: 2.1.3
% 19.24/3.65 % (3173516)Termination reason: Instruction limit
% 19.24/3.65 % (3173516)Termination phase: Saturation
% 19.24/3.65 % (3173516)Time elapsed: 0.041 s
% 19.24/3.65 % (3173516)Peak memory usage: 90 MB
% 19.24/3.65 % (3173516)Instructions burned: 114 (million)
% 19.24/3.65 % (3173520)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3060365931:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.24/3.65 % (3173521)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=88997851:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 19.24/3.65 % (3173521)Instruction limit reached!
% 19.24/3.65 % (3173521)------------------------------
% 19.24/3.65 % (3173521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173521)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173521)Termination reason: Instruction limit
% 27.28/5.33 % (3173521)Termination phase: Saturation
% 27.28/5.33 % (3173521)Time elapsed: 0.030 s
% 27.28/5.33 % (3173521)Peak memory usage: 89 MB
% 27.28/5.33 % (3173521)Instructions burned: 115 (million)
% 27.28/5.33 % (3173520)Instruction limit reached!
% 27.28/5.33 % (3173520)------------------------------
% 27.28/5.33 % (3173520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173520)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173520)Termination reason: Instruction limit
% 27.28/5.33 % (3173520)Termination phase: Saturation
% 27.28/5.33 % (3173520)Time elapsed: 0.065 s
% 27.28/5.33 % (3173520)Peak memory usage: 88 MB
% 27.28/5.33 % (3173520)Instructions burned: 128 (million)
% 27.28/5.33 % (3173513)------------------------------
% 27.28/5.33 % (3173513)------------------------------
% 27.28/5.33 % (3173524)lrs+10_1_sil=8000:sp=occurrence:random_seed=314699413:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 27.28/5.33 % (3173525)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4062585787:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 27.28/5.33 % (3173525)Refutation not found, incomplete strategy
% 27.28/5.33 % (3173525)------------------------------
% 27.28/5.33 % (3173525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173525)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173525)Termination reason: Refutation not found, incomplete strategy
% 27.28/5.33 % (3173525)Time elapsed: 0.006 s
% 27.28/5.33 % (3173525)Peak memory usage: 88 MB
% 27.28/5.33 % (3173525)Instructions burned: 9 (million)
% 27.28/5.33 % (3173526)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3955035357:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 27.28/5.33 % (3173525)------------------------------
% 27.28/5.33 % (3173525)------------------------------
% 27.28/5.33 % (3173530)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1599712989:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 27.28/5.33 % (3173530)Instruction limit reached!
% 27.28/5.33 % (3173530)------------------------------
% 27.28/5.33 % (3173530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173530)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173530)Termination reason: Instruction limit
% 27.28/5.33 % (3173530)Termination phase: Saturation
% 27.28/5.33 % (3173530)Time elapsed: 0.076 s
% 27.28/5.33 % (3173530)Peak memory usage: 90 MB
% 27.28/5.33 % (3173530)Instructions burned: 135 (million)
% 27.28/5.33 % (3173524)Instruction limit reached!
% 27.28/5.33 % (3173524)------------------------------
% 27.28/5.33 % (3173524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173524)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173524)Termination reason: Instruction limit
% 27.28/5.33 % (3173524)Termination phase: Saturation
% 27.28/5.33 % (3173524)Time elapsed: 0.533 s
% 27.28/5.33 % (3173524)Peak memory usage: 101 MB
% 27.28/5.33 % (3173524)Instructions burned: 908 (million)
% 27.28/5.33 % (3173532)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2798534024:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 27.28/5.33 % (3173533)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=411578087:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 27.28/5.33 % (3173532)Instruction limit reached!
% 27.28/5.33 % (3173532)------------------------------
% 27.28/5.33 % (3173532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173532)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173532)Termination reason: Instruction limit
% 27.28/5.33 % (3173532)Termination phase: Saturation
% 27.28/5.33 % (3173532)Time elapsed: 0.319 s
% 27.28/5.33 % (3173532)Peak memory usage: 92 MB
% 27.28/5.33 % (3173532)Instructions burned: 594 (million)
% 27.28/5.33 % (3173536)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=3225869714:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 27.28/5.33 % (3173536)Instruction limit reached!
% 27.28/5.33 % (3173536)------------------------------
% 27.28/5.33 % (3173536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173536)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173536)Termination reason: Instruction limit
% 27.28/5.33 % (3173536)Termination phase: Saturation
% 27.28/5.33 % (3173536)Time elapsed: 0.078 s
% 27.28/5.33 % (3173536)Peak memory usage: 91 MB
% 27.28/5.33 % (3173536)Instructions burned: 125 (million)
% 27.28/5.33 % (3173515)Instruction limit reached!
% 27.28/5.33 % (3173515)------------------------------
% 27.28/5.33 % (3173515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173515)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173515)Termination reason: Instruction limit
% 27.28/5.33 % (3173515)Termination phase: Saturation
% 27.28/5.33 % (3173515)Time elapsed: 1.507 s
% 27.28/5.33 % (3173515)Peak memory usage: 142 MB
% 27.28/5.33 % (3173515)Instructions burned: 2351 (million)
% 27.28/5.33 % (3173538)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1813236863:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 27.28/5.33 % (3173538)Instruction limit reached!
% 27.28/5.33 % (3173538)------------------------------
% 27.28/5.33 % (3173538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173538)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173538)Termination reason: Instruction limit
% 27.28/5.33 % (3173538)Termination phase: Saturation
% 27.28/5.33 % (3173538)Time elapsed: 0.082 s
% 27.28/5.33 % (3173538)Peak memory usage: 90 MB
% 27.28/5.33 % (3173538)Instructions burned: 134 (million)
% 27.28/5.33 % (3173539)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2766442975:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 27.28/5.33 % (3173539)Instruction limit reached!
% 27.28/5.33 % (3173539)------------------------------
% 27.28/5.33 % (3173539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173539)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173539)Termination reason: Instruction limit
% 27.28/5.33 % (3173539)Termination phase: Saturation
% 27.28/5.33 % (3173539)Time elapsed: 0.072 s
% 27.28/5.33 % (3173539)Peak memory usage: 89 MB
% 27.28/5.33 % (3173539)Instructions burned: 141 (million)
% 27.28/5.33 % (3173541)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2323094891:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 27.28/5.33 % (3173541)Refutation not found, incomplete strategy
% 27.28/5.33 % (3173541)------------------------------
% 27.28/5.33 % (3173541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173541)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173541)Termination reason: Refutation not found, incomplete strategy
% 27.28/5.33 % (3173541)Time elapsed: 0.005 s
% 27.28/5.33 % (3173541)Peak memory usage: 88 MB
% 27.28/5.33 % (3173541)Instructions burned: 7 (million)
% 27.28/5.33 % (3173543)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=3743873721:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 27.28/5.33 % (3173541)------------------------------
% 27.28/5.33 % (3173541)------------------------------
% 27.28/5.33 % (3173546)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=3816936506:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 27.28/5.33 % (3173546)Instruction limit reached!
% 27.28/5.33 % (3173546)------------------------------
% 27.28/5.33 % (3173546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173546)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173546)Termination reason: Instruction limit
% 27.28/5.33 % (3173546)Termination phase: Saturation
% 27.28/5.33 % (3173546)Time elapsed: 0.097 s
% 27.28/5.33 % (3173546)Peak memory usage: 91 MB
% 27.28/5.33 % (3173546)Instructions burned: 151 (million)
% 27.28/5.33 % (3173548)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=695684593:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 27.28/5.33 % (3173526)Instruction limit reached!
% 27.28/5.33 % (3173526)------------------------------
% 27.28/5.33 % (3173526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173526)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173526)Termination reason: Instruction limit
% 27.28/5.33 % (3173526)Termination phase: Saturation
% 27.28/5.33 % (3173526)Time elapsed: 2.905 s
% 27.28/5.33 % (3173526)Peak memory usage: 161 MB
% 27.28/5.33 % (3173526)Instructions burned: 5203 (million)
% 27.28/5.33 % (3173550)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=200529758:i=667:av=off:fsr=off_2961 on theBenchmark for (2961ds/667Mi)
% 27.28/5.33 % (3173492)First to succeed.
% 27.28/5.33 % (3173492)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3173487"
% 27.28/5.33 % (3173550)Instruction limit reached!
% 27.28/5.33 % (3173550)------------------------------
% 27.28/5.33 % (3173550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.28/5.33 % (3173550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.28/5.33 % (3173550)CaDiCaL version: 2.1.3
% 27.28/5.33 % (3173550)Termination reason: Instruction limit
% 27.28/5.33 % (3173550)Termination phase: Saturation
% 27.28/5.33 % (3173550)Time elapsed: 0.318 s
% 27.28/5.33 % (3173550)Peak memory usage: 92 MB
% 27.28/5.33 % (3173550)Instructions burned: 667 (million)
% 27.28/5.33 % (3173552)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=1591240068:s2a=on:i=185:s2at=1.8:fdi=4_2957 on theBenchmark for (2957ds/185Mi)
% 27.28/5.33 % (3173492)Refutation found. Thanks to Tanya!
% 27.28/5.33 % SZS status Theorem for theBenchmark
% 27.28/5.33 % SZS output start Proof for theBenchmark
% See solution above
% 32.31/5.53 % (3173492)------------------------------
% 32.31/5.53 % (3173492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.31/5.53 % (3173492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.31/5.53 % (3173492)CaDiCaL version: 2.1.3
% 32.31/5.53 % (3173492)Termination reason: Refutation
% 32.31/5.53 % (3173492)Time elapsed: 4.053 s
% 32.31/5.53 % (3173492)Peak memory usage: 177 MB
% 32.31/5.53 % (3173492)Instructions burned: 6267 (million)
% 32.31/5.53 % (3173492)------------------------------
% 32.31/5.53 % (3173492)------------------------------
% 32.31/5.53 % (3173487)Success in time 4.481 s
% 32.31/5.53 % Vampire exiting
%------------------------------------------------------------------------------