%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP652+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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:20 AM UTC 2026
% Result : Theorem 19.74s 7.39s
% Output : Refutation 42.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 52
% Syntax : Number of formulae : 576 ( 87 unt; 18 def)
% Number of atoms : 2862 ( 309 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 4055 (1769 ~;1978 |; 210 &)
% ( 35 <=>; 63 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 19 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 3 con; 0-4 aty)
% Number of variables : 620 ( 0 sgn 607 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f258,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f1055,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( r2_hidden(X0,k1_relat_1(X1))
=> k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t117_funct_1) ).
fof(f1333,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1392,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f2004,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_funct_2) ).
fof(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/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f2017,axiom,
! [X0,X1,X2,X3] :
( ( ~ v1_xboole_0(X0)
& v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1)
& m1_subset_1(X3,X0) )
=> k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k8_funct_2) ).
fof(f2212,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f6422,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f6788,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f7062,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(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)) )
=> ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_tops_2) ).
fof(f7466,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f7470,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_group_1) ).
fof(f8697,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> v4_group_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_group_2) ).
fof(f8765,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> m1_group_2(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_group_2) ).
fof(f8775,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& m1_group_2(X1,X0) )
=> ( X1 = k5_group_2(X0)
<=> u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_group_2) ).
fof(f8780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> k5_group_2(X1) = k5_group_2(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t75_group_2) ).
fof(f8781,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> k5_group_2(X1) = k5_group_2(X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t76_group_2) ).
fof(f8782,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> m1_group_2(k5_group_2(X0),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t77_group_2) ).
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/sandbox/benchmark/theBenchmark.p',d9_group_2) ).
fof(f8898,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_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/sandbox/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
fof(f8907,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_group_1(k5_group_2(X0))
& m1_group_2(k5_group_2(X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_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/sandbox/benchmark/theBenchmark.p',dt_k7_group_2) ).
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/sandbox/benchmark/theBenchmark.p',dt_k5_group_4) ).
fof(f10325,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ( r1_rlvect_1(k5_group_2(X1),X0)
<=> X0 = k2_group_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_group_5) ).
fof(f11144,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))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k2_group_1(X0)) = k2_group_1(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_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/sandbox/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/sandbox/benchmark/theBenchmark.p',t3_latsubgr) ).
fof(f13969,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))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ? [X4] :
( v1_group_1(X4)
& m1_group_2(X4,X1)
& u1_struct_0(X4) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_latsubgr) ).
fof(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/sandbox/benchmark/theBenchmark.p',d3_latsubgr) ).
fof(f14001,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k1_funct_1(k3_latsubgr(X0,X1,X2),k5_group_2(X0)) = k5_group_2(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t35_latsubgr) ).
fof(f14002,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k1_funct_1(k3_latsubgr(X0,X1,X2),k5_group_2(X0)) = k5_group_2(X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f14001]) ).
fof(f14045,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(f14046,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,[],[f14045]) ).
fof(f14051,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(f14052,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,[],[f14051]) ).
fof(f14057,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ? [X4] :
( v1_group_1(X4)
& m1_group_2(X4,X1)
& u1_struct_0(X4) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
| ~ m1_group_2(X3,X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f13969]) ).
fof(f14058,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ? [X4] :
( v1_group_1(X4)
& m1_group_2(X4,X1)
& u1_struct_0(X4) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
| ~ m1_group_2(X3,X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14057]) ).
fof(f14105,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(f14106,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,[],[f14105]) ).
fof(f14111,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k5_group_2(X1) != k1_funct_1(k3_latsubgr(X0,X1,X2),k5_group_2(X0))
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f14002]) ).
fof(f14112,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k5_group_2(X1) != k1_funct_1(k3_latsubgr(X0,X1,X2),k5_group_2(X0))
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f14111]) ).
fof(f14133,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f14141,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8898]) ).
fof(f14142,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14141]) ).
fof(f14147,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8765]) ).
fof(f14148,plain,
! [X0] :
( m1_group_2(X0,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14147]) ).
fof(f14151,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8697]) ).
fof(f14152,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14151]) ).
fof(f14153,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(ennf_transformation,[],[f2017]) ).
fof(f14154,plain,
! [X0,X1,X2,X3] :
( k8_funct_2(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1)
| ~ m1_subset_1(X3,X0) ),
inference(flattening,[],[f14153]) ).
fof(f14240,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(f14241,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,[],[f14240]) ).
fof(f14260,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(f14261,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,[],[f14260]) ).
fof(f14341,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(f14342,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,[],[f14341]) ).
fof(f14343,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f2004]) ).
fof(f14344,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f14343]) ).
fof(f14365,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k2_group_1(X0)) = k2_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f11144]) ).
fof(f14366,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k2_group_1(X0)) = k2_group_1(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14365]) ).
fof(f14453,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f7470]) ).
fof(f14454,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14453]) ).
fof(f14465,plain,
! [X0,X1] :
( ( r1_rlvect_1(k5_group_2(X1),X0)
<=> X0 = k2_group_1(X1) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(ennf_transformation,[],[f10325]) ).
fof(f14466,plain,
! [X0,X1] :
( ( r1_rlvect_1(k5_group_2(X1),X0)
<=> X0 = k2_group_1(X1) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(flattening,[],[f14465]) ).
fof(f14469,plain,
! [X0] :
( ( v1_group_1(k5_group_2(X0))
& m1_group_2(k5_group_2(X0),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8907]) ).
fof(f14470,plain,
! [X0] :
( ( v1_group_1(k5_group_2(X0))
& m1_group_2(k5_group_2(X0),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14469]) ).
fof(f14473,plain,
! [X0] :
( ! [X1] :
( m1_group_2(k5_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(ennf_transformation,[],[f8782]) ).
fof(f14474,plain,
! [X0] :
( ! [X1] :
( m1_group_2(k5_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(flattening,[],[f14473]) ).
fof(f14475,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k5_group_2(X1) = k5_group_2(X2)
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8781]) ).
fof(f14476,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k5_group_2(X1) = k5_group_2(X2)
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14475]) ).
fof(f14477,plain,
! [X0] :
( ! [X1] :
( k5_group_2(X1) = k5_group_2(X0)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8780]) ).
fof(f14478,plain,
! [X0] :
( ! [X1] :
( k5_group_2(X1) = k5_group_2(X0)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14477]) ).
fof(f14479,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_group_2(X0)
<=> u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) )
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f8775]) ).
fof(f14480,plain,
! [X0] :
( ! [X1] :
( ( X1 = k5_group_2(X0)
<=> u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) )
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f14479]) ).
fof(f14681,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1392]) ).
fof(f14682,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f15042,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(f15043,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,[],[f15042]) ).
fof(f15058,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(f15059,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,[],[f15058]) ).
fof(f15132,plain,
! [X0,X1] :
( k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f1055]) ).
fof(f15133,plain,
! [X0,X1] :
( k9_relat_1(X1,k1_tarski(X0)) = k1_tarski(k1_funct_1(X1,X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f15132]) ).
fof(f15185,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2212]) ).
fof(f15186,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f15185]) ).
fof(f15839,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f7466]) ).
fof(f15848,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6422]) ).
fof(f15849,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f15848]) ).
fof(f16447,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f7062]) ).
fof(f16448,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k1_relat_1(X2) = k2_pre_topc(X0)
& r1_tarski(k2_relat_1(X2),k2_pre_topc(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ l1_struct_0(X1) )
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f16447]) ).
fof(f16473,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6788]) ).
fof(f18255,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( v1_group_1(sK20(X0,X1,X2,X3))
& m1_group_2(sK20(X0,X1,X2,X3),X1)
& k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) = u1_struct_0(sK20(X0,X1,X2,X3)) )
| ~ m1_group_2(X3,X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X4,sK20(X0,X1,X2,X3))],[f14058]) ).
fof(f18264,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,[],[f14106]) ).
fof(f18265,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,[],[f18264]) ).
fof(f18266,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ( k1_funct_1(X3,sK23(X0,X1,X2,X3)) != k5_group_4(X1,sK24(X0,X1,X2,X3))
& sK24(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK23(X0,X1,X2,X3)))
& m1_subset_1(sK24(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
& v1_group_1(sK23(X0,X1,X2,X3))
& m1_group_2(sK23(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,[sK23,sK24]),skolemize(X4,sK23(X0,X1,X2,X3)),skolemize(X5,sK24(X0,X1,X2,X3))],[f18265]) ).
fof(f18267,plain,
( k5_group_2(sK26) != k1_funct_1(k3_latsubgr(sK25,sK26,sK27),k5_group_2(sK25))
& v1_funct_1(sK27)
& v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
& v1_group_6(sK27,sK25,sK26)
& m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
& ~ v3_struct_0(sK26)
& v3_group_1(sK26)
& v4_group_1(sK26)
& l1_group_1(sK26)
& ~ v3_struct_0(sK25)
& v3_group_1(sK25)
& v4_group_1(sK25)
& l1_group_1(sK25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27]),skolemize(X0,sK25),skolemize(X1,sK26),skolemize(X2,sK27)],[f14112]) ).
fof(f18281,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f14133]) ).
fof(f18292,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(f18307,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,[],[f14241]) ).
fof(f18368,plain,
! [X0,X1] :
( ( ( r1_rlvect_1(k5_group_2(X1),X0)
| k2_group_1(X1) != X0 )
& ( X0 = k2_group_1(X1)
| ~ r1_rlvect_1(k5_group_2(X1),X0) ) )
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(nnf_transformation,[],[f14466]) ).
fof(f18369,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = k5_group_2(X0)
| u1_struct_0(X1) != k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) )
& ( u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0))
| k5_group_2(X0) != X1 ) )
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f14480]) ).
fof(f19566,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,[],[f14046]) ).
fof(f19567,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,[],[f14046]) ).
fof(f19568,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(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(k3_latsubgr(X0,X1,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,[],[f14046]) ).
fof(f19574,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f14052]) ).
fof(f19578,plain,
! [X2,X3,X0,X1] :
( ~ v1_group_6(X2,X0,X1)
| ~ m1_group_2(X3,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) = u1_struct_0(sK20(X0,X1,X2,X3))
| ~ 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,[],[f18255]) ).
fof(f19579,plain,
! [X2,X3,X0,X1] :
( ~ l1_group_1(X0)
| ~ m1_group_2(X3,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| m1_group_2(sK20(X0,X1,X2,X3),X1) ),
inference(cnf_transformation,[],[f18255]) ).
fof(f19580,plain,
! [X2,X3,X0,X1] :
( v1_group_1(sK20(X0,X1,X2,X3))
| ~ m1_group_2(X3,X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f18255]) ).
fof(f19614,plain,
! [X2,X3,X0,X1,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(cnf_transformation,[],[f18266]) ).
fof(f19622,plain,
l1_group_1(sK25),
inference(cnf_transformation,[],[f18267]) ).
fof(f19623,plain,
v4_group_1(sK25),
inference(cnf_transformation,[],[f18267]) ).
fof(f19624,plain,
v3_group_1(sK25),
inference(cnf_transformation,[],[f18267]) ).
fof(f19625,plain,
~ v3_struct_0(sK25),
inference(cnf_transformation,[],[f18267]) ).
fof(f19626,plain,
l1_group_1(sK26),
inference(cnf_transformation,[],[f18267]) ).
fof(f19627,plain,
v4_group_1(sK26),
inference(cnf_transformation,[],[f18267]) ).
fof(f19628,plain,
v3_group_1(sK26),
inference(cnf_transformation,[],[f18267]) ).
fof(f19629,plain,
~ v3_struct_0(sK26),
inference(cnf_transformation,[],[f18267]) ).
fof(f19630,plain,
m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26)),
inference(cnf_transformation,[],[f18267]) ).
fof(f19631,plain,
v1_group_6(sK27,sK25,sK26),
inference(cnf_transformation,[],[f18267]) ).
fof(f19632,plain,
v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26)),
inference(cnf_transformation,[],[f18267]) ).
fof(f19633,plain,
v1_funct_1(sK27),
inference(cnf_transformation,[],[f18267]) ).
fof(f19634,plain,
k5_group_2(sK26) != k1_funct_1(k3_latsubgr(sK25,sK26,sK27),k5_group_2(sK25)),
inference(cnf_transformation,[],[f18267]) ).
fof(f19660,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f18281]) ).
fof(f19679,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| l1_group_1(X1) ),
inference(cnf_transformation,[],[f14142]) ).
fof(f19680,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v3_group_1(X1) ),
inference(cnf_transformation,[],[f14142]) ).
fof(f19681,plain,
! [X0,X1] :
( ~ v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14142]) ).
fof(f19684,plain,
! [X0] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| m1_group_2(X0,X0) ),
inference(cnf_transformation,[],[f14148]) ).
fof(f19686,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v4_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14152]) ).
fof(f19687,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| v1_xboole_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k1_funct_1(X2,X3) = k8_funct_2(X0,X1,X2,X3)
| ~ m1_subset_1(X3,X0) ),
inference(cnf_transformation,[],[f14154]) ).
fof(f19696,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f18292]) ).
fof(f19809,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,[],[f18307]) ).
fof(f19833,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,[],[f14261]) ).
fof(f19834,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| v1_group_1(k5_group_4(X0,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f14261]) ).
fof(f19941,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| k9_relat_1(X2,X3) = k2_funct_2(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f14342]) ).
fof(f19942,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f14344]) ).
fof(f19961,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_group_6(X2,X0,X1)
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,k2_group_1(X0)) ),
inference(cnf_transformation,[],[f14366]) ).
fof(f20054,plain,
! [X0] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f14454]) ).
fof(f20067,plain,
! [X0,X1] :
( ~ v4_group_1(X1)
| ~ r1_rlvect_1(k5_group_2(X1),X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| k2_group_1(X1) = X0
| ~ l1_group_1(X1) ),
inference(cnf_transformation,[],[f18368]) ).
fof(f20068,plain,
! [X0,X1] :
( r1_rlvect_1(k5_group_2(X1),X0)
| k2_group_1(X1) != X0
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(cnf_transformation,[],[f18368]) ).
fof(f20070,plain,
! [X0] :
( m1_group_2(k5_group_2(X0),X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14470]) ).
fof(f20071,plain,
! [X0] :
( v1_group_1(k5_group_2(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14470]) ).
fof(f20073,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| m1_group_2(k5_group_2(X0),X1) ),
inference(cnf_transformation,[],[f14474]) ).
fof(f20074,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0)
| k5_group_2(X1) = k5_group_2(X2)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14476]) ).
fof(f20075,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| k5_group_2(X0) = k5_group_2(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f14478]) ).
fof(f20076,plain,
! [X0,X1] :
( u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0))
| k5_group_2(X0) != X1
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f18369]) ).
fof(f20077,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| u1_struct_0(X1) != k6_domain_1(u1_struct_0(X0),k2_group_1(X0))
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| k5_group_2(X0) = X1 ),
inference(cnf_transformation,[],[f18369]) ).
fof(f20409,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f14681]) ).
fof(f20410,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f14682]) ).
fof(f20923,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f15043]) ).
fof(f20937,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| u1_struct_0(X1) = k7_group_2(X0,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f15059]) ).
fof(f21005,plain,
! [X0,X1] :
( k1_tarski(k1_funct_1(X1,X0)) = k9_relat_1(X1,k1_tarski(X0))
| ~ r2_hidden(X0,k1_relat_1(X1))
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f15133]) ).
fof(f21085,plain,
! [X0,X1] :
( k1_tarski(X1) = k6_domain_1(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f15186]) ).
fof(f21920,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f15839]) ).
fof(f21931,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f15849]) ).
fof(f22400,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f258]) ).
fof(f22770,plain,
! [X2,X0,X1] :
( ~ l1_struct_0(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| k1_relat_1(X2) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f16448]) ).
fof(f22805,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f16473]) ).
fof(f25652,plain,
! [X0,X1] :
( ~ v1_relat_1(X1)
| ~ r2_hidden(X0,k1_relat_1(X1))
| k2_tarski(k1_funct_1(X1,X0),k1_funct_1(X1,X0)) = k9_relat_1(X1,k2_tarski(X0,X0))
| ~ v1_funct_1(X1) ),
inference(definition_unfolding,[],[f21005,f22400,f22400]) ).
fof(f25670,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0)
| k6_domain_1(X0,X1) = k2_tarski(X1,X1) ),
inference(definition_unfolding,[],[f21085,f22400]) ).
fof(f26492,plain,
! [X2,X0] :
( ~ v4_group_1(X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(u1_struct_0(X2),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| r1_group_2(X0,k5_group_4(X0,u1_struct_0(X2)),X2)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f19574]) ).
fof(f26513,plain,
! [X2,X3,X0,X1,X6] :
( k1_funct_1(X3,X6) = k5_group_4(X1,k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)))
| ~ m1_subset_1(k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)),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(equality_resolution,[],[f19614]) ).
fof(f26514,plain,
! [X2,X0,X1,X6] :
( ~ v1_funct_2(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m1_subset_1(k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6)),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_group_1(X6)
| ~ m1_group_2(X6,X0)
| ~ v1_funct_1(k3_latsubgr(X0,X1,X2))
| k5_group_4(X1,k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X6))) = k1_funct_1(k3_latsubgr(X0,X1,X2),X6)
| ~ m2_relset_1(k3_latsubgr(X0,X1,X2),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(equality_resolution,[],[f26513]) ).
fof(f26548,plain,
! [X1] :
( r1_rlvect_1(k5_group_2(X1),k2_group_1(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(equality_resolution,[],[f20068]) ).
fof(f26549,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v1_group_1(k5_group_2(X0))
| ~ m1_group_2(k5_group_2(X0),X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) = u1_struct_0(k5_group_2(X0)) ),
inference(equality_resolution,[],[f20076]) ).
fof(f27807,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f22805,f21920]) ).
fof(f27808,plain,
u1_struct_0(sK26) = k2_pre_topc(sK26),
inference(resolution,[],[f27807,f19626]) ).
fof(f27809,plain,
u1_struct_0(sK25) = k2_pre_topc(sK25),
inference(resolution,[],[f27807,f19622]) ).
fof(f27810,plain,
v1_funct_2(sK27,u1_struct_0(sK25),k2_pre_topc(sK26)),
inference(superposition,[],[f19632,f27808]) ).
fof(f27811,plain,
m2_relset_1(sK27,u1_struct_0(sK25),k2_pre_topc(sK26)),
inference(superposition,[],[f19630,f27808]) ).
fof(f27812,plain,
m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)),
inference(forward_demodulation,[],[f27811,f27809]) ).
fof(f27813,plain,
v1_funct_2(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)),
inference(forward_demodulation,[],[f27810,f27809]) ).
fof(f27818,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,X1,sK27))
| ~ v1_funct_2(sK27,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(sK27,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(resolution,[],[f19568,f19633]) ).
fof(f27819,plain,
! [X0] :
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,sK26,sK27))
| ~ v1_funct_2(sK27,u1_struct_0(X0),u1_struct_0(sK26))
| ~ m1_relset_1(sK27,u1_struct_0(X0),u1_struct_0(sK26)) ),
inference(resolution,[],[f27818,f19626]) ).
fof(f27822,plain,
! [X0] :
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,sK26,sK27))
| ~ v1_funct_2(sK27,u1_struct_0(X0),u1_struct_0(sK26))
| ~ m1_relset_1(sK27,u1_struct_0(X0),u1_struct_0(sK26)) ),
inference(forward_subsumption_resolution,[],[f27819,f19629]) ).
fof(f27824,plain,
! [X0] :
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(sK26)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,sK26,sK27))
| ~ v1_funct_2(sK27,u1_struct_0(X0),u1_struct_0(sK26))
| ~ m1_relset_1(sK27,u1_struct_0(X0),u1_struct_0(sK26)) ),
inference(forward_subsumption_resolution,[],[f27822,f19628]) ).
fof(f27826,plain,
! [X0] :
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,sK26,sK27))
| ~ v1_funct_2(sK27,u1_struct_0(X0),u1_struct_0(sK26))
| ~ m1_relset_1(sK27,u1_struct_0(X0),u1_struct_0(sK26)) ),
inference(forward_subsumption_resolution,[],[f27824,f19627]) ).
fof(f27828,plain,
! [X0] :
( ~ v1_funct_2(sK27,u1_struct_0(X0),k2_pre_topc(sK26))
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,sK26,sK27))
| ~ m1_relset_1(sK27,u1_struct_0(X0),u1_struct_0(sK26)) ),
inference(forward_demodulation,[],[f27826,f27808]) ).
fof(f27830,plain,
! [X0] :
( ~ v1_funct_2(sK27,u1_struct_0(X0),k2_pre_topc(sK26))
| ~ m1_relset_1(sK27,u1_struct_0(X0),k2_pre_topc(sK26))
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(X0)
| v1_funct_1(k3_latsubgr(X0,sK26,sK27)) ),
inference(forward_demodulation,[],[f27828,f27808]) ).
fof(f27832,plain,
( ~ v1_funct_2(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| v3_struct_0(sK25)
| v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
inference(superposition,[],[f27830,f27809]) ).
fof(f27833,plain,
( ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| v3_struct_0(sK25)
| v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
inference(forward_subsumption_resolution,[],[f27832,f27813]) ).
fof(f27835,plain,
( ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| v3_struct_0(sK25)
| v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
inference(forward_subsumption_resolution,[],[f27833,f19624]) ).
fof(f27837,plain,
( ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ l1_group_1(sK25)
| v3_struct_0(sK25)
| v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
inference(forward_subsumption_resolution,[],[f27835,f19623]) ).
fof(f27839,plain,
( ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| v3_struct_0(sK25)
| v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
inference(forward_subsumption_resolution,[],[f27837,f19622]) ).
fof(f27841,plain,
( ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
inference(forward_subsumption_resolution,[],[f27839,f19625]) ).
fof(f27853,definition,
( spl797_26
<=> v1_funct_1(k3_latsubgr(sK25,sK26,sK27)) ),
introduced(definition,[new_symbols(definition,[spl797_26])],[avatar_definition]) ).
fof(f27854,plain,
( v1_funct_1(k3_latsubgr(sK25,sK26,sK27))
| ~ spl797_26 ),
inference(avatar_component_clause,[],[f27853]) ).
fof(f27856,definition,
( spl797_27
<=> m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)) ),
introduced(definition,[new_symbols(definition,[spl797_27])],[avatar_definition]) ).
fof(f27857,plain,
( ~ m1_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| spl797_27 ),
inference(avatar_component_clause,[],[f27856]) ).
fof(f27858,plain,
( spl797_26
| ~ spl797_27 ),
inference(avatar_split_clause,[],[f27841,f27856,f27853]) ).
fof(f27860,plain,
( ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| spl797_27 ),
inference(resolution,[],[f27857,f19696]) ).
fof(f27862,plain,
( $false
| spl797_27 ),
inference(forward_subsumption_resolution,[],[f27860,f27812]) ).
fof(f27863,plain,
spl797_27,
inference(avatar_contradiction_clause,[],[f27862]) ).
fof(f27925,definition,
( spl797_38
<=> v1_group_1(k5_group_2(sK26)) ),
introduced(definition,[new_symbols(definition,[spl797_38])],[avatar_definition]) ).
fof(f27926,plain,
( v1_group_1(k5_group_2(sK26))
| ~ spl797_38 ),
inference(avatar_component_clause,[],[f27925]) ).
fof(f27946,definition,
( spl797_43
<=> v1_group_1(k5_group_2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl797_43])],[avatar_definition]) ).
fof(f27947,plain,
( v1_group_1(k5_group_2(sK25))
| ~ spl797_43 ),
inference(avatar_component_clause,[],[f27946]) ).
fof(f27949,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(resolution,[],[f21931,f21920]) ).
fof(f27950,plain,
( ~ v1_xboole_0(k2_pre_topc(sK26))
| v3_struct_0(sK26)
| ~ l1_group_1(sK26) ),
inference(superposition,[],[f27949,f27808]) ).
fof(f27951,plain,
( ~ v1_xboole_0(k2_pre_topc(sK25))
| v3_struct_0(sK25)
| ~ l1_group_1(sK25) ),
inference(superposition,[],[f27949,f27809]) ).
fof(f27952,plain,
( ~ v1_xboole_0(k2_pre_topc(sK25))
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f27951,f19625]) ).
fof(f27953,plain,
( ~ v1_xboole_0(k2_pre_topc(sK26))
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f27950,f19629]) ).
fof(f27954,plain,
~ v1_xboole_0(k2_pre_topc(sK25)),
inference(forward_subsumption_resolution,[],[f27952,f19622]) ).
fof(f27955,plain,
~ v1_xboole_0(k2_pre_topc(sK26)),
inference(forward_subsumption_resolution,[],[f27953,f19626]) ).
fof(f27964,plain,
( v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| m1_group_2(sK26,sK26) ),
inference(resolution,[],[f19684,f19626]) ).
fof(f27965,plain,
( v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| m1_group_2(sK25,sK25) ),
inference(resolution,[],[f19684,f19622]) ).
fof(f27966,plain,
( ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| m1_group_2(sK25,sK25) ),
inference(forward_subsumption_resolution,[],[f27965,f19625]) ).
fof(f27967,plain,
( ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| m1_group_2(sK26,sK26) ),
inference(forward_subsumption_resolution,[],[f27964,f19629]) ).
fof(f27968,plain,
( ~ v4_group_1(sK25)
| m1_group_2(sK25,sK25) ),
inference(forward_subsumption_resolution,[],[f27966,f19624]) ).
fof(f27969,plain,
( ~ v4_group_1(sK26)
| m1_group_2(sK26,sK26) ),
inference(forward_subsumption_resolution,[],[f27967,f19628]) ).
fof(f27970,plain,
m1_group_2(sK25,sK25),
inference(forward_subsumption_resolution,[],[f27968,f19623]) ).
fof(f27971,plain,
m1_group_2(sK26,sK26),
inference(forward_subsumption_resolution,[],[f27969,f19627]) ).
fof(f27990,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| m1_group_2(k5_group_2(sK26),X0) ),
inference(resolution,[],[f20073,f19626]) ).
fof(f27991,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| m1_group_2(k5_group_2(sK25),X0) ),
inference(resolution,[],[f20073,f19622]) ).
fof(f27992,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| m1_group_2(k5_group_2(sK25),X0) ),
inference(forward_subsumption_resolution,[],[f27991,f19625]) ).
fof(f27993,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| m1_group_2(k5_group_2(sK26),X0) ),
inference(forward_subsumption_resolution,[],[f27990,f19629]) ).
fof(f27994,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v4_group_1(sK25)
| m1_group_2(k5_group_2(sK25),X0) ),
inference(forward_subsumption_resolution,[],[f27992,f19624]) ).
fof(f27995,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| ~ v4_group_1(sK26)
| m1_group_2(k5_group_2(sK26),X0) ),
inference(forward_subsumption_resolution,[],[f27993,f19628]) ).
fof(f27996,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| m1_group_2(k5_group_2(sK25),X0) ),
inference(forward_subsumption_resolution,[],[f27994,f19623]) ).
fof(f27997,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| m1_group_2(k5_group_2(sK26),X0) ),
inference(forward_subsumption_resolution,[],[f27995,f19627]) ).
fof(f27999,plain,
m1_group_2(k5_group_2(sK26),sK26),
inference(resolution,[],[f27997,f27971]) ).
fof(f28014,plain,
m1_group_2(k5_group_2(sK25),sK25),
inference(resolution,[],[f27996,f27970]) ).
fof(f28076,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f20410,f20409]) ).
fof(f28078,plain,
v1_relat_1(sK27),
inference(resolution,[],[f28076,f27812]) ).
fof(f28082,plain,
( v3_struct_0(sK26)
| m1_subset_1(k2_group_1(sK26),u1_struct_0(sK26)) ),
inference(resolution,[],[f20054,f19626]) ).
fof(f28083,plain,
( v3_struct_0(sK25)
| m1_subset_1(k2_group_1(sK25),u1_struct_0(sK25)) ),
inference(resolution,[],[f20054,f19622]) ).
fof(f28084,plain,
m1_subset_1(k2_group_1(sK25),u1_struct_0(sK25)),
inference(forward_subsumption_resolution,[],[f28083,f19625]) ).
fof(f28085,plain,
m1_subset_1(k2_group_1(sK26),u1_struct_0(sK26)),
inference(forward_subsumption_resolution,[],[f28082,f19629]) ).
fof(f28086,plain,
m1_subset_1(k2_group_1(sK25),k2_pre_topc(sK25)),
inference(forward_demodulation,[],[f28084,f27809]) ).
fof(f28087,plain,
m1_subset_1(k2_group_1(sK26),k2_pre_topc(sK26)),
inference(forward_demodulation,[],[f28085,f27808]) ).
fof(f28090,plain,
( ~ v1_group_1(k5_group_2(sK26))
| ~ m1_group_2(k5_group_2(sK26),sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK26),k2_group_1(sK26)) ),
inference(resolution,[],[f26549,f19626]) ).
fof(f28091,plain,
( ~ v1_group_1(k5_group_2(sK25))
| ~ m1_group_2(k5_group_2(sK25),sK25)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| u1_struct_0(k5_group_2(sK25)) = k6_domain_1(u1_struct_0(sK25),k2_group_1(sK25)) ),
inference(resolution,[],[f26549,f19622]) ).
fof(f28092,plain,
( ~ v1_group_1(k5_group_2(sK25))
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| u1_struct_0(k5_group_2(sK25)) = k6_domain_1(u1_struct_0(sK25),k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28091,f28014]) ).
fof(f28093,plain,
( ~ v1_group_1(k5_group_2(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK26),k2_group_1(sK26)) ),
inference(forward_subsumption_resolution,[],[f28090,f27999]) ).
fof(f28094,plain,
( ~ v1_group_1(k5_group_2(sK25))
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| u1_struct_0(k5_group_2(sK25)) = k6_domain_1(u1_struct_0(sK25),k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28092,f19625]) ).
fof(f28095,plain,
( ~ v1_group_1(k5_group_2(sK26))
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK26),k2_group_1(sK26)) ),
inference(forward_subsumption_resolution,[],[f28093,f19629]) ).
fof(f28096,plain,
( ~ v1_group_1(k5_group_2(sK25))
| ~ v4_group_1(sK25)
| u1_struct_0(k5_group_2(sK25)) = k6_domain_1(u1_struct_0(sK25),k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28094,f19624]) ).
fof(f28097,plain,
( ~ v1_group_1(k5_group_2(sK26))
| ~ v4_group_1(sK26)
| u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK26),k2_group_1(sK26)) ),
inference(forward_subsumption_resolution,[],[f28095,f19628]) ).
fof(f28098,plain,
( ~ v1_group_1(k5_group_2(sK25))
| u1_struct_0(k5_group_2(sK25)) = k6_domain_1(u1_struct_0(sK25),k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28096,f19623]) ).
fof(f28099,plain,
( ~ v1_group_1(k5_group_2(sK26))
| u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK26),k2_group_1(sK26)) ),
inference(forward_subsumption_resolution,[],[f28097,f19627]) ).
fof(f28100,plain,
( u1_struct_0(k5_group_2(sK25)) = k6_domain_1(k2_pre_topc(sK25),k2_group_1(sK25))
| ~ v1_group_1(k5_group_2(sK25)) ),
inference(forward_demodulation,[],[f28098,f27809]) ).
fof(f28101,plain,
( u1_struct_0(k5_group_2(sK26)) = k6_domain_1(k2_pre_topc(sK26),k2_group_1(sK26))
| ~ v1_group_1(k5_group_2(sK26)) ),
inference(forward_demodulation,[],[f28099,f27808]) ).
fof(f28102,plain,
( ~ v1_group_1(k5_group_2(sK25))
| spl797_43 ),
inference(avatar_component_clause,[],[f27946]) ).
fof(f28104,definition,
( spl797_48
<=> u1_struct_0(k5_group_2(sK25)) = k6_domain_1(k2_pre_topc(sK25),k2_group_1(sK25)) ),
introduced(definition,[new_symbols(definition,[spl797_48])],[avatar_definition]) ).
fof(f28105,plain,
( u1_struct_0(k5_group_2(sK25)) = k6_domain_1(k2_pre_topc(sK25),k2_group_1(sK25))
| ~ spl797_48 ),
inference(avatar_component_clause,[],[f28104]) ).
fof(f28106,plain,
( ~ spl797_43
| spl797_48 ),
inference(avatar_split_clause,[],[f28100,f28104,f27946]) ).
fof(f28107,plain,
( ~ v1_group_1(k5_group_2(sK26))
| spl797_38 ),
inference(avatar_component_clause,[],[f27925]) ).
fof(f28109,definition,
( spl797_49
<=> u1_struct_0(k5_group_2(sK26)) = k6_domain_1(k2_pre_topc(sK26),k2_group_1(sK26)) ),
introduced(definition,[new_symbols(definition,[spl797_49])],[avatar_definition]) ).
fof(f28110,plain,
( u1_struct_0(k5_group_2(sK26)) = k6_domain_1(k2_pre_topc(sK26),k2_group_1(sK26))
| ~ spl797_49 ),
inference(avatar_component_clause,[],[f28109]) ).
fof(f28111,plain,
( ~ spl797_38
| spl797_49 ),
inference(avatar_split_clause,[],[f28101,f28109,f27925]) ).
fof(f28113,plain,
( v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| spl797_38 ),
inference(resolution,[],[f28107,f20071]) ).
fof(f28115,plain,
( ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| spl797_38 ),
inference(forward_subsumption_resolution,[],[f28113,f19629]) ).
fof(f28116,plain,
( ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| spl797_38 ),
inference(forward_subsumption_resolution,[],[f28115,f19628]) ).
fof(f28117,plain,
( ~ l1_group_1(sK26)
| spl797_38 ),
inference(forward_subsumption_resolution,[],[f28116,f19627]) ).
fof(f28118,plain,
( $false
| spl797_38 ),
inference(forward_subsumption_resolution,[],[f28117,f19626]) ).
fof(f28119,plain,
spl797_38,
inference(avatar_contradiction_clause,[],[f28118]) ).
fof(f28121,plain,
( v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_43 ),
inference(resolution,[],[f28102,f20071]) ).
fof(f28123,plain,
( ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_43 ),
inference(forward_subsumption_resolution,[],[f28121,f19625]) ).
fof(f28124,plain,
( ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_43 ),
inference(forward_subsumption_resolution,[],[f28123,f19624]) ).
fof(f28125,plain,
( ~ l1_group_1(sK25)
| spl797_43 ),
inference(forward_subsumption_resolution,[],[f28124,f19623]) ).
fof(f28126,plain,
( $false
| spl797_43 ),
inference(forward_subsumption_resolution,[],[f28125,f19622]) ).
fof(f28127,plain,
spl797_43,
inference(avatar_contradiction_clause,[],[f28126]) ).
fof(f28136,plain,
! [X2,X0,X1] :
( ~ l1_struct_0(X2)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ l1_group_1(X1) ),
inference(resolution,[],[f22770,f21920]) ).
fof(f28137,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X2)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f28136,f21920]) ).
fof(f28138,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK26)) ),
inference(resolution,[],[f28137,f19626]) ).
fof(f28141,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(sK26))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK26)) ),
inference(forward_subsumption_resolution,[],[f28138,f19629]) ).
fof(f28143,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,u1_struct_0(X1),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(sK26)) ),
inference(forward_demodulation,[],[f28141,f27808]) ).
fof(f28145,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ m2_relset_1(X0,u1_struct_0(X1),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(X1)
| ~ v1_funct_2(X0,u1_struct_0(X1),k2_pre_topc(sK26)) ),
inference(forward_demodulation,[],[f28143,f27808]) ).
fof(f28147,plain,
! [X0] :
( ~ m2_relset_1(X0,u1_struct_0(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK25)
| ~ v1_funct_2(X0,u1_struct_0(sK25),k2_pre_topc(sK26)) ),
inference(resolution,[],[f28145,f19622]) ).
fof(f28148,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK25)
| ~ v1_funct_2(X0,u1_struct_0(sK25),k2_pre_topc(sK26)) ),
inference(forward_demodulation,[],[f28147,f27809]) ).
fof(f28150,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m2_relset_1(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| k1_relat_1(X0) = k2_pre_topc(sK25) ),
inference(forward_demodulation,[],[f28148,f27809]) ).
fof(f28158,plain,
( ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(sK27)
| k2_pre_topc(sK25) = k1_relat_1(sK27) ),
inference(resolution,[],[f28150,f27813]) ).
fof(f28159,plain,
( ~ v1_funct_1(sK27)
| k2_pre_topc(sK25) = k1_relat_1(sK27) ),
inference(forward_subsumption_resolution,[],[f28158,f27812]) ).
fof(f28160,plain,
k2_pre_topc(sK25) = k1_relat_1(sK27),
inference(forward_subsumption_resolution,[],[f28159,f19633]) ).
fof(f28183,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X1,X0,X2)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0)
| k1_funct_1(X1,X3) = k8_funct_2(X0,X2,X1,X3)
| ~ m1_subset_1(X3,X0)
| ~ m2_relset_1(X1,X0,X2) ),
inference(resolution,[],[f19687,f19696]) ).
fof(f28223,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,X1,X2)
| k9_relat_1(X0,X3) = k2_funct_2(X1,X2,X0,X3)
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[],[f19941,f19696]) ).
fof(f28241,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| ~ v1_funct_1(k3_latsubgr(X0,X1,X2))
| k5_group_4(X1,k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))) = k1_funct_1(k3_latsubgr(X0,X1,X2),X3)
| ~ m2_relset_1(k3_latsubgr(X0,X1,X2),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)
| 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(resolution,[],[f26514,f19567]) ).
fof(f28242,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)),k1_zfmisc_1(u1_struct_0(X1)))
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| ~ v1_funct_1(k3_latsubgr(X0,X1,X2))
| k5_group_4(X1,k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))) = k1_funct_1(k3_latsubgr(X0,X1,X2),X3)
| ~ m2_relset_1(k3_latsubgr(X0,X1,X2),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)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f28241]) ).
fof(f28243,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| ~ v1_funct_1(k3_latsubgr(X0,X1,X2))
| k5_group_4(X1,k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))) = k1_funct_1(k3_latsubgr(X0,X1,X2),X3)
| ~ m1_subset_1(k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)),k1_zfmisc_1(u1_struct_0(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(forward_subsumption_resolution,[],[f28242,f19696]) ).
fof(f28411,plain,
! [X0] :
( v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| v1_group_1(k5_group_4(sK26,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(resolution,[],[f19834,f19626]) ).
fof(f28414,plain,
! [X0] :
( ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| v1_group_1(k5_group_4(sK26,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f28411,f19629]) ).
fof(f28416,plain,
! [X0] :
( ~ v4_group_1(sK26)
| v1_group_1(k5_group_4(sK26,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f28414,f19628]) ).
fof(f28418,plain,
! [X0] :
( v1_group_1(k5_group_4(sK26,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f28416,f19627]) ).
fof(f28420,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK26)))
| v1_group_1(k5_group_4(sK26,X0)) ),
inference(forward_demodulation,[],[f28418,f27808]) ).
fof(f28831,plain,
! [X0] :
( ~ v1_funct_1(sK27)
| v1_xboole_0(k2_pre_topc(sK25))
| k1_funct_1(sK27,X0) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,X0)
| ~ m1_subset_1(X0,k2_pre_topc(sK25))
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)) ),
inference(resolution,[],[f28183,f27813]) ).
fof(f28834,plain,
! [X0] :
( v1_xboole_0(k2_pre_topc(sK25))
| k1_funct_1(sK27,X0) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,X0)
| ~ m1_subset_1(X0,k2_pre_topc(sK25))
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)) ),
inference(forward_subsumption_resolution,[],[f28831,f19633]) ).
fof(f28837,plain,
! [X0] :
( k1_funct_1(sK27,X0) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,X0)
| ~ m1_subset_1(X0,k2_pre_topc(sK25))
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)) ),
inference(forward_subsumption_resolution,[],[f28834,f27954]) ).
fof(f28839,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK25))
| k1_funct_1(sK27,X0) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,X0) ),
inference(forward_subsumption_resolution,[],[f28837,f27812]) ).
fof(f28845,plain,
k1_funct_1(sK27,k2_group_1(sK25)) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,k2_group_1(sK25)),
inference(resolution,[],[f28839,f28086]) ).
fof(f28851,plain,
! [X2,X3,X0,X1] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ v1_funct_1(k3_latsubgr(X1,X2,X3))
| k5_group_4(X2,k2_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(X1,X2,X3),X0)
| ~ m1_subset_1(k2_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,u1_struct_0(X0)),k1_zfmisc_1(u1_struct_0(X2)))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f28243,f19566]) ).
fof(f28852,plain,
! [X2,X3,X0,X1] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ v1_funct_1(k3_latsubgr(X1,X2,X3))
| k5_group_4(X2,k2_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(X1,X2,X3),X0)
| ~ m1_subset_1(k2_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,u1_struct_0(X0)),k1_zfmisc_1(u1_struct_0(X2)))
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(duplicate_literal_removal,[],[f28851]) ).
fof(f28853,plain,
! [X2,X3,X0,X1] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,X1)
| ~ v1_funct_1(k3_latsubgr(X1,X2,X3))
| k5_group_4(X2,k2_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(X1,X2,X3),X0)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(forward_subsumption_resolution,[],[f28852,f19942]) ).
fof(f28854,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(k3_latsubgr(X1,X2,X3))
| ~ m1_group_2(X0,X1)
| ~ v1_group_1(X0)
| k5_group_4(X2,k2_funct_2(u1_struct_0(X1),u1_struct_0(X2),X3,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(X1,X2,X3),X0)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(forward_subsumption_resolution,[],[f28853,f19696]) ).
fof(f28855,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ v1_funct_1(sK27)
| ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(resolution,[],[f28854,f27854]) ).
fof(f28856,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28855,f19633]) ).
fof(f28857,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28856,f19632]) ).
fof(f28858,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28857,f19630]) ).
fof(f28859,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28858,f19629]) ).
fof(f28860,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28859,f19628]) ).
fof(f28861,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28860,f19627]) ).
fof(f28862,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28861,f19626]) ).
fof(f28863,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28862,f19625]) ).
fof(f28864,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28863,f19624]) ).
fof(f28865,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0)
| ~ l1_group_1(sK25) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28864,f19623]) ).
fof(f28866,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0)
| k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0))) = k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0) )
| ~ spl797_26 ),
inference(forward_subsumption_resolution,[],[f28865,f19622]) ).
fof(f28867,plain,
( ! [X0] :
( k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0) = k5_group_4(sK26,k2_funct_2(u1_struct_0(sK25),k2_pre_topc(sK26),sK27,u1_struct_0(X0)))
| ~ m1_group_2(X0,sK25)
| ~ v1_group_1(X0) )
| ~ spl797_26 ),
inference(forward_demodulation,[],[f28866,f27808]) ).
fof(f28868,plain,
( ! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK25)
| k1_funct_1(k3_latsubgr(sK25,sK26,sK27),X0) = k5_group_4(sK26,k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,u1_struct_0(X0))) )
| ~ spl797_26 ),
inference(forward_demodulation,[],[f28867,f27809]) ).
fof(f28871,plain,
( ~ m1_group_2(k5_group_2(sK25),sK25)
| k1_funct_1(k3_latsubgr(sK25,sK26,sK27),k5_group_2(sK25)) = k5_group_4(sK26,k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,u1_struct_0(k5_group_2(sK25))))
| ~ spl797_26
| ~ spl797_43 ),
inference(resolution,[],[f28868,f27947]) ).
fof(f28873,plain,
( k1_funct_1(k3_latsubgr(sK25,sK26,sK27),k5_group_2(sK25)) = k5_group_4(sK26,k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,u1_struct_0(k5_group_2(sK25))))
| ~ spl797_26
| ~ spl797_43 ),
inference(forward_subsumption_resolution,[],[f28871,f28014]) ).
fof(f28920,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK25),u1_struct_0(X1))
| ~ v1_group_6(X0,sK25,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK25),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(resolution,[],[f19961,f19622]) ).
fof(f28921,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK25),u1_struct_0(X1))
| ~ v1_group_6(X0,sK25,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK25),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28920,f19625]) ).
fof(f28923,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK25),u1_struct_0(X1))
| ~ v1_group_6(X0,sK25,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK25),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(sK25)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28921,f19624]) ).
fof(f28925,plain,
! [X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,u1_struct_0(sK25),u1_struct_0(X1))
| ~ v1_group_6(X0,sK25,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK25),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28923,f19623]) ).
fof(f28927,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,X1)
| ~ m2_relset_1(X0,u1_struct_0(sK25),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(forward_demodulation,[],[f28925,f27809]) ).
fof(f28929,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(X1))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| k2_group_1(X1) = k8_funct_2(u1_struct_0(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(forward_demodulation,[],[f28927,f27809]) ).
fof(f28931,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(X1))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(X1))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| k2_group_1(X1) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(X1),X0,k2_group_1(sK25)) ),
inference(forward_demodulation,[],[f28929,f27809]) ).
fof(f28933,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(sK26),X0,k2_group_1(sK25)) ),
inference(resolution,[],[f28931,f19626]) ).
fof(f28936,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(sK26),X0,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28933,f19629]) ).
fof(f28938,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| ~ v4_group_1(sK26)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(sK26),X0,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28936,f19628]) ).
fof(f28940,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(sK26),X0,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28938,f19627]) ).
fof(f28942,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(sK26),X0,k2_group_1(sK25)) ),
inference(forward_demodulation,[],[f28940,f27808]) ).
fof(f28944,plain,
! [X0] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m2_relset_1(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),u1_struct_0(sK26),X0,k2_group_1(sK25)) ),
inference(forward_demodulation,[],[f28942,f27808]) ).
fof(f28946,plain,
! [X0] :
( ~ v1_group_6(X0,sK25,sK26)
| ~ v1_funct_2(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m2_relset_1(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(X0)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),X0,k2_group_1(sK25)) ),
inference(forward_demodulation,[],[f28944,f27808]) ).
fof(f28956,plain,
( ~ v1_funct_2(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(sK27)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,k2_group_1(sK25)) ),
inference(resolution,[],[f28946,f19631]) ).
fof(f28957,plain,
( ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ v1_funct_1(sK27)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28956,f27813]) ).
fof(f28958,plain,
( ~ v1_funct_1(sK27)
| k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,k2_group_1(sK25)) ),
inference(forward_subsumption_resolution,[],[f28957,f27812]) ).
fof(f28959,plain,
k2_group_1(sK26) = k8_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,k2_group_1(sK25)),
inference(forward_subsumption_resolution,[],[f28958,f19633]) ).
fof(f28961,plain,
k2_group_1(sK26) = k1_funct_1(sK27,k2_group_1(sK25)),
inference(superposition,[],[f28845,f28959]) ).
fof(f29752,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK25),u1_struct_0(X2))
| ~ v1_group_6(X1,sK25,X2)
| ~ m2_relset_1(X1,u1_struct_0(sK25),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| m1_group_2(sK20(sK25,X2,X1,X0),X2) ),
inference(resolution,[],[f19579,f19622]) ).
fof(f29753,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK25),u1_struct_0(X2))
| ~ v1_group_6(X1,sK25,X2)
| ~ m2_relset_1(X1,u1_struct_0(sK25),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| m1_group_2(sK20(sK25,X2,X1,X0),X2) ),
inference(forward_subsumption_resolution,[],[f29752,f19625]) ).
fof(f29755,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK25),u1_struct_0(X2))
| ~ v1_group_6(X1,sK25,X2)
| ~ m2_relset_1(X1,u1_struct_0(sK25),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| ~ v4_group_1(sK25)
| m1_group_2(sK20(sK25,X2,X1,X0),X2) ),
inference(forward_subsumption_resolution,[],[f29753,f19624]) ).
fof(f29757,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK25),u1_struct_0(X2))
| ~ v1_group_6(X1,sK25,X2)
| ~ m2_relset_1(X1,u1_struct_0(sK25),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| m1_group_2(sK20(sK25,X2,X1,X0),X2) ),
inference(forward_subsumption_resolution,[],[f29755,f19623]) ).
fof(f29759,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK25),u1_struct_0(X2))
| ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(X1)
| ~ v1_group_6(X1,sK25,X2)
| ~ m2_relset_1(X1,u1_struct_0(sK25),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ l1_group_1(X2)
| m1_group_2(sK20(sK25,X2,X1,X0),X2) ),
inference(forward_demodulation,[],[f29757,f27809]) ).
fof(f29761,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X2)
| ~ v1_funct_2(X1,k2_pre_topc(sK25),u1_struct_0(X2))
| ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(X1)
| ~ v1_group_6(X1,sK25,X2)
| v3_struct_0(X2)
| ~ v3_group_1(X2)
| ~ v4_group_1(X2)
| ~ m2_relset_1(X1,k2_pre_topc(sK25),u1_struct_0(X2))
| m1_group_2(sK20(sK25,X2,X1,X0),X2) ),
inference(forward_demodulation,[],[f29759,f27809]) ).
fof(f29763,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ m1_group_2(X1,sK25)
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| m1_group_2(sK20(sK25,sK26,X0,X1),sK26) ),
inference(resolution,[],[f29761,f19626]) ).
fof(f29766,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ m1_group_2(X1,sK25)
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| m1_group_2(sK20(sK25,sK26,X0,X1),sK26) ),
inference(forward_subsumption_resolution,[],[f29763,f19629]) ).
fof(f29768,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ m1_group_2(X1,sK25)
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| ~ v4_group_1(sK26)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| m1_group_2(sK20(sK25,sK26,X0,X1),sK26) ),
inference(forward_subsumption_resolution,[],[f29766,f19628]) ).
fof(f29770,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| ~ m1_group_2(X1,sK25)
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| m1_group_2(sK20(sK25,sK26,X0,X1),sK26) ),
inference(forward_subsumption_resolution,[],[f29768,f19627]) ).
fof(f29772,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m1_group_2(X1,sK25)
| ~ v1_funct_1(X0)
| ~ v1_group_6(X0,sK25,sK26)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),u1_struct_0(sK26))
| m1_group_2(sK20(sK25,sK26,X0,X1),sK26) ),
inference(forward_demodulation,[],[f29770,f27808]) ).
fof(f29774,plain,
! [X0,X1] :
( ~ v1_group_6(X0,sK25,sK26)
| ~ v1_funct_2(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m1_group_2(X1,sK25)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK25),k2_pre_topc(sK26))
| m1_group_2(sK20(sK25,sK26,X0,X1),sK26) ),
inference(forward_demodulation,[],[f29772,f27808]) ).
fof(f29782,plain,
! [X0] :
( ~ v1_funct_2(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(sK27)
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| m1_group_2(sK20(sK25,sK26,sK27,X0),sK26) ),
inference(resolution,[],[f29774,f19631]) ).
fof(f29783,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(sK27)
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| m1_group_2(sK20(sK25,sK26,sK27,X0),sK26) ),
inference(forward_subsumption_resolution,[],[f29782,f27813]) ).
fof(f29784,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26))
| m1_group_2(sK20(sK25,sK26,sK27,X0),sK26) ),
inference(forward_subsumption_resolution,[],[f29783,f19633]) ).
fof(f29785,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| m1_group_2(sK20(sK25,sK26,sK27,X0),sK26) ),
inference(forward_subsumption_resolution,[],[f29784,f27812]) ).
fof(f29786,plain,
m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26),
inference(resolution,[],[f29785,f28014]) ).
fof(f29790,plain,
m1_group_2(sK20(sK25,sK26,sK27,sK25),sK26),
inference(resolution,[],[f29785,f27970]) ).
fof(f29796,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| k5_group_2(X0) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(resolution,[],[f29790,f20074]) ).
fof(f29797,plain,
( k5_group_2(sK26) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(resolution,[],[f29790,f20075]) ).
fof(f29798,plain,
( k5_group_2(sK26) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29797,f19629]) ).
fof(f29799,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| k5_group_2(X0) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29796,f19629]) ).
fof(f29802,plain,
( k5_group_2(sK26) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29798,f19628]) ).
fof(f29803,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| k5_group_2(X0) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29799,f19628]) ).
fof(f29806,plain,
( k5_group_2(sK26) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29802,f19627]) ).
fof(f29807,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| k5_group_2(X0) = k5_group_2(sK20(sK25,sK26,sK27,sK25))
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29803,f19627]) ).
fof(f29810,plain,
k5_group_2(sK26) = k5_group_2(sK20(sK25,sK26,sK27,sK25)),
inference(forward_subsumption_resolution,[],[f29806,f19626]) ).
fof(f29811,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| k5_group_2(X0) = k5_group_2(sK20(sK25,sK26,sK27,sK25)) ),
inference(forward_subsumption_resolution,[],[f29807,f19626]) ).
fof(f29814,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| k5_group_2(X0) = k5_group_2(sK26) ),
inference(forward_demodulation,[],[f29811,f29810]) ).
fof(f29883,plain,
k5_group_2(sK26) = k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))),
inference(resolution,[],[f29786,f29814]) ).
fof(f29885,plain,
m1_group_2(k5_group_2(sK26),sK20(sK25,sK26,sK27,k5_group_2(sK25))),
inference(resolution,[],[f29786,f27997]) ).
fof(f29886,plain,
( u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k7_group_2(sK26,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(resolution,[],[f29786,f20937]) ).
fof(f29893,plain,
( u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k7_group_2(sK26,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29886,f19629]) ).
fof(f29896,plain,
( u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k7_group_2(sK26,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29893,f19628]) ).
fof(f29899,plain,
( u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k7_group_2(sK26,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f29896,f19627]) ).
fof(f29902,plain,
u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k7_group_2(sK26,sK20(sK25,sK26,sK27,k5_group_2(sK25))),
inference(forward_subsumption_resolution,[],[f29899,f19626]) ).
fof(f29915,plain,
( r1_rlvect_1(k5_group_2(sK26),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ l1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
inference(superposition,[],[f26548,f29883]) ).
fof(f29919,definition,
( spl797_162
<=> v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_162])],[avatar_definition]) ).
fof(f29920,plain,
( v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_162 ),
inference(avatar_component_clause,[],[f29919]) ).
fof(f29922,definition,
( spl797_163
<=> l1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_163])],[avatar_definition]) ).
fof(f29923,plain,
( ~ l1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| spl797_163 ),
inference(avatar_component_clause,[],[f29922]) ).
fof(f29925,definition,
( spl797_164
<=> v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_164])],[avatar_definition]) ).
fof(f29926,plain,
( ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| spl797_164 ),
inference(avatar_component_clause,[],[f29925]) ).
fof(f29928,definition,
( spl797_165
<=> v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_165])],[avatar_definition]) ).
fof(f29929,plain,
( ~ v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| spl797_165 ),
inference(avatar_component_clause,[],[f29928]) ).
fof(f29933,definition,
( spl797_166
<=> r1_rlvect_1(k5_group_2(sK26),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) ),
introduced(definition,[new_symbols(definition,[spl797_166])],[avatar_definition]) ).
fof(f29934,plain,
( r1_rlvect_1(k5_group_2(sK26),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ spl797_166 ),
inference(avatar_component_clause,[],[f29933]) ).
fof(f29935,plain,
( ~ spl797_163
| ~ spl797_164
| ~ spl797_165
| spl797_162
| spl797_166 ),
inference(avatar_split_clause,[],[f29915,f29933,f29919,f29928,f29925,f29922]) ).
fof(f30022,plain,
( $false
| spl797_163 ),
inference(unit_resulting_resolution,[],[f19679,f19629,f19628,f29923,f29786,f19626]) ).
fof(f30026,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| l1_group_1(X0) ),
inference(resolution,[],[f19679,f19626]) ).
fof(f30027,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| l1_group_1(X0) ),
inference(resolution,[],[f19679,f19622]) ).
fof(f30030,plain,
spl797_163,
inference(avatar_contradiction_clause,[],[f30022]) ).
fof(f30034,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v3_group_1(sK25)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f30027,f19625]) ).
fof(f30035,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| ~ v3_group_1(sK26)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f30026,f19629]) ).
fof(f30036,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f30034,f19624]) ).
fof(f30037,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f30035,f19628]) ).
fof(f30142,plain,
l1_group_1(k5_group_2(sK25)),
inference(resolution,[],[f30036,f28014]) ).
fof(f30174,plain,
u1_struct_0(k5_group_2(sK25)) = k2_pre_topc(k5_group_2(sK25)),
inference(resolution,[],[f30142,f27807]) ).
fof(f30523,plain,
( k1_funct_1(k3_latsubgr(sK25,sK26,sK27),k5_group_2(sK25)) = k5_group_4(sK26,k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,k2_pre_topc(k5_group_2(sK25))))
| ~ spl797_26
| ~ spl797_43 ),
inference(superposition,[],[f28873,f30174]) ).
fof(f30614,plain,
l1_group_1(k5_group_2(sK26)),
inference(resolution,[],[f30037,f27999]) ).
fof(f30617,plain,
l1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))),
inference(resolution,[],[f30037,f29786]) ).
fof(f30649,plain,
u1_struct_0(k5_group_2(sK26)) = k2_pre_topc(k5_group_2(sK26)),
inference(resolution,[],[f30614,f27807]) ).
fof(f31158,plain,
( $false
| spl797_165 ),
inference(unit_resulting_resolution,[],[f19680,f19629,f19628,f29929,f29786,f19626]) ).
fof(f31160,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| v3_group_1(X0) ),
inference(resolution,[],[f19680,f19626]) ).
fof(f31165,plain,
spl797_165,
inference(avatar_contradiction_clause,[],[f31158]) ).
fof(f31170,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| ~ v3_group_1(sK26)
| v3_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f31160,f19629]) ).
fof(f31174,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v3_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f31170,f19628]) ).
fof(f31183,plain,
v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))),
inference(resolution,[],[f31174,f29786]) ).
fof(f32446,plain,
! [X0] :
( ~ r1_rlvect_1(k5_group_2(sK26),X0)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| k2_group_1(sK26) = X0
| ~ l1_group_1(sK26) ),
inference(resolution,[],[f20067,f19627]) ).
fof(f32455,plain,
! [X0] :
( ~ r1_rlvect_1(k5_group_2(sK26),X0)
| ~ v3_group_1(sK26)
| k2_group_1(sK26) = X0
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f32446,f19629]) ).
fof(f32460,plain,
! [X0] :
( ~ r1_rlvect_1(k5_group_2(sK26),X0)
| k2_group_1(sK26) = X0
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f32455,f19628]) ).
fof(f32464,plain,
! [X0] :
( ~ r1_rlvect_1(k5_group_2(sK26),X0)
| k2_group_1(sK26) = X0 ),
inference(forward_subsumption_resolution,[],[f32460,f19626]) ).
fof(f32798,plain,
! [X0] :
( v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| m1_subset_1(k7_group_2(sK26,X0),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l1_group_1(sK26)
| ~ m1_group_2(X0,sK26) ),
inference(resolution,[],[f20923,f19627]) ).
fof(f32807,plain,
! [X0] :
( ~ v3_group_1(sK26)
| m1_subset_1(k7_group_2(sK26,X0),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l1_group_1(sK26)
| ~ m1_group_2(X0,sK26) ),
inference(forward_subsumption_resolution,[],[f32798,f19629]) ).
fof(f32812,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK26,X0),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ l1_group_1(sK26)
| ~ m1_group_2(X0,sK26) ),
inference(forward_subsumption_resolution,[],[f32807,f19628]) ).
fof(f32816,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK26,X0),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ m1_group_2(X0,sK26) ),
inference(forward_subsumption_resolution,[],[f32812,f19626]) ).
fof(f32820,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK26,X0),k1_zfmisc_1(k2_pre_topc(sK26)))
| ~ m1_group_2(X0,sK26) ),
inference(forward_demodulation,[],[f32816,f27808]) ).
fof(f32845,plain,
( m1_subset_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k1_zfmisc_1(k2_pre_topc(sK26)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26) ),
inference(superposition,[],[f32820,f29902]) ).
fof(f32846,plain,
m1_subset_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k1_zfmisc_1(k2_pre_topc(sK26))),
inference(forward_subsumption_resolution,[],[f32845,f29786]) ).
fof(f32854,plain,
v1_group_1(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))),
inference(resolution,[],[f32846,f28420]) ).
fof(f32885,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK26)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK26)))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(X0)),X0)
| ~ l1_group_1(sK26) ),
inference(resolution,[],[f26492,f19627]) ).
fof(f32894,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK26)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK26)))
| ~ v3_group_1(sK26)
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(X0)),X0)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f32885,f19629]) ).
fof(f32899,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK26)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK26)))
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(X0)),X0)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f32894,f19628]) ).
fof(f32903,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK26)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK26)))
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(X0)),X0) ),
inference(forward_subsumption_resolution,[],[f32899,f19626]) ).
fof(f32907,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| ~ v1_group_1(X0)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK26)))
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(X0)),X0) ),
inference(forward_demodulation,[],[f32903,f27808]) ).
fof(f32911,plain,
( ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_subset_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k1_zfmisc_1(k2_pre_topc(sK26)))
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
inference(resolution,[],[f32907,f29786]) ).
fof(f32935,plain,
( ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
inference(forward_subsumption_resolution,[],[f32911,f32846]) ).
fof(f32940,definition,
( spl797_346
<=> r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_346])],[avatar_definition]) ).
fof(f32941,plain,
( r1_group_2(sK26,k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_346 ),
inference(avatar_component_clause,[],[f32940]) ).
fof(f32943,definition,
( spl797_347
<=> v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_347])],[avatar_definition]) ).
fof(f32944,plain,
( ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| spl797_347 ),
inference(avatar_component_clause,[],[f32943]) ).
fof(f32945,plain,
( spl797_346
| ~ spl797_347 ),
inference(avatar_split_clause,[],[f32935,f32943,f32940]) ).
fof(f32996,plain,
( ~ m1_group_2(k5_group_2(sK25),sK25)
| ~ v1_funct_1(sK27)
| ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| ~ v1_group_6(sK27,sK25,sK26)
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(resolution,[],[f32944,f19580]) ).
fof(f32998,plain,
( ~ v1_funct_1(sK27)
| ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| ~ v1_group_6(sK27,sK25,sK26)
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f32996,f20070]) ).
fof(f32999,plain,
( ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| ~ v1_group_6(sK27,sK25,sK26)
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f32998,f19633]) ).
fof(f33000,plain,
( ~ v1_group_6(sK27,sK25,sK26)
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f32999,f19632]) ).
fof(f33001,plain,
( ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33000,f19631]) ).
fof(f33002,plain,
( v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33001,f19630]) ).
fof(f33003,plain,
( ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33002,f19629]) ).
fof(f33004,plain,
( ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33003,f19628]) ).
fof(f33005,plain,
( ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33004,f19627]) ).
fof(f33006,plain,
( v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33005,f19626]) ).
fof(f33007,plain,
( ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33006,f19625]) ).
fof(f33008,plain,
( ~ v4_group_1(sK25)
| ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33007,f19624]) ).
fof(f33009,plain,
( ~ l1_group_1(sK25)
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33008,f19623]) ).
fof(f33010,plain,
( $false
| spl797_347 ),
inference(forward_subsumption_resolution,[],[f33009,f19622]) ).
fof(f33011,plain,
spl797_347,
inference(avatar_contradiction_clause,[],[f33010]) ).
fof(f33117,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| ~ v1_group_1(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26)
| ~ spl797_346 ),
inference(resolution,[],[f32941,f19809]) ).
fof(f33118,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| ~ v1_group_1(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26)
| ~ spl797_346 ),
inference(forward_subsumption_resolution,[],[f33117,f19629]) ).
fof(f33119,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| ~ v1_group_1(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26)
| ~ spl797_346 ),
inference(forward_subsumption_resolution,[],[f33118,f19628]) ).
fof(f33120,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ l1_group_1(sK26)
| ~ v1_group_1(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26)
| ~ spl797_346 ),
inference(forward_subsumption_resolution,[],[f33119,f19627]) ).
fof(f33121,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ v1_group_1(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26)
| ~ spl797_346 ),
inference(forward_subsumption_resolution,[],[f33120,f19626]) ).
fof(f33122,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK26)
| ~ spl797_346 ),
inference(forward_subsumption_resolution,[],[f33121,f32854]) ).
fof(f33123,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_346 ),
inference(forward_subsumption_resolution,[],[f33122,f29786]) ).
fof(f33125,definition,
( spl797_362
<=> m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26) ),
introduced(definition,[new_symbols(definition,[spl797_362])],[avatar_definition]) ).
fof(f33126,plain,
( ~ m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26)
| spl797_362 ),
inference(avatar_component_clause,[],[f33125]) ).
fof(f33128,definition,
( spl797_363
<=> sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) ),
introduced(definition,[new_symbols(definition,[spl797_363])],[avatar_definition]) ).
fof(f33129,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ spl797_363 ),
inference(avatar_component_clause,[],[f33128]) ).
fof(f33130,plain,
( ~ spl797_347
| ~ spl797_362
| spl797_363
| ~ spl797_346 ),
inference(avatar_split_clause,[],[f33123,f32940,f33128,f33125,f32943]) ).
fof(f33426,plain,
( v1_xboole_0(k2_pre_topc(sK25))
| k6_domain_1(k2_pre_topc(sK25),k2_group_1(sK25)) = k2_tarski(k2_group_1(sK25),k2_group_1(sK25)) ),
inference(resolution,[],[f25670,f28086]) ).
fof(f33427,plain,
( v1_xboole_0(k2_pre_topc(sK26))
| k6_domain_1(k2_pre_topc(sK26),k2_group_1(sK26)) = k2_tarski(k2_group_1(sK26),k2_group_1(sK26)) ),
inference(resolution,[],[f25670,f28087]) ).
fof(f33445,plain,
k6_domain_1(k2_pre_topc(sK26),k2_group_1(sK26)) = k2_tarski(k2_group_1(sK26),k2_group_1(sK26)),
inference(forward_subsumption_resolution,[],[f33427,f27955]) ).
fof(f33446,plain,
k6_domain_1(k2_pre_topc(sK25),k2_group_1(sK25)) = k2_tarski(k2_group_1(sK25),k2_group_1(sK25)),
inference(forward_subsumption_resolution,[],[f33426,f27954]) ).
fof(f33456,plain,
( u1_struct_0(k5_group_2(sK26)) = k2_tarski(k2_group_1(sK26),k2_group_1(sK26))
| ~ spl797_49 ),
inference(forward_demodulation,[],[f33445,f28110]) ).
fof(f33457,plain,
( u1_struct_0(k5_group_2(sK25)) = k2_tarski(k2_group_1(sK25),k2_group_1(sK25))
| ~ spl797_48 ),
inference(forward_demodulation,[],[f33446,f28105]) ).
fof(f33458,plain,
( k2_pre_topc(k5_group_2(sK26)) = k2_tarski(k2_group_1(sK26),k2_group_1(sK26))
| ~ spl797_49 ),
inference(forward_demodulation,[],[f33456,f30649]) ).
fof(f33459,plain,
( k2_pre_topc(k5_group_2(sK25)) = k2_tarski(k2_group_1(sK25),k2_group_1(sK25))
| ~ spl797_48 ),
inference(forward_demodulation,[],[f33457,f30174]) ).
fof(f33727,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(sK27,X0,X1)
| k9_relat_1(sK27,X2) = k2_funct_2(X0,X1,sK27,X2)
| ~ m2_relset_1(sK27,X0,X1) ),
inference(resolution,[],[f28223,f19633]) ).
fof(f33748,plain,
! [X0] :
( k9_relat_1(sK27,X0) = k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,X0)
| ~ m2_relset_1(sK27,k2_pre_topc(sK25),k2_pre_topc(sK26)) ),
inference(resolution,[],[f33727,f27813]) ).
fof(f33749,plain,
! [X0] : k9_relat_1(sK27,X0) = k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,X0),
inference(forward_subsumption_resolution,[],[f33748,f27812]) ).
fof(f33754,plain,
( k1_funct_1(k3_latsubgr(sK25,sK26,sK27),k5_group_2(sK25)) = k5_group_4(sK26,k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))))
| ~ spl797_26
| ~ spl797_43 ),
inference(superposition,[],[f30523,f33749]) ).
fof(f33756,plain,
( k5_group_2(sK26) != k5_group_4(sK26,k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))))
| ~ spl797_26
| ~ spl797_43 ),
inference(superposition,[],[f19634,f33754]) ).
fof(f35055,plain,
( $false
| spl797_164 ),
inference(unit_resulting_resolution,[],[f19686,f19626,f19629,f19628,f29926,f29786,f19627]) ).
fof(f35060,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| v4_group_1(X0)
| ~ l1_group_1(sK26) ),
inference(resolution,[],[f19686,f19627]) ).
fof(f35065,plain,
spl797_164,
inference(avatar_contradiction_clause,[],[f35055]) ).
fof(f35074,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| ~ v3_group_1(sK26)
| v4_group_1(X0)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f35060,f19629]) ).
fof(f35079,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v4_group_1(X0)
| ~ l1_group_1(sK26) ),
inference(forward_subsumption_resolution,[],[f35074,f19628]) ).
fof(f35083,plain,
! [X0] :
( ~ m1_group_2(X0,sK26)
| v4_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f35079,f19626]) ).
fof(f36157,plain,
( $false
| ~ spl797_162 ),
inference(unit_resulting_resolution,[],[f19681,f19626,f19628,f19629,f29786,f29920]) ).
fof(f36159,plain,
~ spl797_162,
inference(avatar_contradiction_clause,[],[f36157]) ).
fof(f36222,plain,
v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))),
inference(resolution,[],[f35083,f29786]) ).
fof(f36789,plain,
! [X0] :
( v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| m1_group_2(k5_group_4(sK26,X0),sK26)
| ~ l1_group_1(sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(resolution,[],[f19833,f19627]) ).
fof(f36790,plain,
! [X0] :
( ~ v3_group_1(sK26)
| m1_group_2(k5_group_4(sK26,X0),sK26)
| ~ l1_group_1(sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f36789,f19629]) ).
fof(f36796,plain,
! [X0] :
( m1_group_2(k5_group_4(sK26,X0),sK26)
| ~ l1_group_1(sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f36790,f19628]) ).
fof(f36802,plain,
! [X0] :
( m1_group_2(k5_group_4(sK26,X0),sK26)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK26))) ),
inference(forward_subsumption_resolution,[],[f36796,f19626]) ).
fof(f36807,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK26)))
| m1_group_2(k5_group_4(sK26,X0),sK26) ),
inference(forward_demodulation,[],[f36802,f27808]) ).
fof(f36868,plain,
m1_group_2(k5_group_4(sK26,u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))),sK26),
inference(resolution,[],[f36807,f32846]) ).
fof(f36877,plain,
( $false
| spl797_362 ),
inference(forward_subsumption_resolution,[],[f36868,f33126]) ).
fof(f36878,plain,
spl797_362,
inference(avatar_contradiction_clause,[],[f36877]) ).
fof(f38245,plain,
( k2_group_1(sK26) = k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_166 ),
inference(resolution,[],[f29934,f32464]) ).
fof(f38836,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_1(sK27)
| ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(resolution,[],[f19578,f19631]) ).
fof(f38845,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| ~ v1_funct_2(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38836,f19633]) ).
fof(f38849,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ m2_relset_1(sK27,u1_struct_0(sK25),u1_struct_0(sK26))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38845,f19632]) ).
fof(f38853,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| v3_struct_0(sK26)
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38849,f19630]) ).
fof(f38857,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ v3_group_1(sK26)
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38853,f19629]) ).
fof(f38861,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ v4_group_1(sK26)
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38857,f19628]) ).
fof(f38865,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ l1_group_1(sK26)
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38861,f19627]) ).
fof(f38869,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| v3_struct_0(sK25)
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38865,f19626]) ).
fof(f38873,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ v3_group_1(sK25)
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38869,f19625]) ).
fof(f38877,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ v4_group_1(sK25)
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38873,f19624]) ).
fof(f38881,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ l1_group_1(sK25) ),
inference(forward_subsumption_resolution,[],[f38877,f19623]) ).
fof(f38883,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| k2_funct_2(u1_struct_0(sK25),u1_struct_0(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0)) ),
inference(forward_subsumption_resolution,[],[f38881,f19622]) ).
fof(f38885,plain,
! [X0] :
( k2_funct_2(u1_struct_0(sK25),k2_pre_topc(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ m1_group_2(X0,sK25) ),
inference(forward_demodulation,[],[f38883,f27808]) ).
fof(f38887,plain,
! [X0] :
( k2_funct_2(k2_pre_topc(sK25),k2_pre_topc(sK26),sK27,u1_struct_0(X0)) = u1_struct_0(sK20(sK25,sK26,sK27,X0))
| ~ m1_group_2(X0,sK25) ),
inference(forward_demodulation,[],[f38885,f27809]) ).
fof(f38889,plain,
! [X0] :
( ~ m1_group_2(X0,sK25)
| u1_struct_0(sK20(sK25,sK26,sK27,X0)) = k9_relat_1(sK27,u1_struct_0(X0)) ),
inference(forward_demodulation,[],[f38887,f33749]) ).
fof(f38893,plain,
u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k9_relat_1(sK27,u1_struct_0(k5_group_2(sK25))),
inference(resolution,[],[f38889,f28014]) ).
fof(f38910,plain,
u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),
inference(forward_demodulation,[],[f38893,f30174]) ).
fof(f39058,plain,
( sK20(sK25,sK26,sK27,k5_group_2(sK25)) = k5_group_4(sK26,k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))))
| ~ spl797_363 ),
inference(superposition,[],[f33129,f38910]) ).
fof(f39390,plain,
( k5_group_2(sK26) != sK20(sK25,sK26,sK27,k5_group_2(sK25))
| ~ spl797_26
| ~ spl797_43
| ~ spl797_363 ),
inference(superposition,[],[f33756,f39058]) ).
fof(f39976,plain,
( v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
inference(resolution,[],[f30617,f19684]) ).
fof(f39990,plain,
! [X0] :
( u1_struct_0(X0) != k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = X0 ),
inference(resolution,[],[f30617,f20077]) ).
fof(f40004,plain,
( ~ v1_group_1(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ m1_group_2(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v3_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) ),
inference(resolution,[],[f30617,f26549]) ).
fof(f40101,plain,
( ~ v1_group_1(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ m1_group_2(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) ),
inference(forward_subsumption_resolution,[],[f40004,f31183]) ).
fof(f40115,plain,
! [X0] :
( u1_struct_0(X0) != k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = X0 ),
inference(forward_subsumption_resolution,[],[f39990,f31183]) ).
fof(f40129,plain,
( v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v4_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
inference(forward_subsumption_resolution,[],[f39976,f31183]) ).
fof(f40189,plain,
( ~ v1_group_1(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ m1_group_2(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) ),
inference(forward_subsumption_resolution,[],[f40101,f36222]) ).
fof(f40206,plain,
! [X0] :
( u1_struct_0(X0) != k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = X0 ),
inference(forward_subsumption_resolution,[],[f40115,f36222]) ).
fof(f40223,plain,
( v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
inference(forward_subsumption_resolution,[],[f40129,f36222]) ).
fof(f40291,plain,
( ~ v1_group_1(k5_group_2(sK26))
| ~ m1_group_2(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) ),
inference(forward_demodulation,[],[f40189,f29883]) ).
fof(f40316,plain,
( ! [X0] :
( u1_struct_0(X0) != k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK26))
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = X0 )
| ~ spl797_166 ),
inference(forward_demodulation,[],[f40206,f38245]) ).
fof(f40339,definition,
( spl797_957
<=> m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK20(sK25,sK26,sK27,k5_group_2(sK25))) ),
introduced(definition,[new_symbols(definition,[spl797_957])],[avatar_definition]) ).
fof(f40340,plain,
( m1_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25)),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_957 ),
inference(avatar_component_clause,[],[f40339]) ).
fof(f40341,plain,
( spl797_957
| spl797_162 ),
inference(avatar_split_clause,[],[f40223,f29919,f40339]) ).
fof(f40396,plain,
( ~ m1_group_2(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ spl797_38 ),
inference(forward_subsumption_resolution,[],[f40291,f27926]) ).
fof(f40407,plain,
( ! [X0] :
( u1_struct_0(X0) != k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))) = X0 )
| ~ spl797_166 ),
inference(forward_demodulation,[],[f40316,f38910]) ).
fof(f40554,plain,
( ~ m1_group_2(k5_group_2(sK26),sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ spl797_38 ),
inference(forward_demodulation,[],[f40396,f29883]) ).
fof(f40570,plain,
( ! [X0] :
( k5_group_2(sK26) = X0
| u1_struct_0(X0) != k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) )
| ~ spl797_166 ),
inference(forward_demodulation,[],[f40407,f29883]) ).
fof(f40609,plain,
( v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))) = u1_struct_0(k5_group_2(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| ~ spl797_38 ),
inference(forward_subsumption_resolution,[],[f40554,f29885]) ).
fof(f40623,definition,
( spl797_1009
<=> ! [X0] :
( k5_group_2(sK26) = X0
| ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ v1_group_1(X0)
| u1_struct_0(X0) != k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26)) ) ),
introduced(definition,[new_symbols(definition,[spl797_1009])],[avatar_definition]) ).
fof(f40624,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| k5_group_2(sK26) = X0
| ~ v1_group_1(X0)
| u1_struct_0(X0) != k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26)) )
| ~ spl797_1009 ),
inference(avatar_component_clause,[],[f40623]) ).
fof(f40625,plain,
( spl797_162
| spl797_1009
| ~ spl797_166 ),
inference(avatar_split_clause,[],[f40570,f29933,f40623,f29919]) ).
fof(f40647,plain,
( u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25))))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_38 ),
inference(forward_demodulation,[],[f40609,f29883]) ).
fof(f40652,plain,
( u1_struct_0(k5_group_2(sK26)) = k6_domain_1(u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))),k2_group_1(sK26))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_38
| ~ spl797_166 ),
inference(forward_demodulation,[],[f40647,f38245]) ).
fof(f40653,plain,
( u1_struct_0(k5_group_2(sK26)) = k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_38
| ~ spl797_166 ),
inference(forward_demodulation,[],[f40652,f38910]) ).
fof(f40654,plain,
( k2_pre_topc(k5_group_2(sK26)) = k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| v3_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_38
| ~ spl797_166 ),
inference(forward_demodulation,[],[f40653,f30649]) ).
fof(f40656,definition,
( spl797_1016
<=> k2_pre_topc(k5_group_2(sK26)) = k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26)) ),
introduced(definition,[new_symbols(definition,[spl797_1016])],[avatar_definition]) ).
fof(f40657,plain,
( k2_pre_topc(k5_group_2(sK26)) = k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| ~ spl797_1016 ),
inference(avatar_component_clause,[],[f40656]) ).
fof(f40658,plain,
( spl797_162
| spl797_1016
| ~ spl797_38
| ~ spl797_166 ),
inference(avatar_split_clause,[],[f40654,f29933,f27925,f40656,f29919]) ).
fof(f40718,plain,
( k5_group_2(sK26) = sK20(sK25,sK26,sK27,k5_group_2(sK25))
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) != k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| ~ spl797_957
| ~ spl797_1009 ),
inference(resolution,[],[f40340,f40624]) ).
fof(f40727,plain,
( ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) != k6_domain_1(k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))),k2_group_1(sK26))
| ~ spl797_26
| ~ spl797_43
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009 ),
inference(forward_subsumption_resolution,[],[f40718,f39390]) ).
fof(f40729,plain,
( u1_struct_0(sK20(sK25,sK26,sK27,k5_group_2(sK25))) != k2_pre_topc(k5_group_2(sK26))
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_26
| ~ spl797_43
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009
| ~ spl797_1016 ),
inference(forward_demodulation,[],[f40727,f40657]) ).
fof(f40731,plain,
( k2_pre_topc(k5_group_2(sK26)) != k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25)))
| ~ v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_26
| ~ spl797_43
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009
| ~ spl797_1016 ),
inference(forward_demodulation,[],[f40729,f38910]) ).
fof(f41686,plain,
( v1_group_1(sK20(sK25,sK26,sK27,k5_group_2(sK25)))
| ~ spl797_347 ),
inference(avatar_component_clause,[],[f32943]) ).
fof(f42058,plain,
! [X0] :
( ~ r2_hidden(X0,k1_relat_1(sK27))
| k2_tarski(k1_funct_1(sK27,X0),k1_funct_1(sK27,X0)) = k9_relat_1(sK27,k2_tarski(X0,X0))
| ~ v1_funct_1(sK27) ),
inference(resolution,[],[f25652,f28078]) ).
fof(f42063,plain,
! [X0] :
( ~ r2_hidden(X0,k1_relat_1(sK27))
| k2_tarski(k1_funct_1(sK27,X0),k1_funct_1(sK27,X0)) = k9_relat_1(sK27,k2_tarski(X0,X0)) ),
inference(forward_subsumption_resolution,[],[f42058,f19633]) ).
fof(f42065,plain,
! [X0] :
( ~ r2_hidden(X0,k2_pre_topc(sK25))
| k2_tarski(k1_funct_1(sK27,X0),k1_funct_1(sK27,X0)) = k9_relat_1(sK27,k2_tarski(X0,X0)) ),
inference(forward_demodulation,[],[f42063,f28160]) ).
fof(f42066,plain,
! [X0] :
( k2_tarski(k1_funct_1(sK27,X0),k1_funct_1(sK27,X0)) = k9_relat_1(sK27,k2_tarski(X0,X0))
| ~ m1_subset_1(X0,k2_pre_topc(sK25))
| v1_xboole_0(k2_pre_topc(sK25)) ),
inference(resolution,[],[f42065,f19660]) ).
fof(f42069,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK25))
| k2_tarski(k1_funct_1(sK27,X0),k1_funct_1(sK27,X0)) = k9_relat_1(sK27,k2_tarski(X0,X0)) ),
inference(forward_subsumption_resolution,[],[f42066,f27954]) ).
fof(f42070,plain,
k2_tarski(k1_funct_1(sK27,k2_group_1(sK25)),k1_funct_1(sK27,k2_group_1(sK25))) = k9_relat_1(sK27,k2_tarski(k2_group_1(sK25),k2_group_1(sK25))),
inference(resolution,[],[f42069,f28086]) ).
fof(f42075,plain,
( k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25))) = k2_tarski(k1_funct_1(sK27,k2_group_1(sK25)),k1_funct_1(sK27,k2_group_1(sK25)))
| ~ spl797_48 ),
inference(forward_demodulation,[],[f42070,f33459]) ).
fof(f42076,plain,
( k2_tarski(k2_group_1(sK26),k2_group_1(sK26)) = k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25)))
| ~ spl797_48 ),
inference(forward_demodulation,[],[f42075,f28961]) ).
fof(f42077,plain,
( k2_pre_topc(k5_group_2(sK26)) = k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25)))
| ~ spl797_48
| ~ spl797_49 ),
inference(forward_demodulation,[],[f42076,f33458]) ).
fof(f42084,plain,
( k2_pre_topc(k5_group_2(sK26)) != k9_relat_1(sK27,k2_pre_topc(k5_group_2(sK25)))
| ~ spl797_26
| ~ spl797_43
| ~ spl797_347
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009
| ~ spl797_1016 ),
inference(forward_subsumption_resolution,[],[f40731,f41686]) ).
fof(f42085,plain,
( $false
| ~ spl797_26
| ~ spl797_43
| ~ spl797_48
| ~ spl797_49
| ~ spl797_347
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009
| ~ spl797_1016 ),
inference(forward_subsumption_resolution,[],[f42084,f42077]) ).
fof(f42086,plain,
( ~ spl797_26
| ~ spl797_43
| ~ spl797_48
| ~ spl797_49
| ~ spl797_347
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009
| ~ spl797_1016 ),
inference(avatar_contradiction_clause,[],[f42085]) ).
cnf(s18,plain,
( spl797_26
| ~ spl797_27 ),
inference(sat_conversion,[],[f27858]) ).
cnf(s20,plain,
spl797_27,
inference(sat_conversion,[],[f27863]) ).
cnf(s27,plain,
( ~ spl797_43
| spl797_48 ),
inference(sat_conversion,[],[f28106]) ).
cnf(s28,plain,
( ~ spl797_38
| spl797_49 ),
inference(sat_conversion,[],[f28111]) ).
cnf(s30,plain,
spl797_38,
inference(sat_conversion,[],[f28119]) ).
cnf(s32,plain,
spl797_43,
inference(sat_conversion,[],[f28127]) ).
cnf(s109,plain,
( spl797_162
| ~ spl797_163
| ~ spl797_164
| ~ spl797_165
| spl797_166 ),
inference(sat_conversion,[],[f29935]) ).
cnf(s131,plain,
spl797_163,
inference(sat_conversion,[],[f30030]) ).
cnf(s178,plain,
spl797_165,
inference(sat_conversion,[],[f31165]) ).
cnf(s254,plain,
( spl797_346
| ~ spl797_347 ),
inference(sat_conversion,[],[f32945]) ).
cnf(s260,plain,
spl797_347,
inference(sat_conversion,[],[f33011]) ).
cnf(s269,plain,
( ~ spl797_346
| ~ spl797_347
| ~ spl797_362
| spl797_363 ),
inference(sat_conversion,[],[f33130]) ).
cnf(s341,plain,
spl797_164,
inference(sat_conversion,[],[f35065]) ).
cnf(s478,plain,
~ spl797_162,
inference(sat_conversion,[],[f36159]) ).
cnf(s543,plain,
spl797_362,
inference(sat_conversion,[],[f36878]) ).
cnf(s744,plain,
( spl797_162
| spl797_957 ),
inference(sat_conversion,[],[f40341]) ).
cnf(s796,plain,
( spl797_162
| ~ spl797_166
| spl797_1009 ),
inference(sat_conversion,[],[f40625]) ).
cnf(s803,plain,
( ~ spl797_38
| spl797_162
| ~ spl797_166
| spl797_1016 ),
inference(sat_conversion,[],[f40658]) ).
cnf(s890,plain,
( ~ spl797_26
| ~ spl797_43
| ~ spl797_48
| ~ spl797_49
| ~ spl797_347
| ~ spl797_363
| ~ spl797_957
| ~ spl797_1009
| ~ spl797_1016 ),
inference(sat_conversion,[],[f42086]) ).
cnf(s954,plain,
spl797_957,
inference(rat,[],[s744,s478]) ).
cnf(s1108,plain,
( ~ spl797_346
| ~ spl797_347
| spl797_363 ),
inference(rat,[],[s269,s543]) ).
cnf(s1125,plain,
spl797_346,
inference(rat,[],[s254,s260]) ).
cnf(s1126,plain,
spl797_363,
inference(rat,[],[s1108,s260,s1125]) ).
cnf(s1296,plain,
spl797_166,
inference(rat,[],[s109,s178,s341,s131,s478]) ).
cnf(s1300,plain,
spl797_1009,
inference(rat,[],[s796,s478,s1296]) ).
cnf(s1320,plain,
spl797_1016,
inference(rat,[],[s803,s1296,s478,s30]) ).
cnf(s1322,plain,
spl797_49,
inference(rat,[],[s28,s30]) ).
cnf(s1323,plain,
spl797_48,
inference(rat,[],[s27,s32]) ).
cnf(s1325,plain,
~ spl797_26,
inference(rat,[],[s890,s1320,s1300,s954,s1126,s260,s1322,s32,s1323]) ).
cnf(s1331,plain,
$false,
inference(rat,[],[s18,s20,s1325]) ).
fof(f42087,plain,
$false,
inference(avatar_sat_refutation,[],[s1331]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP652+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 % Computer : n015.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sun Sep 27 10:33:33 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.43 Running first-order theorem proving
% 0.10/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.23/3.59 % (1458008)Detected formulas, will run a generic FOF schedule.
% 14.23/3.59 % (1458308)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2445104219:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 14.23/3.59 % (1458304)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=2551268242:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 14.23/3.59 % (1458305)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=431612668:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 14.23/3.59 % (1458307)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=22271443:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 14.23/3.59 % (1458311)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2213257202:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 14.23/3.59 % (1458310)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1816608191:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 14.23/3.59 % (1458313)dis-21_1_sil=8000:lcm=predicate:random_seed=4283908975: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)
% 14.23/3.59 % (1458308)Instruction limit reached!
% 14.23/3.59 % (1458308)------------------------------
% 14.23/3.59 % (1458308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.23/3.59 % (1458308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.23/3.59 % (1458308)CaDiCaL version: 2.1.3
% 14.23/3.59 % (1458308)Termination reason: Instruction limit
% 14.23/3.59 % (1458308)Termination phase: Saturation
% 14.23/3.59 % (1458308)Time elapsed: 0.051 s
% 14.23/3.59 % (1458308)Peak memory usage: 107 MB
% 14.23/3.59 % (1458308)Instructions burned: 110 (million)
% 14.23/3.59 % (1458311)Instruction limit reached!
% 14.23/3.59 % (1458311)------------------------------
% 14.23/3.59 % (1458311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.23/3.59 % (1458311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.23/3.59 % (1458311)CaDiCaL version: 2.1.3
% 14.23/3.59 % (1458311)Termination reason: Instruction limit
% 14.23/3.59 % (1458311)Termination phase: Property scanning
% 14.23/3.59 % (1458311)Time elapsed: 0.058 s
% 14.23/3.59 % (1458311)Peak memory usage: 103 MB
% 14.23/3.59 % (1458311)Instructions burned: 139 (million)
% 14.23/3.59 % (1458313)Instruction limit reached!
% 14.23/3.59 % (1458313)------------------------------
% 14.23/3.59 % (1458313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.23/3.59 % (1458313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.23/3.59 % (1458313)CaDiCaL version: 2.1.3
% 14.23/3.59 % (1458313)Termination reason: Instruction limit
% 14.23/3.59 % (1458313)Termination phase: Preprocessing 1
% 14.23/3.59 % (1458313)Time elapsed: 0.095 s
% 14.23/3.59 % (1458313)Peak memory usage: 104 MB
% 14.23/3.59 % (1458313)Instructions burned: 130 (million)
% 14.23/3.59 % (1458310)Instruction limit reached!
% 14.23/3.59 % (1458310)------------------------------
% 14.23/3.59 % (1458310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.23/3.59 % (1458310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.23/3.59 % (1458310)CaDiCaL version: 2.1.3
% 14.23/3.59 % (1458310)Termination reason: Instruction limit
% 14.23/3.59 % (1458310)Termination phase: Naming
% 14.23/3.59 % (1458310)Time elapsed: 0.105 s
% 14.23/3.59 % (1458310)Peak memory usage: 106 MB
% 14.23/3.59 % (1458310)Instructions burned: 120 (million)
% 14.23/3.59 % (1458361)lrs+10_1_sil=8000:sp=occurrence:random_seed=1732244979:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 14.23/3.59 % (1458374)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2504248643:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 14.23/3.59 % (1458361)Instruction limit reached!
% 14.23/3.59 % (1458361)------------------------------
% 14.23/3.59 % (1458361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.23/3.59 % (1458361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.23/3.59 % (1458361)CaDiCaL version: 2.1.3
% 14.23/3.59 % (1458361)Termination reason: Instruction limit
% 22.38/4.80 % (1458361)Termination phase: Saturation
% 22.38/4.80 % (1458361)Time elapsed: 0.111 s
% 22.38/4.80 % (1458361)Peak memory usage: 111 MB
% 22.38/4.80 % (1458361)Instructions burned: 285 (million)
% 22.38/4.80 % (1458385)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4126351782:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 22.38/4.80 % (1458389)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=2727936995:s2a=on:i=248:s2at=1.23:gtg=position_2990 on theBenchmark for (2990ds/248Mi)
% 22.38/4.80 % (1458374)Instruction limit reached!
% 22.38/4.80 % (1458374)------------------------------
% 22.38/4.80 % (1458374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.80 % (1458374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.80 % (1458374)CaDiCaL version: 2.1.3
% 22.38/4.80 % (1458374)Termination reason: Instruction limit
% 22.38/4.80 % (1458374)Termination phase: Property scanning
% 22.38/4.80 % (1458374)Time elapsed: 0.067 s
% 22.38/4.80 % (1458374)Peak memory usage: 103 MB
% 22.38/4.80 % (1458374)Instructions burned: 159 (million)
% 22.38/4.80 % (1458426)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1959109060:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 22.38/4.80 % (1458389)Instruction limit reached!
% 22.38/4.80 % (1458389)------------------------------
% 22.38/4.80 % (1458389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.80 % (1458389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.80 % (1458389)CaDiCaL version: 2.1.3
% 22.38/4.80 % (1458389)Termination reason: Instruction limit
% 22.38/4.80 % (1458389)Termination phase: SInE selection
% 22.38/4.80 % (1458389)Time elapsed: 0.126 s
% 22.38/4.80 % (1458389)Peak memory usage: 103 MB
% 22.38/4.80 % (1458389)Instructions burned: 249 (million)
% 22.38/4.80 % (1458438)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1326265643:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 22.38/4.80 % (1458385)Instruction limit reached!
% 22.38/4.80 % (1458385)------------------------------
% 22.38/4.80 % (1458385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.80 % (1458385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.80 % (1458385)CaDiCaL version: 2.1.3
% 22.38/4.80 % (1458385)Termination reason: Instruction limit
% 22.38/4.80 % (1458385)Termination phase: Saturation
% 22.38/4.80 % (1458385)Time elapsed: 0.209 s
% 22.38/4.80 % (1458385)Peak memory usage: 111 MB
% 22.38/4.80 % (1458385)Instructions burned: 326 (million)
% 22.38/4.80 % (1458426)Instruction limit reached!
% 22.38/4.80 % (1458426)------------------------------
% 22.38/4.80 % (1458426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.80 % (1458426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.80 % (1458426)CaDiCaL version: 2.1.3
% 22.38/4.80 % (1458426)Termination reason: Instruction limit
% 22.38/4.80 % (1458426)Termination phase: Saturation
% 22.38/4.80 % (1458426)Time elapsed: 0.112 s
% 22.38/4.80 % (1458426)Peak memory usage: 111 MB
% 22.38/4.80 % (1458426)Instructions burned: 297 (million)
% 22.38/4.80 % (1458468)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4096246452:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 22.89/4.80 % (1458487)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4125150231:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 22.89/4.80 % (1458497)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1112381465:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 22.89/4.80 % (1458497)Instruction limit reached!
% 22.89/4.80 % (1458497)------------------------------
% 22.89/4.80 % (1458497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.89/4.80 % (1458497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.89/4.80 % (1458497)CaDiCaL version: 2.1.3
% 22.89/4.80 % (1458497)Termination reason: Instruction limit
% 22.89/4.80 % (1458497)Termination phase: Property scanning
% 22.89/4.80 % (1458497)Time elapsed: 0.026 s
% 22.89/4.80 % (1458497)Peak memory usage: 103 MB
% 22.89/4.80 % (1458497)Instructions burned: 115 (million)
% 22.89/4.80 % (1458468)Instruction limit reached!
% 22.89/4.80 % (1458468)------------------------------
% 22.89/4.80 % (1458468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458468)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458468)Termination reason: Instruction limit
% 19.74/7.39 % (1458468)Termination phase: Preprocessing 2
% 19.74/7.39 % (1458468)Time elapsed: 0.101 s
% 19.74/7.39 % (1458468)Peak memory usage: 106 MB
% 19.74/7.39 % (1458468)Instructions burned: 113 (million)
% 19.74/7.39 % (1458487)Instruction limit reached!
% 19.74/7.39 % (1458487)------------------------------
% 19.74/7.39 % (1458487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458487)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458487)Termination reason: Instruction limit
% 19.74/7.39 % (1458487)Termination phase: Preprocessing 2
% 19.74/7.39 % (1458487)Time elapsed: 0.103 s
% 19.74/7.39 % (1458487)Peak memory usage: 106 MB
% 19.74/7.39 % (1458487)Instructions burned: 128 (million)
% 19.74/7.39 % (1458537)lrs+10_1_sil=8000:sp=occurrence:random_seed=2198459725:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 19.74/7.39 % (1458543)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2994014008:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 19.74/7.39 % (1458557)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=194413739:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 19.74/7.39 % (1458537)Instruction limit reached!
% 19.74/7.39 % (1458537)------------------------------
% 19.74/7.39 % (1458537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458537)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458537)Termination reason: Instruction limit
% 19.74/7.39 % (1458537)Termination phase: Saturation
% 19.74/7.39 % (1458537)Time elapsed: 0.293 s
% 19.74/7.39 % (1458537)Peak memory usage: 122 MB
% 19.74/7.39 % (1458537)Instructions burned: 908 (million)
% 19.74/7.39 % (1458543)Instruction limit reached!
% 19.74/7.39 % (1458543)------------------------------
% 19.74/7.39 % (1458543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458543)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458543)Termination reason: Instruction limit
% 19.74/7.39 % (1458543)Termination phase: Saturation
% 19.74/7.39 % (1458543)Time elapsed: 0.264 s
% 19.74/7.39 % (1458543)Peak memory usage: 110 MB
% 19.74/7.39 % (1458543)Instructions burned: 438 (million)
% 19.74/7.39 % (1458649)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1903142761:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 19.74/7.39 % (1458659)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1281193549:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 19.74/7.39 % (1458649)Instruction limit reached!
% 19.74/7.39 % (1458649)------------------------------
% 19.74/7.39 % (1458649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458649)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458649)Termination reason: Instruction limit
% 19.74/7.39 % (1458649)Termination phase: Property scanning
% 19.74/7.39 % (1458649)Time elapsed: 0.066 s
% 19.74/7.39 % (1458649)Peak memory usage: 107 MB
% 19.74/7.39 % (1458649)Instructions burned: 137 (million)
% 19.74/7.39 % (1458705)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3720562183:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 19.74/7.39 % (1458659)Instruction limit reached!
% 19.74/7.39 % (1458659)------------------------------
% 19.74/7.39 % (1458659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458659)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458659)Termination reason: Instruction limit
% 19.74/7.39 % (1458659)Termination phase: Property scanning
% 19.74/7.39 % (1458659)Time elapsed: 0.414 s
% 19.74/7.39 % (1458659)Peak memory usage: 126 MB
% 19.74/7.39 % (1458659)Instructions burned: 594 (million)
% 19.74/7.39 % (1458805)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=4234610839:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/125Mi)
% 19.74/7.39 % (1458438)Instruction limit reached!
% 19.74/7.39 % (1458438)------------------------------
% 19.74/7.39 % (1458438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458438)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458438)Termination reason: Instruction limit
% 19.74/7.39 % (1458438)Termination phase: Saturation
% 19.74/7.39 % (1458438)Time elapsed: 1.418 s
% 19.74/7.39 % (1458438)Peak memory usage: 220 MB
% 19.74/7.39 % (1458438)Instructions burned: 2350 (million)
% 19.74/7.39 % (1458805)Instruction limit reached!
% 19.74/7.39 % (1458805)------------------------------
% 19.74/7.39 % (1458805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458805)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458805)Termination reason: Instruction limit
% 19.74/7.39 % (1458805)Termination phase: Property scanning
% 19.74/7.39 % (1458805)Time elapsed: 0.054 s
% 19.74/7.39 % (1458805)Peak memory usage: 103 MB
% 19.74/7.39 % (1458805)Instructions burned: 125 (million)
% 19.74/7.39 % (1458836)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3664749567:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 19.74/7.39 % (1458844)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3475852427:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 19.74/7.39 % (1458836)Instruction limit reached!
% 19.74/7.39 % (1458836)------------------------------
% 19.74/7.39 % (1458836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458836)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458836)Termination reason: Instruction limit
% 19.74/7.39 % (1458836)Termination phase: Property scanning
% 19.74/7.39 % (1458836)Time elapsed: 0.058 s
% 19.74/7.39 % (1458836)Peak memory usage: 103 MB
% 19.74/7.39 % (1458836)Instructions burned: 135 (million)
% 19.74/7.39 % (1458844)Refutation not found, incomplete strategy
% 19.74/7.39 % (1458844)------------------------------
% 19.74/7.39 % (1458844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458844)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458844)Termination reason: Refutation not found, incomplete strategy
% 19.74/7.39 % (1458844)Time elapsed: 0.076 s
% 19.74/7.39 % (1458844)Peak memory usage: 108 MB
% 19.74/7.39 % (1458844)Instructions burned: 91 (million)
% 19.74/7.39 % (1458892)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3725635212:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 19.74/7.39 % (1458844)------------------------------
% 19.74/7.39 % (1458844)------------------------------
% 19.74/7.39 % (1458892)Instruction limit reached!
% 19.74/7.39 % (1458892)------------------------------
% 19.74/7.39 % (1458892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458892)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458892)Termination reason: Instruction limit
% 19.74/7.39 % (1458892)Termination phase: Saturation
% 19.74/7.39 % (1458892)Time elapsed: 0.265 s
% 19.74/7.39 % (1458892)Peak memory usage: 109 MB
% 19.74/7.39 % (1458892)Instructions burned: 432 (million)
% 19.74/7.39 % (1458909)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=333500497:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi)
% 19.74/7.39 % (1458941)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=232687033:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 19.74/7.39 % (1458941)Instruction limit reached!
% 19.74/7.39 % (1458941)------------------------------
% 19.74/7.39 % (1458941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458941)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458941)Termination reason: Instruction limit
% 19.74/7.39 % (1458941)Termination phase: Preprocessing 1
% 19.74/7.39 % (1458941)Time elapsed: 0.180 s
% 19.74/7.39 % (1458941)Peak memory usage: 104 MB
% 19.74/7.39 % (1458941)Instructions burned: 150 (million)
% 19.74/7.39 % (1458944)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1352402143:i=14155:bd=all_2960 on theBenchmark for (2960ds/14155Mi)
% 19.74/7.39 % (1458305)First to succeed.
% 19.74/7.39 % (1458305)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1458008"
% 19.74/7.39 % (1458557)Instruction limit reached!
% 19.74/7.39 % (1458557)------------------------------
% 19.74/7.39 % (1458557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/7.39 % (1458557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/7.39 % (1458557)CaDiCaL version: 2.1.3
% 19.74/7.39 % (1458557)Termination reason: Instruction limit
% 19.74/7.39 % (1458557)Termination phase: Saturation
% 19.74/7.39 % (1458557)Time elapsed: 4.207 s
% 19.74/7.39 % (1458557)Peak memory usage: 218 MB
% 19.74/7.39 % (1458557)Instructions burned: 5202 (million)
% 19.74/7.39 % (1458946)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4253466109:i=667:av=off:fsr=off_2939 on theBenchmark for (2939ds/667Mi)
% 19.74/7.39 % (1458305)Refutation found. Thanks to Tanya!
% 19.74/7.39 % SZS status Theorem for theBenchmark
% 19.74/7.39 % SZS output start Proof for theBenchmark
% See solution above
% 42.10/7.65 % (1458305)------------------------------
% 42.10/7.65 % (1458305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.10/7.65 % (1458305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.10/7.65 % (1458305)CaDiCaL version: 2.1.3
% 42.10/7.65 % (1458305)Termination reason: Refutation
% 42.10/7.65 % (1458305)Time elapsed: 5.025 s
% 42.10/7.65 % (1458305)Peak memory usage: 229 MB
% 42.10/7.65 % (1458305)Instructions burned: 6154 (million)
% 42.10/7.65 % (1458305)------------------------------
% 42.10/7.65 % (1458305)------------------------------
% 42.10/7.65 % (1458008)Success in time 6.52 s
% 42.10/7.65 % Vampire exiting
%------------------------------------------------------------------------------