%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP638+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 : n005.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:12 AM UTC 2026
% Result : Theorem 40.46s 10.85s
% Output : Refutation 56.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 18
% Syntax : Number of formulae : 179 ( 57 unt; 3 def)
% Number of atoms : 612 ( 51 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 713 ( 280 ~; 282 |; 108 &)
% ( 8 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 4 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-4 aty)
% Number of variables : 213 ( 0 sgn 199 !; 14 ?)
% 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(f888,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t178_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_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(f2096,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X2)
& m1_relset_1(X2,X0,X1) )
=> k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k3_funct_2) ).
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(f21806,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> v4_group_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_group_2) ).
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(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(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(f27005,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_group_6) ).
fof(f36500,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4) )
=> m1_group_6(X5,X0,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_latsubgr) ).
fof(f36501,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X3] :
( m1_group_2(X3,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4) )
=> m1_group_6(X5,X0,X6) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f36500]) ).
fof(f36604,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X0,X6)
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4)
& m1_group_2(X6,X0) )
& m1_group_2(X5,X0) )
& m1_group_2(X4,X1) )
& m1_group_2(X3,X1) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f36501]) ).
fof(f36605,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ? [X6] :
( ~ m1_group_6(X5,X0,X6)
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& m1_group_6(X3,X1,X4)
& m1_group_2(X6,X0) )
& m1_group_2(X5,X0) )
& m1_group_2(X4,X1) )
& m1_group_2(X3,X1) )
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f36604]) ).
fof(f36632,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(f36633,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,[],[f36632]) ).
fof(f36634,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(f36635,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,[],[f36634]) ).
fof(f36646,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f21806]) ).
fof(f36647,plain,
! [X0] :
( ! [X1] :
( v4_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f36646]) ).
fof(f36974,plain,
! [X0,X1,X2,X3] :
( k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f2096]) ).
fof(f36975,plain,
! [X0,X1,X2,X3] :
( k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(flattening,[],[f36974]) ).
fof(f36998,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f27005]) ).
fof(f36999,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f36998]) ).
fof(f37094,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f37095,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f37770,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(f37771,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,[],[f37770]) ).
fof(f37786,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(f37787,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,[],[f37786]) ).
fof(f38519,plain,
! [X0,X1,X2] :
( r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f888]) ).
fof(f38520,plain,
! [X0,X1,X2] :
( r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2) ),
inference(flattening,[],[f38519]) ).
fof(f38631,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f39890,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f42071,plain,
( ~ m1_group_6(sK37,sK32,sK38)
& u1_struct_0(sK37) = k3_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK34,u1_struct_0(sK35))
& u1_struct_0(sK38) = k3_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK34,u1_struct_0(sK36))
& m1_group_6(sK35,sK33,sK36)
& m1_group_2(sK38,sK32)
& m1_group_2(sK37,sK32)
& m1_group_2(sK36,sK33)
& m1_group_2(sK35,sK33)
& v1_funct_1(sK34)
& v1_funct_2(sK34,u1_struct_0(sK32),u1_struct_0(sK33))
& v1_group_6(sK34,sK32,sK33)
& m2_relset_1(sK34,u1_struct_0(sK32),u1_struct_0(sK33))
& ~ v3_struct_0(sK33)
& v3_group_1(sK33)
& v4_group_1(sK33)
& l1_group_1(sK33)
& ~ v3_struct_0(sK32)
& v3_group_1(sK32)
& v4_group_1(sK32)
& l1_group_1(sK32) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33,sK34,sK35,sK36,sK37,sK38]),skolemize(X0,sK32),skolemize(X1,sK33),skolemize(X2,sK34),skolemize(X3,sK35),skolemize(X4,sK36),skolemize(X5,sK37),skolemize(X6,sK38)],[f36605]) ).
fof(f42102,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(f42182,plain,
! [X0,X1] :
( ! [X2] :
( ( m1_group_6(X2,X0,X1)
| ~ m1_group_2(X2,X1) )
& ( m1_group_2(X2,X1)
| ~ m1_group_6(X2,X0,X1) ) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(nnf_transformation,[],[f36999]) ).
fof(f42197,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(f43646,plain,
l1_group_1(sK32),
inference(cnf_transformation,[],[f42071]) ).
fof(f43647,plain,
v4_group_1(sK32),
inference(cnf_transformation,[],[f42071]) ).
fof(f43648,plain,
v3_group_1(sK32),
inference(cnf_transformation,[],[f42071]) ).
fof(f43649,plain,
~ v3_struct_0(sK32),
inference(cnf_transformation,[],[f42071]) ).
fof(f43650,plain,
l1_group_1(sK33),
inference(cnf_transformation,[],[f42071]) ).
fof(f43651,plain,
v4_group_1(sK33),
inference(cnf_transformation,[],[f42071]) ).
fof(f43652,plain,
v3_group_1(sK33),
inference(cnf_transformation,[],[f42071]) ).
fof(f43653,plain,
~ v3_struct_0(sK33),
inference(cnf_transformation,[],[f42071]) ).
fof(f43654,plain,
m2_relset_1(sK34,u1_struct_0(sK32),u1_struct_0(sK33)),
inference(cnf_transformation,[],[f42071]) ).
fof(f43657,plain,
v1_funct_1(sK34),
inference(cnf_transformation,[],[f42071]) ).
fof(f43658,plain,
m1_group_2(sK35,sK33),
inference(cnf_transformation,[],[f42071]) ).
fof(f43659,plain,
m1_group_2(sK36,sK33),
inference(cnf_transformation,[],[f42071]) ).
fof(f43660,plain,
m1_group_2(sK37,sK32),
inference(cnf_transformation,[],[f42071]) ).
fof(f43661,plain,
m1_group_2(sK38,sK32),
inference(cnf_transformation,[],[f42071]) ).
fof(f43662,plain,
m1_group_6(sK35,sK33,sK36),
inference(cnf_transformation,[],[f42071]) ).
fof(f43663,plain,
u1_struct_0(sK38) = k3_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK34,u1_struct_0(sK36)),
inference(cnf_transformation,[],[f42071]) ).
fof(f43664,plain,
u1_struct_0(sK37) = k3_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK34,u1_struct_0(sK35)),
inference(cnf_transformation,[],[f42071]) ).
fof(f43665,plain,
~ m1_group_6(sK37,sK32,sK38),
inference(cnf_transformation,[],[f42071]) ).
fof(f43711,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,[],[f36633]) ).
fof(f43712,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| v3_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36633]) ).
fof(f43713,plain,
! [X0,X1] :
( ~ v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36633]) ).
fof(f43714,plain,
! [X2,X0,X1] :
( ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| m1_group_2(X1,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(cnf_transformation,[],[f36635]) ).
fof(f43721,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| v4_group_1(X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36647]) ).
fof(f43738,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f42102]) ).
fof(f44110,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X2)
| k10_relat_1(X2,X3) = k3_funct_2(X0,X1,X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f36975]) ).
fof(f44132,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_6(X2,X0,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| m1_group_2(X2,X1)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f42182]) ).
fof(f44133,plain,
! [X2,X0,X1] :
( m1_group_6(X2,X0,X1)
| ~ m1_group_2(X2,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f42182]) ).
fof(f44216,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f42197]) ).
fof(f44282,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f37094]) ).
fof(f44283,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f37095]) ).
fof(f45214,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,[],[f37771]) ).
fof(f45228,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| u1_struct_0(X1) = k7_group_2(X0,X1)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f37787]) ).
fof(f46224,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k10_relat_1(X2,X0),k10_relat_1(X2,X1)) ),
inference(cnf_transformation,[],[f38520]) ).
fof(f46380,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f38631]) ).
fof(f47691,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f39890]) ).
fof(f53295,plain,
( ~ m1_group_2(sK37,sK38)
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK38,sK32) ),
inference(resolution,[],[f44133,f43665]) ).
fof(f53296,plain,
( ~ m1_group_2(sK37,sK38)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK38,sK32) ),
inference(forward_subsumption_resolution,[],[f53295,f43649]) ).
fof(f53297,plain,
( ~ m1_group_2(sK37,sK38)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK38,sK32) ),
inference(forward_subsumption_resolution,[],[f53296,f43648]) ).
fof(f53298,plain,
( ~ m1_group_2(sK37,sK38)
| ~ l1_group_1(sK32)
| ~ m1_group_2(sK38,sK32) ),
inference(forward_subsumption_resolution,[],[f53297,f43647]) ).
fof(f53299,plain,
( ~ m1_group_2(sK37,sK38)
| ~ m1_group_2(sK38,sK32) ),
inference(forward_subsumption_resolution,[],[f53298,f43646]) ).
fof(f53300,plain,
~ m1_group_2(sK37,sK38),
inference(forward_subsumption_resolution,[],[f53299,f43661]) ).
fof(f53312,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK33,X1)
| v3_struct_0(sK33)
| ~ v3_group_1(sK33)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK33)
| ~ m1_group_2(X1,sK33) ),
inference(resolution,[],[f44132,f43651]) ).
fof(f53313,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK33,X1)
| ~ v3_group_1(sK33)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK33)
| ~ m1_group_2(X1,sK33) ),
inference(forward_subsumption_resolution,[],[f53312,f43653]) ).
fof(f53315,plain,
! [X0,X1] :
( ~ m1_group_6(X0,sK33,X1)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK33)
| ~ m1_group_2(X1,sK33) ),
inference(forward_subsumption_resolution,[],[f53313,f43652]) ).
fof(f53317,plain,
! [X0,X1] :
( ~ m1_group_2(X1,sK33)
| m1_group_2(X0,X1)
| ~ m1_group_6(X0,sK33,X1) ),
inference(forward_subsumption_resolution,[],[f53315,f43650]) ).
fof(f53321,plain,
! [X0] :
( ~ m1_group_6(X0,sK33,sK36)
| m1_group_2(X0,sK36) ),
inference(resolution,[],[f53317,f43659]) ).
fof(f53324,plain,
m1_group_2(sK35,sK36),
inference(resolution,[],[f53321,f43662]) ).
fof(f53336,plain,
m1_relset_1(sK34,u1_struct_0(sK32),u1_struct_0(sK33)),
inference(resolution,[],[f43738,f43654]) ).
fof(f53341,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(sK34,X1,X2)
| k10_relat_1(sK34,X0) = k3_funct_2(X1,X2,sK34,X0) ),
inference(resolution,[],[f44110,f43657]) ).
fof(f53342,plain,
! [X0] : k3_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK34,X0) = k10_relat_1(sK34,X0),
inference(resolution,[],[f53341,f53336]) ).
fof(f53365,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| v3_struct_0(sK32)
| l1_group_1(X0)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f43711,f43648]) ).
fof(f53366,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v3_struct_0(sK33)
| l1_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(resolution,[],[f43711,f43652]) ).
fof(f53367,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| l1_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(forward_subsumption_resolution,[],[f53366,f43653]) ).
fof(f53368,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| l1_group_1(X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f53365,f43649]) ).
fof(f53369,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f53367,f43650]) ).
fof(f53370,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f53368,f43646]) ).
fof(f53371,plain,
l1_group_1(sK36),
inference(resolution,[],[f53369,f43659]) ).
fof(f53372,plain,
l1_group_1(sK35),
inference(resolution,[],[f53369,f43658]) ).
fof(f53373,plain,
l1_group_1(sK37),
inference(resolution,[],[f53370,f43660]) ).
fof(f53374,plain,
l1_group_1(sK38),
inference(resolution,[],[f53370,f43661]) ).
fof(f53411,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f47691,f46380]) ).
fof(f53412,plain,
u1_struct_0(sK32) = k2_pre_topc(sK32),
inference(resolution,[],[f53411,f43646]) ).
fof(f53413,plain,
u1_struct_0(sK33) = k2_pre_topc(sK33),
inference(resolution,[],[f53411,f43650]) ).
fof(f53414,plain,
u1_struct_0(sK35) = k2_pre_topc(sK35),
inference(resolution,[],[f53411,f53372]) ).
fof(f53415,plain,
u1_struct_0(sK36) = k2_pre_topc(sK36),
inference(resolution,[],[f53411,f53371]) ).
fof(f53416,plain,
u1_struct_0(sK37) = k2_pre_topc(sK37),
inference(resolution,[],[f53411,f53373]) ).
fof(f53417,plain,
u1_struct_0(sK38) = k2_pre_topc(sK38),
inference(resolution,[],[f53411,f53374]) ).
fof(f53418,plain,
m2_relset_1(sK34,u1_struct_0(sK32),k2_pre_topc(sK33)),
inference(superposition,[],[f43654,f53413]) ).
fof(f53420,plain,
u1_struct_0(sK38) = k3_funct_2(u1_struct_0(sK32),k2_pre_topc(sK33),sK34,u1_struct_0(sK36)),
inference(superposition,[],[f43663,f53413]) ).
fof(f53421,plain,
u1_struct_0(sK37) = k3_funct_2(u1_struct_0(sK32),k2_pre_topc(sK33),sK34,u1_struct_0(sK35)),
inference(superposition,[],[f43664,f53413]) ).
fof(f53424,plain,
! [X0] : k10_relat_1(sK34,X0) = k3_funct_2(u1_struct_0(sK32),k2_pre_topc(sK33),sK34,X0),
inference(superposition,[],[f53342,f53413]) ).
fof(f53435,plain,
! [X0] : k10_relat_1(sK34,X0) = k3_funct_2(k2_pre_topc(sK32),k2_pre_topc(sK33),sK34,X0),
inference(forward_demodulation,[],[f53424,f53412]) ).
fof(f53438,plain,
u1_struct_0(sK37) = k3_funct_2(u1_struct_0(sK32),k2_pre_topc(sK33),sK34,k2_pre_topc(sK35)),
inference(forward_demodulation,[],[f53421,f53414]) ).
fof(f53439,plain,
u1_struct_0(sK38) = k3_funct_2(u1_struct_0(sK32),k2_pre_topc(sK33),sK34,k2_pre_topc(sK36)),
inference(forward_demodulation,[],[f53420,f53415]) ).
fof(f53441,plain,
m2_relset_1(sK34,k2_pre_topc(sK32),k2_pre_topc(sK33)),
inference(forward_demodulation,[],[f53418,f53412]) ).
fof(f53445,plain,
u1_struct_0(sK37) = k3_funct_2(k2_pre_topc(sK32),k2_pre_topc(sK33),sK34,k2_pre_topc(sK35)),
inference(forward_demodulation,[],[f53438,f53412]) ).
fof(f53446,plain,
u1_struct_0(sK38) = k3_funct_2(k2_pre_topc(sK32),k2_pre_topc(sK33),sK34,k2_pre_topc(sK36)),
inference(forward_demodulation,[],[f53439,f53412]) ).
fof(f53449,plain,
u1_struct_0(sK37) = k10_relat_1(sK34,k2_pre_topc(sK35)),
inference(forward_demodulation,[],[f53445,f53435]) ).
fof(f53450,plain,
u1_struct_0(sK38) = k10_relat_1(sK34,k2_pre_topc(sK36)),
inference(forward_demodulation,[],[f53446,f53435]) ).
fof(f53453,plain,
k2_pre_topc(sK37) = k10_relat_1(sK34,k2_pre_topc(sK35)),
inference(forward_demodulation,[],[f53449,f53416]) ).
fof(f53454,plain,
k2_pre_topc(sK38) = k10_relat_1(sK34,k2_pre_topc(sK36)),
inference(forward_demodulation,[],[f53450,f53417]) ).
fof(f53556,definition,
( spl1101_57
<=> v3_struct_0(sK36) ),
introduced(definition,[new_symbols(definition,[spl1101_57])],[avatar_definition]) ).
fof(f53557,plain,
( v3_struct_0(sK36)
| ~ spl1101_57 ),
inference(avatar_component_clause,[],[f53556]) ).
fof(f53597,plain,
! [X0,X1] :
( ~ m1_group_2(sK37,X1)
| m1_group_2(sK37,X0)
| ~ m1_group_2(X0,X1)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(X0))
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
inference(superposition,[],[f43714,f53416]) ).
fof(f53673,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v3_struct_0(sK33)
| v3_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(resolution,[],[f43712,f43652]) ).
fof(f53674,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v3_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(forward_subsumption_resolution,[],[f53673,f43653]) ).
fof(f53676,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v3_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f53674,f43650]) ).
fof(f53678,plain,
v3_group_1(sK36),
inference(resolution,[],[f53676,f43659]) ).
fof(f53692,plain,
( $false
| ~ spl1101_57 ),
inference(unit_resulting_resolution,[],[f43713,f43650,f43652,f43653,f43659,f53557]) ).
fof(f53694,plain,
~ spl1101_57,
inference(avatar_contradiction_clause,[],[f53692]) ).
fof(f53751,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v3_struct_0(sK33)
| ~ v3_group_1(sK33)
| v4_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(resolution,[],[f43721,f43651]) ).
fof(f53756,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| ~ v3_group_1(sK33)
| v4_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(forward_subsumption_resolution,[],[f53751,f43653]) ).
fof(f53758,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v4_group_1(X0)
| ~ l1_group_1(sK33) ),
inference(forward_subsumption_resolution,[],[f53756,f43652]) ).
fof(f53760,plain,
! [X0] :
( ~ m1_group_2(X0,sK33)
| v4_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f53758,f43650]) ).
fof(f53770,plain,
v4_group_1(sK36),
inference(resolution,[],[f53760,f43659]) ).
fof(f53777,plain,
! [X0] :
( v3_struct_0(sK36)
| ~ v3_group_1(sK36)
| m1_subset_1(k7_group_2(sK36,X0),k1_zfmisc_1(u1_struct_0(sK36)))
| ~ l1_group_1(sK36)
| ~ m1_group_2(X0,sK36) ),
inference(resolution,[],[f53770,f45214]) ).
fof(f53778,plain,
! [X0] :
( ~ m1_group_2(X0,sK36)
| v3_struct_0(sK36)
| ~ v3_group_1(sK36)
| u1_struct_0(X0) = k7_group_2(sK36,X0)
| ~ l1_group_1(sK36) ),
inference(resolution,[],[f53770,f45228]) ).
fof(f53781,plain,
! [X0] :
( ~ m1_group_2(X0,sK36)
| v3_struct_0(sK36)
| u1_struct_0(X0) = k7_group_2(sK36,X0)
| ~ l1_group_1(sK36) ),
inference(forward_subsumption_resolution,[],[f53778,f53678]) ).
fof(f53782,plain,
! [X0] :
( v3_struct_0(sK36)
| m1_subset_1(k7_group_2(sK36,X0),k1_zfmisc_1(u1_struct_0(sK36)))
| ~ l1_group_1(sK36)
| ~ m1_group_2(X0,sK36) ),
inference(forward_subsumption_resolution,[],[f53777,f53678]) ).
fof(f53789,plain,
! [X0] :
( ~ m1_group_2(X0,sK36)
| v3_struct_0(sK36)
| u1_struct_0(X0) = k7_group_2(sK36,X0) ),
inference(forward_subsumption_resolution,[],[f53781,f53371]) ).
fof(f53790,plain,
! [X0] :
( v3_struct_0(sK36)
| m1_subset_1(k7_group_2(sK36,X0),k1_zfmisc_1(u1_struct_0(sK36)))
| ~ m1_group_2(X0,sK36) ),
inference(forward_subsumption_resolution,[],[f53782,f53371]) ).
fof(f53801,definition,
( spl1101_79
<=> ! [X0] :
( ~ m1_group_2(X0,sK36)
| u1_struct_0(X0) = k7_group_2(sK36,X0) ) ),
introduced(definition,[new_symbols(definition,[spl1101_79])],[avatar_definition]) ).
fof(f53802,plain,
( ! [X0] :
( ~ m1_group_2(X0,sK36)
| u1_struct_0(X0) = k7_group_2(sK36,X0) )
| ~ spl1101_79 ),
inference(avatar_component_clause,[],[f53801]) ).
fof(f53803,plain,
( spl1101_57
| spl1101_79 ),
inference(avatar_split_clause,[],[f53789,f53801,f53556]) ).
fof(f53804,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK36,X0),k1_zfmisc_1(k2_pre_topc(sK36)))
| v3_struct_0(sK36)
| ~ m1_group_2(X0,sK36) ),
inference(forward_demodulation,[],[f53790,f53415]) ).
fof(f53826,definition,
( spl1101_85
<=> ! [X0] :
( m1_subset_1(k7_group_2(sK36,X0),k1_zfmisc_1(k2_pre_topc(sK36)))
| ~ m1_group_2(X0,sK36) ) ),
introduced(definition,[new_symbols(definition,[spl1101_85])],[avatar_definition]) ).
fof(f53827,plain,
( ! [X0] :
( m1_subset_1(k7_group_2(sK36,X0),k1_zfmisc_1(k2_pre_topc(sK36)))
| ~ m1_group_2(X0,sK36) )
| ~ spl1101_85 ),
inference(avatar_component_clause,[],[f53826]) ).
fof(f53828,plain,
( spl1101_57
| spl1101_85 ),
inference(avatar_split_clause,[],[f53804,f53826,f53556]) ).
fof(f54002,plain,
( u1_struct_0(sK35) = k7_group_2(sK36,sK35)
| ~ spl1101_79 ),
inference(resolution,[],[f53802,f53324]) ).
fof(f54003,plain,
( k7_group_2(sK36,sK35) = k2_pre_topc(sK35)
| ~ spl1101_79 ),
inference(forward_demodulation,[],[f54002,f53414]) ).
fof(f54005,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| v1_relat_1(X0) ),
inference(resolution,[],[f44283,f44282]) ).
fof(f54007,plain,
v1_relat_1(sK34),
inference(resolution,[],[f54005,f53441]) ).
fof(f54754,plain,
( m1_subset_1(k2_pre_topc(sK35),k1_zfmisc_1(k2_pre_topc(sK36)))
| ~ m1_group_2(sK35,sK36)
| ~ spl1101_79
| ~ spl1101_85 ),
inference(superposition,[],[f53827,f54003]) ).
fof(f54757,plain,
( m1_subset_1(k2_pre_topc(sK35),k1_zfmisc_1(k2_pre_topc(sK36)))
| ~ spl1101_79
| ~ spl1101_85 ),
inference(forward_subsumption_resolution,[],[f54754,f53324]) ).
fof(f54799,plain,
! [X0] :
( m1_group_2(sK37,X0)
| ~ m1_group_2(X0,sK32)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(X0))
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f53597,f43660]) ).
fof(f54802,plain,
! [X0] :
( m1_group_2(sK37,X0)
| ~ m1_group_2(X0,sK32)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(X0))
| ~ v3_group_1(sK32)
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f54799,f43649]) ).
fof(f54804,plain,
! [X0] :
( m1_group_2(sK37,X0)
| ~ m1_group_2(X0,sK32)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(X0))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f54802,f43648]) ).
fof(f54806,plain,
! [X0] :
( m1_group_2(sK37,X0)
| ~ m1_group_2(X0,sK32)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(X0))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f54804,f43647]) ).
fof(f54811,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| m1_group_2(sK37,X0)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f54806,f43646]) ).
fof(f54813,plain,
( m1_group_2(sK37,sK38)
| ~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(sK38)) ),
inference(resolution,[],[f54811,f43661]) ).
fof(f54815,plain,
~ r1_tarski(k2_pre_topc(sK37),u1_struct_0(sK38)),
inference(forward_subsumption_resolution,[],[f54813,f53300]) ).
fof(f54816,plain,
~ r1_tarski(k2_pre_topc(sK37),k2_pre_topc(sK38)),
inference(forward_demodulation,[],[f54815,f53417]) ).
fof(f58146,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| r1_tarski(k10_relat_1(sK34,X0),k10_relat_1(sK34,X1)) ),
inference(resolution,[],[f46224,f54007]) ).
fof(f61397,plain,
( r1_tarski(k2_pre_topc(sK35),k2_pre_topc(sK36))
| ~ spl1101_79
| ~ spl1101_85 ),
inference(resolution,[],[f44216,f54757]) ).
fof(f87461,plain,
( r1_tarski(k10_relat_1(sK34,k2_pre_topc(sK35)),k10_relat_1(sK34,k2_pre_topc(sK36)))
| ~ spl1101_79
| ~ spl1101_85 ),
inference(resolution,[],[f61397,f58146]) ).
fof(f87462,plain,
( r1_tarski(k10_relat_1(sK34,k2_pre_topc(sK35)),k2_pre_topc(sK38))
| ~ spl1101_79
| ~ spl1101_85 ),
inference(forward_demodulation,[],[f87461,f53454]) ).
fof(f87463,plain,
( r1_tarski(k2_pre_topc(sK37),k2_pre_topc(sK38))
| ~ spl1101_79
| ~ spl1101_85 ),
inference(forward_demodulation,[],[f87462,f53453]) ).
fof(f87464,plain,
( $false
| ~ spl1101_79
| ~ spl1101_85 ),
inference(forward_subsumption_resolution,[],[f87463,f54816]) ).
fof(f87465,plain,
( ~ spl1101_79
| ~ spl1101_85 ),
inference(avatar_contradiction_clause,[],[f87464]) ).
cnf(s55,plain,
~ spl1101_57,
inference(sat_conversion,[],[f53694]) ).
cnf(s74,plain,
( spl1101_57
| spl1101_79 ),
inference(sat_conversion,[],[f53803]) ).
cnf(s80,plain,
( spl1101_57
| spl1101_85 ),
inference(sat_conversion,[],[f53828]) ).
cnf(s2742,plain,
( ~ spl1101_79
| ~ spl1101_85 ),
inference(sat_conversion,[],[f87465]) ).
cnf(s4506,plain,
spl1101_85,
inference(rat,[],[s80,s55]) ).
cnf(s4512,plain,
spl1101_79,
inference(rat,[],[s74,s55]) ).
cnf(s4520,plain,
$false,
inference(rat,[],[s2742,s4506,s4512]) ).
fof(f87466,plain,
$false,
inference(avatar_sat_refutation,[],[s4520]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP638+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.13/0.37 % Computer : n005.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sun Sep 27 10:20:53 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 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.89/5.00 % (3783288)Detected formulas, will run a generic FOF schedule.
% 13.89/5.00 % (3783298)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2622078958:s2a=on:i=139:gtg=position_2976 on theBenchmark for (2976ds/139Mi)
% 13.89/5.00 % (3783293)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=1642178351:i=141193_2976 on theBenchmark for (2976ds/141193Mi)
% 13.89/5.00 % (3783294)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=4025069881:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2976 on theBenchmark for (2976ds/134677Mi)
% 13.89/5.00 % (3783298)Instruction limit reached!
% 13.89/5.00 % (3783298)------------------------------
% 13.89/5.00 % (3783298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.89/5.00 % (3783298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.89/5.00 % (3783298)CaDiCaL version: 2.1.3
% 13.89/5.00 % (3783298)Termination reason: Instruction limit
% 13.89/5.00 % (3783298)Termination phase: Property scanning
% 13.89/5.00 % (3783298)Time elapsed: 0.035 s
% 13.89/5.00 % (3783298)Peak memory usage: 139 MB
% 13.89/5.00 % (3783298)Instructions burned: 143 (million)
% 13.89/5.00 % (3783295)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=132471884:i=141695:sd=1:nm=32:gsp=on:ss=included_2976 on theBenchmark for (2976ds/141695Mi)
% 13.89/5.00 % (3783297)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4159849675:i=119:av=off:ss=axioms_2976 on theBenchmark for (2976ds/119Mi)
% 13.89/5.00 % (3783296)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1070468844:i=109:sd=1:ins=1:gsp=on:ss=axioms_2976 on theBenchmark for (2976ds/109Mi)
% 13.89/5.00 % (3783299)dis-21_1_sil=8000:lcm=predicate:random_seed=3114409067: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.89/5.00 % (3783296)Instruction limit reached!
% 13.89/5.00 % (3783296)------------------------------
% 13.89/5.00 % (3783296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.89/5.00 % (3783296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.89/5.00 % (3783296)CaDiCaL version: 2.1.3
% 13.89/5.00 % (3783296)Termination reason: Instruction limit
% 13.89/5.00 % (3783296)Termination phase: SInE selection
% 13.89/5.00 % (3783296)Time elapsed: 0.081 s
% 13.89/5.00 % (3783296)Peak memory usage: 139 MB
% 13.89/5.00 % (3783296)Instructions burned: 109 (million)
% 13.89/5.00 % (3783297)Instruction limit reached!
% 13.89/5.00 % (3783297)------------------------------
% 13.89/5.00 % (3783297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.89/5.00 % (3783297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.89/5.00 % (3783297)CaDiCaL version: 2.1.3
% 13.89/5.00 % (3783297)Termination reason: Instruction limit
% 13.89/5.00 % (3783297)Termination phase: SInE selection
% 13.89/5.00 % (3783297)Time elapsed: 0.087 s
% 13.89/5.00 % (3783297)Peak memory usage: 139 MB
% 13.89/5.00 % (3783297)Instructions burned: 119 (million)
% 13.89/5.00 % (3783299)Instruction limit reached!
% 13.89/5.00 % (3783299)------------------------------
% 13.89/5.00 % (3783299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.89/5.00 % (3783299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.89/5.00 % (3783299)CaDiCaL version: 2.1.3
% 13.89/5.00 % (3783299)Termination reason: Instruction limit
% 13.89/5.00 % (3783299)Termination phase: SInE selection
% 13.89/5.00 % (3783299)Time elapsed: 0.094 s
% 13.89/5.00 % (3783299)Peak memory usage: 139 MB
% 13.89/5.00 % (3783299)Instructions burned: 130 (million)
% 13.89/5.00 % (3783306)lrs+10_1_sil=8000:sp=occurrence:random_seed=2474099966:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 13.89/5.00 % (3783309)lrs+1011_1_sil=32000:sp=occurrence:random_seed=877128727:i=325:sd=1:ss=axioms:sgt=32_2974 on theBenchmark for (2974ds/325Mi)
% 13.89/5.00 % (3783308)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1966225210:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/157Mi)
% 13.89/5.00 % (3783310)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=19390334:s2a=on:i=248:s2at=1.23:gtg=position_2973 on theBenchmark for (2973ds/248Mi)
% 13.89/5.00 % (3783308)Instruction limit reached!
% 22.90/6.09 % (3783308)------------------------------
% 22.90/6.09 % (3783308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783308)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783308)Termination reason: Instruction limit
% 22.90/6.09 % (3783308)Termination phase: Property scanning
% 22.90/6.09 % (3783308)Time elapsed: 0.070 s
% 22.90/6.09 % (3783308)Peak memory usage: 139 MB
% 22.90/6.09 % (3783308)Instructions burned: 159 (million)
% 22.90/6.09 % (3783309)Instruction limit reached!
% 22.90/6.09 % (3783309)------------------------------
% 22.90/6.09 % (3783309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783309)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783309)Termination reason: Instruction limit
% 22.90/6.09 % (3783309)Termination phase: Saturation
% 22.90/6.09 % (3783309)Time elapsed: 0.146 s
% 22.90/6.09 % (3783309)Peak memory usage: 145 MB
% 22.90/6.09 % (3783309)Instructions burned: 325 (million)
% 22.90/6.09 % (3783310)Instruction limit reached!
% 22.90/6.09 % (3783310)------------------------------
% 22.90/6.09 % (3783310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783310)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783310)Termination reason: Instruction limit
% 22.90/6.09 % (3783310)Termination phase: Property scanning
% 22.90/6.09 % (3783310)Time elapsed: 0.111 s
% 22.90/6.09 % (3783310)Peak memory usage: 139 MB
% 22.90/6.09 % (3783310)Instructions burned: 250 (million)
% 22.90/6.09 % (3783306)Instruction limit reached!
% 22.90/6.09 % (3783306)------------------------------
% 22.90/6.09 % (3783306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783306)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783306)Termination reason: Instruction limit
% 22.90/6.09 % (3783306)Termination phase: Naming
% 22.90/6.09 % (3783306)Time elapsed: 0.242 s
% 22.90/6.09 % (3783306)Peak memory usage: 142 MB
% 22.90/6.09 % (3783306)Instructions burned: 286 (million)
% 22.90/6.09 % (3783316)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2904602087:i=2350_2971 on theBenchmark for (2971ds/2350Mi)
% 22.90/6.09 % (3783315)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2581842815:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2971 on theBenchmark for (2971ds/294Mi)
% 22.90/6.09 % (3783317)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4057159383:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 22.90/6.09 % (3783318)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1495175398:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 22.90/6.09 % (3783317)Instruction limit reached!
% 22.90/6.09 % (3783317)------------------------------
% 22.90/6.09 % (3783317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783317)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783317)Termination reason: Instruction limit
% 22.90/6.09 % (3783317)Termination phase: SInE selection
% 22.90/6.09 % (3783317)Time elapsed: 0.088 s
% 22.90/6.09 % (3783317)Peak memory usage: 138 MB
% 22.90/6.09 % (3783317)Instructions burned: 114 (million)
% 22.90/6.09 % (3783315)Instruction limit reached!
% 22.90/6.09 % (3783315)------------------------------
% 22.90/6.09 % (3783315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783315)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783315)Termination reason: Instruction limit
% 22.90/6.09 % (3783315)Termination phase: SInE selection
% 22.90/6.09 % (3783315)Time elapsed: 0.192 s
% 22.90/6.09 % (3783315)Peak memory usage: 140 MB
% 22.90/6.09 % (3783315)Instructions burned: 295 (million)
% 22.90/6.09 % (3783318)Instruction limit reached!
% 22.90/6.09 % (3783318)------------------------------
% 22.90/6.09 % (3783318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.90/6.09 % (3783318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.90/6.09 % (3783318)CaDiCaL version: 2.1.3
% 22.90/6.09 % (3783318)Termination reason: Instruction limit
% 48.87/9.73 % (3783318)Termination phase: Preprocessing 1
% 48.87/9.73 % (3783318)Time elapsed: 0.096 s
% 48.87/9.73 % (3783318)Peak memory usage: 140 MB
% 48.87/9.73 % (3783318)Instructions burned: 127 (million)
% 48.87/9.73 % (3783323)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1850452824:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2968 on theBenchmark for (2968ds/114Mi)
% 48.87/9.73 % (3783324)lrs+10_1_sil=8000:sp=occurrence:random_seed=1160201106:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 48.87/9.73 % (3783323)Instruction limit reached!
% 48.87/9.73 % (3783323)------------------------------
% 48.87/9.73 % (3783323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.87/9.73 % (3783323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.87/9.73 % (3783323)CaDiCaL version: 2.1.3
% 48.87/9.73 % (3783323)Termination reason: Instruction limit
% 48.87/9.73 % (3783323)Termination phase: Property scanning
% 48.87/9.73 % (3783323)Time elapsed: 0.053 s
% 48.87/9.73 % (3783323)Peak memory usage: 139 MB
% 48.87/9.73 % (3783323)Instructions burned: 115 (million)
% 48.87/9.73 % (3783325)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=244740304:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 48.87/9.73 % (3783329)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3906986956:i=5202:ss=axioms:sgt=16_2966 on theBenchmark for (2966ds/5202Mi)
% 48.87/9.73 % (3783325)Instruction limit reached!
% 48.87/9.73 % (3783325)------------------------------
% 48.87/9.73 % (3783325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.87/9.73 % (3783325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.87/9.73 % (3783325)CaDiCaL version: 2.1.3
% 48.87/9.73 % (3783325)Termination reason: Instruction limit
% 48.87/9.73 % (3783325)Termination phase: Saturation
% 48.87/9.73 % (3783325)Time elapsed: 0.323 s
% 48.87/9.73 % (3783325)Peak memory usage: 146 MB
% 48.87/9.73 % (3783325)Instructions burned: 437 (million)
% 48.87/9.73 % (3783331)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1807919510:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2963 on theBenchmark for (2963ds/134Mi)
% 48.87/9.73 % (3783316)Instruction limit reached!
% 48.87/9.73 % (3783316)------------------------------
% 48.87/9.73 % (3783316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.87/9.73 % (3783316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.87/9.73 % (3783316)CaDiCaL version: 2.1.3
% 48.87/9.73 % (3783316)Termination reason: Instruction limit
% 48.87/9.73 % (3783316)Termination phase: Property scanning
% 48.87/9.73 % (3783316)Time elapsed: 0.896 s
% 48.87/9.73 % (3783316)Peak memory usage: 242 MB
% 48.87/9.73 % (3783316)Instructions burned: 2351 (million)
% 48.87/9.73 % (3783324)Instruction limit reached!
% 48.87/9.73 % (3783324)------------------------------
% 48.87/9.73 % (3783324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.87/9.73 % (3783324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.87/9.73 % (3783324)CaDiCaL version: 2.1.3
% 48.87/9.73 % (3783324)Termination reason: Instruction limit
% 48.87/9.73 % (3783324)Termination phase: Property scanning
% 48.87/9.73 % (3783324)Time elapsed: 0.605 s
% 48.87/9.73 % (3783324)Peak memory usage: 158 MB
% 48.87/9.73 % (3783324)Instructions burned: 908 (million)
% 48.87/9.73 % (3783331)Instruction limit reached!
% 48.87/9.73 % (3783331)------------------------------
% 48.87/9.73 % (3783331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.87/9.73 % (3783331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.87/9.73 % (3783331)CaDiCaL version: 2.1.3
% 48.87/9.73 % (3783331)Termination reason: Instruction limit
% 48.87/9.73 % (3783331)Termination phase: SInE selection
% 48.87/9.73 % (3783331)Time elapsed: 0.100 s
% 48.87/9.73 % (3783331)Peak memory usage: 139 MB
% 48.87/9.73 % (3783331)Instructions burned: 135 (million)
% 48.87/9.73 % (3783333)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4258226354:st=8:i=592:sd=3:ep=RST:ss=axioms_2961 on theBenchmark for (2961ds/592Mi)
% 48.87/9.73 % (3783334)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2405457679:st=3:i=13193:sd=3:ss=axioms_2960 on theBenchmark for (2960ds/13193Mi)
% 48.87/9.73 % (3783335)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=1595556243:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/125Mi)
% 40.46/10.85 % (3783335)Instruction limit reached!
% 40.46/10.85 % (3783335)------------------------------
% 40.46/10.85 % (3783335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783335)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783335)Termination reason: Instruction limit
% 40.46/10.85 % (3783335)Termination phase: Property scanning
% 40.46/10.85 % (3783335)Time elapsed: 0.059 s
% 40.46/10.85 % (3783335)Peak memory usage: 139 MB
% 40.46/10.85 % (3783335)Instructions burned: 127 (million)
% 40.46/10.85 % (3783333)Instruction limit reached!
% 40.46/10.85 % (3783333)------------------------------
% 40.46/10.85 % (3783333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783333)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783333)Termination reason: Instruction limit
% 40.46/10.85 % (3783333)Termination phase: Unused predicate definition removal
% 40.46/10.85 % (3783333)Time elapsed: 0.258 s
% 40.46/10.85 % (3783333)Peak memory usage: 144 MB
% 40.46/10.85 % (3783333)Instructions burned: 592 (million)
% 40.46/10.85 % (3783339)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=382497611:i=134:gtgl=5:slsql=off:gtg=exists_sym_2957 on theBenchmark for (2957ds/134Mi)
% 40.46/10.85 % (3783340)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2687359829:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/141Mi)
% 40.46/10.85 % (3783339)Instruction limit reached!
% 40.46/10.85 % (3783339)------------------------------
% 40.46/10.85 % (3783339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783339)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783339)Termination reason: Instruction limit
% 40.46/10.85 % (3783339)Termination phase: Property scanning
% 40.46/10.85 % (3783339)Time elapsed: 0.062 s
% 40.46/10.85 % (3783339)Peak memory usage: 139 MB
% 40.46/10.85 % (3783339)Instructions burned: 136 (million)
% 40.46/10.85 % (3783340)Instruction limit reached!
% 40.46/10.85 % (3783340)------------------------------
% 40.46/10.85 % (3783340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783340)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783340)Termination reason: Instruction limit
% 40.46/10.85 % (3783340)Termination phase: SInE selection
% 40.46/10.85 % (3783340)Time elapsed: 0.061 s
% 40.46/10.85 % (3783340)Peak memory usage: 139 MB
% 40.46/10.85 % (3783340)Instructions burned: 142 (million)
% 40.46/10.85 % (3783344)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=3593108240:i=6060:aac=none:ins=25_2955 on theBenchmark for (2955ds/6060Mi)
% 40.46/10.85 % (3783343)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3368600787:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2955 on theBenchmark for (2955ds/431Mi)
% 40.46/10.85 % (3783343)Instruction limit reached!
% 40.46/10.85 % (3783343)------------------------------
% 40.46/10.85 % (3783343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783343)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783343)Termination reason: Instruction limit
% 40.46/10.85 % (3783343)Termination phase: Saturation
% 40.46/10.85 % (3783343)Time elapsed: 0.322 s
% 40.46/10.85 % (3783343)Peak memory usage: 147 MB
% 40.46/10.85 % (3783343)Instructions burned: 431 (million)
% 40.46/10.85 % (3783347)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=4044496384:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 40.46/10.85 % (3783347)Instruction limit reached!
% 40.46/10.85 % (3783347)------------------------------
% 40.46/10.85 % (3783347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783347)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783347)Termination reason: Instruction limit
% 40.46/10.85 % (3783347)Termination phase: SInE selection
% 40.46/10.85 % (3783347)Time elapsed: 0.120 s
% 40.46/10.85 % (3783347)Peak memory usage: 139 MB
% 40.46/10.85 % (3783347)Instructions burned: 151 (million)
% 40.46/10.85 % (3783349)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4290088246:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 40.46/10.85 % (3783329)Instruction limit reached!
% 40.46/10.85 % (3783329)------------------------------
% 40.46/10.85 % (3783329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783329)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783329)Termination reason: Instruction limit
% 40.46/10.85 % (3783329)Termination phase: Saturation
% 40.46/10.85 % (3783329)Time elapsed: 3.173 s
% 40.46/10.85 % (3783329)Peak memory usage: 273 MB
% 40.46/10.85 % (3783329)Instructions burned: 5204 (million)
% 40.46/10.85 % (3783344)Instruction limit reached!
% 40.46/10.85 % (3783344)------------------------------
% 40.46/10.85 % (3783344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783344)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783344)Termination reason: Instruction limit
% 40.46/10.85 % (3783344)Termination phase: Function definition elimination
% 40.46/10.85 % (3783344)Time elapsed: 2.220 s
% 40.46/10.85 % (3783344)Peak memory usage: 254 MB
% 40.46/10.85 % (3783344)Instructions burned: 6063 (million)
% 40.46/10.85 % (3783351)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3420313534:i=667:av=off:fsr=off_2932 on theBenchmark for (2932ds/667Mi)
% 40.46/10.85 % (3783352)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=2485245281:s2a=on:i=185:s2at=1.8:fdi=4_2931 on theBenchmark for (2931ds/185Mi)
% 40.46/10.85 % (3783352)Instruction limit reached!
% 40.46/10.85 % (3783352)------------------------------
% 40.46/10.85 % (3783352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783352)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783352)Termination reason: Instruction limit
% 40.46/10.85 % (3783352)Termination phase: SInE selection
% 40.46/10.85 % (3783352)Time elapsed: 0.076 s
% 40.46/10.85 % (3783352)Peak memory usage: 139 MB
% 40.46/10.85 % (3783352)Instructions burned: 187 (million)
% 40.46/10.85 % (3783355)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3589233081:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2929 on theBenchmark for (2929ds/193Mi)
% 40.46/10.85 % (3783355)Instruction limit reached!
% 40.46/10.85 % (3783355)------------------------------
% 40.46/10.85 % (3783355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783355)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783355)Termination reason: Instruction limit
% 40.46/10.85 % (3783355)Termination phase: SInE selection
% 40.46/10.85 % (3783355)Time elapsed: 0.086 s
% 40.46/10.85 % (3783355)Peak memory usage: 139 MB
% 40.46/10.85 % (3783355)Instructions burned: 195 (million)
% 40.46/10.85 % (3783357)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1391180646:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2927 on theBenchmark for (2927ds/4850Mi)
% 40.46/10.85 % (3783351)Instruction limit reached!
% 40.46/10.85 % (3783351)------------------------------
% 40.46/10.85 % (3783351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783351)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783351)Termination reason: Instruction limit
% 40.46/10.85 % (3783351)Termination phase: NewCNF
% 40.46/10.85 % (3783351)Time elapsed: 0.551 s
% 40.46/10.85 % (3783351)Peak memory usage: 190 MB
% 40.46/10.85 % (3783351)Instructions burned: 667 (million)
% 40.46/10.85 % (3783359)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3893905826:i=12111:sd=1:ss=included_2925 on theBenchmark for (2925ds/12111Mi)
% 40.46/10.85 % (3783357)Instruction limit reached!
% 40.46/10.85 % (3783357)------------------------------
% 40.46/10.85 % (3783357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783357)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783357)Termination reason: Instruction limit
% 40.46/10.85 % (3783357)Termination phase: Property scanning
% 40.46/10.85 % (3783357)Time elapsed: 1.476 s
% 40.46/10.85 % (3783357)Peak memory usage: 227 MB
% 40.46/10.85 % (3783357)Instructions burned: 4856 (million)
% 40.46/10.85 % (3783361)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2112515856:i=319:kws=precedence:fsr=off_2911 on theBenchmark for (2911ds/319Mi)
% 40.46/10.85 % (3783361)Instruction limit reached!
% 40.46/10.85 % (3783361)------------------------------
% 40.46/10.85 % (3783361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.46/10.85 % (3783361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.46/10.85 % (3783361)CaDiCaL version: 2.1.3
% 40.46/10.85 % (3783361)Termination reason: Instruction limit
% 40.46/10.85 % (3783361)Termination phase: Unused predicate definition removal
% 40.46/10.85 % (3783361)Time elapsed: 0.139 s
% 40.46/10.85 % (3783361)Peak memory usage: 143 MB
% 40.46/10.85 % (3783361)Instructions burned: 319 (million)
% 40.46/10.85 % (3783363)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1954172356:i=2064:ep=RST_2908 on theBenchmark for (2908ds/2064Mi)
% 40.46/10.85 % (3783294)First to succeed.
% 40.46/10.85 % (3783294)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3783288"
% 40.46/10.85 % (3783294)Refutation found. Thanks to Tanya!
% 40.46/10.85 % SZS status Theorem for theBenchmark
% 40.46/10.85 % SZS output start Proof for theBenchmark
% See solution above
% 56.74/11.10 % (3783294)------------------------------
% 56.74/11.10 % (3783294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.74/11.10 % (3783294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.74/11.10 % (3783294)CaDiCaL version: 2.1.3
% 56.74/11.10 % (3783294)Termination reason: Refutation
% 56.74/11.10 % (3783294)Time elapsed: 7.082 s
% 56.74/11.10 % (3783294)Peak memory usage: 292 MB
% 56.74/11.10 % (3783294)Instructions burned: 11063 (million)
% 56.74/11.10 % (3783294)------------------------------
% 56.74/11.10 % (3783294)------------------------------
% 56.74/11.10 % (3783288)Success in time 9.992 s
% 56.74/11.10 % Vampire exiting
%------------------------------------------------------------------------------