%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP650+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:19 AM UTC 2026
% Result : Theorem 123.64s 24.05s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 32
% Syntax : Number of formulae : 388 ( 59 unt; 3 def)
% Number of atoms : 2120 ( 287 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 3065 (1333 ~;1503 |; 171 &)
% ( 17 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 27 ( 25 usr; 4 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 1 con; 0-4 aty)
% Number of variables : 514 ( 0 sgn 505 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f677,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f917,axiom,
! [X0] :
( v1_relat_1(k6_relat_1(X0))
& v1_funct_1(k6_relat_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
fof(f966,axiom,
! [X0,X1] :
( r2_hidden(X1,X0)
=> k1_funct_1(k6_relat_1(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_funct_1) ).
fof(f1101,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> k9_relat_1(k6_relat_1(X0),X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t162_funct_1) ).
fof(f1452,axiom,
! [X0] : m2_relset_1(k6_relat_1(X0),X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1725,axiom,
! [X0] : k6_partfun1(X0) = k6_relat_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_partfun1) ).
fof(f1895,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> ( ( v1_funct_1(X2)
& v1_partfun1(X2,X0,X1) )
=> ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_funct_2) ).
fof(f2094,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1)
& m1_relset_1(X2,X0,X1) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f6038,axiom,
! [X0] :
( v3_relat_2(k6_partfun1(X0))
& v8_relat_2(k6_partfun1(X0))
& v1_partfun1(k6_partfun1(X0),X0,X0)
& m2_relset_1(k6_partfun1(X0),X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_eqrel_1) ).
fof(f18256,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f18989,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f18993,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_group_1(X0) )
=> m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_group_1) ).
fof(f21877,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)
=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
=> m1_group_2(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t66_group_2) ).
fof(f21900,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> k7_group_2(X0,X1) = u1_struct_0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_group_2) ).
fof(f21952,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( k12_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1)
& k13_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t132_group_2) ).
fof(f21954,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k12_group_2(X0,k6_group_2(X0),X1) = u1_struct_0(X0)
& k13_group_2(X0,k6_group_2(X0),X1) = u1_struct_0(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t134_group_2) ).
fof(f22007,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f22011,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_1(X1)
& m1_group_2(X1,X0)
& v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
fof(f22017,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_group_1(k6_group_2(X0))
& m1_group_2(k6_group_2(X0),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_group_2) ).
fof(f22018,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_group_2) ).
fof(f22557,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_group_3) ).
fof(f22987,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> u1_struct_0(k11_group_4(X0)) = k1_group_3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t92_group_4) ).
fof(f23001,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( v1_group_1(k5_group_4(X0,X1))
& m1_group_2(k5_group_4(X0,X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_group_4) ).
fof(f26890,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k6_group_2(X0))
& v1_group_1(k6_group_2(X0))
& v2_group_1(k6_group_2(X0))
& v3_group_1(k6_group_2(X0))
& v4_group_1(k6_group_2(X0))
& v1_group_3(k6_group_2(X0),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_group_6) ).
fof(f26949,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t47_group_6) ).
fof(f36492,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( X1 = u1_struct_0(X2)
=> r1_group_2(X0,k5_group_4(X0,X1),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_latsubgr) ).
fof(f36524,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
& m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))) )
=> ( X3 = k3_latsubgr(X0,X1,X2)
<=> ! [X4] :
( ( v1_group_1(X4)
& m1_group_2(X4,X0) )
=> ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1)))
=> ( X5 = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
=> k1_funct_1(X3,X4) = k5_group_4(X1,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_latsubgr) ).
fof(f36525,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) = k6_partfun1(u1_struct_0(k11_group_4(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_latsubgr) ).
fof(f36526,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) = k6_partfun1(u1_struct_0(k11_group_4(X0))) ),
inference(negated_conjecture,[status(cth)],[f36525]) ).
fof(f36620,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,[],[f36492]) ).
fof(f36621,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,[],[f36620]) ).
fof(f36674,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,[],[f36524]) ).
fof(f36675,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,[],[f36674]) ).
fof(f36676,plain,
? [X0] :
( k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) != k6_partfun1(u1_struct_0(k11_group_4(X0)))
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f36526]) ).
fof(f36677,plain,
? [X0] :
( k3_latsubgr(X0,X0,k6_partfun1(u1_struct_0(X0))) != k6_partfun1(u1_struct_0(k11_group_4(X0)))
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f36676]) ).
fof(f36693,plain,
! [X0] :
( ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22557]) ).
fof(f36694,plain,
! [X0] :
( ! [X1] :
( X1 = k1_group_3(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36693]) ).
fof(f36704,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22007]) ).
fof(f36705,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,[],[f36704]) ).
fof(f36706,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(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,[],[f21877]) ).
fof(f36707,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(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,[],[f36706]) ).
fof(f36732,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22987]) ).
fof(f36733,plain,
! [X0] :
( u1_struct_0(k11_group_4(X0)) = k1_group_3(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36732]) ).
fof(f36825,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,[],[f22011]) ).
fof(f36826,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,[],[f36825]) ).
fof(f36847,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,[],[f23001]) ).
fof(f36848,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,[],[f36847]) ).
fof(f36981,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,[],[f2094]) ).
fof(f36982,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,[],[f36981]) ).
fof(f36999,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f26949]) ).
fof(f37000,plain,
! [X0] :
( ( v1_funct_1(k6_partfun1(u1_struct_0(X0)))
& v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
& v1_group_6(k6_partfun1(u1_struct_0(X0)),X0,X0)
& m2_relset_1(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36999]) ).
fof(f37119,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18993]) ).
fof(f37120,plain,
! [X0] :
( m1_subset_1(k2_group_1(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37119]) ).
fof(f37376,plain,
! [X0] :
( ( ~ v3_struct_0(k6_group_2(X0))
& v1_group_1(k6_group_2(X0))
& v2_group_1(k6_group_2(X0))
& v3_group_1(k6_group_2(X0))
& v4_group_1(k6_group_2(X0))
& v1_group_3(k6_group_2(X0),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f26890]) ).
fof(f37377,plain,
! [X0] :
( ( ~ v3_struct_0(k6_group_2(X0))
& v1_group_1(k6_group_2(X0))
& v2_group_1(k6_group_2(X0))
& v3_group_1(k6_group_2(X0))
& v4_group_1(k6_group_2(X0))
& v1_group_3(k6_group_2(X0),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37376]) ).
fof(f37384,plain,
! [X0] :
( ( v1_group_1(k6_group_2(X0))
& m1_group_2(k6_group_2(X0),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f22017]) ).
fof(f37385,plain,
! [X0] :
( ( v1_group_1(k6_group_2(X0))
& m1_group_2(k6_group_2(X0),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37384]) ).
fof(f37386,plain,
! [X0] :
( ! [X1] :
( ( k12_group_2(X0,k6_group_2(X0),X1) = u1_struct_0(X0)
& k13_group_2(X0,k6_group_2(X0),X1) = u1_struct_0(X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21954]) ).
fof(f37387,plain,
! [X0] :
( ! [X1] :
( ( k12_group_2(X0,k6_group_2(X0),X1) = u1_struct_0(X0)
& k13_group_2(X0,k6_group_2(X0),X1) = u1_struct_0(X0) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f37386]) ).
fof(f37824,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,[],[f22018]) ).
fof(f37825,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,[],[f37824]) ).
fof(f37840,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,[],[f21900]) ).
fof(f37841,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,[],[f37840]) ).
fof(f38156,plain,
! [X0,X1] :
( k9_relat_1(k6_relat_1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f1101]) ).
fof(f38216,plain,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_partfun1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1895]) ).
fof(f38217,plain,
! [X0,X1,X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,X0,X1) )
| ~ v1_funct_1(X2)
| ~ v1_partfun1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f38216]) ).
fof(f38585,plain,
! [X0] :
( ! [X1] :
( ( k12_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1)
& k13_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21952]) ).
fof(f38586,plain,
! [X0] :
( ! [X1] :
( ( k12_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1)
& k13_group_2(X0,X1,k2_group_1(X0)) = k7_group_2(X0,X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f38585]) ).
fof(f39243,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f39981,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f40282,plain,
! [X0,X1] :
( k1_funct_1(k6_relat_1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(ennf_transformation,[],[f966]) ).
fof(f42305,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,[],[f36675]) ).
fof(f42306,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,[],[f42305]) ).
fof(f42307,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k3_latsubgr(X0,X1,X2)
| ( k1_funct_1(X3,sK35(X0,X1,X2,X3)) != k5_group_4(X1,sK36(X0,X1,X2,X3))
& sK36(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK35(X0,X1,X2,X3)))
& m1_subset_1(sK36(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
& v1_group_1(sK35(X0,X1,X2,X3))
& m1_group_2(sK35(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,[sK35,sK36]),skolemize(X4,sK35(X0,X1,X2,X3)),skolemize(X5,sK36(X0,X1,X2,X3))],[f42306]) ).
fof(f42308,plain,
( k3_latsubgr(sK37,sK37,k6_partfun1(u1_struct_0(sK37))) != k6_partfun1(u1_struct_0(k11_group_4(sK37)))
& ~ v3_struct_0(sK37)
& v3_group_1(sK37)
& v4_group_1(sK37)
& l1_group_1(sK37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(X0,sK37)],[f36677]) ).
fof(f42324,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(nnf_transformation,[],[f36694]) ).
fof(f42325,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| ~ r2_hidden(X2,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f42324]) ).
fof(f42326,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ? [X2] :
( ( ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0)
| ~ r2_hidden(X2,X1) )
& ( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0) )
& ( ( v1_group_1(X3)
& m1_group_2(X3,X0) )
| ~ r2_hidden(X3,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(rectify,[],[f42325]) ).
fof(f42327,plain,
! [X0] :
( ! [X1] :
( ( X1 = k1_group_3(X0)
| ( ( ~ v1_group_1(sK46(X0,X1))
| ~ m1_group_2(sK46(X0,X1),X0)
| ~ r2_hidden(sK46(X0,X1),X1) )
& ( ( v1_group_1(sK46(X0,X1))
& m1_group_2(sK46(X0,X1),X0) )
| r2_hidden(sK46(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0) )
& ( ( v1_group_1(X3)
& m1_group_2(X3,X0) )
| ~ r2_hidden(X3,X1) ) )
| k1_group_3(X0) != X1 ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X2,sK46(X0,X1))],[f42326]) ).
fof(f42339,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,[],[f1483]) ).
fof(f42355,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,[],[f36826]) ).
fof(f42420,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f677]) ).
fof(f43972,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,[],[f36621]) ).
fof(f44013,plain,
! [X2,X3,X0,X1] :
( ~ v4_group_1(X0)
| m1_group_2(sK35(X0,X1,X2,X3),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)
| k3_latsubgr(X0,X1,X2) = X3
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42307]) ).
fof(f44014,plain,
! [X2,X3,X0,X1] :
( ~ v4_group_1(X0)
| v1_group_1(sK35(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)
| k3_latsubgr(X0,X1,X2) = X3
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42307]) ).
fof(f44016,plain,
! [X2,X3,X0,X1] :
( ~ v4_group_1(X0)
| sK36(X0,X1,X2,X3) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(sK35(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)
| k3_latsubgr(X0,X1,X2) = X3
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42307]) ).
fof(f44017,plain,
! [X2,X3,X0,X1] :
( k1_funct_1(X3,sK35(X0,X1,X2,X3)) != k5_group_4(X1,sK36(X0,X1,X2,X3))
| k3_latsubgr(X0,X1,X2) = X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ m2_relset_1(X3,u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42307]) ).
fof(f44018,plain,
l1_group_1(sK37),
inference(cnf_transformation,[],[f42308]) ).
fof(f44019,plain,
v4_group_1(sK37),
inference(cnf_transformation,[],[f42308]) ).
fof(f44020,plain,
v3_group_1(sK37),
inference(cnf_transformation,[],[f42308]) ).
fof(f44021,plain,
~ v3_struct_0(sK37),
inference(cnf_transformation,[],[f42308]) ).
fof(f44022,plain,
k3_latsubgr(sK37,sK37,k6_partfun1(u1_struct_0(sK37))) != k6_partfun1(u1_struct_0(k11_group_4(sK37))),
inference(cnf_transformation,[],[f42308]) ).
fof(f44048,plain,
! [X3,X0,X1] :
( m1_group_2(X3,X0)
| ~ r2_hidden(X3,X1)
| k1_group_3(X0) != X1
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42327]) ).
fof(f44049,plain,
! [X3,X0,X1] :
( v1_group_1(X3)
| ~ r2_hidden(X3,X1)
| k1_group_3(X0) != X1
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42327]) ).
fof(f44050,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| k1_group_3(X0) != X1
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f42327]) ).
fof(f44068,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| l1_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36705]) ).
fof(f44071,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(X1,X2)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36707]) ).
fof(f44095,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f42339]) ).
fof(f44106,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k1_group_3(X0) = u1_struct_0(k11_group_4(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36733]) ).
fof(f44223,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ r1_group_2(X0,X1,X2)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| X1 = X2
| ~ 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,[],[f42355]) ).
fof(f44248,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,[],[f36848]) ).
fof(f44249,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v1_group_1(k5_group_4(X0,X1))
| ~ l1_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f36848]) ).
fof(f44400,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,[],[f36982]) ).
fof(f44419,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v1_funct_2(k6_partfun1(u1_struct_0(X0)),u1_struct_0(X0),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37000]) ).
fof(f44512,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f42420]) ).
fof(f44558,plain,
! [X0] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| m1_subset_1(k2_group_1(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f37120]) ).
fof(f44941,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v4_group_1(k6_group_2(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37377]) ).
fof(f44942,plain,
! [X0] :
( ~ v4_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v3_group_1(k6_group_2(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37377]) ).
fof(f44945,plain,
! [X0] :
( ~ v3_struct_0(k6_group_2(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37377]) ).
fof(f44951,plain,
! [X0] :
( ~ l1_group_1(X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| m1_group_2(k6_group_2(X0),X0) ),
inference(cnf_transformation,[],[f37385]) ).
fof(f44954,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| u1_struct_0(X0) = k12_group_2(X0,k6_group_2(X0),X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37387]) ).
fof(f45613,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,[],[f37825]) ).
fof(f45627,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,[],[f37841]) ).
fof(f46091,plain,
! [X0,X1] :
( k9_relat_1(k6_relat_1(X0),X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f38156]) ).
fof(f46171,plain,
! [X2,X0,X1] :
( ~ v1_partfun1(X2,X0,X1)
| ~ v1_funct_1(X2)
| v1_funct_2(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f38217]) ).
fof(f46624,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| k7_group_2(X0,X1) = k12_group_2(X0,X1,k2_group_1(X0)) ),
inference(cnf_transformation,[],[f38586]) ).
fof(f47130,plain,
! [X0] : v1_partfun1(k6_partfun1(X0),X0,X0),
inference(cnf_transformation,[],[f6038]) ).
fof(f47427,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f39243]) ).
fof(f48240,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f39981]) ).
fof(f48694,plain,
! [X0] : k6_relat_1(X0) = k6_partfun1(X0),
inference(cnf_transformation,[],[f1725]) ).
fof(f48700,plain,
! [X0] : m2_relset_1(k6_relat_1(X0),X0,X0),
inference(cnf_transformation,[],[f1452]) ).
fof(f48714,plain,
! [X0,X1] :
( k1_funct_1(k6_relat_1(X0),X1) = X1
| ~ r2_hidden(X1,X0) ),
inference(cnf_transformation,[],[f40282]) ).
fof(f48719,plain,
! [X0] : v1_funct_1(k6_relat_1(X0)),
inference(cnf_transformation,[],[f917]) ).
fof(f52169,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k9_relat_1(k6_partfun1(X0),X1) = X1 ),
inference(definition_unfolding,[],[f46091,f48694]) ).
fof(f52589,plain,
! [X0] : m2_relset_1(k6_partfun1(X0),X0,X0),
inference(definition_unfolding,[],[f48700,f48694]) ).
fof(f52603,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| k1_funct_1(k6_partfun1(X0),X1) = X1 ),
inference(definition_unfolding,[],[f48714,f48694]) ).
fof(f52609,plain,
! [X0] : v1_funct_1(k6_partfun1(X0)),
inference(definition_unfolding,[],[f48719,f48694]) ).
fof(f53045,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,[],[f43972]) ).
fof(f53070,plain,
! [X3,X0] :
( ~ v4_group_1(X0)
| ~ v1_group_1(X3)
| ~ m1_group_2(X3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| r2_hidden(X3,k1_group_3(X0))
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f44050]) ).
fof(f53071,plain,
! [X3,X0] :
( ~ l1_group_1(X0)
| ~ r2_hidden(X3,k1_group_3(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| v1_group_1(X3) ),
inference(equality_resolution,[],[f44049]) ).
fof(f53072,plain,
! [X3,X0] :
( ~ v4_group_1(X0)
| ~ r2_hidden(X3,k1_group_3(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(X3,X0)
| ~ l1_group_1(X0) ),
inference(equality_resolution,[],[f44048]) ).
fof(f54314,plain,
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| u1_struct_0(k11_group_4(sK37)) = k1_group_3(sK37)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44106,f44019]) ).
fof(f54315,plain,
( ~ v3_group_1(sK37)
| u1_struct_0(k11_group_4(sK37)) = k1_group_3(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54314,f44021]) ).
fof(f54316,plain,
( u1_struct_0(k11_group_4(sK37)) = k1_group_3(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54315,f44020]) ).
fof(f54317,plain,
u1_struct_0(k11_group_4(sK37)) = k1_group_3(sK37),
inference(forward_subsumption_resolution,[],[f54316,f44018]) ).
fof(f54343,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f48240,f47427]) ).
fof(f54344,plain,
u1_struct_0(sK37) = k2_pre_topc(sK37),
inference(resolution,[],[f54343,f44018]) ).
fof(f54345,plain,
k6_partfun1(u1_struct_0(k11_group_4(sK37))) != k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))),
inference(superposition,[],[f44022,f54344]) ).
fof(f54347,plain,
k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) != k6_partfun1(k1_group_3(sK37)),
inference(forward_demodulation,[],[f54345,f54317]) ).
fof(f54348,plain,
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| v1_funct_2(k6_partfun1(u1_struct_0(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44419,f44019]) ).
fof(f54349,plain,
( ~ v3_group_1(sK37)
| v1_funct_2(k6_partfun1(u1_struct_0(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54348,f44021]) ).
fof(f54350,plain,
( v1_funct_2(k6_partfun1(u1_struct_0(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54349,f44020]) ).
fof(f54351,plain,
v1_funct_2(k6_partfun1(u1_struct_0(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)),
inference(forward_subsumption_resolution,[],[f54350,f44018]) ).
fof(f54352,plain,
v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK37),k2_pre_topc(sK37)),
inference(forward_demodulation,[],[f54351,f54344]) ).
fof(f54383,plain,
( v3_struct_0(sK37)
| m1_subset_1(k2_group_1(sK37),u1_struct_0(sK37)) ),
inference(resolution,[],[f44558,f44018]) ).
fof(f54384,plain,
m1_subset_1(k2_group_1(sK37),u1_struct_0(sK37)),
inference(forward_subsumption_resolution,[],[f54383,f44021]) ).
fof(f54385,plain,
m1_subset_1(k2_group_1(sK37),k2_pre_topc(sK37)),
inference(forward_demodulation,[],[f54384,f54344]) ).
fof(f54404,plain,
! [X0] : m1_relset_1(k6_partfun1(X0),X0,X0),
inference(resolution,[],[f44095,f52589]) ).
fof(f54420,plain,
! [X2,X0,X1] :
( v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44014,f44019]) ).
fof(f54421,plain,
! [X2,X0,X1] :
( v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(sK37)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54420,f44021]) ).
fof(f54422,plain,
! [X2,X0,X1] :
( v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54421,f44020]) ).
fof(f54423,plain,
! [X2,X0,X1] :
( v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f54422,f44018]) ).
fof(f54424,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54423,f54317]) ).
fof(f54425,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54424,f54317]) ).
fof(f54426,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54425,f54344]) ).
fof(f54427,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ v1_funct_2(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| v1_group_1(sK35(sK37,X0,X1,X2))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54426,f54344]) ).
fof(f54428,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(resolution,[],[f54427,f44019]) ).
fof(f54429,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ v3_group_1(sK37)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54428,f44021]) ).
fof(f54430,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54429,f44020]) ).
fof(f54431,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54430,f44018]) ).
fof(f54432,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54431,f54344]) ).
fof(f54433,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54432,f54317]) ).
fof(f54434,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54433,f54317]) ).
fof(f54435,plain,
! [X0,X1] :
( v1_group_1(sK35(sK37,sK37,X0,X1))
| ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54434,f54344]) ).
fof(f54436,plain,
! [X2,X0,X1] :
( sK36(sK37,X0,X1,X2) = k2_funct_2(u1_struct_0(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44016,f44019]) ).
fof(f54437,plain,
! [X2,X0,X1] :
( sK36(sK37,X0,X1,X2) = k2_funct_2(u1_struct_0(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(sK37)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54436,f44021]) ).
fof(f54438,plain,
! [X2,X0,X1] :
( sK36(sK37,X0,X1,X2) = k2_funct_2(u1_struct_0(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54437,f44020]) ).
fof(f54439,plain,
! [X2,X0,X1] :
( sK36(sK37,X0,X1,X2) = k2_funct_2(u1_struct_0(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f54438,f44018]) ).
fof(f54440,plain,
! [X2,X0,X1] :
( sK36(sK37,X0,X1,X2) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54439,f54344]) ).
fof(f54441,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| sK36(sK37,X0,X1,X2) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54440,f54317]) ).
fof(f54442,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| sK36(sK37,X0,X1,X2) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54441,f54317]) ).
fof(f54443,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| sK36(sK37,X0,X1,X2) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54442,f54344]) ).
fof(f54444,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ v1_funct_2(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| sK36(sK37,X0,X1,X2) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(X0),X1,u1_struct_0(sK35(sK37,X0,X1,X2)))
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54443,f54344]) ).
fof(f54445,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(resolution,[],[f54444,f44019]) ).
fof(f54446,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ v3_group_1(sK37)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54445,f44021]) ).
fof(f54447,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54446,f44020]) ).
fof(f54448,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54447,f44018]) ).
fof(f54449,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54448,f54344]) ).
fof(f54450,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54449,f54317]) ).
fof(f54451,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),u1_struct_0(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54450,f54317]) ).
fof(f54452,plain,
! [X0,X1] :
( sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54451,f54344]) ).
fof(f54453,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| sK36(sK37,sK37,X0,X1) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,X1)))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54452,f54344]) ).
fof(f54458,plain,
! [X2,X0,X1] :
( m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44013,f44019]) ).
fof(f54459,plain,
! [X2,X0,X1] :
( m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(sK37)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54458,f44021]) ).
fof(f54460,plain,
! [X2,X0,X1] :
( m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54459,f44020]) ).
fof(f54461,plain,
! [X2,X0,X1] :
( m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f54460,f44018]) ).
fof(f54462,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ m2_relset_1(X2,u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54461,f54317]) ).
fof(f54463,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,u1_struct_0(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54462,f54317]) ).
fof(f54464,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK37),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54463,f54344]) ).
fof(f54465,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ v1_funct_2(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ m2_relset_1(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| ~ v1_funct_2(X2,k1_group_3(sK37),u1_struct_0(k11_group_4(X0)))
| m1_group_2(sK35(sK37,X0,X1,X2),sK37)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ m2_relset_1(X1,k2_pre_topc(sK37),u1_struct_0(X0))
| ~ l1_group_1(X0)
| k3_latsubgr(sK37,X0,X1) = X2 ),
inference(forward_demodulation,[],[f54464,f54344]) ).
fof(f54466,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(resolution,[],[f54465,f44019]) ).
fof(f54467,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ v3_group_1(sK37)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54466,f44021]) ).
fof(f54468,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54467,f44020]) ).
fof(f54469,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54468,f44018]) ).
fof(f54470,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54469,f54344]) ).
fof(f54471,plain,
! [X0,X1] :
( ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_2(X1,k1_group_3(sK37),u1_struct_0(k11_group_4(sK37)))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54470,f54317]) ).
fof(f54472,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,k2_pre_topc(sK37),u1_struct_0(sK37))
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54471,f54317]) ).
fof(f54473,plain,
! [X0,X1] :
( m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_demodulation,[],[f54472,f54344]) ).
fof(f54474,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK37,sK37,X1) = X0
| u1_struct_0(sK35(sK37,sK37,X1,X0)) = k7_group_2(sK37,sK35(sK37,sK37,X1,X0))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f54473,f45627]) ).
fof(f54475,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK37,sK37,X1) = X0
| u1_struct_0(sK35(sK37,sK37,X1,X0)) = k7_group_2(sK37,sK35(sK37,sK37,X1,X0))
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54474,f44021]) ).
fof(f54476,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK37,sK37,X1) = X0
| u1_struct_0(sK35(sK37,sK37,X1,X0)) = k7_group_2(sK37,sK35(sK37,sK37,X1,X0))
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54475,f44020]) ).
fof(f54477,plain,
! [X0,X1] :
( ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK37,sK37,X1) = X0
| u1_struct_0(sK35(sK37,sK37,X1,X0)) = k7_group_2(sK37,sK35(sK37,sK37,X1,X0))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54476,f44019]) ).
fof(f54478,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X1)
| k3_latsubgr(sK37,sK37,X1) = X0
| u1_struct_0(sK35(sK37,sK37,X1,X0)) = k7_group_2(sK37,sK35(sK37,sK37,X1,X0)) ),
inference(forward_subsumption_resolution,[],[f54477,f44018]) ).
fof(f54508,plain,
! [X0] :
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| v1_group_1(k5_group_4(sK37,X0))
| ~ l1_group_1(sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(resolution,[],[f44249,f44019]) ).
fof(f54509,plain,
! [X0] :
( ~ v3_group_1(sK37)
| v1_group_1(k5_group_4(sK37,X0))
| ~ l1_group_1(sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(forward_subsumption_resolution,[],[f54508,f44021]) ).
fof(f54510,plain,
! [X0] :
( v1_group_1(k5_group_4(sK37,X0))
| ~ l1_group_1(sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(forward_subsumption_resolution,[],[f54509,f44020]) ).
fof(f54511,plain,
! [X0] :
( v1_group_1(k5_group_4(sK37,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(forward_subsumption_resolution,[],[f54510,f44018]) ).
fof(f54512,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK37)))
| v1_group_1(k5_group_4(sK37,X0)) ),
inference(forward_demodulation,[],[f54511,f54344]) ).
fof(f54678,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| r2_hidden(X0,k1_group_3(sK37))
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f53070,f44019]) ).
fof(f54679,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ v3_group_1(sK37)
| r2_hidden(X0,k1_group_3(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54678,f44021]) ).
fof(f54680,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| r2_hidden(X0,k1_group_3(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54679,f44020]) ).
fof(f54681,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| r2_hidden(X0,k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f54680,f44018]) ).
fof(f54682,plain,
! [X0,X1] :
( ~ m1_group_2(sK35(sK37,sK37,X0,X1),sK37)
| r2_hidden(sK35(sK37,sK37,X0,X1),k1_group_3(sK37))
| ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(resolution,[],[f54681,f54435]) ).
fof(f54683,plain,
! [X0,X1] :
( ~ v1_funct_2(X1,k1_group_3(sK37),k1_group_3(sK37))
| r2_hidden(sK35(sK37,sK37,X0,X1),k1_group_3(sK37))
| ~ m2_relset_1(X1,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X1)
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = X1 ),
inference(forward_subsumption_resolution,[],[f54682,f54473]) ).
fof(f54685,plain,
! [X0] :
( ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = X0
| u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),X0)) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),X0)) ),
inference(resolution,[],[f54478,f54352]) ).
fof(f54686,plain,
! [X0] :
( ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_1(X0)
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = X0
| u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),X0)) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),X0)) ),
inference(forward_subsumption_resolution,[],[f54685,f52589]) ).
fof(f54687,plain,
! [X0] :
( ~ v1_funct_2(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ m2_relset_1(X0,k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = X0
| u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),X0)) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),X0)) ),
inference(forward_subsumption_resolution,[],[f54686,f52609]) ).
fof(f54818,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| m1_group_2(X0,sK37)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f53072,f44019]) ).
fof(f54819,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| ~ v3_group_1(sK37)
| m1_group_2(X0,sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54818,f44021]) ).
fof(f54820,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| m1_group_2(X0,sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f54819,f44020]) ).
fof(f54821,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| m1_group_2(X0,sK37) ),
inference(forward_subsumption_resolution,[],[f54820,f44018]) ).
fof(f55037,plain,
! [X0] :
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| m1_subset_1(k7_group_2(sK37,X0),k1_zfmisc_1(u1_struct_0(sK37)))
| ~ l1_group_1(sK37)
| ~ m1_group_2(X0,sK37) ),
inference(resolution,[],[f45613,f44019]) ).
fof(f55038,plain,
! [X0] :
( ~ v3_group_1(sK37)
| m1_subset_1(k7_group_2(sK37,X0),k1_zfmisc_1(u1_struct_0(sK37)))
| ~ l1_group_1(sK37)
| ~ m1_group_2(X0,sK37) ),
inference(forward_subsumption_resolution,[],[f55037,f44021]) ).
fof(f55039,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK37,X0),k1_zfmisc_1(u1_struct_0(sK37)))
| ~ l1_group_1(sK37)
| ~ m1_group_2(X0,sK37) ),
inference(forward_subsumption_resolution,[],[f55038,f44020]) ).
fof(f55040,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK37,X0),k1_zfmisc_1(u1_struct_0(sK37)))
| ~ m1_group_2(X0,sK37) ),
inference(forward_subsumption_resolution,[],[f55039,f44018]) ).
fof(f55041,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| m1_subset_1(k7_group_2(sK37,X0),k1_zfmisc_1(k2_pre_topc(sK37))) ),
inference(forward_demodulation,[],[f55040,f54344]) ).
fof(f55058,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| v3_struct_0(sK37)
| l1_group_1(X0)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44068,f44020]) ).
fof(f55059,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| l1_group_1(X0)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55058,f44021]) ).
fof(f55060,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f55059,f44018]) ).
fof(f55090,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK37)))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(X0)),X0)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f53045,f44019]) ).
fof(f55091,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK37)))
| ~ v3_group_1(sK37)
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(X0)),X0)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55090,f44021]) ).
fof(f55092,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK37)))
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(X0)),X0)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55091,f44020]) ).
fof(f55093,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(u1_struct_0(sK37)))
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(X0)),X0) ),
inference(forward_subsumption_resolution,[],[f55092,f44018]) ).
fof(f55094,plain,
! [X0] :
( ~ v1_group_1(X0)
| ~ m1_subset_1(u1_struct_0(X0),k1_zfmisc_1(k2_pre_topc(sK37)))
| ~ m1_group_2(X0,sK37)
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(X0)),X0) ),
inference(forward_demodulation,[],[f55093,f54344]) ).
fof(f55179,plain,
! [X0,X1] :
( ~ r1_group_2(sK37,X0,X1)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| X0 = X1
| ~ l1_group_1(sK37)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK37) ),
inference(resolution,[],[f44223,f44019]) ).
fof(f55180,plain,
! [X0,X1] :
( ~ r1_group_2(sK37,X0,X1)
| ~ v3_group_1(sK37)
| X0 = X1
| ~ l1_group_1(sK37)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK37) ),
inference(forward_subsumption_resolution,[],[f55179,f44021]) ).
fof(f55181,plain,
! [X0,X1] :
( ~ r1_group_2(sK37,X0,X1)
| X0 = X1
| ~ l1_group_1(sK37)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK37) ),
inference(forward_subsumption_resolution,[],[f55180,f44020]) ).
fof(f55182,plain,
! [X0,X1] :
( ~ r1_group_2(sK37,X0,X1)
| X0 = X1
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK37)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,sK37) ),
inference(forward_subsumption_resolution,[],[f55181,f44018]) ).
fof(f55202,plain,
! [X0] :
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| m1_group_2(k5_group_4(sK37,X0),sK37)
| ~ l1_group_1(sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(resolution,[],[f44248,f44019]) ).
fof(f55203,plain,
! [X0] :
( ~ v3_group_1(sK37)
| m1_group_2(k5_group_4(sK37,X0),sK37)
| ~ l1_group_1(sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(forward_subsumption_resolution,[],[f55202,f44021]) ).
fof(f55204,plain,
! [X0] :
( m1_group_2(k5_group_4(sK37,X0),sK37)
| ~ l1_group_1(sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(forward_subsumption_resolution,[],[f55203,f44020]) ).
fof(f55205,plain,
! [X0] :
( m1_group_2(k5_group_4(sK37,X0),sK37)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK37))) ),
inference(forward_subsumption_resolution,[],[f55204,f44018]) ).
fof(f55206,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK37)))
| m1_group_2(k5_group_4(sK37,X0),sK37) ),
inference(forward_demodulation,[],[f55205,f54344]) ).
fof(f55219,plain,
! [X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK37)
| ~ m1_group_2(X0,sK37)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44071,f44019]) ).
fof(f55220,plain,
! [X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK37)
| ~ m1_group_2(X0,sK37)
| ~ v3_group_1(sK37)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55219,f44021]) ).
fof(f55221,plain,
! [X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK37)
| ~ m1_group_2(X0,sK37)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55220,f44020]) ).
fof(f55222,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK37)
| ~ m1_group_2(X1,sK37)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f55221,f44018]) ).
fof(f55661,plain,
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| v3_group_1(k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44942,f44019]) ).
fof(f55664,plain,
( ~ v3_group_1(sK37)
| v3_group_1(k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55661,f44021]) ).
fof(f55666,plain,
( v3_group_1(k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f55664,f44020]) ).
fof(f55667,plain,
v3_group_1(k6_group_2(sK37)),
inference(forward_subsumption_resolution,[],[f55666,f44018]) ).
fof(f55677,definition,
( spl1148_65
<=> v3_struct_0(k6_group_2(sK37)) ),
introduced(definition,[new_symbols(definition,[spl1148_65])],[avatar_definition]) ).
fof(f55678,plain,
( v3_struct_0(k6_group_2(sK37))
| ~ spl1148_65 ),
inference(avatar_component_clause,[],[f55677]) ).
fof(f56003,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| u1_struct_0(sK37) = k12_group_2(sK37,k6_group_2(sK37),X0)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44954,f44019]) ).
fof(f56006,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK37))
| ~ v3_group_1(sK37)
| u1_struct_0(sK37) = k12_group_2(sK37,k6_group_2(sK37),X0)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f56003,f44021]) ).
fof(f56008,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK37))
| u1_struct_0(sK37) = k12_group_2(sK37,k6_group_2(sK37),X0)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f56006,f44020]) ).
fof(f56009,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK37))
| u1_struct_0(sK37) = k12_group_2(sK37,k6_group_2(sK37),X0) ),
inference(forward_subsumption_resolution,[],[f56008,f44018]) ).
fof(f56010,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK37))
| u1_struct_0(sK37) = k12_group_2(sK37,k6_group_2(sK37),X0) ),
inference(forward_demodulation,[],[f56009,f54344]) ).
fof(f56011,plain,
! [X0] :
( ~ m1_subset_1(X0,k2_pre_topc(sK37))
| k2_pre_topc(sK37) = k12_group_2(sK37,k6_group_2(sK37),X0) ),
inference(forward_demodulation,[],[f56010,f54344]) ).
fof(f56012,plain,
k2_pre_topc(sK37) = k12_group_2(sK37,k6_group_2(sK37),k2_group_1(sK37)),
inference(resolution,[],[f56011,f54385]) ).
fof(f56047,plain,
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| v4_group_1(k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f44941,f44019]) ).
fof(f56050,plain,
( ~ v3_group_1(sK37)
| v4_group_1(k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f56047,f44021]) ).
fof(f56052,plain,
( v4_group_1(k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f56050,f44020]) ).
fof(f56053,plain,
v4_group_1(k6_group_2(sK37)),
inference(forward_subsumption_resolution,[],[f56052,f44018]) ).
fof(f56079,plain,
! [X0] :
( v3_struct_0(k6_group_2(sK37))
| ~ v3_group_1(k6_group_2(sK37))
| m1_subset_1(k7_group_2(k6_group_2(sK37),X0),k1_zfmisc_1(u1_struct_0(k6_group_2(sK37))))
| ~ l1_group_1(k6_group_2(sK37))
| ~ m1_group_2(X0,k6_group_2(sK37)) ),
inference(resolution,[],[f56053,f45613]) ).
fof(f56455,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| v1_group_1(X0) ),
inference(resolution,[],[f53071,f44018]) ).
fof(f56458,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| v1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f56455,f44021]) ).
fof(f56460,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| ~ v4_group_1(sK37)
| v1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f56458,f44020]) ).
fof(f56461,plain,
! [X0] :
( ~ r2_hidden(X0,k1_group_3(sK37))
| v1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f56460,f44019]) ).
fof(f57594,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| k7_group_2(sK37,X0) = k12_group_2(sK37,X0,k2_group_1(sK37)) ),
inference(resolution,[],[f46624,f44018]) ).
fof(f57598,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| k7_group_2(sK37,X0) = k12_group_2(sK37,X0,k2_group_1(sK37)) ),
inference(forward_subsumption_resolution,[],[f57594,f44021]) ).
fof(f57600,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| ~ v4_group_1(sK37)
| k7_group_2(sK37,X0) = k12_group_2(sK37,X0,k2_group_1(sK37)) ),
inference(forward_subsumption_resolution,[],[f57598,f44020]) ).
fof(f57601,plain,
! [X0] :
( ~ m1_group_2(X0,sK37)
| k7_group_2(sK37,X0) = k12_group_2(sK37,X0,k2_group_1(sK37)) ),
inference(forward_subsumption_resolution,[],[f57600,f44019]) ).
fof(f57615,plain,
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| m1_group_2(k6_group_2(sK37),sK37) ),
inference(resolution,[],[f44951,f44018]) ).
fof(f57619,plain,
( ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| m1_group_2(k6_group_2(sK37),sK37) ),
inference(forward_subsumption_resolution,[],[f57615,f44021]) ).
fof(f57621,plain,
( ~ v4_group_1(sK37)
| m1_group_2(k6_group_2(sK37),sK37) ),
inference(forward_subsumption_resolution,[],[f57619,f44020]) ).
fof(f57622,plain,
m1_group_2(k6_group_2(sK37),sK37),
inference(forward_subsumption_resolution,[],[f57621,f44019]) ).
fof(f57627,plain,
l1_group_1(k6_group_2(sK37)),
inference(resolution,[],[f57622,f55060]) ).
fof(f57634,plain,
k12_group_2(sK37,k6_group_2(sK37),k2_group_1(sK37)) = k7_group_2(sK37,k6_group_2(sK37)),
inference(resolution,[],[f57622,f57601]) ).
fof(f57635,plain,
( u1_struct_0(k6_group_2(sK37)) = k7_group_2(sK37,k6_group_2(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(resolution,[],[f57622,f45627]) ).
fof(f57638,plain,
( u1_struct_0(k6_group_2(sK37)) = k7_group_2(sK37,k6_group_2(sK37))
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f57635,f44021]) ).
fof(f57639,plain,
k2_pre_topc(sK37) = k7_group_2(sK37,k6_group_2(sK37)),
inference(forward_demodulation,[],[f57634,f56012]) ).
fof(f57643,plain,
( u1_struct_0(k6_group_2(sK37)) = k7_group_2(sK37,k6_group_2(sK37))
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f57638,f44020]) ).
fof(f57644,plain,
( u1_struct_0(k6_group_2(sK37)) = k7_group_2(sK37,k6_group_2(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f57643,f44019]) ).
fof(f57645,plain,
u1_struct_0(k6_group_2(sK37)) = k7_group_2(sK37,k6_group_2(sK37)),
inference(forward_subsumption_resolution,[],[f57644,f44018]) ).
fof(f57646,plain,
k2_pre_topc(sK37) = u1_struct_0(k6_group_2(sK37)),
inference(forward_demodulation,[],[f57645,f57639]) ).
fof(f57661,plain,
( v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37)
| ~ spl1148_65 ),
inference(resolution,[],[f55678,f44945]) ).
fof(f57667,plain,
( ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37)
| ~ spl1148_65 ),
inference(forward_subsumption_resolution,[],[f57661,f44021]) ).
fof(f57672,plain,
( ~ v4_group_1(sK37)
| ~ l1_group_1(sK37)
| ~ spl1148_65 ),
inference(forward_subsumption_resolution,[],[f57667,f44020]) ).
fof(f57673,plain,
( ~ l1_group_1(sK37)
| ~ spl1148_65 ),
inference(forward_subsumption_resolution,[],[f57672,f44019]) ).
fof(f57674,plain,
( $false
| ~ spl1148_65 ),
inference(forward_subsumption_resolution,[],[f57673,f44018]) ).
fof(f57675,plain,
~ spl1148_65,
inference(avatar_contradiction_clause,[],[f57674]) ).
fof(f57700,plain,
! [X0] :
( v3_struct_0(k6_group_2(sK37))
| m1_subset_1(k7_group_2(k6_group_2(sK37),X0),k1_zfmisc_1(u1_struct_0(k6_group_2(sK37))))
| ~ l1_group_1(k6_group_2(sK37))
| ~ m1_group_2(X0,k6_group_2(sK37)) ),
inference(forward_subsumption_resolution,[],[f56079,f55667]) ).
fof(f57751,plain,
! [X0] :
( v3_struct_0(k6_group_2(sK37))
| m1_subset_1(k7_group_2(k6_group_2(sK37),X0),k1_zfmisc_1(u1_struct_0(k6_group_2(sK37))))
| ~ m1_group_2(X0,k6_group_2(sK37)) ),
inference(forward_subsumption_resolution,[],[f57700,f57627]) ).
fof(f57830,plain,
! [X0] :
( m1_subset_1(k7_group_2(k6_group_2(sK37),X0),k1_zfmisc_1(k2_pre_topc(sK37)))
| v3_struct_0(k6_group_2(sK37))
| ~ m1_group_2(X0,k6_group_2(sK37)) ),
inference(forward_demodulation,[],[f57751,f57646]) ).
fof(f57906,definition,
( spl1148_178
<=> ! [X0] :
( m1_subset_1(k7_group_2(k6_group_2(sK37),X0),k1_zfmisc_1(k2_pre_topc(sK37)))
| ~ m1_group_2(X0,k6_group_2(sK37)) ) ),
introduced(definition,[new_symbols(definition,[spl1148_178])],[avatar_definition]) ).
fof(f57907,plain,
( ! [X0] :
( ~ m1_group_2(X0,k6_group_2(sK37))
| m1_subset_1(k7_group_2(k6_group_2(sK37),X0),k1_zfmisc_1(k2_pre_topc(sK37))) )
| ~ spl1148_178 ),
inference(avatar_component_clause,[],[f57906]) ).
fof(f57908,plain,
( spl1148_65
| spl1148_178 ),
inference(avatar_split_clause,[],[f57830,f57906,f55677]) ).
fof(f63044,plain,
! [X0,X1] :
( ~ v1_funct_1(k6_partfun1(X0))
| ~ v1_funct_2(k6_partfun1(X0),X0,X0)
| k9_relat_1(k6_partfun1(X0),X1) = k2_funct_2(X0,X0,k6_partfun1(X0),X1) ),
inference(resolution,[],[f44400,f54404]) ).
fof(f63049,plain,
! [X0,X1] :
( ~ v1_funct_2(k6_partfun1(X0),X0,X0)
| k9_relat_1(k6_partfun1(X0),X1) = k2_funct_2(X0,X0,k6_partfun1(X0),X1) ),
inference(forward_subsumption_resolution,[],[f63044,f52609]) ).
fof(f67896,plain,
! [X0] :
( ~ v1_funct_1(k6_partfun1(X0))
| v1_funct_2(k6_partfun1(X0),X0,X0)
| ~ m1_relset_1(k6_partfun1(X0),X0,X0) ),
inference(resolution,[],[f46171,f47130]) ).
fof(f67897,plain,
! [X0] :
( v1_funct_2(k6_partfun1(X0),X0,X0)
| ~ m1_relset_1(k6_partfun1(X0),X0,X0) ),
inference(forward_subsumption_resolution,[],[f67896,f52609]) ).
fof(f67898,plain,
! [X0] : v1_funct_2(k6_partfun1(X0),X0,X0),
inference(forward_subsumption_resolution,[],[f67897,f54404]) ).
fof(f67914,plain,
! [X0] :
( sK36(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37)))))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = k6_partfun1(k1_group_3(sK37)) ),
inference(resolution,[],[f67898,f54453]) ).
fof(f67918,plain,
! [X0] :
( r2_hidden(sK35(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = k6_partfun1(k1_group_3(sK37)) ),
inference(resolution,[],[f67898,f54683]) ).
fof(f67919,plain,
( ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),k1_group_3(sK37),k1_group_3(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37))
| u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
inference(resolution,[],[f67898,f54687]) ).
fof(f68001,plain,
( ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37))
| u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
inference(forward_subsumption_resolution,[],[f67919,f52589]) ).
fof(f68002,plain,
! [X0] :
( r2_hidden(sK35(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f67918,f52589]) ).
fof(f68006,plain,
! [X0] :
( sK36(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37)))))
| ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f67914,f52589]) ).
fof(f68031,plain,
( k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37))
| u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
inference(forward_subsumption_resolution,[],[f68001,f52609]) ).
fof(f68032,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| r2_hidden(sK35(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f68002,f52609]) ).
fof(f68036,plain,
! [X0] :
( ~ m2_relset_1(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| sK36(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),X0,u1_struct_0(sK35(sK37,sK37,X0,k6_partfun1(k1_group_3(sK37)))))
| ~ v1_funct_2(X0,k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(X0)
| k3_latsubgr(sK37,sK37,X0) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f68006,f52609]) ).
fof(f68037,plain,
u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(forward_subsumption_resolution,[],[f68031,f54347]) ).
fof(f68073,plain,
( sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK37),k2_pre_topc(sK37))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37)) ),
inference(resolution,[],[f68036,f52589]) ).
fof(f68074,plain,
( sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f68073,f54352]) ).
fof(f68075,plain,
( sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f68074,f52609]) ).
fof(f68076,plain,
sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k2_funct_2(k2_pre_topc(sK37),k2_pre_topc(sK37),k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),
inference(forward_subsumption_resolution,[],[f68075,f54347]) ).
fof(f68257,plain,
( ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK37),k2_pre_topc(sK37))
| r2_hidden(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37)) ),
inference(resolution,[],[f68032,f52589]) ).
fof(f68258,plain,
( r2_hidden(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f68257,f54352]) ).
fof(f68259,plain,
( r2_hidden(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37)) ),
inference(forward_subsumption_resolution,[],[f68258,f52609]) ).
fof(f68260,plain,
r2_hidden(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k1_group_3(sK37)),
inference(forward_subsumption_resolution,[],[f68259,f54347]) ).
fof(f68261,plain,
v1_group_1(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(resolution,[],[f68260,f56461]) ).
fof(f68262,plain,
m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37),
inference(resolution,[],[f68260,f54821]) ).
fof(f68268,plain,
sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k1_funct_1(k6_partfun1(k1_group_3(sK37)),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(resolution,[],[f68260,f52603]) ).
fof(f68270,plain,
m1_subset_1(k7_group_2(sK37,sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k1_zfmisc_1(k2_pre_topc(sK37))),
inference(resolution,[],[f68262,f55041]) ).
fof(f68271,plain,
l1_group_1(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(resolution,[],[f68262,f55060]) ).
fof(f68274,plain,
! [X0] :
( ~ r1_tarski(u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),u1_struct_0(X0))
| ~ m1_group_2(X0,sK37)
| m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),X0) ),
inference(resolution,[],[f68262,f55222]) ).
fof(f68296,plain,
m1_subset_1(u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k1_zfmisc_1(k2_pre_topc(sK37))),
inference(forward_demodulation,[],[f68270,f68037]) ).
fof(f68322,plain,
( ~ m1_subset_1(u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k1_zfmisc_1(k2_pre_topc(sK37)))
| ~ m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37)
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
inference(resolution,[],[f68261,f55094]) ).
fof(f68324,plain,
( ~ m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37)
| r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
inference(forward_subsumption_resolution,[],[f68322,f68296]) ).
fof(f68328,plain,
r1_group_2(sK37,k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(forward_subsumption_resolution,[],[f68324,f68262]) ).
fof(f68371,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37)
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(superposition,[],[f44017,f68268]) ).
fof(f68372,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| k3_latsubgr(sK37,sK37,k6_partfun1(k2_pre_topc(sK37))) = k6_partfun1(k1_group_3(sK37))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(duplicate_literal_removal,[],[f68371]) ).
fof(f68373,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_1(k6_partfun1(k2_pre_topc(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f68372,f54347]) ).
fof(f68374,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_1(k6_partfun1(k1_group_3(sK37)))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f68373,f52609]) ).
fof(f68375,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f68374,f52609]) ).
fof(f68376,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ v3_group_1(sK37)
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f68375,f44021]) ).
fof(f68377,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ v4_group_1(sK37)
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f68376,f44020]) ).
fof(f68378,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ l1_group_1(sK37) ),
inference(forward_subsumption_resolution,[],[f68377,f44019]) ).
fof(f68379,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f68378,f44018]) ).
fof(f68380,plain,
( ~ v1_funct_2(k6_partfun1(k1_group_3(sK37)),k1_group_3(sK37),k1_group_3(sK37))
| sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f68379,f54317]) ).
fof(f68381,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),u1_struct_0(k11_group_4(sK37)),u1_struct_0(k11_group_4(sK37)))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f68380,f67898]) ).
fof(f68382,plain,
( ~ m2_relset_1(k6_partfun1(k1_group_3(sK37)),k1_group_3(sK37),k1_group_3(sK37))
| sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f68381,f54317]) ).
fof(f68383,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f68382,f52589]) ).
fof(f68384,plain,
( ~ v1_funct_2(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK37),k2_pre_topc(sK37))
| sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f68383,f54344]) ).
fof(f68385,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK37),u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f68384,f54352]) ).
fof(f68386,plain,
( ~ m2_relset_1(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK37),k2_pre_topc(sK37))
| sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
inference(forward_demodulation,[],[f68385,f54344]) ).
fof(f68387,plain,
sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) != k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(forward_subsumption_resolution,[],[f68386,f52589]) ).
fof(f68438,plain,
m1_group_2(k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),sK37),
inference(resolution,[],[f68296,f55206]) ).
fof(f68439,plain,
v1_group_1(k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))),
inference(resolution,[],[f68296,f54512]) ).
fof(f68440,plain,
r1_tarski(u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k2_pre_topc(sK37)),
inference(resolution,[],[f68296,f44512]) ).
fof(f69962,plain,
u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),
inference(resolution,[],[f68271,f54343]) ).
fof(f117798,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ v1_group_1(k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))))
| ~ m1_group_2(k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),sK37)
| ~ v1_group_1(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37) ),
inference(resolution,[],[f68328,f55182]) ).
fof(f117801,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ m1_group_2(k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),sK37)
| ~ v1_group_1(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37) ),
inference(forward_subsumption_resolution,[],[f117798,f68439]) ).
fof(f117803,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ v1_group_1(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37) ),
inference(forward_subsumption_resolution,[],[f117801,f68438]) ).
fof(f117805,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),sK37) ),
inference(forward_subsumption_resolution,[],[f117803,f68261]) ).
fof(f117807,plain,
sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),
inference(forward_subsumption_resolution,[],[f117805,f68262]) ).
fof(f117809,plain,
sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),
inference(forward_demodulation,[],[f117807,f69962]) ).
fof(f123343,plain,
( ~ r1_tarski(u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k2_pre_topc(sK37))
| ~ m1_group_2(k6_group_2(sK37),sK37)
| m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k6_group_2(sK37)) ),
inference(superposition,[],[f68274,f57646]) ).
fof(f123353,plain,
( ~ m1_group_2(k6_group_2(sK37),sK37)
| m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k6_group_2(sK37)) ),
inference(forward_subsumption_resolution,[],[f123343,f68440]) ).
fof(f123363,plain,
m1_group_2(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))),k6_group_2(sK37)),
inference(forward_subsumption_resolution,[],[f123353,f57622]) ).
fof(f123383,plain,
( u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| v3_struct_0(k6_group_2(sK37))
| ~ v3_group_1(k6_group_2(sK37))
| ~ v4_group_1(k6_group_2(sK37))
| ~ l1_group_1(k6_group_2(sK37)) ),
inference(resolution,[],[f123363,f45627]) ).
fof(f123384,plain,
( u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| v3_struct_0(k6_group_2(sK37))
| ~ v4_group_1(k6_group_2(sK37))
| ~ l1_group_1(k6_group_2(sK37)) ),
inference(forward_subsumption_resolution,[],[f123383,f55667]) ).
fof(f123390,plain,
( u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| v3_struct_0(k6_group_2(sK37))
| ~ l1_group_1(k6_group_2(sK37)) ),
inference(forward_subsumption_resolution,[],[f123384,f56053]) ).
fof(f123393,plain,
( u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| v3_struct_0(k6_group_2(sK37)) ),
inference(forward_subsumption_resolution,[],[f123390,f57627]) ).
fof(f123395,plain,
( k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| v3_struct_0(k6_group_2(sK37)) ),
inference(forward_demodulation,[],[f123393,f69962]) ).
fof(f123397,definition,
( spl1148_1673
<=> k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) ),
introduced(definition,[new_symbols(definition,[spl1148_1673])],[avatar_definition]) ).
fof(f123398,plain,
( k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ spl1148_1673 ),
inference(avatar_component_clause,[],[f123397]) ).
fof(f123399,plain,
( spl1148_65
| spl1148_1673 ),
inference(avatar_split_clause,[],[f123395,f123397,f55677]) ).
fof(f237258,plain,
! [X0,X1] : k9_relat_1(k6_partfun1(X0),X1) = k2_funct_2(X0,X0,k6_partfun1(X0),X1),
inference(resolution,[],[f63049,f67898]) ).
fof(f237323,plain,
sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k9_relat_1(k6_partfun1(k2_pre_topc(sK37)),u1_struct_0(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),
inference(superposition,[],[f68076,f237258]) ).
fof(f237324,plain,
sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k9_relat_1(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))),
inference(forward_demodulation,[],[f237323,f69962]) ).
fof(f274628,plain,
( m1_subset_1(k7_group_2(k6_group_2(sK37),sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k1_zfmisc_1(k2_pre_topc(sK37)))
| ~ spl1148_178 ),
inference(resolution,[],[f57907,f123363]) ).
fof(f274645,plain,
( m1_subset_1(k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))),k1_zfmisc_1(k2_pre_topc(sK37)))
| ~ spl1148_178
| ~ spl1148_1673 ),
inference(forward_demodulation,[],[f274628,f123398]) ).
fof(f274793,plain,
( k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))) = k9_relat_1(k6_partfun1(k2_pre_topc(sK37)),k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37)))))
| ~ spl1148_178
| ~ spl1148_1673 ),
inference(resolution,[],[f274645,f52169]) ).
fof(f274827,plain,
( sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k2_pre_topc(sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ spl1148_178
| ~ spl1148_1673 ),
inference(forward_demodulation,[],[f274793,f237324]) ).
fof(f274867,plain,
( sK35(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))) = k5_group_4(sK37,sK36(sK37,sK37,k6_partfun1(k2_pre_topc(sK37)),k6_partfun1(k1_group_3(sK37))))
| ~ spl1148_178
| ~ spl1148_1673 ),
inference(superposition,[],[f117809,f274827]) ).
fof(f274878,plain,
( $false
| ~ spl1148_178
| ~ spl1148_1673 ),
inference(forward_subsumption_resolution,[],[f274867,f68387]) ).
fof(f274879,plain,
( ~ spl1148_178
| ~ spl1148_1673 ),
inference(avatar_contradiction_clause,[],[f274878]) ).
cnf(s142,plain,
~ spl1148_65,
inference(sat_conversion,[],[f57675]) ).
cnf(s165,plain,
( spl1148_65
| spl1148_178 ),
inference(sat_conversion,[],[f57908]) ).
cnf(s1715,plain,
( spl1148_65
| spl1148_1673 ),
inference(sat_conversion,[],[f123399]) ).
cnf(s5704,plain,
( ~ spl1148_178
| ~ spl1148_1673 ),
inference(sat_conversion,[],[f274879]) ).
cnf(s6631,plain,
spl1148_1673,
inference(rat,[],[s1715,s142]) ).
cnf(s6724,plain,
spl1148_178,
inference(rat,[],[s165,s142]) ).
cnf(s6760,plain,
$false,
inference(rat,[],[s5704,s6631,s6724]) ).
fof(f274880,plain,
$false,
inference(avatar_sat_refutation,[],[s6760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP650+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 % Computer : n011.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sun Sep 27 10:28:42 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.45 Running first-order theorem proving
% 0.11/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.51/4.92 % (2196791)Detected formulas, will run a generic FOF schedule.
% 13.51/4.92 % (2196800)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1036468437:i=119:av=off:ss=axioms_2976 on theBenchmark for (2976ds/119Mi)
% 13.51/4.92 % (2196797)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=612147938:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2976 on theBenchmark for (2976ds/134677Mi)
% 13.51/4.92 % (2196798)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=1315621690:i=141695:sd=1:nm=32:gsp=on:ss=included_2976 on theBenchmark for (2976ds/141695Mi)
% 13.51/4.92 % (2196796)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=1177531205:i=141193_2976 on theBenchmark for (2976ds/141193Mi)
% 13.51/4.92 % (2196802)dis-21_1_sil=8000:lcm=predicate:random_seed=637663892:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2976 on theBenchmark for (2976ds/129Mi)
% 13.51/4.92 % (2196799)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=391520100:i=109:sd=1:ins=1:gsp=on:ss=axioms_2976 on theBenchmark for (2976ds/109Mi)
% 13.51/4.92 % (2196801)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=486888810:s2a=on:i=139:gtg=position_2976 on theBenchmark for (2976ds/139Mi)
% 13.51/4.92 % (2196800)Instruction limit reached!
% 13.51/4.92 % (2196800)------------------------------
% 13.51/4.92 % (2196800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.51/4.92 % (2196800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/4.92 % (2196800)CaDiCaL version: 2.1.3
% 13.51/4.92 % (2196800)Termination reason: Instruction limit
% 13.51/4.92 % (2196800)Termination phase: SInE selection
% 13.51/4.92 % (2196800)Time elapsed: 0.054 s
% 13.51/4.92 % (2196800)Peak memory usage: 139 MB
% 13.51/4.92 % (2196800)Instructions burned: 119 (million)
% 13.51/4.92 % (2196801)Instruction limit reached!
% 13.51/4.92 % (2196801)------------------------------
% 13.51/4.92 % (2196801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.51/4.92 % (2196801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/4.92 % (2196801)CaDiCaL version: 2.1.3
% 13.51/4.92 % (2196801)Termination reason: Instruction limit
% 13.51/4.92 % (2196801)Termination phase: Property scanning
% 13.51/4.92 % (2196801)Time elapsed: 0.063 s
% 13.51/4.92 % (2196801)Peak memory usage: 139 MB
% 13.51/4.92 % (2196801)Instructions burned: 141 (million)
% 13.51/4.92 % (2196799)Instruction limit reached!
% 13.51/4.92 % (2196799)------------------------------
% 13.51/4.92 % (2196799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.51/4.92 % (2196799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/4.92 % (2196799)CaDiCaL version: 2.1.3
% 13.51/4.92 % (2196799)Termination reason: Instruction limit
% 13.51/4.92 % (2196799)Termination phase: SInE selection
% 13.51/4.92 % (2196799)Time elapsed: 0.078 s
% 13.51/4.92 % (2196799)Peak memory usage: 139 MB
% 13.51/4.92 % (2196799)Instructions burned: 109 (million)
% 13.51/4.92 % (2196802)Instruction limit reached!
% 13.51/4.92 % (2196802)------------------------------
% 13.51/4.92 % (2196802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.51/4.92 % (2196802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.51/4.92 % (2196802)CaDiCaL version: 2.1.3
% 13.51/4.92 % (2196802)Termination reason: Instruction limit
% 13.51/4.92 % (2196802)Termination phase: SInE selection
% 13.51/4.92 % (2196802)Time elapsed: 0.089 s
% 13.51/4.92 % (2196802)Peak memory usage: 139 MB
% 13.51/4.92 % (2196802)Instructions burned: 130 (million)
% 13.51/4.92 % (2196810)lrs+10_1_sil=8000:sp=occurrence:random_seed=72782705:i=285:sd=3:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/285Mi)
% 13.51/4.92 % (2196811)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1711693067:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/157Mi)
% 13.51/4.92 % (2196812)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3437434157:i=325:sd=1:ss=axioms:sgt=32_2974 on theBenchmark for (2974ds/325Mi)
% 13.51/4.92 % (2196814)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=637982669:s2a=on:i=248:s2at=1.23:gtg=position_2974 on theBenchmark for (2974ds/248Mi)
% 13.51/4.92 % (2196810)Instruction limit reached!
% 20.61/5.90 % (2196810)------------------------------
% 20.61/5.90 % (2196810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196810)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196810)Termination reason: Instruction limit
% 20.61/5.90 % (2196810)Termination phase: Preprocessing 3
% 20.61/5.90 % (2196810)Time elapsed: 0.138 s
% 20.61/5.90 % (2196810)Peak memory usage: 142 MB
% 20.61/5.90 % (2196810)Instructions burned: 287 (million)
% 20.61/5.90 % (2196811)Instruction limit reached!
% 20.61/5.90 % (2196811)------------------------------
% 20.61/5.90 % (2196811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196811)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196811)Termination reason: Instruction limit
% 20.61/5.90 % (2196811)Termination phase: Property scanning
% 20.61/5.90 % (2196811)Time elapsed: 0.071 s
% 20.61/5.90 % (2196811)Peak memory usage: 139 MB
% 20.61/5.90 % (2196811)Instructions burned: 158 (million)
% 20.61/5.90 % (2196818)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1067449169:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2972 on theBenchmark for (2972ds/294Mi)
% 20.61/5.90 % (2196814)Instruction limit reached!
% 20.61/5.90 % (2196814)------------------------------
% 20.61/5.90 % (2196814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196814)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196814)Termination reason: Instruction limit
% 20.61/5.90 % (2196814)Termination phase: Property scanning
% 20.61/5.90 % (2196814)Time elapsed: 0.111 s
% 20.61/5.90 % (2196814)Peak memory usage: 139 MB
% 20.61/5.90 % (2196814)Instructions burned: 250 (million)
% 20.61/5.90 % (2196819)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2412260944:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 20.61/5.90 % (2196812)Refutation not found, incomplete strategy
% 20.61/5.90 % (2196812)------------------------------
% 20.61/5.90 % (2196812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196812)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196812)Termination reason: Refutation not found, incomplete strategy
% 20.61/5.90 % (2196812)Time elapsed: 0.208 s
% 20.61/5.90 % (2196812)Peak memory usage: 145 MB
% 20.61/5.90 % (2196812)Instructions burned: 257 (million)
% 20.61/5.90 % (2196818)Instruction limit reached!
% 20.61/5.90 % (2196818)------------------------------
% 20.61/5.90 % (2196818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196818)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196818)Termination reason: Instruction limit
% 20.61/5.90 % (2196818)Termination phase: SInE selection
% 20.61/5.90 % (2196818)Time elapsed: 0.106 s
% 20.61/5.90 % (2196818)Peak memory usage: 140 MB
% 20.61/5.90 % (2196818)Instructions burned: 295 (million)
% 20.61/5.90 % (2196821)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2566225015:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 20.61/5.90 % (2196823)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=484769183:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 20.61/5.90 % (2196821)Instruction limit reached!
% 20.61/5.90 % (2196821)------------------------------
% 20.61/5.90 % (2196821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196821)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196821)Termination reason: Instruction limit
% 20.61/5.90 % (2196821)Termination phase: SInE selection
% 20.61/5.90 % (2196821)Time elapsed: 0.091 s
% 20.61/5.90 % (2196821)Peak memory usage: 139 MB
% 20.61/5.90 % (2196821)Instructions burned: 113 (million)
% 20.61/5.90 % (2196823)Instruction limit reached!
% 20.61/5.90 % (2196823)------------------------------
% 20.61/5.90 % (2196823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.61/5.90 % (2196823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.61/5.90 % (2196823)CaDiCaL version: 2.1.3
% 20.61/5.90 % (2196823)Termination reason: Instruction limit
% 49.33/9.81 % (2196823)Termination phase: Preprocessing 1
% 49.33/9.81 % (2196823)Time elapsed: 0.057 s
% 49.33/9.81 % (2196823)Peak memory usage: 140 MB
% 49.33/9.81 % (2196823)Instructions burned: 127 (million)
% 49.33/9.81 % (2196827)lrs+10_1_sil=8000:sp=occurrence:random_seed=550588666:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 49.33/9.81 % (2196812)------------------------------
% 49.33/9.81 % (2196812)------------------------------
% 49.33/9.81 % (2196826)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=722211746:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 49.33/9.81 % (2196826)Instruction limit reached!
% 49.33/9.81 % (2196826)------------------------------
% 49.33/9.81 % (2196826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.33/9.81 % (2196826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.33/9.81 % (2196826)CaDiCaL version: 2.1.3
% 49.33/9.81 % (2196826)Termination reason: Instruction limit
% 49.33/9.81 % (2196826)Termination phase: Property scanning
% 49.33/9.81 % (2196826)Time elapsed: 0.052 s
% 49.33/9.81 % (2196826)Peak memory usage: 139 MB
% 49.33/9.81 % (2196826)Instructions burned: 114 (million)
% 49.33/9.81 % (2196829)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1175958107:i=437:sd=1:aac=none:ss=included_2967 on theBenchmark for (2967ds/437Mi)
% 49.33/9.81 % (2196831)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1013508251:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 49.33/9.81 % (2196827)Instruction limit reached!
% 49.33/9.81 % (2196827)------------------------------
% 49.33/9.81 % (2196827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.33/9.81 % (2196827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.33/9.81 % (2196827)CaDiCaL version: 2.1.3
% 49.33/9.81 % (2196827)Termination reason: Instruction limit
% 49.33/9.81 % (2196827)Termination phase: Property scanning
% 49.33/9.81 % (2196827)Time elapsed: 0.353 s
% 49.33/9.81 % (2196827)Peak memory usage: 158 MB
% 49.33/9.81 % (2196827)Instructions burned: 911 (million)
% 49.33/9.81 % (2196829)Refutation not found, incomplete strategy
% 49.33/9.81 % (2196829)------------------------------
% 49.33/9.81 % (2196829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.33/9.81 % (2196829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.33/9.81 % (2196829)CaDiCaL version: 2.1.3
% 49.33/9.81 % (2196829)Termination reason: Refutation not found, incomplete strategy
% 49.33/9.81 % (2196829)Time elapsed: 0.258 s
% 49.33/9.81 % (2196829)Peak memory usage: 145 MB
% 49.33/9.81 % (2196829)Instructions burned: 325 (million)
% 49.33/9.81 % (2196834)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1698942421:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 49.33/9.81 % (2196834)Instruction limit reached!
% 49.33/9.81 % (2196834)------------------------------
% 49.33/9.81 % (2196834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.33/9.81 % (2196834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.33/9.81 % (2196834)CaDiCaL version: 2.1.3
% 49.33/9.81 % (2196834)Termination reason: Instruction limit
% 49.33/9.81 % (2196834)Termination phase: SInE selection
% 49.33/9.81 % (2196834)Time elapsed: 0.058 s
% 49.33/9.81 % (2196834)Peak memory usage: 139 MB
% 49.33/9.81 % (2196834)Instructions burned: 136 (million)
% 49.33/9.81 % (2196836)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1123339915:st=8:i=592:sd=3:ep=RST:ss=axioms_2963 on theBenchmark for (2963ds/592Mi)
% 49.33/9.81 % (2196829)------------------------------
% 49.33/9.81 % (2196829)------------------------------
% 49.33/9.81 % (2196838)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3566524467:st=3:i=13193:sd=3:ss=axioms_2961 on theBenchmark for (2961ds/13193Mi)
% 49.33/9.81 % (2196836)Instruction limit reached!
% 49.33/9.81 % (2196836)------------------------------
% 49.33/9.81 % (2196836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.33/9.81 % (2196836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.33/9.81 % (2196836)CaDiCaL version: 2.1.3
% 49.33/9.81 % (2196836)Termination reason: Instruction limit
% 49.33/9.81 % (2196836)Termination phase: Unused predicate definition removal
% 49.33/9.81 % (2196836)Time elapsed: 0.257 s
% 49.33/9.81 % (2196836)Peak memory usage: 144 MB
% 75.02/13.56 % (2196836)Instructions burned: 592 (million)
% 75.02/13.56 % (2196840)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=247307467:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/125Mi)
% 75.02/13.56 % (2196840)Instruction limit reached!
% 75.02/13.56 % (2196840)------------------------------
% 75.02/13.56 % (2196840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.02/13.56 % (2196840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.02/13.56 % (2196840)CaDiCaL version: 2.1.3
% 75.02/13.56 % (2196840)Termination reason: Instruction limit
% 75.02/13.56 % (2196840)Termination phase: Property scanning
% 75.02/13.56 % (2196840)Time elapsed: 0.032 s
% 75.02/13.56 % (2196840)Peak memory usage: 139 MB
% 75.02/13.56 % (2196840)Instructions burned: 130 (million)
% 75.02/13.56 % (2196842)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3969112690:i=134:gtgl=5:slsql=off:gtg=exists_sym_2958 on theBenchmark for (2958ds/134Mi)
% 75.02/13.56 % (2196842)Instruction limit reached!
% 75.02/13.56 % (2196842)------------------------------
% 75.02/13.56 % (2196842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.02/13.56 % (2196842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.02/13.56 % (2196842)CaDiCaL version: 2.1.3
% 75.02/13.56 % (2196842)Termination reason: Instruction limit
% 75.02/13.56 % (2196842)Termination phase: Property scanning
% 75.02/13.56 % (2196842)Time elapsed: 0.034 s
% 75.02/13.56 % (2196842)Peak memory usage: 139 MB
% 75.02/13.56 % (2196842)Instructions burned: 137 (million)
% 75.02/13.56 % (2196844)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1662631804:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/141Mi)
% 75.02/13.56 % (2196844)Instruction limit reached!
% 75.02/13.56 % (2196844)------------------------------
% 75.02/13.56 % (2196844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.02/13.56 % (2196844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.02/13.56 % (2196844)CaDiCaL version: 2.1.3
% 75.02/13.56 % (2196844)Termination reason: Instruction limit
% 75.02/13.56 % (2196844)Termination phase: SInE selection
% 75.02/13.56 % (2196844)Time elapsed: 0.062 s
% 75.02/13.56 % (2196844)Peak memory usage: 139 MB
% 75.02/13.56 % (2196844)Instructions burned: 143 (million)
% 75.02/13.56 % (2196819)Instruction limit reached!
% 75.02/13.56 % (2196819)------------------------------
% 75.02/13.56 % (2196819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.02/13.56 % (2196819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.02/13.56 % (2196819)CaDiCaL version: 2.1.3
% 75.02/13.56 % (2196819)Termination reason: Instruction limit
% 75.02/13.56 % (2196819)Termination phase: Property scanning
% 75.02/13.56 % (2196819)Time elapsed: 1.616 s
% 75.02/13.56 % (2196819)Peak memory usage: 242 MB
% 75.02/13.56 % (2196819)Instructions burned: 2352 (million)
% 75.02/13.56 % (2196846)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1419665645:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2955 on theBenchmark for (2955ds/431Mi)
% 75.02/13.56 % (2196846)Refutation not found, incomplete strategy
% 75.02/13.56 % (2196846)------------------------------
% 75.02/13.56 % (2196846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.02/13.56 % (2196846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.02/13.56 % (2196846)CaDiCaL version: 2.1.3
% 75.02/13.56 % (2196846)Termination reason: Refutation not found, incomplete strategy
% 75.02/13.56 % (2196846)Time elapsed: 0.123 s
% 75.02/13.56 % (2196846)Peak memory usage: 145 MB
% 75.02/13.56 % (2196846)Instructions burned: 257 (million)
% 75.02/13.56 % (2196847)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=2673313345:i=6060:aac=none:ins=25_2954 on theBenchmark for (2954ds/6060Mi)
% 75.02/13.56 % (2196846)------------------------------
% 75.02/13.56 % (2196846)------------------------------
% 75.02/13.56 % (2196850)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=2110888508:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2951 on theBenchmark for (2951ds/150Mi)
% 75.02/13.56 % (2196850)Instruction limit reached!
% 75.02/13.56 % (2196850)------------------------------
% 110.94/18.56 % (2196850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.94/18.56 % (2196850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.94/18.56 % (2196850)CaDiCaL version: 2.1.3
% 110.94/18.56 % (2196850)Termination reason: Instruction limit
% 110.94/18.56 % (2196850)Termination phase: SInE selection
% 110.94/18.56 % (2196850)Time elapsed: 0.068 s
% 110.94/18.56 % (2196850)Peak memory usage: 139 MB
% 110.94/18.56 % (2196850)Instructions burned: 151 (million)
% 110.94/18.56 % (2196852)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=801138411:i=14155:bd=all_2949 on theBenchmark for (2949ds/14155Mi)
% 110.94/18.56 % (2196831)Instruction limit reached!
% 110.94/18.56 % (2196831)------------------------------
% 110.94/18.56 % (2196831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.94/18.56 % (2196831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.94/18.56 % (2196831)CaDiCaL version: 2.1.3
% 110.94/18.56 % (2196831)Termination reason: Instruction limit
% 110.94/18.56 % (2196831)Termination phase: Saturation
% 110.94/18.56 % (2196831)Time elapsed: 3.227 s
% 110.94/18.56 % (2196831)Peak memory usage: 275 MB
% 110.94/18.56 % (2196831)Instructions burned: 5202 (million)
% 110.94/18.56 % (2196854)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1706836804:i=667:av=off:fsr=off_2933 on theBenchmark for (2933ds/667Mi)
% 110.94/18.56 % (2196854)Instruction limit reached!
% 110.94/18.56 % (2196854)------------------------------
% 110.94/18.56 % (2196854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.94/18.56 % (2196854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.94/18.56 % (2196854)CaDiCaL version: 2.1.3
% 110.94/18.56 % (2196854)Termination reason: Instruction limit
% 110.94/18.56 % (2196854)Termination phase: NewCNF
% 110.94/18.56 % (2196854)Time elapsed: 0.538 s
% 110.94/18.56 % (2196854)Peak memory usage: 190 MB
% 110.94/18.56 % (2196854)Instructions burned: 667 (million)
% 110.94/18.56 % (2196856)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3093699002:s2a=on:i=185:s2at=1.8:fdi=4_2926 on theBenchmark for (2926ds/185Mi)
% 110.94/18.56 % (2196856)Instruction limit reached!
% 110.94/18.56 % (2196856)------------------------------
% 110.94/18.56 % (2196856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.94/18.56 % (2196856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.94/18.56 % (2196856)CaDiCaL version: 2.1.3
% 110.94/18.56 % (2196856)Termination reason: Instruction limit
% 110.94/18.56 % (2196856)Termination phase: SInE selection
% 110.94/18.56 % (2196856)Time elapsed: 0.130 s
% 110.94/18.56 % (2196856)Peak memory usage: 139 MB
% 110.94/18.56 % (2196856)Instructions burned: 185 (million)
% 110.94/18.56 % (2196858)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4238948192:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2923 on theBenchmark for (2923ds/193Mi)
% 110.94/18.56 % (2196858)Instruction limit reached!
% 110.94/18.56 % (2196858)------------------------------
% 110.94/18.56 % (2196858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.94/18.56 % (2196858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.94/18.56 % (2196858)CaDiCaL version: 2.1.3
% 110.94/18.56 % (2196858)Termination reason: Instruction limit
% 110.94/18.56 % (2196858)Termination phase: SInE selection
% 110.94/18.56 % (2196858)Time elapsed: 0.148 s
% 110.94/18.56 % (2196858)Peak memory usage: 139 MB
% 110.94/18.56 % (2196858)Instructions burned: 194 (million)
% 110.94/18.56 % (2196860)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3682067983:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2920 on theBenchmark for (2920ds/4850Mi)
% 110.94/18.56 % (2196847)Instruction limit reached!
% 110.94/18.56 % (2196847)------------------------------
% 110.94/18.56 % (2196847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.94/18.56 % (2196847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.94/18.56 % (2196847)CaDiCaL version: 2.1.3
% 110.94/18.56 % (2196847)Termination reason: Instruction limit
% 110.94/18.56 % (2196847)Termination phase: Function definition elimination
% 110.94/18.56 % (2196847)Time elapsed: 4.074 s
% 110.94/18.56 % (2196847)Peak memory usage: 254 MB
% 110.94/18.56 % (2196847)Instructions burned: 6061 (million)
% 110.94/18.56 % (2196862)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1211050471:i=12111:sd=1:ss=included_2912 on theBenchmark for (2912ds/12111Mi)
% 137.35/22.22 % (2196860)Instruction limit reached!
% 137.35/22.22 % (2196860)------------------------------
% 137.35/22.22 % (2196860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.35/22.22 % (2196860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.35/22.22 % (2196860)CaDiCaL version: 2.1.3
% 137.35/22.22 % (2196860)Termination reason: Instruction limit
% 137.35/22.22 % (2196860)Termination phase: Property scanning
% 137.35/22.22 % (2196860)Time elapsed: 2.662 s
% 137.35/22.22 % (2196860)Peak memory usage: 230 MB
% 137.35/22.22 % (2196860)Instructions burned: 4852 (million)
% 137.35/22.22 % (2196864)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=765169754:i=319:kws=precedence:fsr=off_2892 on theBenchmark for (2892ds/319Mi)
% 137.35/22.22 % (2196852)Instruction limit reached!
% 137.35/22.22 % (2196852)------------------------------
% 137.35/22.22 % (2196852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.35/22.22 % (2196852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.35/22.22 % (2196852)CaDiCaL version: 2.1.3
% 137.35/22.22 % (2196852)Termination reason: Instruction limit
% 137.35/22.22 % (2196852)Termination phase: Saturation
% 137.35/22.22 % (2196852)Time elapsed: 5.946 s
% 137.35/22.22 % (2196852)Peak memory usage: 1377 MB
% 137.35/22.22 % (2196852)Instructions burned: 14159 (million)
% 137.35/22.22 % (2196864)Instruction limit reached!
% 137.35/22.22 % (2196864)------------------------------
% 137.35/22.22 % (2196864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.35/22.22 % (2196864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.35/22.22 % (2196864)CaDiCaL version: 2.1.3
% 137.35/22.22 % (2196864)Termination reason: Instruction limit
% 137.35/22.22 % (2196864)Termination phase: Unused predicate definition removal
% 137.35/22.22 % (2196864)Time elapsed: 0.239 s
% 137.35/22.22 % (2196864)Peak memory usage: 143 MB
% 137.35/22.22 % (2196864)Instructions burned: 319 (million)
% 137.35/22.22 % (2196867)dis-1011_128_sil=32000:random_seed=2039896597:i=3706:ep=RST:av=off_2888 on theBenchmark for (2888ds/3706Mi)
% 137.35/22.22 % (2196866)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1518149793:i=2064:ep=RST_2888 on theBenchmark for (2888ds/2064Mi)
% 137.35/22.22 % (2196838)Instruction limit reached!
% 137.35/22.22 % (2196838)------------------------------
% 137.35/22.22 % (2196838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.35/22.22 % (2196838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.35/22.22 % (2196838)CaDiCaL version: 2.1.3
% 137.35/22.22 % (2196838)Termination reason: Instruction limit
% 137.35/22.22 % (2196838)Termination phase: Saturation
% 137.35/22.22 % (2196838)Time elapsed: 8.103 s
% 137.35/22.22 % (2196838)Peak memory usage: 334 MB
% 137.35/22.22 % (2196838)Instructions burned: 13194 (million)
% 137.35/22.22 % (2196870)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=78234584:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2878 on theBenchmark for (2878ds/757Mi)
% 137.35/22.22 % (2196867)Instruction limit reached!
% 137.35/22.22 % (2196867)------------------------------
% 137.35/22.22 % (2196867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.35/22.22 % (2196867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.35/22.22 % (2196867)CaDiCaL version: 2.1.3
% 137.35/22.22 % (2196867)Termination reason: Instruction limit
% 137.35/22.22 % (2196867)Termination phase: Function definition elimination
% 137.35/22.22 % (2196867)Time elapsed: 1.129 s
% 137.35/22.22 % (2196867)Peak memory usage: 246 MB
% 137.35/22.22 % (2196867)Instructions burned: 3708 (million)
% 137.35/22.22 % (2196872)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=448091877:i=13913:ss=axioms:sgt=8_2876 on theBenchmark for (2876ds/13913Mi)
% 137.35/22.22 % (2196870)Refutation not found, incomplete strategy
% 137.35/22.22 % (2196870)------------------------------
% 137.35/22.22 % (2196870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.35/22.22 % (2196870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.35/22.22 % (2196870)CaDiCaL version: 2.1.3
% 137.35/22.22 % (2196870)Termination reason: Refutation not found, incomplete strategy
% 137.35/22.22 % (2196870)Time elapsed: 0.251 s
% 137.35/22.22 % (2196870)Peak memory usage: 145 MB
% 137.35/22.22 % (2196870)Instructions burned: 308 (million)
% 137.35/22.22 % (2196866)Instruction limit reached!
% 123.64/24.05 % (2196866)------------------------------
% 123.64/24.05 % (2196866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196866)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196866)Termination reason: Instruction limit
% 123.64/24.05 % (2196866)Termination phase: Property scanning
% 123.64/24.05 % (2196866)Time elapsed: 1.433 s
% 123.64/24.05 % (2196866)Peak memory usage: 241 MB
% 123.64/24.05 % (2196866)Instructions burned: 2067 (million)
% 123.64/24.05 % (2196874)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2759395877:i=9925:aac=none_2872 on theBenchmark for (2872ds/9925Mi)
% 123.64/24.05 % (2196870)------------------------------
% 123.64/24.05 % (2196870)------------------------------
% 123.64/24.05 % (2196876)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=422381149:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2871 on theBenchmark for (2871ds/2479Mi)
% 123.64/24.05 % (2196876)Instruction limit reached!
% 123.64/24.05 % (2196876)------------------------------
% 123.64/24.05 % (2196876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196876)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196876)Termination reason: Instruction limit
% 123.64/24.05 % (2196876)Termination phase: Saturation
% 123.64/24.05 % (2196876)Time elapsed: 1.495 s
% 123.64/24.05 % (2196876)Peak memory usage: 155 MB
% 123.64/24.05 % (2196876)Instructions burned: 2480 (million)
% 123.64/24.05 % (2196878)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1703007816:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2854 on theBenchmark for (2854ds/440Mi)
% 123.64/24.05 % (2196878)Instruction limit reached!
% 123.64/24.05 % (2196878)------------------------------
% 123.64/24.05 % (2196878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196878)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196878)Termination reason: Instruction limit
% 123.64/24.05 % (2196878)Termination phase: Property scanning
% 123.64/24.05 % (2196878)Time elapsed: 0.185 s
% 123.64/24.05 % (2196878)Peak memory usage: 139 MB
% 123.64/24.05 % (2196878)Instructions burned: 442 (million)
% 123.64/24.05 % (2196880)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2592636697:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2851 on theBenchmark for (2851ds/11145Mi)
% 123.64/24.05 % (2196862)Instruction limit reached!
% 123.64/24.05 % (2196862)------------------------------
% 123.64/24.05 % (2196862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196862)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196862)Termination reason: Instruction limit
% 123.64/24.05 % (2196862)Termination phase: Saturation
% 123.64/24.05 % (2196862)Time elapsed: 7.442 s
% 123.64/24.05 % (2196862)Peak memory usage: 297 MB
% 123.64/24.05 % (2196862)Instructions burned: 12112 (million)
% 123.64/24.05 % (2196882)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1776345992:cts=off:i=3034:av=off:er=known:fsd=on_2835 on theBenchmark for (2835ds/3034Mi)
% 123.64/24.05 % (2196872)Instruction limit reached!
% 123.64/24.05 % (2196872)------------------------------
% 123.64/24.05 % (2196872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196872)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196872)Termination reason: Instruction limit
% 123.64/24.05 % (2196872)Termination phase: Saturation
% 123.64/24.05 % (2196872)Time elapsed: 4.876 s
% 123.64/24.05 % (2196872)Peak memory usage: 303 MB
% 123.64/24.05 % (2196872)Instructions burned: 13914 (million)
% 123.64/24.05 % (2196884)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=731275102:st=2:s2a=on:i=524:s2at=2:ss=axioms_2826 on theBenchmark for (2826ds/524Mi)
% 123.64/24.05 % (2196884)Instruction limit reached!
% 123.64/24.05 % (2196884)------------------------------
% 123.64/24.05 % (2196884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196884)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196884)Termination reason: Instruction limit
% 123.64/24.05 % (2196884)Termination phase: SInE selection
% 123.64/24.05 % (2196884)Time elapsed: 0.232 s
% 123.64/24.05 % (2196884)Peak memory usage: 141 MB
% 123.64/24.05 % (2196884)Instructions burned: 527 (million)
% 123.64/24.05 % (2196886)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=484665312:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2823 on theBenchmark for (2823ds/1016Mi)
% 123.64/24.05 % (2196886)Refutation not found, incomplete strategy
% 123.64/24.05 % (2196886)------------------------------
% 123.64/24.05 % (2196886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196886)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196886)Termination reason: Refutation not found, incomplete strategy
% 123.64/24.05 % (2196886)Time elapsed: 0.121 s
% 123.64/24.05 % (2196886)Peak memory usage: 145 MB
% 123.64/24.05 % (2196886)Instructions burned: 267 (million)
% 123.64/24.05 % (2196874)Instruction limit reached!
% 123.64/24.05 % (2196874)------------------------------
% 123.64/24.05 % (2196874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196874)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196874)Termination reason: Instruction limit
% 123.64/24.05 % (2196874)Termination phase: Saturation
% 123.64/24.05 % (2196874)Time elapsed: 5.221 s
% 123.64/24.05 % (2196874)Peak memory usage: 506 MB
% 123.64/24.05 % (2196874)Instructions burned: 9925 (million)
% 123.64/24.05 % (2196886)------------------------------
% 123.64/24.05 % (2196886)------------------------------
% 123.64/24.05 % (2196888)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=146389160:i=14123:bd=preordered:ins=4_2819 on theBenchmark for (2819ds/14123Mi)
% 123.64/24.05 % (2196889)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3053157034:i=5781:kws=precedence:bd=all:rawr=on_2818 on theBenchmark for (2818ds/5781Mi)
% 123.64/24.05 % (2196882)Instruction limit reached!
% 123.64/24.05 % (2196882)------------------------------
% 123.64/24.05 % (2196882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196882)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196882)Termination reason: Instruction limit
% 123.64/24.05 % (2196882)Termination phase: Property scanning
% 123.64/24.05 % (2196882)Time elapsed: 1.866 s
% 123.64/24.05 % (2196882)Peak memory usage: 242 MB
% 123.64/24.05 % (2196882)Instructions burned: 3035 (million)
% 123.64/24.05 % (2196892)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1023472457:i=2448:gtgl=5:bd=preordered:gtg=all_2815 on theBenchmark for (2815ds/2448Mi)
% 123.64/24.05 % (2196892)Instruction limit reached!
% 123.64/24.05 % (2196892)------------------------------
% 123.64/24.05 % (2196892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196892)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196892)Termination reason: Instruction limit
% 123.64/24.05 % (2196892)Termination phase: Naming
% 123.64/24.05 % (2196892)Time elapsed: 1.404 s
% 123.64/24.05 % (2196892)Peak memory usage: 186 MB
% 123.64/24.05 % (2196892)Instructions burned: 2449 (million)
% 123.64/24.05 % (2196894)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=392203053:i=3223:kws=precedence:fgj=on:av=off_2799 on theBenchmark for (2799ds/3223Mi)
% 123.64/24.05 % (2196889)Instruction limit reached!
% 123.64/24.05 % (2196889)------------------------------
% 123.64/24.05 % (2196889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196889)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196889)Termination reason: Instruction limit
% 123.64/24.05 % (2196889)Termination phase: Property scanning
% 123.64/24.05 % (2196889)Time elapsed: 2.920 s
% 123.64/24.05 % (2196889)Peak memory usage: 255 MB
% 123.64/24.05 % (2196889)Instructions burned: 5783 (million)
% 123.64/24.05 % (2196896)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=95295049:st=5.6:i=2033:sd=3:ss=axioms_2787 on theBenchmark for (2787ds/2033Mi)
% 123.64/24.05 % (2196894)Instruction limit reached!
% 123.64/24.05 % (2196894)------------------------------
% 123.64/24.05 % (2196894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196894)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196894)Termination reason: Instruction limit
% 123.64/24.05 % (2196894)Termination phase: Property scanning
% 123.64/24.05 % (2196894)Time elapsed: 2.0000 s
% 123.64/24.05 % (2196894)Peak memory usage: 242 MB
% 123.64/24.05 % (2196894)Instructions burned: 3223 (million)
% 123.64/24.05 % (2196898)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=430597425:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2778 on theBenchmark for (2778ds/2055Mi)
% 123.64/24.05 % (2196880)Instruction limit reached!
% 123.64/24.05 % (2196880)------------------------------
% 123.64/24.05 % (2196880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196880)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196880)Termination reason: Instruction limit
% 123.64/24.05 % (2196880)Termination phase: Saturation
% 123.64/24.05 % (2196880)Time elapsed: 7.444 s
% 123.64/24.05 % (2196880)Peak memory usage: 289 MB
% 123.64/24.05 % (2196880)Instructions burned: 11145 (million)
% 123.64/24.05 % (2196900)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2187277039:i=21611:sd=3:ss=axioms_2775 on theBenchmark for (2775ds/21611Mi)
% 123.64/24.05 % (2196896)Instruction limit reached!
% 123.64/24.05 % (2196896)------------------------------
% 123.64/24.05 % (2196896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.64/24.05 % (2196896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.64/24.05 % (2196896)CaDiCaL version: 2.1.3
% 123.64/24.05 % (2196896)Termination reason: Instruction limit
% 123.64/24.05 % (2196896)Termination phase: Property scanning
% 123.64/24.05 % (2196896)Time elapsed: 1.287 s
% 123.64/24.05 % (2196896)Peak memory usage: 179 MB
% 123.64/24.05 % (2196896)Instructions burned: 2034 (million)
% 123.64/24.05 % (2196797)First to succeed.
% 123.64/24.05 % (2196797)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2196791"
% 123.64/24.05 % (2196902)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2016924274:i=4835:sd=13:ss=axioms:sgt=23_2773 on theBenchmark for (2773ds/4835Mi)
% 123.64/24.05 % (2196797)Refutation found. Thanks to Tanya!
% 123.64/24.05 % SZS status Theorem for theBenchmark
% 123.64/24.05 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/24.31 % (2196797)------------------------------
% 0.15/24.31 % (2196797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/24.31 % (2196797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/24.31 % (2196797)CaDiCaL version: 2.1.3
% 0.15/24.31 % (2196797)Termination reason: Refutation
% 0.15/24.31 % (2196797)Time elapsed: 20.192 s
% 0.15/24.31 % (2196797)Peak memory usage: 438 MB
% 0.15/24.31 % (2196797)Instructions burned: 30678 (million)
% 0.15/24.31 % (2196797)------------------------------
% 0.15/24.31 % (2196797)------------------------------
% 0.15/24.31 % (2196791)Success in time 23.17 s
% 0.15/24.31 % Vampire exiting
%------------------------------------------------------------------------------