%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP640+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 : n007.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:13 AM UTC 2026
% Result : Theorem 30.95s 7.98s
% Output : Refutation 36.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 10
% Syntax : Number of formulae : 100 ( 39 unt; 0 def)
% Number of atoms : 342 ( 64 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 384 ( 142 ~; 132 |; 83 &)
% ( 1 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-4 aty)
% Number of variables : 132 ( 120 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f570,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_subset_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(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(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(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(f22957,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)
=> k8_group_4(X0,X1,X2) = k5_group_4(X0,k4_subset_1(u1_struct_0(X0),k7_group_2(X0,X1),k7_group_2(X0,X2))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_group_4) ).
fof(f36502,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] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X5 = k2_xboole_0(u1_struct_0(X2),u1_struct_0(X3))
=> k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k8_group_4(X0,X2,X3))) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k5_group_4(X0,X5))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_latsubgr) ).
fof(f36503,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] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
=> ! [X5] :
( m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0)))
=> ( X5 = k2_xboole_0(u1_struct_0(X2),u1_struct_0(X3))
=> k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k8_group_4(X0,X2,X3))) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k5_group_4(X0,X5))) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f36502]) ).
fof(f36610,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k8_group_4(X0,X2,X3))) != k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k5_group_4(X0,X5)))
& X5 = k2_xboole_0(u1_struct_0(X2),u1_struct_0(X3))
& m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
& m1_group_2(X3,X0) )
& m1_group_2(X2,X0) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f36503]) ).
fof(f36611,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k8_group_4(X0,X2,X3))) != k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X4,u1_struct_0(k5_group_4(X0,X5)))
& X5 = k2_xboole_0(u1_struct_0(X2),u1_struct_0(X3))
& m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X0))) )
& v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
& m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1)) )
& m1_group_2(X3,X0) )
& m1_group_2(X2,X0) )
& ~ v3_struct_0(X1)
& v3_group_1(X1)
& v4_group_1(X1)
& l1_group_1(X1) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f36610]) ).
fof(f36638,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(f36639,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,[],[f36638]) ).
fof(f36873,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k8_group_4(X0,X1,X2) = k5_group_4(X0,k4_subset_1(u1_struct_0(X0),k7_group_2(X0,X1),k7_group_2(X0,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,[],[f22957]) ).
fof(f36874,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k8_group_4(X0,X1,X2) = k5_group_4(X0,k4_subset_1(u1_struct_0(X0),k7_group_2(X0,X1),k7_group_2(X0,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,[],[f36873]) ).
fof(f36921,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(f36922,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,[],[f36921]) ).
fof(f37678,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(f37679,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,[],[f37678]) ).
fof(f37694,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(f37695,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,[],[f37694]) ).
fof(f37739,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f570]) ).
fof(f37740,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k2_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f37739]) ).
fof(f38539,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f18989]) ).
fof(f39422,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f18256]) ).
fof(f42077,plain,
( k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,u1_struct_0(k8_group_4(sK32,sK34,sK35))) != k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,u1_struct_0(k5_group_4(sK32,sK37)))
& sK37 = k2_xboole_0(u1_struct_0(sK34),u1_struct_0(sK35))
& m1_subset_1(sK37,k1_zfmisc_1(u1_struct_0(sK32)))
& v1_funct_1(sK36)
& v1_funct_2(sK36,u1_struct_0(sK32),u1_struct_0(sK33))
& m2_relset_1(sK36,u1_struct_0(sK32),u1_struct_0(sK33))
& m1_group_2(sK35,sK32)
& m1_group_2(sK34,sK32)
& ~ 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]),skolemize(X0,sK32),skolemize(X1,sK33),skolemize(X2,sK34),skolemize(X3,sK35),skolemize(X4,sK36),skolemize(X5,sK37)],[f36611]) ).
fof(f42108,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(f43654,plain,
l1_group_1(sK32),
inference(cnf_transformation,[],[f42077]) ).
fof(f43655,plain,
v4_group_1(sK32),
inference(cnf_transformation,[],[f42077]) ).
fof(f43656,plain,
v3_group_1(sK32),
inference(cnf_transformation,[],[f42077]) ).
fof(f43657,plain,
~ v3_struct_0(sK32),
inference(cnf_transformation,[],[f42077]) ).
fof(f43662,plain,
m1_group_2(sK34,sK32),
inference(cnf_transformation,[],[f42077]) ).
fof(f43663,plain,
m1_group_2(sK35,sK32),
inference(cnf_transformation,[],[f42077]) ).
fof(f43664,plain,
m2_relset_1(sK36,u1_struct_0(sK32),u1_struct_0(sK33)),
inference(cnf_transformation,[],[f42077]) ).
fof(f43665,plain,
v1_funct_2(sK36,u1_struct_0(sK32),u1_struct_0(sK33)),
inference(cnf_transformation,[],[f42077]) ).
fof(f43666,plain,
v1_funct_1(sK36),
inference(cnf_transformation,[],[f42077]) ).
fof(f43668,plain,
sK37 = k2_xboole_0(u1_struct_0(sK34),u1_struct_0(sK35)),
inference(cnf_transformation,[],[f42077]) ).
fof(f43669,plain,
k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,u1_struct_0(k8_group_4(sK32,sK34,sK35))) != k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,u1_struct_0(k5_group_4(sK32,sK37))),
inference(cnf_transformation,[],[f42077]) ).
fof(f43715,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,[],[f36639]) ).
fof(f43742,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f42108]) ).
fof(f44015,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| k8_group_4(X0,X1,X2) = k5_group_4(X0,k4_subset_1(u1_struct_0(X0),k7_group_2(X0,X1),k7_group_2(X0,X2)))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f36874]) ).
fof(f44050,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,[],[f36922]) ).
fof(f45117,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_subset_1(k7_group_2(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f37679]) ).
fof(f45131,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,[],[f37695]) ).
fof(f45213,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f37740]) ).
fof(f46283,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f38539]) ).
fof(f47273,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f39422]) ).
fof(f53302,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| u1_struct_0(X0) = k7_group_2(sK32,X0)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f45131,f43655]) ).
fof(f53303,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| ~ v3_group_1(sK32)
| u1_struct_0(X0) = k7_group_2(sK32,X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f53302,f43657]) ).
fof(f53305,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| u1_struct_0(X0) = k7_group_2(sK32,X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f53303,f43656]) ).
fof(f53307,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| u1_struct_0(X0) = k7_group_2(sK32,X0) ),
inference(forward_subsumption_resolution,[],[f53305,f43654]) ).
fof(f53316,plain,
u1_struct_0(sK35) = k7_group_2(sK32,sK35),
inference(resolution,[],[f53307,f43663]) ).
fof(f53317,plain,
u1_struct_0(sK34) = k7_group_2(sK32,sK34),
inference(resolution,[],[f53307,f43662]) ).
fof(f53362,plain,
m1_relset_1(sK36,u1_struct_0(sK32),u1_struct_0(sK33)),
inference(resolution,[],[f43742,f43664]) ).
fof(f53363,plain,
! [X0] :
( ~ v1_funct_1(sK36)
| ~ v1_funct_2(sK36,u1_struct_0(sK32),u1_struct_0(sK33))
| k9_relat_1(sK36,X0) = k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,X0) ),
inference(resolution,[],[f53362,f44050]) ).
fof(f53364,plain,
! [X0] :
( ~ v1_funct_2(sK36,u1_struct_0(sK32),u1_struct_0(sK33))
| k9_relat_1(sK36,X0) = k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,X0) ),
inference(forward_subsumption_resolution,[],[f53363,f43666]) ).
fof(f53365,plain,
! [X0] : k9_relat_1(sK36,X0) = k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,X0),
inference(forward_subsumption_resolution,[],[f53364,f43665]) ).
fof(f53366,plain,
k2_funct_2(u1_struct_0(sK32),u1_struct_0(sK33),sK36,u1_struct_0(k5_group_4(sK32,sK37))) != k9_relat_1(sK36,u1_struct_0(k8_group_4(sK32,sK34,sK35))),
inference(superposition,[],[f43669,f53365]) ).
fof(f53367,plain,
k9_relat_1(sK36,u1_struct_0(k8_group_4(sK32,sK34,sK35))) != k9_relat_1(sK36,u1_struct_0(k5_group_4(sK32,sK37))),
inference(forward_demodulation,[],[f53366,f53365]) ).
fof(f53503,plain,
! [X0] :
( ~ l1_group_1(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(resolution,[],[f47273,f46283]) ).
fof(f53505,plain,
u1_struct_0(sK32) = k2_pre_topc(sK32),
inference(resolution,[],[f53503,f43654]) ).
fof(f53659,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK32)
| ~ m1_group_2(X1,sK32)
| v3_struct_0(sK32)
| ~ v3_group_1(sK32)
| k8_group_4(sK32,X1,X0) = k5_group_4(sK32,k4_subset_1(u1_struct_0(sK32),k7_group_2(sK32,X1),k7_group_2(sK32,X0)))
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f44015,f43655]) ).
fof(f53660,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK32)
| ~ m1_group_2(X1,sK32)
| ~ v3_group_1(sK32)
| k8_group_4(sK32,X1,X0) = k5_group_4(sK32,k4_subset_1(u1_struct_0(sK32),k7_group_2(sK32,X1),k7_group_2(sK32,X0)))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f53659,f43657]) ).
fof(f53662,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK32)
| ~ m1_group_2(X1,sK32)
| k8_group_4(sK32,X1,X0) = k5_group_4(sK32,k4_subset_1(u1_struct_0(sK32),k7_group_2(sK32,X1),k7_group_2(sK32,X0)))
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f53660,f43656]) ).
fof(f53664,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK32)
| ~ m1_group_2(X1,sK32)
| k8_group_4(sK32,X1,X0) = k5_group_4(sK32,k4_subset_1(u1_struct_0(sK32),k7_group_2(sK32,X1),k7_group_2(sK32,X0))) ),
inference(forward_subsumption_resolution,[],[f53662,f43654]) ).
fof(f53666,plain,
! [X0,X1] :
( ~ m1_group_2(X1,sK32)
| ~ m1_group_2(X0,sK32)
| k8_group_4(sK32,X1,X0) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),k7_group_2(sK32,X1),k7_group_2(sK32,X0))) ),
inference(forward_demodulation,[],[f53664,f53505]) ).
fof(f53669,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| k8_group_4(sK32,sK34,X0) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),k7_group_2(sK32,sK34),k7_group_2(sK32,X0))) ),
inference(resolution,[],[f53666,f43662]) ).
fof(f53674,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| k8_group_4(sK32,sK34,X0) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),u1_struct_0(sK34),k7_group_2(sK32,X0))) ),
inference(forward_demodulation,[],[f53669,f53317]) ).
fof(f53683,plain,
k8_group_4(sK32,sK34,sK35) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),u1_struct_0(sK34),k7_group_2(sK32,sK35))),
inference(resolution,[],[f53674,f43663]) ).
fof(f53690,plain,
k8_group_4(sK32,sK34,sK35) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),u1_struct_0(sK34),u1_struct_0(sK35))),
inference(forward_demodulation,[],[f53683,f53316]) ).
fof(f53949,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| v3_struct_0(sK32)
| l1_group_1(X0)
| ~ l1_group_1(sK32) ),
inference(resolution,[],[f43715,f43656]) ).
fof(f53950,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| l1_group_1(X0)
| ~ l1_group_1(sK32) ),
inference(forward_subsumption_resolution,[],[f53949,f43657]) ).
fof(f53952,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f53950,f43654]) ).
fof(f53954,plain,
l1_group_1(sK35),
inference(resolution,[],[f53952,f43663]) ).
fof(f53955,plain,
l1_group_1(sK34),
inference(resolution,[],[f53952,f43662]) ).
fof(f53967,plain,
u1_struct_0(sK34) = k2_pre_topc(sK34),
inference(resolution,[],[f53955,f53503]) ).
fof(f53968,plain,
u1_struct_0(sK35) = k2_pre_topc(sK35),
inference(resolution,[],[f53954,f53503]) ).
fof(f53981,plain,
k8_group_4(sK32,sK34,sK35) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),k2_pre_topc(sK34),u1_struct_0(sK35))),
inference(superposition,[],[f53690,f53967]) ).
fof(f53984,plain,
sK37 = k2_xboole_0(k2_pre_topc(sK34),u1_struct_0(sK35)),
inference(superposition,[],[f43668,f53967]) ).
fof(f54011,plain,
sK37 = k2_xboole_0(k2_pre_topc(sK34),k2_pre_topc(sK35)),
inference(forward_demodulation,[],[f53984,f53968]) ).
fof(f54013,plain,
k8_group_4(sK32,sK34,sK35) = k5_group_4(sK32,k4_subset_1(k2_pre_topc(sK32),k2_pre_topc(sK34),k2_pre_topc(sK35))),
inference(forward_demodulation,[],[f53981,f53968]) ).
fof(f56224,plain,
! [X0] :
( v3_struct_0(sK32)
| m1_subset_1(k7_group_2(sK32,X0),k1_zfmisc_1(u1_struct_0(sK32)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(X0,sK32) ),
inference(resolution,[],[f45117,f43656]) ).
fof(f56231,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK32,X0),k1_zfmisc_1(u1_struct_0(sK32)))
| ~ v4_group_1(sK32)
| ~ l1_group_1(sK32)
| ~ m1_group_2(X0,sK32) ),
inference(forward_subsumption_resolution,[],[f56224,f43657]) ).
fof(f56235,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK32,X0),k1_zfmisc_1(u1_struct_0(sK32)))
| ~ l1_group_1(sK32)
| ~ m1_group_2(X0,sK32) ),
inference(forward_subsumption_resolution,[],[f56231,f43655]) ).
fof(f56239,plain,
! [X0] :
( m1_subset_1(k7_group_2(sK32,X0),k1_zfmisc_1(u1_struct_0(sK32)))
| ~ m1_group_2(X0,sK32) ),
inference(forward_subsumption_resolution,[],[f56235,f43654]) ).
fof(f56249,plain,
! [X0] :
( ~ m1_group_2(X0,sK32)
| m1_subset_1(k7_group_2(sK32,X0),k1_zfmisc_1(k2_pre_topc(sK32))) ),
inference(forward_demodulation,[],[f56239,f53505]) ).
fof(f56250,plain,
m1_subset_1(k7_group_2(sK32,sK35),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(resolution,[],[f56249,f43663]) ).
fof(f56251,plain,
m1_subset_1(k7_group_2(sK32,sK34),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(resolution,[],[f56249,f43662]) ).
fof(f56258,plain,
m1_subset_1(u1_struct_0(sK34),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(forward_demodulation,[],[f56251,f53317]) ).
fof(f56259,plain,
m1_subset_1(u1_struct_0(sK35),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(forward_demodulation,[],[f56250,f53316]) ).
fof(f56262,plain,
m1_subset_1(k2_pre_topc(sK34),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(forward_demodulation,[],[f56258,f53967]) ).
fof(f56263,plain,
m1_subset_1(k2_pre_topc(sK35),k1_zfmisc_1(k2_pre_topc(sK32))),
inference(forward_demodulation,[],[f56259,f53968]) ).
fof(f56292,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k2_pre_topc(sK32)))
| k2_xboole_0(X0,k2_pre_topc(sK35)) = k4_subset_1(k2_pre_topc(sK32),X0,k2_pre_topc(sK35)) ),
inference(resolution,[],[f56263,f45213]) ).
fof(f62879,plain,
k2_xboole_0(k2_pre_topc(sK34),k2_pre_topc(sK35)) = k4_subset_1(k2_pre_topc(sK32),k2_pre_topc(sK34),k2_pre_topc(sK35)),
inference(resolution,[],[f56292,f56262]) ).
fof(f62884,plain,
sK37 = k4_subset_1(k2_pre_topc(sK32),k2_pre_topc(sK34),k2_pre_topc(sK35)),
inference(forward_demodulation,[],[f62879,f54011]) ).
fof(f62886,plain,
k8_group_4(sK32,sK34,sK35) = k5_group_4(sK32,sK37),
inference(superposition,[],[f54013,f62884]) ).
fof(f62889,plain,
k9_relat_1(sK36,u1_struct_0(k5_group_4(sK32,sK37))) != k9_relat_1(sK36,u1_struct_0(k5_group_4(sK32,sK37))),
inference(superposition,[],[f53367,f62886]) ).
fof(f62918,plain,
$false,
inference(trivial_inequality_removal,[],[f62889]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP640+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.40 % Computer : n007.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 10:20:47 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.68/5.10 % (1208331)Detected formulas, will run a generic FOF schedule.
% 15.68/5.10 % (1208340)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2611856926:i=119:av=off:ss=axioms_2976 on theBenchmark for (2976ds/119Mi)
% 15.68/5.10 % (1208338)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=2683908603:i=141695:sd=1:nm=32:gsp=on:ss=included_2976 on theBenchmark for (2976ds/141695Mi)
% 15.68/5.10 % (1208337)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=60846178:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2976 on theBenchmark for (2976ds/134677Mi)
% 15.68/5.10 % (1208336)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=3761554346:i=141193_2976 on theBenchmark for (2976ds/141193Mi)
% 15.68/5.10 % (1208341)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=404191248:s2a=on:i=139:gtg=position_2976 on theBenchmark for (2976ds/139Mi)
% 15.68/5.10 % (1208339)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4189678761:i=109:sd=1:ins=1:gsp=on:ss=axioms_2976 on theBenchmark for (2976ds/109Mi)
% 15.68/5.10 % (1208340)Instruction limit reached!
% 15.68/5.10 % (1208340)------------------------------
% 15.68/5.10 % (1208340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.68/5.10 % (1208340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/5.10 % (1208340)CaDiCaL version: 2.1.3
% 15.68/5.10 % (1208340)Termination reason: Instruction limit
% 15.68/5.10 % (1208340)Termination phase: SInE selection
% 15.68/5.10 % (1208340)Time elapsed: 0.055 s
% 15.68/5.10 % (1208340)Peak memory usage: 139 MB
% 15.68/5.10 % (1208340)Instructions burned: 122 (million)
% 15.68/5.10 % (1208342)dis-21_1_sil=8000:lcm=predicate:random_seed=750292730: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)
% 15.68/5.10 % (1208341)Instruction limit reached!
% 15.68/5.10 % (1208341)------------------------------
% 15.68/5.10 % (1208341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.68/5.10 % (1208341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/5.10 % (1208341)CaDiCaL version: 2.1.3
% 15.68/5.10 % (1208341)Termination reason: Instruction limit
% 15.68/5.10 % (1208341)Termination phase: Property scanning
% 15.68/5.10 % (1208341)Time elapsed: 0.064 s
% 15.68/5.10 % (1208341)Peak memory usage: 139 MB
% 15.68/5.10 % (1208341)Instructions burned: 141 (million)
% 15.68/5.10 % (1208339)Instruction limit reached!
% 15.68/5.10 % (1208339)------------------------------
% 15.68/5.10 % (1208339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.68/5.10 % (1208339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/5.10 % (1208339)CaDiCaL version: 2.1.3
% 15.68/5.10 % (1208339)Termination reason: Instruction limit
% 15.68/5.10 % (1208339)Termination phase: SInE selection
% 15.68/5.10 % (1208339)Time elapsed: 0.086 s
% 15.68/5.10 % (1208339)Peak memory usage: 139 MB
% 15.68/5.10 % (1208339)Instructions burned: 110 (million)
% 15.68/5.10 % (1208350)lrs+10_1_sil=8000:sp=occurrence:random_seed=1082608231:i=285:sd=3:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/285Mi)
% 15.68/5.10 % (1208342)Instruction limit reached!
% 15.68/5.10 % (1208342)------------------------------
% 15.68/5.10 % (1208342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.68/5.10 % (1208342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.68/5.10 % (1208342)CaDiCaL version: 2.1.3
% 15.68/5.10 % (1208342)Termination reason: Instruction limit
% 15.68/5.10 % (1208342)Termination phase: SInE selection
% 15.68/5.10 % (1208342)Time elapsed: 0.100 s
% 15.68/5.10 % (1208342)Peak memory usage: 139 MB
% 15.68/5.10 % (1208342)Instructions burned: 129 (million)
% 15.68/5.10 % (1208351)lrs+10_1_sil=32000:urr=on:br=off:random_seed=956762197:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/157Mi)
% 15.68/5.10 % (1208353)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2548496923:i=325:sd=1:ss=axioms:sgt=32_2974 on theBenchmark for (2974ds/325Mi)
% 15.68/5.10 % (1208350)Instruction limit reached!
% 15.68/5.10 % (1208350)------------------------------
% 15.68/5.10 % (1208350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.68/5.10 % (1208350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208350)CaDiCaL version: 2.1.3
% 22.79/6.11 % (1208350)Termination reason: Instruction limit
% 22.79/6.11 % (1208350)Termination phase: Preprocessing 3
% 22.79/6.11 % (1208350)Time elapsed: 0.137 s
% 22.79/6.11 % (1208350)Peak memory usage: 142 MB
% 22.79/6.11 % (1208350)Instructions burned: 285 (million)
% 22.79/6.11 % (1208354)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=1334527852:s2a=on:i=248:s2at=1.23:gtg=position_2973 on theBenchmark for (2973ds/248Mi)
% 22.79/6.11 % (1208351)Instruction limit reached!
% 22.79/6.11 % (1208351)------------------------------
% 22.79/6.11 % (1208351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/6.11 % (1208351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208351)CaDiCaL version: 2.1.3
% 22.79/6.11 % (1208351)Termination reason: Instruction limit
% 22.79/6.11 % (1208351)Termination phase: Property scanning
% 22.79/6.11 % (1208351)Time elapsed: 0.071 s
% 22.79/6.11 % (1208351)Peak memory usage: 139 MB
% 22.79/6.11 % (1208351)Instructions burned: 157 (million)
% 22.79/6.11 % (1208357)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=375103638:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2972 on theBenchmark for (2972ds/294Mi)
% 22.79/6.11 % (1208354)Instruction limit reached!
% 22.79/6.11 % (1208354)------------------------------
% 22.79/6.11 % (1208354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/6.11 % (1208354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208354)CaDiCaL version: 2.1.3
% 22.79/6.11 % (1208354)Termination reason: Instruction limit
% 22.79/6.11 % (1208354)Termination phase: Property scanning
% 22.79/6.11 % (1208354)Time elapsed: 0.110 s
% 22.79/6.11 % (1208354)Peak memory usage: 139 MB
% 22.79/6.11 % (1208354)Instructions burned: 249 (million)
% 22.79/6.11 % (1208359)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2643866373:i=2350_2972 on theBenchmark for (2972ds/2350Mi)
% 22.79/6.11 % (1208357)Instruction limit reached!
% 22.79/6.11 % (1208357)------------------------------
% 22.79/6.11 % (1208357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/6.11 % (1208357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208357)CaDiCaL version: 2.1.3
% 22.79/6.11 % (1208357)Termination reason: Instruction limit
% 22.79/6.11 % (1208357)Termination phase: SInE selection
% 22.79/6.11 % (1208357)Time elapsed: 0.105 s
% 22.79/6.11 % (1208357)Peak memory usage: 140 MB
% 22.79/6.11 % (1208357)Instructions burned: 294 (million)
% 22.79/6.11 % (1208353)Instruction limit reached!
% 22.79/6.11 % (1208353)------------------------------
% 22.79/6.11 % (1208353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/6.11 % (1208353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208353)CaDiCaL version: 2.1.3
% 22.79/6.11 % (1208353)Termination reason: Instruction limit
% 22.79/6.11 % (1208353)Termination phase: Saturation
% 22.79/6.11 % (1208353)Time elapsed: 0.264 s
% 22.79/6.11 % (1208353)Peak memory usage: 145 MB
% 22.79/6.11 % (1208353)Instructions burned: 325 (million)
% 22.79/6.11 % (1208361)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1069800771:cts=off:i=113:fsr=off:ss=included:sgt=4_2971 on theBenchmark for (2971ds/113Mi)
% 22.79/6.11 % (1208363)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3111123708:i=127:av=off:fsr=off:sup=off_2970 on theBenchmark for (2970ds/127Mi)
% 22.79/6.11 % (1208363)Instruction limit reached!
% 22.79/6.11 % (1208363)------------------------------
% 22.79/6.11 % (1208363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/6.11 % (1208363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208363)CaDiCaL version: 2.1.3
% 22.79/6.11 % (1208363)Termination reason: Instruction limit
% 22.79/6.11 % (1208363)Termination phase: Preprocessing 1
% 22.79/6.11 % (1208363)Time elapsed: 0.056 s
% 22.79/6.11 % (1208363)Peak memory usage: 140 MB
% 22.79/6.11 % (1208363)Instructions burned: 128 (million)
% 22.79/6.11 % (1208361)Instruction limit reached!
% 22.79/6.11 % (1208361)------------------------------
% 22.79/6.11 % (1208361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.79/6.11 % (1208361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.79/6.11 % (1208361)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208361)Termination reason: Instruction limit
% 30.95/7.98 % (1208361)Termination phase: SInE selection
% 30.95/7.98 % (1208361)Time elapsed: 0.092 s
% 30.95/7.98 % (1208361)Peak memory usage: 139 MB
% 30.95/7.98 % (1208361)Instructions burned: 114 (million)
% 30.95/7.98 % (1208364)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1828281483:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 30.95/7.98 % (1208367)lrs+10_1_sil=8000:sp=occurrence:random_seed=3107348495:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 30.95/7.98 % (1208364)Instruction limit reached!
% 30.95/7.98 % (1208364)------------------------------
% 30.95/7.98 % (1208364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208364)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208364)Termination reason: Instruction limit
% 30.95/7.98 % (1208364)Termination phase: Property scanning
% 30.95/7.98 % (1208364)Time elapsed: 0.052 s
% 30.95/7.98 % (1208364)Peak memory usage: 139 MB
% 30.95/7.98 % (1208364)Instructions burned: 115 (million)
% 30.95/7.98 % (1208368)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3858789324:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 30.95/7.98 % (1208371)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3834559479:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 30.95/7.98 % (1208367)Instruction limit reached!
% 30.95/7.98 % (1208367)------------------------------
% 30.95/7.98 % (1208367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208367)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208367)Termination reason: Instruction limit
% 30.95/7.98 % (1208367)Termination phase: Property scanning
% 30.95/7.98 % (1208367)Time elapsed: 0.346 s
% 30.95/7.98 % (1208367)Peak memory usage: 158 MB
% 30.95/7.98 % (1208367)Instructions burned: 911 (million)
% 30.95/7.98 % (1208368)Instruction limit reached!
% 30.95/7.98 % (1208368)------------------------------
% 30.95/7.98 % (1208368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208368)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208368)Termination reason: Instruction limit
% 30.95/7.98 % (1208368)Termination phase: Saturation
% 30.95/7.98 % (1208368)Time elapsed: 0.309 s
% 30.95/7.98 % (1208368)Peak memory usage: 146 MB
% 30.95/7.98 % (1208368)Instructions burned: 438 (million)
% 30.95/7.98 % (1208374)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1323140669:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 30.95/7.98 % (1208374)Instruction limit reached!
% 30.95/7.98 % (1208374)------------------------------
% 30.95/7.98 % (1208374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208374)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208374)Termination reason: Instruction limit
% 30.95/7.98 % (1208374)Termination phase: SInE selection
% 30.95/7.98 % (1208374)Time elapsed: 0.057 s
% 30.95/7.98 % (1208374)Peak memory usage: 139 MB
% 30.95/7.98 % (1208374)Instructions burned: 134 (million)
% 30.95/7.98 % (1208375)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2992925839:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 30.95/7.98 % (1208377)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3607490936:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 30.95/7.98 % (1208375)Instruction limit reached!
% 30.95/7.98 % (1208375)------------------------------
% 30.95/7.98 % (1208375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208375)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208375)Termination reason: Instruction limit
% 30.95/7.98 % (1208375)Termination phase: Preprocessing 1
% 30.95/7.98 % (1208375)Time elapsed: 0.423 s
% 30.95/7.98 % (1208375)Peak memory usage: 142 MB
% 30.95/7.98 % (1208375)Instructions burned: 593 (million)
% 30.95/7.98 % (1208380)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=1985934224:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/125Mi)
% 30.95/7.98 % (1208380)Instruction limit reached!
% 30.95/7.98 % (1208380)------------------------------
% 30.95/7.98 % (1208380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208380)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208380)Termination reason: Instruction limit
% 30.95/7.98 % (1208380)Termination phase: Property scanning
% 30.95/7.98 % (1208380)Time elapsed: 0.058 s
% 30.95/7.98 % (1208380)Peak memory usage: 139 MB
% 30.95/7.98 % (1208380)Instructions burned: 127 (million)
% 30.95/7.98 % (1208382)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=55546779:i=134:gtgl=5:slsql=off:gtg=exists_sym_2957 on theBenchmark for (2957ds/134Mi)
% 30.95/7.98 % (1208382)Instruction limit reached!
% 30.95/7.98 % (1208382)------------------------------
% 30.95/7.98 % (1208382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208382)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208382)Termination reason: Instruction limit
% 30.95/7.98 % (1208382)Termination phase: Property scanning
% 30.95/7.98 % (1208382)Time elapsed: 0.061 s
% 30.95/7.98 % (1208382)Peak memory usage: 139 MB
% 30.95/7.98 % (1208382)Instructions burned: 136 (million)
% 30.95/7.98 % (1208359)Instruction limit reached!
% 30.95/7.98 % (1208359)------------------------------
% 30.95/7.98 % (1208359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208359)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208359)Termination reason: Instruction limit
% 30.95/7.98 % (1208359)Termination phase: Property scanning
% 30.95/7.98 % (1208359)Time elapsed: 1.600 s
% 30.95/7.98 % (1208359)Peak memory usage: 242 MB
% 30.95/7.98 % (1208359)Instructions burned: 2353 (million)
% 30.95/7.98 % (1208384)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2500167393:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/141Mi)
% 30.95/7.98 % (1208385)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3682397274:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2954 on theBenchmark for (2954ds/431Mi)
% 30.95/7.98 % (1208384)Instruction limit reached!
% 30.95/7.98 % (1208384)------------------------------
% 30.95/7.98 % (1208384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208384)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208384)Termination reason: Instruction limit
% 30.95/7.98 % (1208384)Termination phase: SInE selection
% 30.95/7.98 % (1208384)Time elapsed: 0.110 s
% 30.95/7.98 % (1208384)Peak memory usage: 139 MB
% 30.95/7.98 % (1208384)Instructions burned: 142 (million)
% 30.95/7.98 % (1208388)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=1332265629:i=6060:aac=none:ins=25_2952 on theBenchmark for (2952ds/6060Mi)
% 30.95/7.98 % (1208385)Instruction limit reached!
% 30.95/7.98 % (1208385)------------------------------
% 30.95/7.98 % (1208385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208385)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208385)Termination reason: Instruction limit
% 30.95/7.98 % (1208385)Termination phase: Saturation
% 30.95/7.98 % (1208385)Time elapsed: 0.320 s
% 30.95/7.98 % (1208385)Peak memory usage: 146 MB
% 30.95/7.98 % (1208385)Instructions burned: 432 (million)
% 30.95/7.98 % (1208390)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=684028933:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 30.95/7.98 % (1208390)Instruction limit reached!
% 30.95/7.98 % (1208390)------------------------------
% 30.95/7.98 % (1208390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208390)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208390)Termination reason: Instruction limit
% 30.95/7.98 % (1208390)Termination phase: SInE selection
% 30.95/7.98 % (1208390)Time elapsed: 0.116 s
% 30.95/7.98 % (1208390)Peak memory usage: 139 MB
% 30.95/7.98 % (1208390)Instructions burned: 150 (million)
% 30.95/7.98 % (1208392)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2049940144:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 30.95/7.98 % (1208371)Instruction limit reached!
% 30.95/7.98 % (1208371)------------------------------
% 30.95/7.98 % (1208371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.95/7.98 % (1208371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.95/7.98 % (1208371)CaDiCaL version: 2.1.3
% 30.95/7.98 % (1208371)Termination reason: Instruction limit
% 30.95/7.98 % (1208371)Termination phase: Saturation
% 30.95/7.98 % (1208371)Time elapsed: 3.299 s
% 30.95/7.98 % (1208371)Peak memory usage: 274 MB
% 30.95/7.98 % (1208371)Instructions burned: 5203 (million)
% 30.95/7.98 % (1208337)First to succeed.
% 30.95/7.98 % (1208337)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1208331"
% 30.95/7.98 % (1208394)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=433805704:i=667:av=off:fsr=off_2933 on theBenchmark for (2933ds/667Mi)
% 30.95/7.98 % (1208337)Refutation found. Thanks to Tanya!
% 30.95/7.98 % SZS status Theorem for theBenchmark
% 30.95/7.98 % SZS output start Proof for theBenchmark
% See solution above
% 36.47/8.09 % (1208337)------------------------------
% 36.47/8.09 % (1208337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.47/8.09 % (1208337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.47/8.09 % (1208337)CaDiCaL version: 2.1.3
% 36.47/8.09 % (1208337)Termination reason: Refutation
% 36.47/8.09 % (1208337)Time elapsed: 4.250 s
% 36.47/8.09 % (1208337)Peak memory usage: 296 MB
% 36.47/8.09 % (1208337)Instructions burned: 6553 (million)
% 36.47/8.09 % (1208337)------------------------------
% 36.47/8.09 % (1208337)------------------------------
% 36.47/8.09 % (1208331)Success in time 7.105 s
% 36.47/8.09 % Vampire exiting
%------------------------------------------------------------------------------