%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP650+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:18 AM UTC 2026
% Result : Theorem 123.84s 19.03s
% Output : Refutation 125.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 75
% Syntax : Number of formulae : 475 ( 95 unt; 55 def)
% Number of atoms : 3028 ( 321 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 4599 (2046 ~;2323 |; 142 &)
% ( 62 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 69 ( 67 usr; 50 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 7 con; 0-4 aty)
% Number of variables : 476 ( 0 sgn 467 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f777,axiom,
! [X0] :
( k1_relat_1(k6_relat_1(X0)) = X0
& k2_relat_1(k6_relat_1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t71_relat_1) ).
fof(f917,axiom,
! [X0] :
( v1_relat_1(k6_relat_1(X0))
& v1_funct_1(k6_relat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
fof(f966,axiom,
! [X0,X1] :
( r2_hidden(X1,X0)
=> k1_funct_1(k6_relat_1(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_funct_1) ).
fof(f1101,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k9_relat_1(k6_relat_1(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t162_funct_1) ).
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1636,axiom,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f1818,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ( v1_funct_1(X0)
& v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0))
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_funct_2) ).
fof(f2005,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/sandbox2/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f3987,axiom,
! [X0] :
( v3_relat_2(k6_partfun1(X0))
& v8_relat_2(k6_partfun1(X0))
& v1_partfun1(k6_partfun1(X0),X0,X0)
& m2_relset_1(k6_partfun1(X0),X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_eqrel_1) ).
fof(f8791,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> k7_group_2(X0,X1) = u1_struct_0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_group_2) ).
fof(f8902,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_1(X1)
& m1_group_2(X1,X0)
& v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
fof(f8909,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_group_2) ).
fof(f9168,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_group_3) ).
fof(f9568,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> u1_struct_0(k11_group_4(X0)) = k1_group_3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t92_group_4) ).
fof(f9582,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_group_4) ).
fof(f11151,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_group_6) ).
fof(f13963,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k3_latsubgr(X0,X1,X2))
& v1_funct_2(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
& m2_relset_1(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_latsubgr) ).
fof(f13966,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)))
=> ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( X1 = u1_struct_0(X2)
=> r1_group_2(X0,k5_group_4(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_latsubgr) ).
fof(f13998,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
& m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
=> ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ( v1_group_1(X4)
& m1_group_2(X4,X0) )
=> ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X5 = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
=> k1_funct_1(X3,X4) = k5_group_4(X1,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_latsubgr) ).
fof(f13999,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) = k6_partfun1(u1_struct_0(k11_group_4(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_latsubgr) ).
fof(f14000,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) = k6_partfun1(u1_struct_0(k11_group_4(X0))) ),
inference(negated_conjecture,[status(cth)],[f13999]) ).
fof(f14123,plain,
? [X0] :
( k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) != k6_partfun1(u1_struct_0(k11_group_4(X0)))
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f14000]) ).
fof(f14124,plain,
? [X0] :
( k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) != k6_partfun1(u1_struct_0(k11_group_4(X0)))
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f14123]) ).
fof(f14125,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f11151]) ).
fof(f14126,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14125]) ).
fof(f14152,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f9568]) ).
fof(f14153,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14152]) ).
fof(f14156,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X4) = k5_group_4(X1,X5)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X4)
| ~ m1_group_2(X4,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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,[],[f13998]) ).
fof(f14157,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X4) = k5_group_4(X1,X5)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X4)
| ~ m1_group_2(X4,X0) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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,[],[f14156]) ).
fof(f14158,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_latsubgr(X0,X1,X2))
& v1_funct_2(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
& m2_relset_1(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f13963]) ).
fof(f14159,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k3_latsubgr(X0,X1,X2))
& v1_funct_2(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
& m2_relset_1(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f14158]) ).
fof(f14326,plain,
! [X0] :
( ( v1_funct_1(X0)
& v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0))
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f1818]) ).
fof(f14327,plain,
! [X0] :
( ( v1_funct_1(X0)
& v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0))
& m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f14326]) ).
fof(f14711,plain,
! [X0,X1] :
( k9_relat_1(k6_relat_1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f1101]) ).
fof(f14726,plain,
! [X0,X1] :
( k1_funct_1(k6_relat_1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(ennf_transformation,[],[f966]) ).
fof(f15009,plain,
! [X0] :
( ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f9168]) ).
fof(f15010,plain,
! [X0] :
( ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f15009]) ).
fof(f15075,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,[],[f2005]) ).
fof(f15076,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,[],[f15075]) ).
fof(f15091,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_group_2(X0,k5_group_4(X0,X1),X2)
| u1_struct_0(X2) != X1
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,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,[],[f13966]) ).
fof(f15092,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r1_group_2(X0,k5_group_4(X0,X1),X2)
| u1_struct_0(X2) != X1
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,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,[],[f15091]) ).
fof(f15107,plain,
! [X0,X1] :
( ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f9582]) ).
fof(f15108,plain,
! [X0,X1] :
( ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f15107]) ).
fof(f16195,plain,
! [X0,X1,X2] :
( ( r1_group_2(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(ennf_transformation,[],[f8902]) ).
fof(f16196,plain,
! [X0,X1,X2] :
( ( r1_group_2(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(flattening,[],[f16195]) ).
fof(f16275,plain,
! [X0,X1] :
( m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f8909]) ).
fof(f16276,plain,
! [X0,X1] :
( m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f16275]) ).
fof(f16291,plain,
! [X0] :
( ! [X1] :
( k7_group_2(X0,X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8791]) ).
fof(f16292,plain,
! [X0] :
( ! [X1] :
( k7_group_2(X0,X1) = u1_struct_0(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f16291]) ).
fof(f16615,plain,
( k3_latsubgr(sK30,sK30,k6_partfun1(u1_struct_0(sK30))) != k6_partfun1(u1_struct_0(k11_group_4(sK30)))
& ~ v3_struct_0(sK30)
& v3_group_1(sK30)
& v4_group_1(sK30)
& l1_group_1(sK30) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(X0,sK30)],[f14124]) ).
fof(f16621,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ? [X4] :
( ? [X5] :
( k1_funct_1(X3,X4) != k5_group_4(X1,X5)
& k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) = X5
& m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
& v1_group_1(X4)
& m1_group_2(X4,X0) ) )
& ( ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X4) = k5_group_4(X1,X5)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) != X5
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X4)
| ~ m1_group_2(X4,X0) )
| k3_latsubgr(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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(nnf_transformation,[],[f14157]) ).
fof(f16622,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ? [X4] :
( ? [X5] :
( k1_funct_1(X3,X4) != k5_group_4(X1,X5)
& k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4)) = X5
& m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) )
& v1_group_1(X4)
& m1_group_2(X4,X0) ) )
& ( ! [X6] :
( ! [X7] :
( k1_funct_1(X3,X6) = k5_group_4(X1,X7)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)) != X7
| ~ m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X6)
| ~ m1_group_2(X6,X0) )
| k3_latsubgr(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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(rectify,[],[f16621]) ).
fof(f16623,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ( k1_funct_1(X3,sK32(X0,X1,X2,X3)) != k5_group_4(X1,sK33(X0,X1,X2,X3))
& sK33(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK32(X0,X1,X2,X3)))
& m1_subset_1(sK33(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
& v1_group_1(sK32(X0,X1,X2,X3))
& m1_group_2(sK32(X0,X1,X2,X3),X0) ) )
& ( ! [X6] :
( ! [X7] :
( k1_funct_1(X3,X6) = k5_group_4(X1,X7)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)) != X7
| ~ m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X1))) )
| ~ v1_group_1(X6)
| ~ m1_group_2(X6,X0) )
| k3_latsubgr(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33]),skolemize(X4,sK32(X0,X1,X2,X3)),skolemize(X5,sK33(X0,X1,X2,X3))],[f16622]) ).
fof(f16818,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f15010]) ).
fof(f16819,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f16818]) ).
fof(f16820,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0) )
& ( ( v1_group_1(X3)
& m1_group_2(X3,X0) )
| ~ r2_hidden(X3,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f16819]) ).
fof(f16821,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ( ( ~ v1_group_1(sK152(X0,X1))
| ~ m1_group_2(sK152(X0,X1),X0)
| ~ r2_hidden(sK152(X0,X1),X1) )
& ( ( v1_group_1(sK152(X0,X1))
& m1_group_2(sK152(X0,X1),X0) )
| r2_hidden(sK152(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0) )
& ( ( v1_group_1(X3)
& m1_group_2(X3,X0) )
| ~ r2_hidden(X3,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK152]),skolemize(X2,sK152(X0,X1))],[f16820]) ).
fof(f16861,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,[],[f1394]) ).
fof(f17270,plain,
! [X0,X1,X2] :
( ( ( r1_group_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_group_2(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(nnf_transformation,[],[f16196]) ).
fof(f17390,plain,
l1_group_1(sK30),
inference(cnf_transformation,[],[f16615]) ).
fof(f17391,plain,
v4_group_1(sK30),
inference(cnf_transformation,[],[f16615]) ).
fof(f17392,plain,
v3_group_1(sK30),
inference(cnf_transformation,[],[f16615]) ).
fof(f17393,plain,
~ v3_struct_0(sK30),
inference(cnf_transformation,[],[f16615]) ).
fof(f17394,plain,
k3_latsubgr(sK30,sK30,k6_partfun1(u1_struct_0(sK30))) != k6_partfun1(u1_struct_0(k11_group_4(sK30))),
inference(cnf_transformation,[],[f16615]) ).
fof(f17395,plain,
! [X0] :
( m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14126]) ).
fof(f17397,plain,
! [X0] :
( v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14126]) ).
fof(f17403,plain,
! [X0] : m2_relset_1(k6_partfun1(X0),X0,X0),
inference(cnf_transformation,[],[f3987]) ).
fof(f17410,plain,
! [X0] : k6_relat_1(X0) = k6_partfun1(X0),
inference(cnf_transformation,[],[f1636]) ).
fof(f17429,plain,
! [X0] :
( k1_group_3(X0) = u1_struct_0(k11_group_4(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14153]) ).
fof(f17443,plain,
! [X2,X3,X0,X1,X6,X7] :
( ~ v4_group_1(X1)
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)) != X7
| ~ m1_subset_1(X7,k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_group_1(X6)
| ~ m1_group_2(X6,X0)
| k3_latsubgr(X0,X1,X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ v3_group_1(X1)
| k1_funct_1(X3,X6) = k5_group_4(X1,X7)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f16623]) ).
fof(f17444,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK32(X0,X1,X2,X3),X0)
| ~ v1_funct_1(X3)
| k3_latsubgr(X0,X1,X2) = X3
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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,[],[f16623]) ).
fof(f17445,plain,
! [X2,X3,X0,X1] :
( v1_group_1(sK32(X0,X1,X2,X3))
| k3_latsubgr(X0,X1,X2) = X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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,[],[f16623]) ).
fof(f17447,plain,
! [X2,X3,X0,X1] :
( ~ v4_group_1(X1)
| sK33(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK32(X0,X1,X2,X3)))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ v3_group_1(X1)
| k3_latsubgr(X0,X1,X2) = X3
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f16623]) ).
fof(f17448,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X3,sK32(X0,X1,X2,X3)) != k5_group_4(X1,sK33(X0,X1,X2,X3))
| k3_latsubgr(X0,X1,X2) = X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(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)
| ~ 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,[],[f16623]) ).
fof(f17449,plain,
! [X2,X0,X1] :
( m2_relset_1(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f14159]) ).
fof(f17450,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f14159]) ).
fof(f17451,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| v1_funct_1(k3_latsubgr(X0,X1,X2))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f14159]) ).
fof(f17679,plain,
! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| v1_funct_2(X0,k1_relat_1(X0),k2_relat_1(X0)) ),
inference(cnf_transformation,[],[f14327]) ).
fof(f18209,plain,
! [X0,X1] :
( k9_relat_1(k6_relat_1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f14711]) ).
fof(f18222,plain,
! [X0,X1] :
( k1_funct_1(k6_relat_1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(cnf_transformation,[],[f14726]) ).
fof(f18227,plain,
! [X0] : v1_funct_1(k6_relat_1(X0)),
inference(cnf_transformation,[],[f917]) ).
fof(f18228,plain,
! [X0] : v1_relat_1(k6_relat_1(X0)),
inference(cnf_transformation,[],[f917]) ).
fof(f18247,plain,
! [X0] : k2_relat_1(k6_relat_1(X0)) = X0,
inference(cnf_transformation,[],[f777]) ).
fof(f18248,plain,
! [X0] : k1_relat_1(k6_relat_1(X0)) = X0,
inference(cnf_transformation,[],[f777]) ).
fof(f18551,plain,
! [X3,X0,X1] :
( k1_group_3(X0) != X1
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| r2_hidden(X3,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f16821]) ).
fof(f18663,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X2,X3) = k2_funct_2(X0,X1,X2,X3)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f15076]) ).
fof(f18676,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| u1_struct_0(X2) != X1
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| r1_group_2(X0,k5_group_4(X0,X1),X2)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f15092]) ).
fof(f18693,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(k5_group_4(X0,X1),X0)
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f15108]) ).
fof(f18694,plain,
! [X0,X1] :
( ~ 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)
| v1_group_1(k5_group_4(X0,X1)) ),
inference(cnf_transformation,[],[f15108]) ).
fof(f18719,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f16861]) ).
fof(f20158,plain,
! [X2,X0,X1] :
( ~ r1_group_2(X0,X1,X2)
| X1 = X2
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(cnf_transformation,[],[f17270]) ).
fof(f20246,plain,
! [X0,X1] :
( m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f16276]) ).
fof(f20260,plain,
! [X0,X1] :
( u1_struct_0(X1) = k7_group_2(X0,X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f16292]) ).
fof(f20864,plain,
! [X0,X1] :
( k9_relat_1(k6_partfun1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(definition_unfolding,[],[f18209,f17410]) ).
fof(f20877,plain,
! [X0,X1] :
( k1_funct_1(k6_partfun1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(definition_unfolding,[],[f18222,f17410]) ).
fof(f20882,plain,
! [X0] : v1_relat_1(k6_partfun1(X0)),
inference(definition_unfolding,[],[f18228,f17410]) ).
fof(f20883,plain,
! [X0] : v1_funct_1(k6_partfun1(X0)),
inference(definition_unfolding,[],[f18227,f17410]) ).
fof(f20902,plain,
! [X0] : k1_relat_1(k6_partfun1(X0)) = X0,
inference(definition_unfolding,[],[f18248,f17410]) ).
fof(f20903,plain,
! [X0] : k2_relat_1(k6_partfun1(X0)) = X0,
inference(definition_unfolding,[],[f18247,f17410]) ).
fof(f21392,definition,
sF484 = u1_struct_0(sK30),
introduced(definition,[new_symbols(definition,[sF484])],[function_definition]) ).
fof(f21393,plain,
u1_struct_0(sK30) = sF484,
inference(reorient_equations,[],[f21392]) ).
fof(f21394,definition,
sF485 = k6_partfun1(sF484),
introduced(definition,[new_symbols(definition,[sF485])],[function_definition]) ).
fof(f21395,plain,
k6_partfun1(sF484) = sF485,
inference(reorient_equations,[],[f21394]) ).
fof(f21396,definition,
sF486 = k3_latsubgr(sK30,sK30,sF485),
introduced(definition,[new_symbols(definition,[sF486])],[function_definition]) ).
fof(f21397,plain,
k3_latsubgr(sK30,sK30,sF485) = sF486,
inference(reorient_equations,[],[f21396]) ).
fof(f21398,definition,
sF487 = k11_group_4(sK30),
introduced(definition,[new_symbols(definition,[sF487])],[function_definition]) ).
fof(f21399,plain,
k11_group_4(sK30) = sF487,
inference(reorient_equations,[],[f21398]) ).
fof(f21400,definition,
sF488 = u1_struct_0(sF487),
introduced(definition,[new_symbols(definition,[sF488])],[function_definition]) ).
fof(f21401,plain,
u1_struct_0(sF487) = sF488,
inference(reorient_equations,[],[f21400]) ).
fof(f21402,definition,
sF489 = k6_partfun1(sF488),
introduced(definition,[new_symbols(definition,[sF489])],[function_definition]) ).
fof(f21403,plain,
k6_partfun1(sF488) = sF489,
inference(reorient_equations,[],[f21402]) ).
fof(f21404,plain,
sF486 != sF489,
inference(definition_folding,[],[f17394,f21403,f21401,f21399,f21397,f21395,f21393]) ).
fof(f21481,definition,
( spl490_9
<=> l1_group_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl490_9])],[avatar_definition]) ).
fof(f21485,definition,
( spl490_10
<=> v4_group_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl490_10])],[avatar_definition]) ).
fof(f21486,plain,
( v4_group_1(sK30)
| ~ spl490_10 ),
inference(avatar_component_clause,[],[f21485]) ).
fof(f21489,definition,
( spl490_11
<=> v3_group_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl490_11])],[avatar_definition]) ).
fof(f21493,definition,
( spl490_12
<=> v3_struct_0(sK30) ),
introduced(definition,[new_symbols(definition,[spl490_12])],[avatar_definition]) ).
fof(f21503,plain,
spl490_9,
inference(avatar_split_clause,[],[f17390,f21481]) ).
fof(f21506,plain,
spl490_10,
inference(avatar_split_clause,[],[f17391,f21485]) ).
fof(f21509,plain,
spl490_11,
inference(avatar_split_clause,[],[f17392,f21489]) ).
fof(f21510,plain,
( u1_struct_0(sF487) = k1_group_3(sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(superposition,[],[f17429,f21399]) ).
fof(f21511,plain,
( sF488 = k1_group_3(sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f21510,f21401]) ).
fof(f21513,definition,
( spl490_14
<=> sF488 = k1_group_3(sK30) ),
introduced(definition,[new_symbols(definition,[spl490_14])],[avatar_definition]) ).
fof(f21515,plain,
( sF488 = k1_group_3(sK30)
| ~ spl490_14 ),
inference(avatar_component_clause,[],[f21513]) ).
fof(f21516,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_14 ),
inference(avatar_split_clause,[],[f21511,f21513,f21493,f21489,f21485,f21481]) ).
fof(f21519,plain,
~ spl490_12,
inference(avatar_split_clause,[],[f17393,f21493]) ).
fof(f21536,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_latsubgr(X1,X0,X2),u1_struct_0(k11_group_4(X1)),k1_group_3(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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(superposition,[],[f17450,f17429]) ).
fof(f21537,plain,
! [X2,X0,X1] :
( v1_funct_2(k3_latsubgr(X1,X0,X2),u1_struct_0(k11_group_4(X1)),k1_group_3(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)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X1),u1_struct_0(X0))
| ~ m1_relset_1(X2,u1_struct_0(X1),u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f21536]) ).
fof(f21559,definition,
( spl490_19
<=> v1_funct_1(sF485) ),
introduced(definition,[new_symbols(definition,[spl490_19])],[avatar_definition]) ).
fof(f21563,definition,
( spl490_20
<=> v1_funct_2(sF486,sF488,sF488) ),
introduced(definition,[new_symbols(definition,[spl490_20])],[avatar_definition]) ).
fof(f21567,definition,
( spl490_21
<=> v1_funct_2(sF485,sF484,sF484) ),
introduced(definition,[new_symbols(definition,[spl490_21])],[avatar_definition]) ).
fof(f21568,plain,
( v1_funct_2(sF485,sF484,sF484)
| ~ spl490_21 ),
inference(avatar_component_clause,[],[f21567]) ).
fof(f21571,definition,
( spl490_22
<=> m1_relset_1(sF485,sF484,sF484) ),
introduced(definition,[new_symbols(definition,[spl490_22])],[avatar_definition]) ).
fof(f21573,plain,
( ~ m1_relset_1(sF485,sF484,sF484)
| spl490_22 ),
inference(avatar_component_clause,[],[f21571]) ).
fof(f21576,plain,
! [X0] :
( k1_funct_1(sF489,X0) = X0
| ~ r2_hidden(X0,sF488) ),
inference(superposition,[],[f20877,f21403]) ).
fof(f21579,plain,
! [X0] :
( k9_relat_1(sF485,X0) = X0
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484)) ),
inference(superposition,[],[f20864,f21395]) ).
fof(f21588,plain,
sF488 = k1_relat_1(sF489),
inference(superposition,[],[f20902,f21403]) ).
fof(f21589,plain,
( m2_relset_1(sF486,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(superposition,[],[f17449,f21397]) ).
fof(f21596,plain,
( m2_relset_1(sF486,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(duplicate_literal_removal,[],[f21589]) ).
fof(f21599,plain,
( m2_relset_1(sF486,u1_struct_0(sF487),u1_struct_0(sF487))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(forward_demodulation,[],[f21596,f21399]) ).
fof(f21602,plain,
( m2_relset_1(sF486,sF488,sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(forward_demodulation,[],[f21599,f21401]) ).
fof(f21605,plain,
( ~ v1_funct_2(sF485,sF484,sF484)
| m2_relset_1(sF486,sF488,sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(forward_demodulation,[],[f21602,f21393]) ).
fof(f21614,plain,
( ~ m1_relset_1(sF485,sF484,sF484)
| ~ v1_funct_2(sF485,sF484,sF484)
| m2_relset_1(sF486,sF488,sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485) ),
inference(forward_demodulation,[],[f21605,f21393]) ).
fof(f21616,definition,
( spl490_26
<=> m2_relset_1(sF486,sF488,sF488) ),
introduced(definition,[new_symbols(definition,[spl490_26])],[avatar_definition]) ).
fof(f21619,plain,
( ~ spl490_19
| ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_26
| ~ spl490_21
| ~ spl490_22 ),
inference(avatar_split_clause,[],[f21614,f21571,f21567,f21616,f21493,f21489,f21485,f21481,f21559]) ).
fof(f21627,plain,
sF488 = k2_relat_1(sF489),
inference(superposition,[],[f20903,f21403]) ).
fof(f21685,plain,
( v1_funct_2(k6_partfun1(sF484),sF484,sF484)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(superposition,[],[f17397,f21393]) ).
fof(f21687,plain,
( v1_funct_2(sF485,sF484,sF484)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f21685,f21395]) ).
fof(f21688,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_21 ),
inference(avatar_split_clause,[],[f21687,f21567,f21493,f21489,f21485,f21481]) ).
fof(f21703,plain,
v1_funct_1(sF485),
inference(superposition,[],[f20883,f21395]) ).
fof(f21704,plain,
v1_funct_1(sF489),
inference(superposition,[],[f20883,f21403]) ).
fof(f21705,plain,
spl490_19,
inference(avatar_split_clause,[],[f21703,f21559]) ).
fof(f21706,plain,
( ~ m2_relset_1(sF485,sF484,sF484)
| spl490_22 ),
inference(resolution,[],[f21573,f18719]) ).
fof(f21734,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| v1_group_1(k5_group_4(sK30,X0)) ),
inference(superposition,[],[f18694,f21393]) ).
fof(f21737,definition,
( spl490_42
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| v1_group_1(k5_group_4(sK30,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl490_42])],[avatar_definition]) ).
fof(f21738,plain,
( ! [X0] :
( v1_group_1(k5_group_4(sK30,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484)) )
| ~ spl490_42 ),
inference(avatar_component_clause,[],[f21737]) ).
fof(f21739,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_42 ),
inference(avatar_split_clause,[],[f21734,f21737,f21493,f21489,f21485,f21481]) ).
fof(f21768,plain,
v1_relat_1(sF489),
inference(superposition,[],[f20882,f21403]) ).
fof(f21833,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,sF484,u1_struct_0(X1))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X0)
| v1_funct_1(k3_latsubgr(sK30,X1,X0))
| ~ m1_relset_1(X0,sF484,u1_struct_0(X1)) ),
inference(superposition,[],[f17451,f21393]) ).
fof(f21845,definition,
( spl490_53
<=> ! [X0,X1] :
( ~ v1_funct_2(X0,sF484,u1_struct_0(X1))
| ~ m1_relset_1(X0,sF484,u1_struct_0(X1))
| v1_funct_1(k3_latsubgr(sK30,X1,X0))
| ~ v1_funct_1(X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl490_53])],[avatar_definition]) ).
fof(f21846,plain,
( ! [X0,X1] :
( ~ v4_group_1(X1)
| ~ m1_relset_1(X0,sF484,u1_struct_0(X1))
| v1_funct_1(k3_latsubgr(sK30,X1,X0))
| ~ v1_funct_1(X0)
| ~ l1_group_1(X1)
| ~ v1_funct_2(X0,sF484,u1_struct_0(X1))
| ~ v3_group_1(X1)
| v3_struct_0(X1) )
| ~ spl490_53 ),
inference(avatar_component_clause,[],[f21845]) ).
fof(f21847,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_53 ),
inference(avatar_split_clause,[],[f21833,f21845,f21493,f21489,f21485,f21481]) ).
fof(f21859,plain,
( m2_relset_1(k6_partfun1(sF484),sF484,sF484)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(superposition,[],[f17395,f21393]) ).
fof(f21861,plain,
( m2_relset_1(sF485,sF484,sF484)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f21859,f21395]) ).
fof(f21863,definition,
( spl490_55
<=> m2_relset_1(sF485,sF484,sF484) ),
introduced(definition,[new_symbols(definition,[spl490_55])],[avatar_definition]) ).
fof(f21866,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_55 ),
inference(avatar_split_clause,[],[f21861,f21863,f21493,f21489,f21485,f21481]) ).
fof(f21897,plain,
( ! [X0,X1] :
( sF488 != X0
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK30)
| r2_hidden(X1,X0)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) )
| ~ spl490_14 ),
inference(superposition,[],[f18551,f21515]) ).
fof(f21900,definition,
( spl490_60
<=> ! [X0,X1] :
( sF488 != X0
| ~ v1_group_1(X1)
| r2_hidden(X1,X0)
| ~ m1_group_2(X1,sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_60])],[avatar_definition]) ).
fof(f21901,plain,
( ! [X0,X1] :
( sF488 != X0
| ~ v1_group_1(X1)
| r2_hidden(X1,X0)
| ~ m1_group_2(X1,sK30) )
| ~ spl490_60 ),
inference(avatar_component_clause,[],[f21900]) ).
fof(f21902,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_60
| ~ spl490_14 ),
inference(avatar_split_clause,[],[f21897,f21513,f21900,f21493,f21489,f21485,f21481]) ).
fof(f21903,plain,
( ! [X0] :
( r2_hidden(X0,sF488)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30) )
| ~ spl490_60 ),
inference(equality_resolution,[],[f21901]) ).
fof(f21910,definition,
( spl490_61
<=> v1_relat_1(sF489) ),
introduced(definition,[new_symbols(definition,[spl490_61])],[avatar_definition]) ).
fof(f21930,plain,
m2_relset_1(sF489,sF488,sF488),
inference(superposition,[],[f17403,f21403]) ).
fof(f21972,plain,
( v1_funct_2(sF486,u1_struct_0(k11_group_4(sK30)),k1_group_3(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(superposition,[],[f21537,f21397]) ).
fof(f21977,plain,
( v1_funct_2(sF486,u1_struct_0(k11_group_4(sK30)),k1_group_3(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30)) ),
inference(duplicate_literal_removal,[],[f21972]) ).
fof(f21980,plain,
( v1_funct_2(sF486,u1_struct_0(k11_group_4(sK30)),sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ spl490_14 ),
inference(forward_demodulation,[],[f21977,f21515]) ).
fof(f21983,plain,
( v1_funct_2(sF486,u1_struct_0(sF487),sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ spl490_14 ),
inference(forward_demodulation,[],[f21980,f21399]) ).
fof(f21986,plain,
( v1_funct_2(sF486,sF488,sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ spl490_14 ),
inference(forward_demodulation,[],[f21983,f21401]) ).
fof(f21991,plain,
( ~ v1_funct_2(sF485,sF484,sF484)
| v1_funct_2(sF486,sF488,sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ m1_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ spl490_14 ),
inference(forward_demodulation,[],[f21986,f21393]) ).
fof(f21992,plain,
( ~ m1_relset_1(sF485,sF484,sF484)
| ~ v1_funct_2(sF485,sF484,sF484)
| v1_funct_2(sF486,sF488,sF488)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_funct_1(sF485)
| ~ spl490_14 ),
inference(forward_demodulation,[],[f21991,f21393]) ).
fof(f22083,plain,
( ~ spl490_55
| spl490_22 ),
inference(avatar_split_clause,[],[f21706,f21571,f21863]) ).
fof(f22085,plain,
( ~ spl490_19
| ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_20
| ~ spl490_21
| ~ spl490_22
| ~ spl490_14 ),
inference(avatar_split_clause,[],[f21992,f21513,f21571,f21567,f21563,f21493,f21489,f21485,f21481,f21559]) ).
fof(f22215,plain,
! [X0,X1] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X0,X1)
| ~ m1_group_2(X0,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(superposition,[],[f20246,f20260]) ).
fof(f22220,plain,
! [X0,X1] :
( ~ v4_group_1(X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(duplicate_literal_removal,[],[f22215]) ).
fof(f22230,definition,
( spl490_85
<=> ! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sF484))
| ~ m1_group_2(X0,sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_85])],[avatar_definition]) ).
fof(f22231,plain,
( ! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sF484))
| ~ m1_group_2(X0,sK30) )
| ~ spl490_85 ),
inference(avatar_component_clause,[],[f22230]) ).
fof(f22240,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(sF487),u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(sF487),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK30),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK30),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(superposition,[],[f17444,f21399]) ).
fof(f22249,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X0,sF488,u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ m2_relset_1(X0,u1_struct_0(sF487),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK30),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK30),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f22240,f21401]) ).
fof(f22251,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X0,sF488,u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(sK30),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(sK30),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f22249,f21401]) ).
fof(f22253,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,sF484,u1_struct_0(X1))
| ~ m2_relset_1(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X0,sF488,u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(sK30),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f22251,f21393]) ).
fof(f22255,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,sF484,u1_struct_0(X1))
| ~ v1_funct_2(X2,sF484,u1_struct_0(X1))
| ~ m2_relset_1(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X0,sF488,u1_struct_0(k11_group_4(X1)))
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ v1_funct_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30) ),
inference(forward_demodulation,[],[f22253,f21393]) ).
fof(f22261,definition,
( spl490_87
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X2,sF484,u1_struct_0(X1))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ v1_funct_1(X2)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ v1_funct_1(X0)
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_2(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X2,sF484,u1_struct_0(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl490_87])],[avatar_definition]) ).
fof(f22262,plain,
( ! [X2,X0,X1] :
( ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m2_relset_1(X2,sF484,u1_struct_0(X1))
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ v1_funct_1(X2)
| k3_latsubgr(sK30,X1,X2) = X0
| ~ v1_funct_1(X0)
| m1_group_2(sK32(sK30,X1,X2,X0),sK30)
| ~ v1_funct_2(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X0,sF488,u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_2(X2,sF484,u1_struct_0(X1)) )
| ~ spl490_87 ),
inference(avatar_component_clause,[],[f22261]) ).
fof(f22263,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_87 ),
inference(avatar_split_clause,[],[f22255,f22261,f21493,f21489,f21485,f21481]) ).
fof(f22430,plain,
spl490_61,
inference(avatar_split_clause,[],[f21768,f21910]) ).
fof(f22437,definition,
( spl490_99
<=> v1_funct_1(sF489) ),
introduced(definition,[new_symbols(definition,[spl490_99])],[avatar_definition]) ).
fof(f22438,plain,
( v1_funct_1(sF489)
| ~ spl490_99 ),
inference(avatar_component_clause,[],[f22437]) ).
fof(f22548,plain,
( ! [X0] :
( v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| m1_group_2(k5_group_4(sK30,X0),sK30)
| ~ l1_group_1(sK30)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK30))) )
| ~ spl490_10 ),
inference(resolution,[],[f18693,f21486]) ).
fof(f22549,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| m1_group_2(k5_group_4(sK30,X0),sK30)
| ~ l1_group_1(sK30) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22548,f21393]) ).
fof(f22551,definition,
( spl490_119
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| m1_group_2(k5_group_4(sK30,X0),sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_119])],[avatar_definition]) ).
fof(f22552,plain,
( ! [X0] :
( m1_group_2(k5_group_4(sK30,X0),sK30)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484)) )
| ~ spl490_119 ),
inference(avatar_component_clause,[],[f22551]) ).
fof(f22553,plain,
( ~ spl490_9
| ~ spl490_11
| spl490_12
| spl490_119
| ~ spl490_10 ),
inference(avatar_split_clause,[],[f22549,f21485,f22551,f21493,f21489,f21481]) ).
fof(f22627,definition,
( spl490_124
<=> ! [X0] :
( ~ v1_funct_2(X0,sF484,sF484)
| ~ v1_funct_1(X0)
| v1_funct_1(k3_latsubgr(sK30,sK30,X0))
| ~ m1_relset_1(X0,sF484,sF484) ) ),
introduced(definition,[new_symbols(definition,[spl490_124])],[avatar_definition]) ).
fof(f22628,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF484,sF484)
| ~ v1_funct_1(X0)
| v1_funct_1(k3_latsubgr(sK30,sK30,X0))
| ~ m1_relset_1(X0,sF484,sF484) )
| ~ spl490_124 ),
inference(avatar_component_clause,[],[f22627]) ).
fof(f22640,plain,
spl490_99,
inference(avatar_split_clause,[],[f21704,f22437]) ).
fof(f22783,plain,
( ! [X0,X1] :
( u1_struct_0(X0) != X1
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK30)))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| r1_group_2(sK30,k5_group_4(sK30,X1),X0)
| ~ l1_group_1(sK30) )
| ~ spl490_10 ),
inference(resolution,[],[f18676,f21486]) ).
fof(f22784,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF484))
| u1_struct_0(X0) != X1
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| r1_group_2(sK30,k5_group_4(sK30,X1),X0)
| ~ l1_group_1(sK30) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22783,f21393]) ).
fof(f22786,definition,
( spl490_134
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF484))
| r1_group_2(sK30,k5_group_4(sK30,X1),X0)
| ~ m1_group_2(X0,sK30)
| ~ v1_group_1(X0)
| u1_struct_0(X0) != X1 ) ),
introduced(definition,[new_symbols(definition,[spl490_134])],[avatar_definition]) ).
fof(f22787,plain,
( ! [X0,X1] :
( r1_group_2(sK30,k5_group_4(sK30,X1),X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(sF484))
| ~ m1_group_2(X0,sK30)
| ~ v1_group_1(X0)
| u1_struct_0(X0) != X1 )
| ~ spl490_134 ),
inference(avatar_component_clause,[],[f22786]) ).
fof(f22788,plain,
( ~ spl490_9
| ~ spl490_11
| spl490_12
| spl490_134
| ~ spl490_10 ),
inference(avatar_split_clause,[],[f22784,f21485,f22786,f21493,f21489,f21481]) ).
fof(f22795,plain,
( ! [X2,X0,X1] :
( sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),u1_struct_0(sK30),X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(resolution,[],[f17447,f21486]) ).
fof(f22798,plain,
( ! [X2,X0,X1] :
( sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22795,f21393]) ).
fof(f22799,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(sF487))
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22798,f21399]) ).
fof(f22800,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22799,f21401]) ).
fof(f22801,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),u1_struct_0(sF487))
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22800,f21399]) ).
fof(f22802,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22801,f21401]) ).
fof(f22803,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X1,u1_struct_0(X0),sF484)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22802,f21393]) ).
fof(f22804,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),sF484)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF484)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f22803,f21393]) ).
fof(f22806,definition,
( spl490_136
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),sF484)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF484) ) ),
introduced(definition,[new_symbols(definition,[spl490_136])],[avatar_definition]) ).
fof(f22807,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k3_latsubgr(X0,sK30,X1) = X2
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X2)
| sK33(X0,sK30,X1,X2) = k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(sK32(X0,sK30,X1,X2)))
| ~ m2_relset_1(X1,u1_struct_0(X0),sF484)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF484) )
| ~ spl490_136 ),
inference(avatar_component_clause,[],[f22806]) ).
fof(f22808,plain,
( ~ spl490_9
| ~ spl490_11
| spl490_12
| spl490_136
| ~ spl490_10 ),
inference(avatar_split_clause,[],[f22804,f21485,f22806,f21493,f21489,f21481]) ).
fof(f23475,definition,
( spl490_203
<=> v1_funct_1(sF486) ),
introduced(definition,[new_symbols(definition,[spl490_203])],[avatar_definition]) ).
fof(f23529,plain,
( ! [X0] :
( ~ m1_relset_1(X0,sF484,u1_struct_0(sK30))
| v1_funct_1(k3_latsubgr(sK30,sK30,X0))
| ~ v1_funct_1(X0)
| ~ l1_group_1(sK30)
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30))
| ~ v3_group_1(sK30)
| v3_struct_0(sK30) )
| ~ spl490_10
| ~ spl490_53 ),
inference(resolution,[],[f21846,f21486]) ).
fof(f23530,plain,
( ! [X0] :
( ~ m1_relset_1(X0,sF484,sF484)
| v1_funct_1(k3_latsubgr(sK30,sK30,X0))
| ~ v1_funct_1(X0)
| ~ l1_group_1(sK30)
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30))
| ~ v3_group_1(sK30)
| v3_struct_0(sK30) )
| ~ spl490_10
| ~ spl490_53 ),
inference(forward_demodulation,[],[f23529,f21393]) ).
fof(f23531,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF484,sF484)
| ~ m1_relset_1(X0,sF484,sF484)
| v1_funct_1(k3_latsubgr(sK30,sK30,X0))
| ~ v1_funct_1(X0)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30) )
| ~ spl490_10
| ~ spl490_53 ),
inference(forward_demodulation,[],[f23530,f21393]) ).
fof(f23532,plain,
( spl490_12
| ~ spl490_11
| ~ spl490_9
| spl490_124
| ~ spl490_10
| ~ spl490_53 ),
inference(avatar_split_clause,[],[f23531,f21845,f21485,f22627,f21481,f21489,f21493]) ).
fof(f23727,plain,
( ! [X2,X3,X0,X1,X4] :
( k2_funct_2(u1_struct_0(X0),u1_struct_0(sK30),X1,u1_struct_0(X2)) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK30)))
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(resolution,[],[f17443,f21486]) ).
fof(f23730,plain,
( ! [X2,X3,X0,X1,X4] :
( k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(sK30)))
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23727,f21393]) ).
fof(f23731,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23730,f21393]) ).
fof(f23732,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(sF487))
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23731,f21399]) ).
fof(f23733,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23732,f21401]) ).
fof(f23734,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),u1_struct_0(sF487))
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23733,f21399]) ).
fof(f23735,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(X0),u1_struct_0(sK30))
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23734,f21401]) ).
fof(f23736,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X1,u1_struct_0(X0),sF484)
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(X0),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23735,f21393]) ).
fof(f23737,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X1,u1_struct_0(X0),sF484)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF484)
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X1)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ l1_group_1(sK30)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23736,f21393]) ).
fof(f23739,definition,
( spl490_233
<=> ! [X4,X0,X3,X2,X1] :
( ~ m2_relset_1(X1,u1_struct_0(X0),sF484)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X4)
| k3_latsubgr(X0,sK30,X1) != X4
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF484) ) ),
introduced(definition,[new_symbols(definition,[spl490_233])],[avatar_definition]) ).
fof(f23740,plain,
( ! [X2,X3,X0,X1,X4] :
( k3_latsubgr(X0,sK30,X1) != X4
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k1_funct_1(X4,X2) = k5_group_4(sK30,X3)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X1,u1_struct_0(X0),sF484)
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| k2_funct_2(u1_struct_0(X0),sF484,X1,u1_struct_0(X2)) != X3
| ~ m1_subset_1(X3,k1_zfmisc_1(sF484))
| ~ v1_funct_2(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ m2_relset_1(X4,u1_struct_0(k11_group_4(X0)),sF488)
| ~ v1_funct_2(X1,u1_struct_0(X0),sF484) )
| ~ spl490_233 ),
inference(avatar_component_clause,[],[f23739]) ).
fof(f23741,plain,
( ~ spl490_9
| ~ spl490_11
| spl490_12
| spl490_233
| ~ spl490_10 ),
inference(avatar_split_clause,[],[f23737,f21485,f23739,f21493,f21489,f21481]) ).
fof(f23995,plain,
( ! [X0] :
( v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK30)))
| ~ l1_group_1(sK30)
| ~ m1_group_2(X0,sK30) )
| ~ spl490_10 ),
inference(resolution,[],[f22220,f21486]) ).
fof(f23996,plain,
( ! [X0] :
( m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(sF484))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ m1_group_2(X0,sK30) )
| ~ spl490_10 ),
inference(forward_demodulation,[],[f23995,f21393]) ).
fof(f23997,plain,
( ~ spl490_9
| ~ spl490_11
| spl490_12
| spl490_85
| ~ spl490_10 ),
inference(avatar_split_clause,[],[f23996,f21485,f22230,f21493,f21489,f21481]) ).
fof(f24780,plain,
( ~ v1_funct_1(sF485)
| v1_funct_1(k3_latsubgr(sK30,sK30,sF485))
| ~ m1_relset_1(sF485,sF484,sF484)
| ~ spl490_21
| ~ spl490_124 ),
inference(resolution,[],[f22628,f21568]) ).
fof(f24781,plain,
( v1_funct_1(sF486)
| ~ v1_funct_1(sF485)
| ~ m1_relset_1(sF485,sF484,sF484)
| ~ spl490_21
| ~ spl490_124 ),
inference(forward_demodulation,[],[f24780,f21397]) ).
fof(f24782,plain,
( ~ spl490_22
| ~ spl490_19
| spl490_203
| ~ spl490_21
| ~ spl490_124 ),
inference(avatar_split_clause,[],[f24781,f22627,f21567,f23475,f21559,f21571]) ).
fof(f25852,definition,
( spl490_384
<=> ! [X0,X1] :
( ~ v1_funct_2(X0,sF484,sF484)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF484,sF484)
| ~ m2_relset_1(X1,sF488,sF488)
| ~ v1_funct_2(X1,sF488,sF488) ) ),
introduced(definition,[new_symbols(definition,[spl490_384])],[avatar_definition]) ).
fof(f25853,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF484,sF484)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,sF484,sF484)
| ~ m2_relset_1(X1,sF488,sF488)
| ~ v1_funct_2(X1,sF488,sF488) )
| ~ spl490_384 ),
inference(avatar_component_clause,[],[f25852]) ).
fof(f25891,plain,
( ! [X0,X1] :
( ~ l1_group_1(sK30)
| ~ m2_relset_1(X0,sF484,u1_struct_0(sK30))
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ v1_funct_2(X1,sF488,u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X1,sF488,u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30)) )
| ~ spl490_10
| ~ spl490_87 ),
inference(resolution,[],[f22262,f21486]) ).
fof(f25893,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X0,sF484,sF484)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ v1_funct_2(X1,sF488,u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(X1,sF488,u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30)) )
| ~ spl490_10
| ~ spl490_87 ),
inference(forward_demodulation,[],[f25891,f21393]) ).
fof(f25894,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF488,u1_struct_0(sF487))
| ~ m2_relset_1(X0,sF484,sF484)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ m2_relset_1(X1,sF488,u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30)) )
| ~ spl490_10
| ~ spl490_87 ),
inference(forward_demodulation,[],[f25893,f21399]) ).
fof(f25895,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF488,sF488)
| ~ m2_relset_1(X0,sF484,sF484)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ m2_relset_1(X1,sF488,u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30)) )
| ~ spl490_10
| ~ spl490_87 ),
inference(forward_demodulation,[],[f25894,f21401]) ).
fof(f25896,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X1,sF488,u1_struct_0(sF487))
| ~ v1_funct_2(X1,sF488,sF488)
| ~ m2_relset_1(X0,sF484,sF484)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30)) )
| ~ spl490_10
| ~ spl490_87 ),
inference(forward_demodulation,[],[f25895,f21399]) ).
fof(f25897,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X1,sF488,sF488)
| ~ v1_funct_2(X1,sF488,sF488)
| ~ m2_relset_1(X0,sF484,sF484)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30)
| ~ v1_funct_2(X0,sF484,u1_struct_0(sK30)) )
| ~ spl490_10
| ~ spl490_87 ),
inference(forward_demodulation,[],[f25896,f21401]) ).
fof(f25898,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF484,sF484)
| ~ m2_relset_1(X1,sF488,sF488)
| ~ v1_funct_2(X1,sF488,sF488)
| ~ m2_relset_1(X0,sF484,sF484)
| ~ l1_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,X0) = X1
| ~ v1_funct_1(X1)
| m1_group_2(sK32(sK30,sK30,X0,X1),sK30) )
| ~ spl490_10
| ~ spl490_87 ),
inference(forward_demodulation,[],[f25897,f21393]) ).
fof(f25899,plain,
( spl490_12
| ~ spl490_11
| ~ spl490_9
| spl490_384
| ~ spl490_10
| ~ spl490_87 ),
inference(avatar_split_clause,[],[f25898,f22261,f21485,f25852,f21481,f21489,f21493]) ).
fof(f28341,definition,
( spl490_494
<=> m2_relset_1(sF489,sF488,sF488) ),
introduced(definition,[new_symbols(definition,[spl490_494])],[avatar_definition]) ).
fof(f30475,plain,
( ! [X0] :
( m1_group_2(sK32(sK30,sK30,sF485,X0),sK30)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK30,sK30,sF485) = X0
| ~ v1_funct_1(sF485)
| ~ m2_relset_1(sF485,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488)
| ~ v1_funct_2(X0,sF488,sF488) )
| ~ spl490_21
| ~ spl490_384 ),
inference(resolution,[],[f25853,f21568]) ).
fof(f30476,plain,
( ! [X0] :
( sF486 = X0
| m1_group_2(sK32(sK30,sK30,sF485,X0),sK30)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sF485)
| ~ m2_relset_1(sF485,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488)
| ~ v1_funct_2(X0,sF488,sF488) )
| ~ spl490_21
| ~ spl490_384 ),
inference(forward_demodulation,[],[f30475,f21397]) ).
fof(f30478,definition,
( spl490_707
<=> ! [X0] :
( sF486 = X0
| ~ v1_funct_2(X0,sF488,sF488)
| ~ m2_relset_1(X0,sF488,sF488)
| ~ v1_funct_1(X0)
| m1_group_2(sK32(sK30,sK30,sF485,X0),sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_707])],[avatar_definition]) ).
fof(f30479,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF488,sF488)
| sF486 = X0
| ~ m2_relset_1(X0,sF488,sF488)
| ~ v1_funct_1(X0)
| m1_group_2(sK32(sK30,sK30,sF485,X0),sK30) )
| ~ spl490_707 ),
inference(avatar_component_clause,[],[f30478]) ).
fof(f30480,plain,
( ~ spl490_55
| ~ spl490_19
| spl490_707
| ~ spl490_21
| ~ spl490_384 ),
inference(avatar_split_clause,[],[f30476,f25852,f21567,f30478,f21559,f21863]) ).
fof(f32308,plain,
( ! [X2,X0,X1] :
( sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(sF485,u1_struct_0(sK30),sF484)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| k2_funct_2(u1_struct_0(sK30),sF484,sF485,u1_struct_0(X1)) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_funct_2(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(superposition,[],[f23740,f21397]) ).
fof(f32310,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| k2_funct_2(u1_struct_0(sK30),sF484,sF485,u1_struct_0(X1)) != X2
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_funct_2(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32308,f21393]) ).
fof(f32311,plain,
( ! [X2,X0,X1] :
( k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_funct_2(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32310,f21393]) ).
fof(f32312,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(sF487),sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32311,f21399]) ).
fof(f32313,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(X0,sF488,sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ m2_relset_1(X0,u1_struct_0(k11_group_4(sK30)),sF488)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32312,f21401]) ).
fof(f32314,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X0,u1_struct_0(sF487),sF488)
| ~ v1_funct_2(X0,sF488,sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32313,f21399]) ).
fof(f32315,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF488,sF488)
| ~ v1_funct_2(X0,sF488,sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_funct_2(sF485,u1_struct_0(sK30),sF484) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32314,f21401]) ).
fof(f32316,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(sF485,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488)
| ~ v1_funct_2(X0,sF488,sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ m2_relset_1(sF485,sF484,sF484)
| sF486 != X0
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ v1_funct_1(sF485)
| ~ v1_funct_1(X0)
| ~ m1_group_2(X1,sK30)
| ~ v1_group_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484)) )
| ~ spl490_233 ),
inference(forward_demodulation,[],[f32315,f21393]) ).
fof(f32318,definition,
( spl490_863
<=> ! [X2,X0,X1] :
( ~ m2_relset_1(X0,sF488,sF488)
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK30)
| ~ v1_funct_1(X0)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| sF486 != X0
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ v1_funct_2(X0,sF488,sF488) ) ),
introduced(definition,[new_symbols(definition,[spl490_863])],[avatar_definition]) ).
fof(f32319,plain,
( ! [X2,X0,X1] :
( sF486 != X0
| ~ m1_subset_1(X2,k1_zfmisc_1(sF484))
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK30)
| ~ v1_funct_1(X0)
| k1_funct_1(X0,X1) = k5_group_4(sK30,X2)
| ~ m2_relset_1(X0,sF488,sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X2
| ~ v1_funct_2(X0,sF488,sF488) )
| ~ spl490_863 ),
inference(avatar_component_clause,[],[f32318]) ).
fof(f32320,plain,
( ~ spl490_19
| spl490_12
| ~ spl490_11
| ~ spl490_10
| ~ spl490_9
| ~ spl490_55
| spl490_863
| ~ spl490_21
| ~ spl490_233 ),
inference(avatar_split_clause,[],[f32316,f23739,f21567,f32318,f21863,f21481,f21485,f21489,f21493,f21559]) ).
fof(f32321,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK30)
| ~ v1_funct_1(sF486)
| k5_group_4(sK30,X0) = k1_funct_1(sF486,X1)
| ~ m2_relset_1(sF486,sF488,sF488)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X0
| ~ v1_funct_2(sF486,sF488,sF488) )
| ~ spl490_863 ),
inference(equality_resolution,[],[f32319]) ).
fof(f32323,definition,
( spl490_864
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X0
| k5_group_4(sK30,X0) = k1_funct_1(sF486,X1)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_864])],[avatar_definition]) ).
fof(f32324,plain,
( ! [X0,X1] :
( ~ v1_group_1(X1)
| k2_funct_2(sF484,sF484,sF485,u1_struct_0(X1)) != X0
| k5_group_4(sK30,X0) = k1_funct_1(sF486,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| ~ m1_group_2(X1,sK30) )
| ~ spl490_864 ),
inference(avatar_component_clause,[],[f32323]) ).
fof(f32325,plain,
( ~ spl490_20
| ~ spl490_26
| ~ spl490_203
| spl490_864
| ~ spl490_863 ),
inference(avatar_split_clause,[],[f32321,f32318,f32323,f23475,f21616,f21563]) ).
fof(f34351,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,u1_struct_0(sF487),sF488)
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(u1_struct_0(sK30),sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ m2_relset_1(X1,u1_struct_0(sK30),sF484)
| ~ m2_relset_1(X0,u1_struct_0(sF487),sF488)
| ~ v1_funct_2(X1,u1_struct_0(sK30),sF484) )
| ~ spl490_136 ),
inference(superposition,[],[f22807,f21399]) ).
fof(f34355,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X0,sF488,sF488)
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(u1_struct_0(sK30),sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ m2_relset_1(X1,u1_struct_0(sK30),sF484)
| ~ m2_relset_1(X0,u1_struct_0(sF487),sF488)
| ~ v1_funct_2(X1,u1_struct_0(sK30),sF484) )
| ~ spl490_136 ),
inference(forward_demodulation,[],[f34351,f21401]) ).
fof(f34356,plain,
( ! [X0,X1] :
( sK33(sK30,sK30,X1,X0) = k2_funct_2(sF484,sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ v1_funct_2(X0,sF488,sF488)
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X1,u1_struct_0(sK30),sF484)
| ~ m2_relset_1(X0,u1_struct_0(sF487),sF488)
| ~ v1_funct_2(X1,u1_struct_0(sK30),sF484) )
| ~ spl490_136 ),
inference(forward_demodulation,[],[f34355,f21393]) ).
fof(f34357,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X1,sF484,sF484)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(sF484,sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ v1_funct_2(X0,sF488,sF488)
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(sF487),sF488)
| ~ v1_funct_2(X1,u1_struct_0(sK30),sF484) )
| ~ spl490_136 ),
inference(forward_demodulation,[],[f34356,f21393]) ).
fof(f34358,plain,
( ! [X0,X1] :
( ~ m2_relset_1(X0,sF488,sF488)
| ~ m2_relset_1(X1,sF484,sF484)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(sF484,sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ v1_funct_2(X0,sF488,sF488)
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X1,u1_struct_0(sK30),sF484) )
| ~ spl490_136 ),
inference(forward_demodulation,[],[f34357,f21401]) ).
fof(f34359,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488)
| ~ m2_relset_1(X1,sF484,sF484)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(sF484,sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ v1_funct_2(X0,sF488,sF488)
| ~ l1_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ v3_group_1(sK30)
| v3_struct_0(sK30)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0) )
| ~ spl490_136 ),
inference(forward_demodulation,[],[f34358,f21393]) ).
fof(f34361,definition,
( spl490_947
<=> ! [X0,X1] :
( ~ v1_funct_2(X1,sF484,sF484)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_2(X0,sF488,sF488)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(sF484,sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ m2_relset_1(X1,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488) ) ),
introduced(definition,[new_symbols(definition,[spl490_947])],[avatar_definition]) ).
fof(f34362,plain,
( ! [X0,X1] :
( ~ v1_funct_2(X1,sF484,sF484)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK30,sK30,X1) = X0
| ~ v1_funct_2(X0,sF488,sF488)
| sK33(sK30,sK30,X1,X0) = k2_funct_2(sF484,sF484,X1,u1_struct_0(sK32(sK30,sK30,X1,X0)))
| ~ m2_relset_1(X1,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488) )
| ~ spl490_947 ),
inference(avatar_component_clause,[],[f34361]) ).
fof(f34363,plain,
( spl490_12
| ~ spl490_11
| ~ spl490_10
| ~ spl490_9
| spl490_947
| ~ spl490_136 ),
inference(avatar_split_clause,[],[f34359,f22806,f34361,f21481,f21485,f21489,f21493]) ).
fof(f34364,plain,
( ! [X0] :
( ~ v1_funct_1(X0)
| ~ v1_funct_1(sF485)
| k3_latsubgr(sK30,sK30,sF485) = X0
| ~ v1_funct_2(X0,sF488,sF488)
| sK33(sK30,sK30,sF485,X0) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,X0)))
| ~ m2_relset_1(sF485,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488) )
| ~ spl490_21
| ~ spl490_947 ),
inference(resolution,[],[f34362,f21568]) ).
fof(f34365,plain,
( ! [X0] :
( sF486 = X0
| ~ v1_funct_1(X0)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(X0,sF488,sF488)
| sK33(sK30,sK30,sF485,X0) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,X0)))
| ~ m2_relset_1(sF485,sF484,sF484)
| ~ m2_relset_1(X0,sF488,sF488) )
| ~ spl490_21
| ~ spl490_947 ),
inference(forward_demodulation,[],[f34364,f21397]) ).
fof(f34367,definition,
( spl490_948
<=> ! [X0] :
( sF486 = X0
| ~ m2_relset_1(X0,sF488,sF488)
| sK33(sK30,sK30,sF485,X0) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,X0)))
| ~ v1_funct_2(X0,sF488,sF488)
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl490_948])],[avatar_definition]) ).
fof(f34368,plain,
( ! [X0] :
( ~ v1_funct_2(X0,sF488,sF488)
| ~ m2_relset_1(X0,sF488,sF488)
| sK33(sK30,sK30,sF485,X0) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,X0)))
| sF486 = X0
| ~ v1_funct_1(X0) )
| ~ spl490_948 ),
inference(avatar_component_clause,[],[f34367]) ).
fof(f34369,plain,
( ~ spl490_55
| ~ spl490_19
| spl490_948
| ~ spl490_21
| ~ spl490_947 ),
inference(avatar_split_clause,[],[f34365,f34361,f21567,f34367,f21559,f21863]) ).
fof(f36636,plain,
( ~ v1_relat_1(sF489)
| v1_funct_2(sF489,k1_relat_1(sF489),k2_relat_1(sF489))
| ~ spl490_99 ),
inference(resolution,[],[f17679,f22438]) ).
fof(f36637,plain,
( v1_funct_2(sF489,k1_relat_1(sF489),sF488)
| ~ v1_relat_1(sF489)
| ~ spl490_99 ),
inference(forward_demodulation,[],[f36636,f21627]) ).
fof(f36645,plain,
( v1_funct_2(sF489,sF488,sF488)
| ~ v1_relat_1(sF489)
| ~ spl490_99 ),
inference(forward_demodulation,[],[f36637,f21588]) ).
fof(f36649,definition,
( spl490_1149
<=> v1_funct_2(sF489,sF488,sF488) ),
introduced(definition,[new_symbols(definition,[spl490_1149])],[avatar_definition]) ).
fof(f36651,plain,
( v1_funct_2(sF489,sF488,sF488)
| ~ spl490_1149 ),
inference(avatar_component_clause,[],[f36649]) ).
fof(f36652,plain,
( ~ spl490_61
| spl490_1149
| ~ spl490_99 ),
inference(avatar_split_clause,[],[f36645,f22437,f36649,f21910]) ).
fof(f36653,plain,
( ~ m2_relset_1(sF489,sF488,sF488)
| sK33(sK30,sK30,sF485,sF489) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489)))
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ spl490_948
| ~ spl490_1149 ),
inference(resolution,[],[f36651,f34368]) ).
fof(f36654,plain,
( sF486 = sF489
| ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_1(sF489)
| m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30)
| ~ spl490_707
| ~ spl490_1149 ),
inference(resolution,[],[f36651,f30479]) ).
fof(f36656,definition,
( spl490_1150
<=> m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30) ),
introduced(definition,[new_symbols(definition,[spl490_1150])],[avatar_definition]) ).
fof(f36660,definition,
( spl490_1151
<=> sF486 = sF489 ),
introduced(definition,[new_symbols(definition,[spl490_1151])],[avatar_definition]) ).
fof(f36663,plain,
( spl490_1150
| ~ spl490_99
| ~ spl490_494
| spl490_1151
| ~ spl490_707
| ~ spl490_1149 ),
inference(avatar_split_clause,[],[f36654,f36649,f30478,f36660,f28341,f22437,f36656]) ).
fof(f36665,definition,
( spl490_1152
<=> sK33(sK30,sK30,sF485,sF489) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489))) ),
introduced(definition,[new_symbols(definition,[spl490_1152])],[avatar_definition]) ).
fof(f36667,plain,
( sK33(sK30,sK30,sF485,sF489) = k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489)))
| ~ spl490_1152 ),
inference(avatar_component_clause,[],[f36665]) ).
fof(f36668,plain,
( ~ spl490_99
| spl490_1151
| spl490_1152
| ~ spl490_494
| ~ spl490_948
| ~ spl490_1149 ),
inference(avatar_split_clause,[],[f36653,f36649,f34367,f28341,f36665,f36660,f22437]) ).
fof(f38091,plain,
spl490_494,
inference(avatar_split_clause,[],[f21930,f28341]) ).
fof(f38220,plain,
~ spl490_1151,
inference(avatar_split_clause,[],[f21404,f36660]) ).
fof(f38269,plain,
( sK33(sK30,sK30,sF485,sF489) = k9_relat_1(sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,sF484,sF484)
| ~ m1_relset_1(sF485,sF484,sF484)
| ~ spl490_1152 ),
inference(superposition,[],[f36667,f18663]) ).
fof(f38274,definition,
( spl490_1224
<=> sK33(sK30,sK30,sF485,sF489) = k9_relat_1(sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489))) ),
introduced(definition,[new_symbols(definition,[spl490_1224])],[avatar_definition]) ).
fof(f38276,plain,
( sK33(sK30,sK30,sF485,sF489) = k9_relat_1(sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489)))
| ~ spl490_1224 ),
inference(avatar_component_clause,[],[f38274]) ).
fof(f38279,plain,
( ~ spl490_22
| ~ spl490_21
| ~ spl490_19
| spl490_1224
| ~ spl490_1152 ),
inference(avatar_split_clause,[],[f38269,f36665,f38274,f21559,f21567,f21571]) ).
fof(f38287,definition,
( spl490_1225
<=> r2_hidden(sK32(sK30,sK30,sF485,sF489),sF488) ),
introduced(definition,[new_symbols(definition,[spl490_1225])],[avatar_definition]) ).
fof(f38289,plain,
( ~ r2_hidden(sK32(sK30,sK30,sF485,sF489),sF488)
| spl490_1225 ),
inference(avatar_component_clause,[],[f38287]) ).
fof(f38291,definition,
( spl490_1226
<=> ! [X0] :
( sK33(sK30,sK30,sF485,sF489) != X0
| k5_group_4(sK30,X0) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484)) ) ),
introduced(definition,[new_symbols(definition,[spl490_1226])],[avatar_definition]) ).
fof(f38292,plain,
( ! [X0] :
( sK33(sK30,sK30,sF485,sF489) != X0
| k5_group_4(sK30,X0) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484)) )
| ~ spl490_1226 ),
inference(avatar_component_clause,[],[f38291]) ).
fof(f38294,plain,
( sK33(sK30,sK30,sF485,sF489) = u1_struct_0(sK32(sK30,sK30,sF485,sF489))
| ~ m1_subset_1(u1_struct_0(sK32(sK30,sK30,sF485,sF489)),k1_zfmisc_1(sF484))
| ~ spl490_1224 ),
inference(superposition,[],[f38276,f21579]) ).
fof(f38328,definition,
( spl490_1231
<=> m1_subset_1(u1_struct_0(sK32(sK30,sK30,sF485,sF489)),k1_zfmisc_1(sF484)) ),
introduced(definition,[new_symbols(definition,[spl490_1231])],[avatar_definition]) ).
fof(f38330,plain,
( ~ m1_subset_1(u1_struct_0(sK32(sK30,sK30,sF485,sF489)),k1_zfmisc_1(sF484))
| spl490_1231 ),
inference(avatar_component_clause,[],[f38328]) ).
fof(f38332,definition,
( spl490_1232
<=> sK33(sK30,sK30,sF485,sF489) = u1_struct_0(sK32(sK30,sK30,sF485,sF489)) ),
introduced(definition,[new_symbols(definition,[spl490_1232])],[avatar_definition]) ).
fof(f38334,plain,
( sK33(sK30,sK30,sF485,sF489) = u1_struct_0(sK32(sK30,sK30,sF485,sF489))
| ~ spl490_1232 ),
inference(avatar_component_clause,[],[f38332]) ).
fof(f38336,plain,
( ~ spl490_1231
| spl490_1232
| ~ spl490_1224 ),
inference(avatar_split_clause,[],[f38294,f38274,f38332,f38328]) ).
fof(f38337,plain,
( ~ v1_group_1(sK32(sK30,sK30,sF485,sF489))
| ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30)
| ~ spl490_60
| spl490_1225 ),
inference(resolution,[],[f38289,f21903]) ).
fof(f38356,definition,
( spl490_1234
<=> v1_group_1(sK32(sK30,sK30,sF485,sF489)) ),
introduced(definition,[new_symbols(definition,[spl490_1234])],[avatar_definition]) ).
fof(f38357,plain,
( v1_group_1(sK32(sK30,sK30,sF485,sF489))
| ~ spl490_1234 ),
inference(avatar_component_clause,[],[f38356]) ).
fof(f38358,plain,
( ~ v1_group_1(sK32(sK30,sK30,sF485,sF489))
| spl490_1234 ),
inference(avatar_component_clause,[],[f38356]) ).
fof(f38359,plain,
( ~ spl490_1150
| ~ spl490_1234
| ~ spl490_60
| spl490_1225 ),
inference(avatar_split_clause,[],[f38337,f38287,f21900,f38356,f36656]) ).
fof(f38362,plain,
( k3_latsubgr(sK30,sK30,sF485) = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_2(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(resolution,[],[f38358,f17445]) ).
fof(f38364,plain,
( k3_latsubgr(sK30,sK30,sF485) = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_2(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(duplicate_literal_removal,[],[f38362]) ).
fof(f38365,plain,
( sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_2(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38364,f21397]) ).
fof(f38366,plain,
( ~ v1_funct_2(sF489,u1_struct_0(sF487),u1_struct_0(sF487))
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38365,f21399]) ).
fof(f38367,plain,
( ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38366,f21401]) ).
fof(f38368,plain,
( ~ m2_relset_1(sF489,u1_struct_0(sF487),u1_struct_0(sF487))
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38367,f21399]) ).
fof(f38369,plain,
( ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38368,f21401]) ).
fof(f38370,plain,
( ~ v1_funct_2(sF485,sF484,sF484)
| ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38369,f21393]) ).
fof(f38371,plain,
( ~ m2_relset_1(sF485,sF484,sF484)
| ~ v1_funct_2(sF485,sF484,sF484)
| ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| spl490_1234 ),
inference(forward_demodulation,[],[f38370,f21393]) ).
fof(f38372,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_19
| ~ spl490_99
| spl490_1151
| ~ spl490_1149
| ~ spl490_494
| ~ spl490_21
| ~ spl490_55
| spl490_1234 ),
inference(avatar_split_clause,[],[f38371,f38356,f21863,f21567,f28341,f36649,f36660,f22437,f21559,f21493,f21489,f21485,f21481]) ).
fof(f38382,plain,
( ! [X0] :
( k2_funct_2(sF484,sF484,sF485,u1_struct_0(sK32(sK30,sK30,sF485,sF489))) != X0
| k5_group_4(sK30,X0) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30) )
| ~ spl490_864
| ~ spl490_1234 ),
inference(resolution,[],[f38357,f32324]) ).
fof(f38406,plain,
( ! [X0] :
( sK33(sK30,sK30,sF485,sF489) != X0
| k5_group_4(sK30,X0) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ m1_subset_1(X0,k1_zfmisc_1(sF484))
| ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30) )
| ~ spl490_864
| ~ spl490_1152
| ~ spl490_1234 ),
inference(forward_demodulation,[],[f38382,f36667]) ).
fof(f38412,plain,
( ~ spl490_1150
| spl490_1226
| ~ spl490_864
| ~ spl490_1152
| ~ spl490_1234 ),
inference(avatar_split_clause,[],[f38406,f38356,f36665,f32323,f38291,f36656]) ).
fof(f38415,plain,
( k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = k5_group_4(sK30,sK33(sK30,sK30,sF485,sF489))
| ~ m1_subset_1(sK33(sK30,sK30,sF485,sF489),k1_zfmisc_1(sF484))
| ~ spl490_1226 ),
inference(equality_resolution,[],[f38292]) ).
fof(f38417,definition,
( spl490_1240
<=> m1_subset_1(sK33(sK30,sK30,sF485,sF489),k1_zfmisc_1(sF484)) ),
introduced(definition,[new_symbols(definition,[spl490_1240])],[avatar_definition]) ).
fof(f38421,definition,
( spl490_1241
<=> k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = k5_group_4(sK30,sK33(sK30,sK30,sF485,sF489)) ),
introduced(definition,[new_symbols(definition,[spl490_1241])],[avatar_definition]) ).
fof(f38423,plain,
( k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = k5_group_4(sK30,sK33(sK30,sK30,sF485,sF489))
| ~ spl490_1241 ),
inference(avatar_component_clause,[],[f38421]) ).
fof(f38424,plain,
( ~ spl490_1240
| spl490_1241
| ~ spl490_1226 ),
inference(avatar_split_clause,[],[f38415,f38291,f38421,f38417]) ).
fof(f39295,plain,
( v1_group_1(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)))
| ~ m1_subset_1(sK33(sK30,sK30,sF485,sF489),k1_zfmisc_1(sF484))
| ~ spl490_42
| ~ spl490_1241 ),
inference(superposition,[],[f21738,f38423]) ).
fof(f39296,plain,
( m1_group_2(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),sK30)
| ~ m1_subset_1(sK33(sK30,sK30,sF485,sF489),k1_zfmisc_1(sF484))
| ~ spl490_119
| ~ spl490_1241 ),
inference(superposition,[],[f22552,f38423]) ).
fof(f39298,plain,
( ! [X0] :
( r1_group_2(sK30,k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),X0)
| ~ m1_subset_1(sK33(sK30,sK30,sF485,sF489),k1_zfmisc_1(sF484))
| ~ m1_group_2(X0,sK30)
| ~ v1_group_1(X0)
| u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489) )
| ~ spl490_134
| ~ spl490_1241 ),
inference(superposition,[],[f22787,f38423]) ).
fof(f39307,plain,
( k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| k3_latsubgr(sK30,sK30,sF485) = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_2(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(superposition,[],[f17448,f38423]) ).
fof(f39310,plain,
( k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| k3_latsubgr(sK30,sK30,sF485) = sF489
| ~ v1_funct_1(sF489)
| ~ v1_funct_2(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(duplicate_literal_removal,[],[f39307]) ).
fof(f39313,plain,
( sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ v1_funct_2(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39310,f21397]) ).
fof(f39331,definition,
( spl490_1392
<=> m1_group_2(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),sK30) ),
introduced(definition,[new_symbols(definition,[spl490_1392])],[avatar_definition]) ).
fof(f39353,definition,
( spl490_1397
<=> ! [X0] :
( k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = X0
| ~ v1_group_1(X0)
| u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489)
| ~ m1_group_2(X0,sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_1397])],[avatar_definition]) ).
fof(f39354,plain,
( ! [X0] :
( u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489)
| ~ v1_group_1(X0)
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = X0
| ~ m1_group_2(X0,sK30) )
| ~ spl490_1397 ),
inference(avatar_component_clause,[],[f39353]) ).
fof(f39356,definition,
( spl490_1398
<=> v1_group_1(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))) ),
introduced(definition,[new_symbols(definition,[spl490_1398])],[avatar_definition]) ).
fof(f39361,definition,
( spl490_1399
<=> ! [X0] :
( r1_group_2(sK30,k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),X0)
| u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30) ) ),
introduced(definition,[new_symbols(definition,[spl490_1399])],[avatar_definition]) ).
fof(f39362,plain,
( ! [X0] :
( r1_group_2(sK30,k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),X0)
| u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30) )
| ~ spl490_1399 ),
inference(avatar_component_clause,[],[f39361]) ).
fof(f39363,plain,
( ~ spl490_1240
| spl490_1399
| ~ spl490_134
| ~ spl490_1241 ),
inference(avatar_split_clause,[],[f39298,f38421,f22786,f39361,f38417]) ).
fof(f39369,plain,
( ~ spl490_1240
| spl490_1392
| ~ spl490_119
| ~ spl490_1241 ),
inference(avatar_split_clause,[],[f39296,f38421,f22551,f39331,f38417]) ).
fof(f39370,plain,
( ~ spl490_1240
| spl490_1398
| ~ spl490_42
| ~ spl490_1241 ),
inference(avatar_split_clause,[],[f39295,f38421,f21737,f39356,f38417]) ).
fof(f39376,plain,
( ~ v1_funct_2(sF489,u1_struct_0(sF487),u1_struct_0(sF487))
| sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39313,f21399]) ).
fof(f39381,plain,
( ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ m2_relset_1(sF489,u1_struct_0(k11_group_4(sK30)),u1_struct_0(k11_group_4(sK30)))
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39376,f21401]) ).
fof(f39382,plain,
( ~ m2_relset_1(sF489,u1_struct_0(sF487),u1_struct_0(sF487))
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39381,f21399]) ).
fof(f39383,plain,
( ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| ~ v1_funct_2(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39382,f21401]) ).
fof(f39384,plain,
( ~ v1_funct_2(sF485,sF484,sF484)
| ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| ~ m2_relset_1(sF485,u1_struct_0(sK30),u1_struct_0(sK30))
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39383,f21393]) ).
fof(f39385,plain,
( ~ m2_relset_1(sF485,sF484,sF484)
| ~ v1_funct_2(sF485,sF484,sF484)
| ~ m2_relset_1(sF489,sF488,sF488)
| ~ v1_funct_2(sF489,sF488,sF488)
| sF486 = sF489
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| ~ v1_funct_1(sF489)
| ~ v1_funct_1(sF485)
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ spl490_1241 ),
inference(forward_demodulation,[],[f39384,f21393]) ).
fof(f39387,definition,
( spl490_1403
<=> k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489)) ),
introduced(definition,[new_symbols(definition,[spl490_1403])],[avatar_definition]) ).
fof(f39389,plain,
( k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) != k1_funct_1(sF489,sK32(sK30,sK30,sF485,sF489))
| spl490_1403 ),
inference(avatar_component_clause,[],[f39387]) ).
fof(f39390,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_19
| ~ spl490_99
| ~ spl490_1403
| spl490_1151
| ~ spl490_1149
| ~ spl490_494
| ~ spl490_21
| ~ spl490_55
| ~ spl490_1241 ),
inference(avatar_split_clause,[],[f39385,f38421,f21863,f21567,f28341,f36649,f36660,f39387,f22437,f21559,f21493,f21489,f21485,f21481]) ).
fof(f39400,plain,
( sK32(sK30,sK30,sF485,sF489) != k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ r2_hidden(sK32(sK30,sK30,sF485,sF489),sF488)
| spl490_1403 ),
inference(superposition,[],[f39389,f21576]) ).
fof(f39402,definition,
( spl490_1404
<=> sK32(sK30,sK30,sF485,sF489) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) ),
introduced(definition,[new_symbols(definition,[spl490_1404])],[avatar_definition]) ).
fof(f39405,plain,
( ~ spl490_1225
| ~ spl490_1404
| spl490_1403 ),
inference(avatar_split_clause,[],[f39400,f39387,f39402,f38287]) ).
fof(f45278,plain,
( ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30)
| ~ spl490_85
| spl490_1231 ),
inference(resolution,[],[f38330,f22231]) ).
fof(f45284,plain,
( ~ spl490_1150
| ~ spl490_85
| spl490_1231 ),
inference(avatar_split_clause,[],[f45278,f38328,f22230,f36656]) ).
fof(f45313,plain,
( m1_subset_1(sK33(sK30,sK30,sF485,sF489),k1_zfmisc_1(sF484))
| ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30)
| ~ spl490_85
| ~ spl490_1232 ),
inference(superposition,[],[f22231,f38334]) ).
fof(f45371,plain,
( ~ spl490_1150
| spl490_1240
| ~ spl490_85
| ~ spl490_1232 ),
inference(avatar_split_clause,[],[f45313,f38332,f22230,f38417,f36656]) ).
fof(f45661,plain,
( ! [X0] :
( u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30)
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = X0
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_group_1(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)))
| ~ m1_group_2(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),sK30)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30) )
| ~ spl490_1399 ),
inference(resolution,[],[f39362,f20158]) ).
fof(f45662,plain,
( ! [X0] :
( u1_struct_0(X0) != sK33(sK30,sK30,sF485,sF489)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK30)
| k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)) = X0
| v3_struct_0(sK30)
| ~ v3_group_1(sK30)
| ~ v4_group_1(sK30)
| ~ l1_group_1(sK30)
| ~ v1_group_1(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)))
| ~ m1_group_2(k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489)),sK30) )
| ~ spl490_1399 ),
inference(duplicate_literal_removal,[],[f45661]) ).
fof(f45663,plain,
( ~ spl490_1392
| ~ spl490_1398
| ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_1397
| ~ spl490_1399 ),
inference(avatar_split_clause,[],[f45662,f39361,f39353,f21493,f21489,f21485,f21481,f39356,f39331]) ).
fof(f45666,plain,
( sK33(sK30,sK30,sF485,sF489) != sK33(sK30,sK30,sF485,sF489)
| ~ v1_group_1(sK32(sK30,sK30,sF485,sF489))
| sK32(sK30,sK30,sF485,sF489) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30)
| ~ spl490_1232
| ~ spl490_1397 ),
inference(superposition,[],[f39354,f38334]) ).
fof(f45667,plain,
( ~ v1_group_1(sK32(sK30,sK30,sF485,sF489))
| sK32(sK30,sK30,sF485,sF489) = k1_funct_1(sF486,sK32(sK30,sK30,sF485,sF489))
| ~ m1_group_2(sK32(sK30,sK30,sF485,sF489),sK30)
| ~ spl490_1232
| ~ spl490_1397 ),
inference(trivial_inequality_removal,[],[f45666]) ).
fof(f45668,plain,
( ~ spl490_1150
| spl490_1404
| ~ spl490_1234
| ~ spl490_1232
| ~ spl490_1397 ),
inference(avatar_split_clause,[],[f45667,f39353,f38332,f38356,f39402,f36656]) ).
cnf(s8,plain,
spl490_9,
inference(sat_conversion,[],[f21503]) ).
cnf(s10,plain,
spl490_10,
inference(sat_conversion,[],[f21506]) ).
cnf(s12,plain,
spl490_11,
inference(sat_conversion,[],[f21509]) ).
cnf(s13,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_14 ),
inference(sat_conversion,[],[f21516]) ).
cnf(s15,plain,
~ spl490_12,
inference(sat_conversion,[],[f21519]) ).
cnf(s24,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_19
| ~ spl490_21
| ~ spl490_22
| spl490_26 ),
inference(sat_conversion,[],[f21619]) ).
cnf(s31,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_21 ),
inference(sat_conversion,[],[f21688]) ).
cnf(s34,plain,
spl490_19,
inference(sat_conversion,[],[f21705]) ).
cnf(s36,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_42 ),
inference(sat_conversion,[],[f21739]) ).
cnf(s46,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_53 ),
inference(sat_conversion,[],[f21847]) ).
cnf(s48,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_55 ),
inference(sat_conversion,[],[f21866]) ).
cnf(s51,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_14
| spl490_60 ),
inference(sat_conversion,[],[f21902]) ).
cnf(s66,plain,
( spl490_22
| ~ spl490_55 ),
inference(sat_conversion,[],[f22083]) ).
cnf(s68,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_14
| ~ spl490_19
| spl490_20
| ~ spl490_21
| ~ spl490_22 ),
inference(sat_conversion,[],[f22085]) ).
cnf(s86,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_87 ),
inference(sat_conversion,[],[f22263]) ).
cnf(s98,plain,
spl490_61,
inference(sat_conversion,[],[f22430]) ).
cnf(s128,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_119 ),
inference(sat_conversion,[],[f22553]) ).
cnf(s137,plain,
spl490_99,
inference(sat_conversion,[],[f22640]) ).
cnf(s147,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_134 ),
inference(sat_conversion,[],[f22788]) ).
cnf(s149,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_136 ),
inference(sat_conversion,[],[f22808]) ).
cnf(s218,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_53
| spl490_124 ),
inference(sat_conversion,[],[f23532]) ).
cnf(s241,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_233 ),
inference(sat_conversion,[],[f23741]) ).
cnf(s271,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| spl490_85 ),
inference(sat_conversion,[],[f23997]) ).
cnf(s348,plain,
( ~ spl490_19
| ~ spl490_21
| ~ spl490_22
| ~ spl490_124
| spl490_203 ),
inference(sat_conversion,[],[f24782]) ).
cnf(s428,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_87
| spl490_384 ),
inference(sat_conversion,[],[f25899]) ).
cnf(s799,plain,
( ~ spl490_19
| ~ spl490_21
| ~ spl490_55
| ~ spl490_384
| spl490_707 ),
inference(sat_conversion,[],[f30480]) ).
cnf(s971,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_19
| ~ spl490_21
| ~ spl490_55
| ~ spl490_233
| spl490_863 ),
inference(sat_conversion,[],[f32320]) ).
cnf(s972,plain,
( ~ spl490_20
| ~ spl490_26
| ~ spl490_203
| ~ spl490_863
| spl490_864 ),
inference(sat_conversion,[],[f32325]) ).
cnf(s1079,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_136
| spl490_947 ),
inference(sat_conversion,[],[f34363]) ).
cnf(s1080,plain,
( ~ spl490_19
| ~ spl490_21
| ~ spl490_55
| ~ spl490_947
| spl490_948 ),
inference(sat_conversion,[],[f34369]) ).
cnf(s1287,plain,
( ~ spl490_61
| ~ spl490_99
| spl490_1149 ),
inference(sat_conversion,[],[f36652]) ).
cnf(s1288,plain,
( ~ spl490_99
| ~ spl490_494
| ~ spl490_707
| ~ spl490_1149
| spl490_1150
| spl490_1151 ),
inference(sat_conversion,[],[f36663]) ).
cnf(s1289,plain,
( ~ spl490_99
| ~ spl490_494
| ~ spl490_948
| ~ spl490_1149
| spl490_1151
| spl490_1152 ),
inference(sat_conversion,[],[f36668]) ).
cnf(s1437,plain,
spl490_494,
inference(sat_conversion,[],[f38091]) ).
cnf(s1441,plain,
~ spl490_1151,
inference(sat_conversion,[],[f38220]) ).
cnf(s1446,plain,
( ~ spl490_19
| ~ spl490_21
| ~ spl490_22
| ~ spl490_1152
| spl490_1224 ),
inference(sat_conversion,[],[f38279]) ).
cnf(s1453,plain,
( ~ spl490_1224
| ~ spl490_1231
| spl490_1232 ),
inference(sat_conversion,[],[f38336]) ).
cnf(s1455,plain,
( ~ spl490_60
| ~ spl490_1150
| spl490_1225
| ~ spl490_1234 ),
inference(sat_conversion,[],[f38359]) ).
cnf(s1456,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_19
| ~ spl490_21
| ~ spl490_55
| ~ spl490_99
| ~ spl490_494
| ~ spl490_1149
| spl490_1151
| spl490_1234 ),
inference(sat_conversion,[],[f38372]) ).
cnf(s1463,plain,
( ~ spl490_864
| ~ spl490_1150
| ~ spl490_1152
| spl490_1226
| ~ spl490_1234 ),
inference(sat_conversion,[],[f38412]) ).
cnf(s1464,plain,
( ~ spl490_1226
| ~ spl490_1240
| spl490_1241 ),
inference(sat_conversion,[],[f38424]) ).
cnf(s1617,plain,
( ~ spl490_134
| ~ spl490_1240
| ~ spl490_1241
| spl490_1399 ),
inference(sat_conversion,[],[f39363]) ).
cnf(s1619,plain,
( ~ spl490_119
| ~ spl490_1240
| ~ spl490_1241
| spl490_1392 ),
inference(sat_conversion,[],[f39369]) ).
cnf(s1620,plain,
( ~ spl490_42
| ~ spl490_1240
| ~ spl490_1241
| spl490_1398 ),
inference(sat_conversion,[],[f39370]) ).
cnf(s1623,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_19
| ~ spl490_21
| ~ spl490_55
| ~ spl490_99
| ~ spl490_494
| ~ spl490_1149
| spl490_1151
| ~ spl490_1241
| ~ spl490_1403 ),
inference(sat_conversion,[],[f39390]) ).
cnf(s1625,plain,
( ~ spl490_1225
| spl490_1403
| ~ spl490_1404 ),
inference(sat_conversion,[],[f39405]) ).
cnf(s2046,plain,
( ~ spl490_85
| ~ spl490_1150
| spl490_1231 ),
inference(sat_conversion,[],[f45284]) ).
cnf(s2056,plain,
( ~ spl490_85
| ~ spl490_1150
| ~ spl490_1232
| spl490_1240 ),
inference(sat_conversion,[],[f45371]) ).
cnf(s2096,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_1392
| spl490_1397
| ~ spl490_1398
| ~ spl490_1399 ),
inference(sat_conversion,[],[f45663]) ).
cnf(s2097,plain,
( ~ spl490_1150
| ~ spl490_1232
| ~ spl490_1234
| ~ spl490_1397
| spl490_1404 ),
inference(sat_conversion,[],[f45668]) ).
cnf(s2133,plain,
( ~ spl490_99
| ~ spl490_948
| ~ spl490_1149
| spl490_1152 ),
inference(rat,[],[s1289,s1441,s1437]) ).
cnf(s2134,plain,
( ~ spl490_99
| ~ spl490_707
| ~ spl490_1149
| spl490_1150 ),
inference(rat,[],[s1288,s1441,s1437]) ).
cnf(s2156,plain,
spl490_1149,
inference(rat,[],[s1287,s137,s98]) ).
cnf(s2442,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_12
| ~ spl490_21
| ~ spl490_22
| spl490_26 ),
inference(rat,[],[s24,s34]) ).
cnf(s2444,plain,
( ~ spl490_9
| ~ spl490_10
| ~ spl490_11
| spl490_14 ),
inference(rat,[],[s13,s15]) ).
cnf(s2502,plain,
spl490_85,
inference(rat,[],[s271,s10,s15,s12,s8]) ).
cnf(s2507,plain,
spl490_233,
inference(rat,[],[s241,s10,s15,s12,s8]) ).
cnf(s2524,plain,
spl490_136,
inference(rat,[],[s149,s10,s15,s12,s8]) ).
cnf(s2525,plain,
spl490_134,
inference(rat,[],[s147,s10,s15,s12,s8]) ).
cnf(s2532,plain,
spl490_119,
inference(rat,[],[s128,s10,s15,s12,s8]) ).
cnf(s2538,plain,
spl490_87,
inference(rat,[],[s86,s10,s15,s12,s8]) ).
cnf(s2546,plain,
spl490_55,
inference(rat,[],[s48,s10,s15,s12,s8]) ).
cnf(s2548,plain,
spl490_53,
inference(rat,[],[s46,s10,s15,s12,s8]) ).
cnf(s2552,plain,
spl490_42,
inference(rat,[],[s36,s10,s15,s12,s8]) ).
cnf(s2554,plain,
spl490_21,
inference(rat,[],[s31,s10,s15,s12,s8]) ).
cnf(s2564,plain,
spl490_14,
inference(rat,[],[s2444,s10,s12,s8]) ).
cnf(s2613,plain,
spl490_947,
inference(rat,[],[s1079,s8,s10,s15,s12,s2524]) ).
cnf(s2637,plain,
spl490_384,
inference(rat,[],[s428,s8,s10,s15,s12,s2538]) ).
cnf(s2644,plain,
spl490_22,
inference(rat,[],[s66,s2546]) ).
cnf(s2645,plain,
spl490_124,
inference(rat,[],[s218,s8,s10,s15,s12,s2548]) ).
cnf(s2653,plain,
spl490_948,
inference(rat,[],[s1080,s2546,s2613,s34,s2554]) ).
cnf(s2654,plain,
spl490_707,
inference(rat,[],[s799,s2546,s2637,s34,s2554]) ).
cnf(s2655,plain,
spl490_1234,
inference(rat,[],[s1456,s2546,s1441,s2156,s1437,s137,s8,s10,s34,s15,s12,s2554]) ).
cnf(s2656,plain,
spl490_863,
inference(rat,[],[s971,s2546,s2507,s8,s10,s34,s15,s12,s2554]) ).
cnf(s2665,plain,
spl490_20,
inference(rat,[],[s68,s2644,s2554,s8,s34,s10,s15,s12,s2564]) ).
cnf(s2666,plain,
spl490_60,
inference(rat,[],[s51,s8,s10,s15,s12,s2564]) ).
cnf(s2923,plain,
spl490_203,
inference(rat,[],[s348,s2554,s2645,s34,s2644]) ).
cnf(s2924,plain,
spl490_26,
inference(rat,[],[s2442,s2554,s8,s10,s15,s12,s2644]) ).
cnf(s2940,plain,
spl490_1152,
inference(rat,[],[s2133,s2156,s137,s2653]) ).
cnf(s2941,plain,
spl490_1150,
inference(rat,[],[s2134,s2156,s137,s2654]) ).
cnf(s2980,plain,
spl490_864,
inference(rat,[],[s972,s2665,s2656,s2923,s2924]) ).
cnf(s3037,plain,
spl490_1224,
inference(rat,[],[s1446,s2644,s2554,s34,s2940]) ).
cnf(s3038,plain,
spl490_1231,
inference(rat,[],[s2046,s2502,s2941]) ).
cnf(s3044,plain,
spl490_1225,
inference(rat,[],[s1455,s2655,s2666,s2941]) ).
cnf(s3164,plain,
spl490_1226,
inference(rat,[],[s1463,s2655,s2941,s2940,s2980]) ).
cnf(s3222,plain,
spl490_1232,
inference(rat,[],[s1453,s3037,s3038]) ).
cnf(s3309,plain,
spl490_1240,
inference(rat,[],[s2056,s2941,s2502,s3222]) ).
cnf(s3457,plain,
spl490_1241,
inference(rat,[],[s1464,s3164,s3309]) ).
cnf(s3467,plain,
spl490_1399,
inference(rat,[],[s1617,s3309,s2525,s3457]) ).
cnf(s3470,plain,
spl490_1392,
inference(rat,[],[s1619,s3309,s2532,s3457]) ).
cnf(s3472,plain,
~ spl490_1403,
inference(rat,[],[s1623,s2554,s2546,s1441,s2156,s1437,s137,s8,s10,s34,s15,s12,s3457]) ).
cnf(s3473,plain,
spl490_1398,
inference(rat,[],[s1620,s3309,s2552,s3457]) ).
cnf(s3476,plain,
spl490_1397,
inference(rat,[],[s2096,s3467,s3473,s8,s10,s15,s12,s3470]) ).
cnf(s3480,plain,
~ spl490_1404,
inference(rat,[],[s1625,s3044,s3472]) ).
cnf(s3482,plain,
$false,
inference(rat,[],[s2097,s3222,s2941,s2655,s3480,s3476]) ).
fof(f45669,plain,
$false,
inference(avatar_sat_refutation,[],[s3482]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP650+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n015.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 10:31:34 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.18/3.77 % (1454578)Detected formulas, will run a generic FOF schedule.
% 15.18/3.77 % (1454583)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=2079087893:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 15.18/3.77 % (1454584)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=1297648648:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 15.18/3.77 % (1454586)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=534819936:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 15.18/3.77 % (1454585)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=2454994290:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 15.18/3.77 % (1454588)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=365922483:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 15.18/3.77 % (1454587)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2633322841:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 15.18/3.77 % (1454589)dis-21_1_sil=8000:lcm=predicate:random_seed=1470238731:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2992 on theBenchmark for (2992ds/129Mi)
% 15.18/3.77 % (1454586)Refutation not found, incomplete strategy
% 15.18/3.77 % (1454586)------------------------------
% 15.18/3.77 % (1454586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/3.77 % (1454586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/3.77 % (1454586)CaDiCaL version: 2.1.3
% 15.18/3.77 % (1454586)Termination reason: Refutation not found, incomplete strategy
% 15.18/3.77 % (1454586)Time elapsed: 0.065 s
% 15.18/3.77 % (1454586)Peak memory usage: 107 MB
% 15.18/3.77 % (1454586)Instructions burned: 82 (million)
% 15.18/3.77 % (1454588)Instruction limit reached!
% 15.18/3.77 % (1454588)------------------------------
% 15.18/3.77 % (1454588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/3.77 % (1454588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/3.77 % (1454588)CaDiCaL version: 2.1.3
% 15.18/3.77 % (1454588)Termination reason: Instruction limit
% 15.18/3.77 % (1454588)Termination phase: Property scanning
% 15.18/3.77 % (1454588)Time elapsed: 0.060 s
% 15.18/3.77 % (1454588)Peak memory usage: 103 MB
% 15.18/3.77 % (1454588)Instructions burned: 140 (million)
% 15.18/3.77 % (1454589)Instruction limit reached!
% 15.18/3.77 % (1454589)------------------------------
% 15.18/3.77 % (1454589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/3.77 % (1454589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/3.77 % (1454589)CaDiCaL version: 2.1.3
% 15.18/3.77 % (1454589)Termination reason: Instruction limit
% 15.18/3.77 % (1454589)Termination phase: Preprocessing 1
% 15.18/3.77 % (1454589)Time elapsed: 0.099 s
% 15.18/3.77 % (1454589)Peak memory usage: 104 MB
% 15.18/3.77 % (1454589)Instructions burned: 129 (million)
% 15.18/3.77 % (1454587)Instruction limit reached!
% 15.18/3.77 % (1454587)------------------------------
% 15.18/3.77 % (1454587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.18/3.77 % (1454587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.18/3.77 % (1454587)CaDiCaL version: 2.1.3
% 15.18/3.77 % (1454587)Termination reason: Instruction limit
% 15.18/3.77 % (1454587)Termination phase: Naming
% 15.18/3.77 % (1454587)Time elapsed: 0.107 s
% 15.18/3.77 % (1454587)Peak memory usage: 106 MB
% 15.18/3.77 % (1454587)Instructions burned: 120 (million)
% 15.18/3.77 % (1454597)lrs+10_1_sil=8000:sp=occurrence:random_seed=2292206373:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 15.18/3.77 % (1454598)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3853775545:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 15.18/3.77 % (1454586)------------------------------
% 15.18/3.77 % (1454586)------------------------------
% 15.18/3.77 % (1454599)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1849849564:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.18/3.77 % (1454598)Instruction limit reached!
% 15.18/3.77 % (1454598)------------------------------
% 15.18/3.77 % (1454598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.68 % (1454598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.68 % (1454598)CaDiCaL version: 2.1.3
% 22.41/4.68 % (1454598)Termination reason: Instruction limit
% 22.41/4.68 % (1454598)Termination phase: Property scanning
% 22.41/4.68 % (1454598)Time elapsed: 0.067 s
% 22.41/4.68 % (1454598)Peak memory usage: 103 MB
% 22.41/4.68 % (1454598)Instructions burned: 159 (million)
% 22.41/4.68 % (1454599)Refutation not found, incomplete strategy
% 22.41/4.68 % (1454599)------------------------------
% 22.41/4.68 % (1454599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.68 % (1454599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.68 % (1454599)CaDiCaL version: 2.1.3
% 22.41/4.68 % (1454599)Termination reason: Refutation not found, incomplete strategy
% 22.41/4.68 % (1454599)Time elapsed: 0.070 s
% 22.41/4.68 % (1454599)Peak memory usage: 107 MB
% 22.41/4.68 % (1454599)Instructions burned: 79 (million)
% 22.41/4.68 % (1454597)Instruction limit reached!
% 22.41/4.68 % (1454597)------------------------------
% 22.41/4.68 % (1454597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.68 % (1454597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.68 % (1454597)CaDiCaL version: 2.1.3
% 22.41/4.68 % (1454597)Termination reason: Instruction limit
% 22.41/4.68 % (1454597)Termination phase: Saturation
% 22.41/4.68 % (1454597)Time elapsed: 0.190 s
% 22.41/4.68 % (1454597)Peak memory usage: 111 MB
% 22.41/4.68 % (1454597)Instructions burned: 285 (million)
% 22.41/4.68 % (1454603)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=1925305412:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 22.41/4.68 % (1454604)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2382754710:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2987 on theBenchmark for (2987ds/294Mi)
% 22.41/4.68 % (1454603)Instruction limit reached!
% 22.41/4.68 % (1454603)------------------------------
% 22.41/4.68 % (1454603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.68 % (1454603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.68 % (1454603)CaDiCaL version: 2.1.3
% 22.41/4.68 % (1454603)Termination reason: Instruction limit
% 22.41/4.68 % (1454603)Termination phase: SInE selection
% 22.41/4.68 % (1454603)Time elapsed: 0.125 s
% 22.41/4.68 % (1454603)Peak memory usage: 103 MB
% 22.41/4.68 % (1454603)Instructions burned: 248 (million)
% 22.41/4.68 % (1454599)------------------------------
% 22.41/4.68 % (1454599)------------------------------
% 22.41/4.68 % (1454605)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=468991744:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 22.41/4.68 % (1454604)Instruction limit reached!
% 22.41/4.68 % (1454604)------------------------------
% 22.41/4.68 % (1454604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.68 % (1454604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.68 % (1454604)CaDiCaL version: 2.1.3
% 22.41/4.68 % (1454604)Termination reason: Instruction limit
% 22.41/4.68 % (1454604)Termination phase: Saturation
% 22.41/4.68 % (1454604)Time elapsed: 0.198 s
% 22.41/4.68 % (1454604)Peak memory usage: 111 MB
% 22.41/4.68 % (1454604)Instructions burned: 295 (million)
% 22.41/4.68 % (1454608)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2811739498:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 22.41/4.68 % (1454610)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2165170154:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 22.41/4.68 % (1454608)Instruction limit reached!
% 22.41/4.68 % (1454608)------------------------------
% 22.41/4.68 % (1454608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.68 % (1454608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.68 % (1454608)CaDiCaL version: 2.1.3
% 22.41/4.68 % (1454608)Termination reason: Instruction limit
% 22.41/4.68 % (1454608)Termination phase: Preprocessing 2
% 22.41/4.68 % (1454608)Time elapsed: 0.099 s
% 22.41/4.68 % (1454608)Peak memory usage: 106 MB
% 22.41/4.68 % (1454608)Instructions burned: 113 (million)
% 22.41/4.68 % (1454610)Instruction limit reached!
% 22.41/4.68 % (1454610)------------------------------
% 22.41/4.68 % (1454610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.50/7.95 % (1454610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.50/7.95 % (1454610)CaDiCaL version: 2.1.3
% 45.50/7.95 % (1454610)Termination reason: Instruction limit
% 45.50/7.95 % (1454610)Termination phase: Preprocessing 2
% 45.50/7.95 % (1454610)Time elapsed: 0.104 s
% 45.50/7.95 % (1454610)Peak memory usage: 106 MB
% 45.50/7.95 % (1454610)Instructions burned: 128 (million)
% 45.50/7.95 % (1454611)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1896211713:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 45.50/7.95 % (1454611)Instruction limit reached!
% 45.50/7.95 % (1454611)------------------------------
% 45.50/7.95 % (1454611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.50/7.95 % (1454611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.50/7.95 % (1454611)CaDiCaL version: 2.1.3
% 45.50/7.95 % (1454611)Termination reason: Instruction limit
% 45.50/7.95 % (1454611)Termination phase: Property scanning
% 45.50/7.95 % (1454611)Time elapsed: 0.051 s
% 45.50/7.95 % (1454611)Peak memory usage: 103 MB
% 45.50/7.95 % (1454611)Instructions burned: 116 (million)
% 45.50/7.95 % (1454614)lrs+10_1_sil=8000:sp=occurrence:random_seed=2126762843:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 45.50/7.95 % (1454616)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2740773797:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 45.50/7.95 % (1454617)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2248529840:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 45.50/7.95 % (1454616)Refutation not found, incomplete strategy
% 45.50/7.95 % (1454616)------------------------------
% 45.50/7.95 % (1454616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.50/7.95 % (1454616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.50/7.95 % (1454616)CaDiCaL version: 2.1.3
% 45.50/7.95 % (1454616)Termination reason: Refutation not found, incomplete strategy
% 45.50/7.95 % (1454616)Time elapsed: 0.105 s
% 45.50/7.95 % (1454616)Peak memory usage: 109 MB
% 45.50/7.95 % (1454616)Instructions burned: 135 (million)
% 45.50/7.95 % (1454614)Instruction limit reached!
% 45.50/7.95 % (1454614)------------------------------
% 45.50/7.95 % (1454614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.50/7.95 % (1454614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.50/7.95 % (1454614)CaDiCaL version: 2.1.3
% 45.50/7.95 % (1454614)Termination reason: Instruction limit
% 45.50/7.95 % (1454614)Termination phase: Saturation
% 45.50/7.95 % (1454614)Time elapsed: 0.305 s
% 45.50/7.95 % (1454614)Peak memory usage: 122 MB
% 45.50/7.95 % (1454614)Instructions burned: 910 (million)
% 45.50/7.95 % (1454621)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1282342110:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 45.50/7.95 % (1454616)------------------------------
% 45.50/7.95 % (1454616)------------------------------
% 45.50/7.95 % (1454621)Instruction limit reached!
% 45.50/7.95 % (1454621)------------------------------
% 45.50/7.95 % (1454621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.50/7.95 % (1454621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.50/7.95 % (1454621)CaDiCaL version: 2.1.3
% 45.50/7.95 % (1454621)Termination reason: Instruction limit
% 45.50/7.95 % (1454621)Termination phase: Property scanning
% 45.50/7.95 % (1454621)Time elapsed: 0.061 s
% 45.50/7.95 % (1454621)Peak memory usage: 107 MB
% 45.50/7.95 % (1454621)Instructions burned: 137 (million)
% 45.50/7.95 % (1454623)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3731347536:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 45.50/7.95 % (1454624)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1343313934:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 45.50/7.95 % (1454623)Instruction limit reached!
% 45.50/7.95 % (1454623)------------------------------
% 45.50/7.95 % (1454623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.50/7.95 % (1454623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.50/7.95 % (1454623)CaDiCaL version: 2.1.3
% 45.50/7.95 % (1454623)Termination reason: Instruction limit
% 45.50/7.95 % (1454623)Termination phase: Property scanning
% 45.50/7.95 % (1454623)Time elapsed: 0.429 s
% 76.53/12.28 % (1454623)Peak memory usage: 126 MB
% 76.53/12.28 % (1454623)Instructions burned: 594 (million)
% 76.53/12.28 % (1454605)Instruction limit reached!
% 76.53/12.28 % (1454605)------------------------------
% 76.53/12.28 % (1454605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.53/12.28 % (1454605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.53/12.28 % (1454605)CaDiCaL version: 2.1.3
% 76.53/12.28 % (1454605)Termination reason: Instruction limit
% 76.53/12.28 % (1454605)Termination phase: Saturation
% 76.53/12.28 % (1454605)Time elapsed: 1.447 s
% 76.53/12.28 % (1454605)Peak memory usage: 218 MB
% 76.53/12.28 % (1454605)Instructions burned: 2350 (million)
% 76.53/12.28 % (1454627)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=3051897345:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 76.53/12.28 % (1454628)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2904898508:i=134:gtgl=5:slsql=off:gtg=exists_sym_2970 on theBenchmark for (2970ds/134Mi)
% 76.53/12.28 % (1454627)Instruction limit reached!
% 76.53/12.28 % (1454627)------------------------------
% 76.53/12.28 % (1454627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.53/12.28 % (1454627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.53/12.28 % (1454627)CaDiCaL version: 2.1.3
% 76.53/12.28 % (1454627)Termination reason: Instruction limit
% 76.53/12.28 % (1454627)Termination phase: Property scanning
% 76.53/12.28 % (1454627)Time elapsed: 0.055 s
% 76.53/12.28 % (1454627)Peak memory usage: 103 MB
% 76.53/12.28 % (1454627)Instructions burned: 126 (million)
% 76.53/12.28 % (1454628)Instruction limit reached!
% 76.53/12.28 % (1454628)------------------------------
% 76.53/12.28 % (1454628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.53/12.28 % (1454628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.53/12.28 % (1454628)CaDiCaL version: 2.1.3
% 76.53/12.28 % (1454628)Termination reason: Instruction limit
% 76.53/12.28 % (1454628)Termination phase: Property scanning
% 76.53/12.28 % (1454628)Time elapsed: 0.058 s
% 76.53/12.28 % (1454628)Peak memory usage: 103 MB
% 76.53/12.28 % (1454628)Instructions burned: 134 (million)
% 76.53/12.28 % (1454631)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3506931825:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/141Mi)
% 76.53/12.28 % (1454632)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2310820422:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 76.53/12.28 % (1454631)Refutation not found, incomplete strategy
% 76.53/12.28 % (1454631)------------------------------
% 76.53/12.28 % (1454631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.53/12.28 % (1454631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.53/12.28 % (1454631)CaDiCaL version: 2.1.3
% 76.53/12.28 % (1454631)Termination reason: Refutation not found, incomplete strategy
% 76.53/12.28 % (1454631)Time elapsed: 0.071 s
% 76.53/12.28 % (1454631)Peak memory usage: 108 MB
% 76.53/12.28 % (1454631)Instructions burned: 80 (million)
% 76.53/12.28 % (1454632)Refutation not found, incomplete strategy
% 76.53/12.28 % (1454632)------------------------------
% 76.53/12.28 % (1454632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.53/12.28 % (1454632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.53/12.28 % (1454632)CaDiCaL version: 2.1.3
% 76.53/12.28 % (1454632)Termination reason: Refutation not found, incomplete strategy
% 76.53/12.28 % (1454632)Time elapsed: 0.068 s
% 76.53/12.28 % (1454632)Peak memory usage: 107 MB
% 76.53/12.28 % (1454632)Instructions burned: 78 (million)
% 76.53/12.28 % (1454631)------------------------------
% 76.53/12.28 % (1454631)------------------------------
% 76.53/12.28 % (1454632)------------------------------
% 76.53/12.28 % (1454632)------------------------------
% 76.53/12.28 % (1454636)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=3727730610:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2963 on theBenchmark for (2963ds/150Mi)
% 76.53/12.28 % (1454635)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=799611336:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 106.04/16.48 % (1454636)Instruction limit reached!
% 106.04/16.48 % (1454636)------------------------------
% 106.04/16.48 % (1454636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.04/16.48 % (1454636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.04/16.48 % (1454636)CaDiCaL version: 2.1.3
% 106.04/16.48 % (1454636)Termination reason: Instruction limit
% 106.04/16.48 % (1454636)Termination phase: Preprocessing 1
% 106.04/16.48 % (1454636)Time elapsed: 0.111 s
% 106.04/16.48 % (1454636)Peak memory usage: 103 MB
% 106.04/16.48 % (1454636)Instructions burned: 151 (million)
% 106.04/16.48 % (1454639)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=281651303:i=14155:bd=all_2960 on theBenchmark for (2960ds/14155Mi)
% 106.04/16.48 % (1454617)Instruction limit reached!
% 106.04/16.48 % (1454617)------------------------------
% 106.04/16.48 % (1454617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.04/16.48 % (1454617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.04/16.48 % (1454617)CaDiCaL version: 2.1.3
% 106.04/16.48 % (1454617)Termination reason: Instruction limit
% 106.04/16.48 % (1454617)Termination phase: Saturation
% 106.04/16.48 % (1454617)Time elapsed: 3.204 s
% 106.04/16.48 % (1454617)Peak memory usage: 219 MB
% 106.04/16.48 % (1454617)Instructions burned: 5203 (million)
% 106.04/16.48 % (1454641)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1146631929:i=667:av=off:fsr=off_2947 on theBenchmark for (2947ds/667Mi)
% 106.04/16.48 % (1454641)Instruction limit reached!
% 106.04/16.48 % (1454641)------------------------------
% 106.04/16.48 % (1454641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.04/16.48 % (1454641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.04/16.48 % (1454641)CaDiCaL version: 2.1.3
% 106.04/16.48 % (1454641)Termination reason: Instruction limit
% 106.04/16.48 % (1454641)Termination phase: NewCNF
% 106.04/16.48 % (1454641)Time elapsed: 0.484 s
% 106.04/16.48 % (1454641)Peak memory usage: 136 MB
% 106.04/16.48 % (1454641)Instructions burned: 667 (million)
% 106.04/16.48 % (1454643)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=3756754099:s2a=on:i=185:s2at=1.8:fdi=4_2941 on theBenchmark for (2941ds/185Mi)
% 106.04/16.48 % (1454643)Instruction limit reached!
% 106.04/16.48 % (1454643)------------------------------
% 106.04/16.48 % (1454643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.04/16.48 % (1454643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.04/16.48 % (1454643)CaDiCaL version: 2.1.3
% 106.04/16.48 % (1454643)Termination reason: Instruction limit
% 106.04/16.48 % (1454643)Termination phase: Preprocessing 1
% 106.04/16.48 % (1454643)Time elapsed: 0.148 s
% 106.04/16.48 % (1454643)Peak memory usage: 104 MB
% 106.04/16.48 % (1454643)Instructions burned: 186 (million)
% 106.04/16.48 % (1454645)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4035166849:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2937 on theBenchmark for (2937ds/193Mi)
% 106.04/16.48 % (1454645)Instruction limit reached!
% 106.04/16.48 % (1454645)------------------------------
% 106.04/16.48 % (1454645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.04/16.48 % (1454645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.04/16.48 % (1454645)CaDiCaL version: 2.1.3
% 106.04/16.48 % (1454645)Termination reason: Instruction limit
% 106.04/16.48 % (1454645)Termination phase: Preprocessing 2
% 106.04/16.48 % (1454645)Time elapsed: 0.167 s
% 106.04/16.48 % (1454645)Peak memory usage: 106 MB
% 106.04/16.48 % (1454645)Instructions burned: 194 (million)
% 106.04/16.48 % (1454647)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=963242775:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2934 on theBenchmark for (2934ds/4850Mi)
% 106.04/16.48 % (1454624)Instruction limit reached!
% 106.04/16.48 % (1454624)------------------------------
% 106.04/16.48 % (1454624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.04/16.48 % (1454624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.04/16.48 % (1454624)CaDiCaL version: 2.1.3
% 106.04/16.48 % (1454624)Termination reason: Instruction limit
% 106.04/16.48 % (1454624)Termination phase: Saturation
% 106.04/16.48 % (1454624)Time elapsed: 4.608 s
% 106.04/16.48 % (1454624)Peak memory usage: 268 MB
% 106.04/16.48 % (1454624)Instructions burned: 13193 (million)
% 123.84/19.03 % (1454649)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1032152125:i=12111:sd=1:ss=included_2929 on theBenchmark for (2929ds/12111Mi)
% 123.84/19.03 % (1454635)Instruction limit reached!
% 123.84/19.03 % (1454635)------------------------------
% 123.84/19.03 % (1454635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454635)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454635)Termination reason: Instruction limit
% 123.84/19.03 % (1454635)Termination phase: Saturation
% 123.84/19.03 % (1454635)Time elapsed: 4.726 s
% 123.84/19.03 % (1454635)Peak memory usage: 586 MB
% 123.84/19.03 % (1454635)Instructions burned: 6061 (million)
% 123.84/19.03 % (1454651)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1905071136:i=319:kws=precedence:fsr=off_2914 on theBenchmark for (2914ds/319Mi)
% 123.84/19.03 % (1454651)Instruction limit reached!
% 123.84/19.03 % (1454651)------------------------------
% 123.84/19.03 % (1454651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454651)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454651)Termination reason: Instruction limit
% 123.84/19.03 % (1454651)Termination phase: Preprocessing 3
% 123.84/19.03 % (1454651)Time elapsed: 0.236 s
% 123.84/19.03 % (1454651)Peak memory usage: 123 MB
% 123.84/19.03 % (1454651)Instructions burned: 320 (million)
% 123.84/19.03 % (1454653)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2050010446:i=2064:ep=RST_2909 on theBenchmark for (2909ds/2064Mi)
% 123.84/19.03 % (1454647)Instruction limit reached!
% 123.84/19.03 % (1454647)------------------------------
% 123.84/19.03 % (1454647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454647)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454647)Termination reason: Instruction limit
% 123.84/19.03 % (1454647)Termination phase: Saturation
% 123.84/19.03 % (1454647)Time elapsed: 2.670 s
% 123.84/19.03 % (1454647)Peak memory usage: 179 MB
% 123.84/19.03 % (1454647)Instructions burned: 4851 (million)
% 123.84/19.03 % (1454655)dis-1011_128_sil=32000:random_seed=2600735412:i=3706:ep=RST:av=off_2905 on theBenchmark for (2905ds/3706Mi)
% 123.84/19.03 % (1454653)Instruction limit reached!
% 123.84/19.03 % (1454653)------------------------------
% 123.84/19.03 % (1454653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454653)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454653)Termination reason: Instruction limit
% 123.84/19.03 % (1454653)Termination phase: Saturation
% 123.84/19.03 % (1454653)Time elapsed: 1.003 s
% 123.84/19.03 % (1454653)Peak memory usage: 147 MB
% 123.84/19.03 % (1454653)Instructions burned: 2065 (million)
% 123.84/19.03 % (1454657)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1746039738:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2898 on theBenchmark for (2898ds/757Mi)
% 123.84/19.03 % (1454657)Refutation not found, incomplete strategy
% 123.84/19.03 % (1454657)------------------------------
% 123.84/19.03 % (1454657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454657)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454657)Termination reason: Refutation not found, incomplete strategy
% 123.84/19.03 % (1454657)Time elapsed: 0.100 s
% 123.84/19.03 % (1454657)Peak memory usage: 109 MB
% 123.84/19.03 % (1454657)Instructions burned: 132 (million)
% 123.84/19.03 % (1454657)------------------------------
% 123.84/19.03 % (1454657)------------------------------
% 123.84/19.03 % (1454659)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=829764909:i=13913:ss=axioms:sgt=8_2892 on theBenchmark for (2892ds/13913Mi)
% 123.84/19.03 % (1454649)Instruction limit reached!
% 123.84/19.03 % (1454649)------------------------------
% 123.84/19.03 % (1454649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454649)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454649)Termination reason: Instruction limit
% 123.84/19.03 % (1454649)Termination phase: Saturation
% 123.84/19.03 % (1454649)Time elapsed: 4.180 s
% 123.84/19.03 % (1454649)Peak memory usage: 263 MB
% 123.84/19.03 % (1454649)Instructions burned: 12114 (million)
% 123.84/19.03 % (1454661)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2351133225:i=9925:aac=none_2885 on theBenchmark for (2885ds/9925Mi)
% 123.84/19.03 % (1454655)Instruction limit reached!
% 123.84/19.03 % (1454655)------------------------------
% 123.84/19.03 % (1454655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454655)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454655)Termination reason: Instruction limit
% 123.84/19.03 % (1454655)Termination phase: Saturation
% 123.84/19.03 % (1454655)Time elapsed: 2.003 s
% 123.84/19.03 % (1454655)Peak memory usage: 165 MB
% 123.84/19.03 % (1454655)Instructions burned: 3706 (million)
% 123.84/19.03 % (1454663)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2533458033:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2883 on theBenchmark for (2883ds/2479Mi)
% 123.84/19.03 % (1454639)Instruction limit reached!
% 123.84/19.03 % (1454639)------------------------------
% 123.84/19.03 % (1454639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454639)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454639)Termination reason: Instruction limit
% 123.84/19.03 % (1454639)Termination phase: Saturation
% 123.84/19.03 % (1454639)Time elapsed: 8.770 s
% 123.84/19.03 % (1454639)Peak memory usage: 516 MB
% 123.84/19.03 % (1454639)Instructions burned: 14155 (million)
% 123.84/19.03 % (1454665)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=299611573:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2870 on theBenchmark for (2870ds/440Mi)
% 123.84/19.03 % (1454665)Instruction limit reached!
% 123.84/19.03 % (1454665)------------------------------
% 123.84/19.03 % (1454665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454665)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454665)Termination reason: Instruction limit
% 123.84/19.03 % (1454665)Termination phase: Preprocessing 1
% 123.84/19.03 % (1454665)Time elapsed: 0.192 s
% 123.84/19.03 % (1454665)Peak memory usage: 104 MB
% 123.84/19.03 % (1454665)Instructions burned: 441 (million)
% 123.84/19.03 % (1454663)Instruction limit reached!
% 123.84/19.03 % (1454663)------------------------------
% 123.84/19.03 % (1454663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454663)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454663)Termination reason: Instruction limit
% 123.84/19.03 % (1454663)Termination phase: Saturation
% 123.84/19.03 % (1454663)Time elapsed: 1.543 s
% 123.84/19.03 % (1454663)Peak memory usage: 128 MB
% 123.84/19.03 % (1454663)Instructions burned: 2480 (million)
% 123.84/19.03 % (1454667)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2589283423:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2867 on theBenchmark for (2867ds/11145Mi)
% 123.84/19.03 % (1454668)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=635945193:cts=off:i=3034:av=off:er=known:fsd=on_2866 on theBenchmark for (2866ds/3034Mi)
% 123.84/19.03 % (1454661)Instruction limit reached!
% 123.84/19.03 % (1454661)------------------------------
% 123.84/19.03 % (1454661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454661)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454661)Termination reason: Instruction limit
% 123.84/19.03 % (1454661)Termination phase: Saturation
% 123.84/19.03 % (1454661)Time elapsed: 3.664 s
% 123.84/19.03 % (1454661)Peak memory usage: 450 MB
% 123.84/19.03 % (1454661)Instructions burned: 9927 (million)
% 123.84/19.03 % (1454671)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3765808025:st=2:s2a=on:i=524:s2at=2:ss=axioms_2847 on theBenchmark for (2847ds/524Mi)
% 123.84/19.03 % (1454671)Instruction limit reached!
% 123.84/19.03 % (1454671)------------------------------
% 123.84/19.03 % (1454671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454671)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454671)Termination reason: Instruction limit
% 123.84/19.03 % (1454671)Termination phase: Preprocessing 3
% 123.84/19.03 % (1454671)Time elapsed: 0.235 s
% 123.84/19.03 % (1454671)Peak memory usage: 118 MB
% 123.84/19.03 % (1454671)Instructions burned: 525 (million)
% 123.84/19.03 % (1454668)Instruction limit reached!
% 123.84/19.03 % (1454668)------------------------------
% 123.84/19.03 % (1454668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454668)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454668)Termination reason: Instruction limit
% 123.84/19.03 % (1454668)Termination phase: Saturation
% 123.84/19.03 % (1454668)Time elapsed: 2.185 s
% 123.84/19.03 % (1454668)Peak memory usage: 419 MB
% 123.84/19.03 % (1454668)Instructions burned: 3034 (million)
% 123.84/19.03 % (1454673)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1067851757:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2843 on theBenchmark for (2843ds/1016Mi)
% 123.84/19.03 % (1454673)Refutation not found, incomplete strategy
% 123.84/19.03 % (1454673)------------------------------
% 123.84/19.03 % (1454673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454673)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454673)Termination reason: Refutation not found, incomplete strategy
% 123.84/19.03 % (1454673)Time elapsed: 0.041 s
% 123.84/19.03 % (1454673)Peak memory usage: 108 MB
% 123.84/19.03 % (1454673)Instructions burned: 83 (million)
% 123.84/19.03 % (1454675)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3030971298:i=14123:bd=preordered:ins=4_2842 on theBenchmark for (2842ds/14123Mi)
% 123.84/19.03 % (1454673)------------------------------
% 123.84/19.03 % (1454673)------------------------------
% 123.84/19.03 % (1454677)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2824149096:i=5781:kws=precedence:bd=all:rawr=on_2840 on theBenchmark for (2840ds/5781Mi)
% 123.84/19.03 % (1454677)Instruction limit reached!
% 123.84/19.03 % (1454677)------------------------------
% 123.84/19.03 % (1454677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.84/19.03 % (1454677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.84/19.03 % (1454677)CaDiCaL version: 2.1.3
% 123.84/19.03 % (1454677)Termination reason: Instruction limit
% 123.84/19.03 % (1454677)Termination phase: Saturation
% 123.84/19.03 % (1454677)Time elapsed: 1.716 s
% 123.84/19.03 % (1454677)Peak memory usage: 201 MB
% 123.84/19.03 % (1454677)Instructions burned: 5783 (million)
% 123.84/19.03 % (1454667)First to succeed.
% 123.84/19.03 % (1454667)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1454578"
% 123.84/19.03 % (1454679)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2559169042:i=2448:gtgl=5:bd=preordered:gtg=all_2822 on theBenchmark for (2822ds/2448Mi)
% 123.84/19.03 % (1454667)Refutation found. Thanks to Tanya!
% 123.84/19.03 % SZS status Theorem for theBenchmark
% 123.84/19.03 % SZS output start Proof for theBenchmark
% See solution above
% 125.04/19.23 % (1454667)------------------------------
% 125.04/19.23 % (1454667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.04/19.23 % (1454667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.04/19.23 % (1454667)CaDiCaL version: 2.1.3
% 125.04/19.23 % (1454667)Termination reason: Refutation
% 125.04/19.23 % (1454667)Time elapsed: 4.351 s
% 125.04/19.23 % (1454667)Peak memory usage: 204 MB
% 125.04/19.23 % (1454667)Instructions burned: 6577 (million)
% 125.04/19.23 % (1454667)------------------------------
% 125.04/19.23 % (1454667)------------------------------
% 125.04/19.23 % (1454578)Success in time 18.156 s
% 125.04/19.23 % Vampire exiting
%------------------------------------------------------------------------------