%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT294+2 : 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 : n010.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 11:46:36 AM UTC 2026
% Result : Theorem 13.40s 3.84s
% Output : Refutation 17.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 3
% Syntax : Number of formulae : 98 ( 24 unt; 0 def)
% Number of atoms : 744 ( 24 equ)
% Maximal formula atoms : 21 ( 7 avg)
% Number of connectives : 1139 ( 493 ~; 518 |; 100 &)
% ( 3 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 130 ( 118 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1979,axiom,
! [X0,X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ( r6_binop_1(X0,X1,X2)
<=> ( r4_binop_1(X0,X1,X2)
& r5_binop_1(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_binop_1) ).
fof(f2918,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
=> ! [X5] :
( ( v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
=> ( ( X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1) )
=> ( ( r4_binop_1(X0,X2,X3)
=> r4_binop_1(X1,X4,X5) )
& ( r5_binop_1(X0,X2,X3)
=> r5_binop_1(X1,X4,X5) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_filter_2) ).
fof(f2919,conjecture,
! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
=> ! [X5] :
( ( v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
=> ( ( X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1)
& r6_binop_1(X0,X2,X3) )
=> r6_binop_1(X1,X4,X5) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_filter_2) ).
fof(f2920,negated_conjecture,
~ ! [X0] :
( ~ v1_xboole_0(X0)
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
=> ! [X5] :
( ( v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
=> ( ( X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1)
& r6_binop_1(X0,X2,X3) )
=> r6_binop_1(X1,X4,X5) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2919]) ).
fof(f3035,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( ( r4_binop_1(X1,X4,X5)
| ~ r4_binop_1(X0,X2,X3) )
& ( r5_binop_1(X1,X4,X5)
| ~ r5_binop_1(X0,X2,X3) ) )
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f2918]) ).
fof(f3036,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ( ( r4_binop_1(X1,X4,X5)
| ~ r4_binop_1(X0,X2,X3) )
& ( r5_binop_1(X1,X4,X5)
| ~ r5_binop_1(X0,X2,X3) ) )
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f3035]) ).
fof(f3037,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ~ r6_binop_1(X1,X4,X5)
& X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1)
& r6_binop_1(X0,X2,X3)
& v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
& v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
& ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f2920]) ).
fof(f3038,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( ~ r6_binop_1(X1,X4,X5)
& X4 = k1_realset1(X2,X1)
& X5 = k1_realset1(X3,X1)
& r6_binop_1(X0,X2,X3)
& v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1) )
& v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1) )
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0) )
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
& ~ v1_xboole_0(X0) ),
inference(flattening,[],[f3037]) ).
fof(f3294,plain,
! [X0,X1] :
( ! [X2] :
( ( r6_binop_1(X0,X1,X2)
<=> ( r4_binop_1(X0,X1,X2)
& r5_binop_1(X0,X1,X2) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f1979]) ).
fof(f3295,plain,
! [X0,X1] :
( ! [X2] :
( ( r6_binop_1(X0,X1,X2)
<=> ( r4_binop_1(X0,X1,X2)
& r5_binop_1(X0,X1,X2) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f3294]) ).
fof(f4629,plain,
( ~ r6_binop_1(sK4,sK7,sK8)
& sK7 = k1_realset1(sK5,sK4)
& sK8 = k1_realset1(sK6,sK4)
& r6_binop_1(sK3,sK5,sK6)
& v1_funct_1(sK8)
& v1_funct_2(sK8,k2_zfmisc_1(sK4,sK4),sK4)
& m2_relset_1(sK8,k2_zfmisc_1(sK4,sK4),sK4)
& v1_funct_1(sK7)
& v1_funct_2(sK7,k2_zfmisc_1(sK4,sK4),sK4)
& m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
& v1_funct_1(sK6)
& v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
& m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
& v1_funct_1(sK5)
& v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
& m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3)
& ~ v1_xboole_0(sK4)
& m1_subset_1(sK4,k1_zfmisc_1(sK3))
& ~ v1_xboole_0(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7),skolemize(X5,sK8)],[f3038]) ).
fof(f4746,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r6_binop_1(X0,X1,X2)
| ~ r4_binop_1(X0,X1,X2)
| ~ r5_binop_1(X0,X1,X2) )
& ( ( r4_binop_1(X0,X1,X2)
& r5_binop_1(X0,X1,X2) )
| ~ r6_binop_1(X0,X1,X2) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(nnf_transformation,[],[f3295]) ).
fof(f4747,plain,
! [X0,X1] :
( ! [X2] :
( ( ( r6_binop_1(X0,X1,X2)
| ~ r4_binop_1(X0,X1,X2)
| ~ r5_binop_1(X0,X1,X2) )
& ( ( r4_binop_1(X0,X1,X2)
& r5_binop_1(X0,X1,X2) )
| ~ r6_binop_1(X0,X1,X2) ) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f4746]) ).
fof(f5298,plain,
! [X2,X3,X0,X1,X4,X5] :
( r5_binop_1(X1,X4,X5)
| ~ r5_binop_1(X0,X2,X3)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f3036]) ).
fof(f5299,plain,
! [X2,X3,X0,X1,X4,X5] :
( r4_binop_1(X1,X4,X5)
| ~ r4_binop_1(X0,X2,X3)
| k1_realset1(X2,X1) != X4
| k1_realset1(X3,X1) != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f3036]) ).
fof(f5300,plain,
~ v1_xboole_0(sK3),
inference(cnf_transformation,[],[f4629]) ).
fof(f5301,plain,
m1_subset_1(sK4,k1_zfmisc_1(sK3)),
inference(cnf_transformation,[],[f4629]) ).
fof(f5302,plain,
~ v1_xboole_0(sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5303,plain,
m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3),
inference(cnf_transformation,[],[f4629]) ).
fof(f5304,plain,
v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3),
inference(cnf_transformation,[],[f4629]) ).
fof(f5305,plain,
v1_funct_1(sK5),
inference(cnf_transformation,[],[f4629]) ).
fof(f5306,plain,
m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3),
inference(cnf_transformation,[],[f4629]) ).
fof(f5307,plain,
v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3),
inference(cnf_transformation,[],[f4629]) ).
fof(f5308,plain,
v1_funct_1(sK6),
inference(cnf_transformation,[],[f4629]) ).
fof(f5309,plain,
m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5310,plain,
v1_funct_2(sK7,k2_zfmisc_1(sK4,sK4),sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5311,plain,
v1_funct_1(sK7),
inference(cnf_transformation,[],[f4629]) ).
fof(f5312,plain,
m2_relset_1(sK8,k2_zfmisc_1(sK4,sK4),sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5313,plain,
v1_funct_2(sK8,k2_zfmisc_1(sK4,sK4),sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5314,plain,
v1_funct_1(sK8),
inference(cnf_transformation,[],[f4629]) ).
fof(f5315,plain,
r6_binop_1(sK3,sK5,sK6),
inference(cnf_transformation,[],[f4629]) ).
fof(f5316,plain,
sK8 = k1_realset1(sK6,sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5317,plain,
sK7 = k1_realset1(sK5,sK4),
inference(cnf_transformation,[],[f4629]) ).
fof(f5318,plain,
~ r6_binop_1(sK4,sK7,sK8),
inference(cnf_transformation,[],[f4629]) ).
fof(f5686,plain,
! [X2,X0,X1] :
( ~ r6_binop_1(X0,X1,X2)
| r5_binop_1(X0,X1,X2)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f4747]) ).
fof(f5687,plain,
! [X2,X0,X1] :
( ~ r6_binop_1(X0,X1,X2)
| r4_binop_1(X0,X1,X2)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f4747]) ).
fof(f5688,plain,
! [X2,X0,X1] :
( ~ r5_binop_1(X0,X1,X2)
| ~ r4_binop_1(X0,X1,X2)
| r6_binop_1(X0,X1,X2)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f4747]) ).
fof(f8151,plain,
! [X2,X3,X0,X1,X5] :
( r4_binop_1(X1,k1_realset1(X2,X1),X5)
| ~ r4_binop_1(X0,X2,X3)
| k1_realset1(X3,X1) != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f5299]) ).
fof(f8152,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X2)
| ~ r4_binop_1(X0,X2,X3)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| r4_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f8151]) ).
fof(f8153,plain,
! [X2,X3,X0,X1,X5] :
( r5_binop_1(X1,k1_realset1(X2,X1),X5)
| ~ r5_binop_1(X0,X2,X3)
| k1_realset1(X3,X1) != X5
| ~ v1_funct_1(X5)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f5298]) ).
fof(f8154,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X2)
| ~ r5_binop_1(X0,X2,X3)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| r5_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(equality_resolution,[],[f8153]) ).
fof(f8657,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(k1_realset1(sK5,X2))
| ~ v1_funct_1(k1_realset1(X1,X2))
| ~ v1_funct_2(k1_realset1(X1,X2),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(k1_realset1(X1,X2),k2_zfmisc_1(X2,X2),X2)
| ~ r4_binop_1(X0,sK5,X1)
| ~ v1_funct_2(k1_realset1(sK5,X2),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(k1_realset1(sK5,X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| r4_binop_1(X2,k1_realset1(sK5,X2),k1_realset1(X1,X2))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(resolution,[],[f5305,f8152]) ).
fof(f8658,plain,
! [X2,X0,X1] :
( ~ v1_funct_1(k1_realset1(sK5,X2))
| ~ v1_funct_1(k1_realset1(X1,X2))
| ~ v1_funct_2(k1_realset1(X1,X2),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(k1_realset1(X1,X2),k2_zfmisc_1(X2,X2),X2)
| ~ r5_binop_1(X0,sK5,X1)
| ~ v1_funct_2(k1_realset1(sK5,X2),k2_zfmisc_1(X2,X2),X2)
| ~ m2_relset_1(k1_realset1(sK5,X2),k2_zfmisc_1(X2,X2),X2)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| r5_binop_1(X2,k1_realset1(sK5,X2),k1_realset1(X1,X2))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X0,X0),X0)
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(resolution,[],[f5305,f8154]) ).
fof(f8663,plain,
( r4_binop_1(sK3,sK5,sK6)
| ~ v1_funct_1(sK6)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(resolution,[],[f5687,f5315]) ).
fof(f8664,plain,
( r4_binop_1(sK3,sK5,sK6)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8663,f5308]) ).
fof(f8665,plain,
( r4_binop_1(sK3,sK5,sK6)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8664,f5307]) ).
fof(f8666,plain,
( r4_binop_1(sK3,sK5,sK6)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8665,f5306]) ).
fof(f8667,plain,
( r4_binop_1(sK3,sK5,sK6)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8666,f5305]) ).
fof(f8668,plain,
( r4_binop_1(sK3,sK5,sK6)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8667,f5304]) ).
fof(f8669,plain,
r4_binop_1(sK3,sK5,sK6),
inference(forward_subsumption_resolution,[],[f8668,f5303]) ).
fof(f8670,plain,
( r5_binop_1(sK3,sK5,sK6)
| ~ v1_funct_1(sK6)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(resolution,[],[f5686,f5315]) ).
fof(f8671,plain,
( r5_binop_1(sK3,sK5,sK6)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8670,f5308]) ).
fof(f8672,plain,
( r5_binop_1(sK3,sK5,sK6)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8671,f5307]) ).
fof(f8673,plain,
( r5_binop_1(sK3,sK5,sK6)
| ~ v1_funct_1(sK5)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8672,f5306]) ).
fof(f8674,plain,
( r5_binop_1(sK3,sK5,sK6)
| ~ v1_funct_2(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8673,f5305]) ).
fof(f8675,plain,
( r5_binop_1(sK3,sK5,sK6)
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f8674,f5304]) ).
fof(f8676,plain,
r5_binop_1(sK3,sK5,sK6),
inference(forward_subsumption_resolution,[],[f8675,f5303]) ).
fof(f8682,plain,
! [X0,X1] :
( ~ v1_funct_1(sK7)
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(X1,sK5,X0)
| ~ v1_funct_2(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(superposition,[],[f8658,f5317]) ).
fof(f8683,plain,
! [X0,X1] :
( ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(X1,sK5,X0)
| ~ v1_funct_2(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8682,f5311]) ).
fof(f8684,plain,
! [X0,X1] :
( ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(X1,sK5,X0)
| ~ m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8683,f5310]) ).
fof(f8685,plain,
! [X0,X1] :
( ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(X1,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8684,f5309]) ).
fof(f8686,plain,
! [X0,X1] :
( ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(X1,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8685,f5302]) ).
fof(f8687,plain,
! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(sK3,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m1_subset_1(sK4,k1_zfmisc_1(sK3))
| v1_xboole_0(sK3) ),
inference(resolution,[],[f8686,f5304]) ).
fof(f8688,plain,
! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(sK3,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ m1_subset_1(sK4,k1_zfmisc_1(sK3))
| v1_xboole_0(sK3) ),
inference(forward_subsumption_resolution,[],[f8687,f5303]) ).
fof(f8689,plain,
! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r5_binop_1(sK3,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| v1_xboole_0(sK3) ),
inference(forward_subsumption_resolution,[],[f8688,f5301]) ).
fof(f8690,plain,
! [X0] :
( ~ r5_binop_1(sK3,sK5,X0)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4)) ),
inference(forward_subsumption_resolution,[],[f8689,f5300]) ).
fof(f8691,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(sK6)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(resolution,[],[f8690,f8676]) ).
fof(f8692,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8691,f5308]) ).
fof(f8693,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8692,f5307]) ).
fof(f8694,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8693,f5306]) ).
fof(f8695,plain,
( ~ m2_relset_1(sK8,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_demodulation,[],[f8694,f5316]) ).
fof(f8696,plain,
( ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8695,f5312]) ).
fof(f8697,plain,
( ~ v1_funct_2(sK8,k2_zfmisc_1(sK4,sK4),sK4)
| r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_demodulation,[],[f8696,f5316]) ).
fof(f8698,plain,
( r5_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8697,f5313]) ).
fof(f8699,plain,
( r5_binop_1(sK4,sK7,sK8)
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_demodulation,[],[f8698,f5316]) ).
fof(f8700,plain,
( ~ v1_funct_1(sK8)
| r5_binop_1(sK4,sK7,sK8) ),
inference(forward_demodulation,[],[f8699,f5316]) ).
fof(f8701,plain,
r5_binop_1(sK4,sK7,sK8),
inference(forward_subsumption_resolution,[],[f8700,f5314]) ).
fof(f8702,plain,
! [X0,X1] :
( ~ v1_funct_1(sK7)
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(X1,sK5,X0)
| ~ v1_funct_2(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(superposition,[],[f8657,f5317]) ).
fof(f8703,plain,
! [X0,X1] :
( ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(X1,sK5,X0)
| ~ v1_funct_2(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8702,f5311]) ).
fof(f8704,plain,
! [X0,X1] :
( ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(X1,sK5,X0)
| ~ m2_relset_1(sK7,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8703,f5310]) ).
fof(f8705,plain,
! [X0,X1] :
( ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(X1,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| v1_xboole_0(sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8704,f5309]) ).
fof(f8706,plain,
! [X0,X1] :
( ~ v1_funct_2(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(X1,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ m2_relset_1(sK5,k2_zfmisc_1(X1,X1),X1)
| ~ m1_subset_1(sK4,k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(forward_subsumption_resolution,[],[f8705,f5302]) ).
fof(f8707,plain,
! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(sK3,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ m2_relset_1(sK5,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m1_subset_1(sK4,k1_zfmisc_1(sK3))
| v1_xboole_0(sK3) ),
inference(resolution,[],[f8706,f5304]) ).
fof(f8708,plain,
! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(sK3,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| ~ m1_subset_1(sK4,k1_zfmisc_1(sK3))
| v1_xboole_0(sK3) ),
inference(forward_subsumption_resolution,[],[f8707,f5303]) ).
fof(f8709,plain,
! [X0] :
( ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ r4_binop_1(sK3,sK5,X0)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4))
| v1_xboole_0(sK3) ),
inference(forward_subsumption_resolution,[],[f8708,f5301]) ).
fof(f8710,plain,
! [X0] :
( ~ r4_binop_1(sK3,sK5,X0)
| ~ m2_relset_1(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(X0,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(X0,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(X0,sK4))
| ~ v1_funct_1(k1_realset1(X0,sK4)) ),
inference(forward_subsumption_resolution,[],[f8709,f5300]) ).
fof(f8711,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_1(sK6)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(resolution,[],[f8710,f8669]) ).
fof(f8712,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8711,f5308]) ).
fof(f8713,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ m2_relset_1(sK6,k2_zfmisc_1(sK3,sK3),sK3)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8712,f5307]) ).
fof(f8714,plain,
( ~ m2_relset_1(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8713,f5306]) ).
fof(f8715,plain,
( ~ m2_relset_1(sK8,k2_zfmisc_1(sK4,sK4),sK4)
| ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_demodulation,[],[f8714,f5316]) ).
fof(f8716,plain,
( ~ v1_funct_2(k1_realset1(sK6,sK4),k2_zfmisc_1(sK4,sK4),sK4)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8715,f5312]) ).
fof(f8717,plain,
( ~ v1_funct_2(sK8,k2_zfmisc_1(sK4,sK4),sK4)
| r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_demodulation,[],[f8716,f5316]) ).
fof(f8718,plain,
( r4_binop_1(sK4,sK7,k1_realset1(sK6,sK4))
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_subsumption_resolution,[],[f8717,f5313]) ).
fof(f8719,plain,
( r4_binop_1(sK4,sK7,sK8)
| ~ v1_funct_1(k1_realset1(sK6,sK4)) ),
inference(forward_demodulation,[],[f8718,f5316]) ).
fof(f8720,plain,
( ~ v1_funct_1(sK8)
| r4_binop_1(sK4,sK7,sK8) ),
inference(forward_demodulation,[],[f8719,f5316]) ).
fof(f8721,plain,
r4_binop_1(sK4,sK7,sK8),
inference(forward_subsumption_resolution,[],[f8720,f5314]) ).
fof(f8722,plain,
$false,
inference(unit_resulting_resolution,[],[f5688,f5314,f5311,f5318,f8721,f8701,f5309,f5310,f5312,f5313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT294+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 % Computer : n010.cluster.edu
% 0.23/0.48 % Model : x86_64 x86_64
% 0.23/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.48 % Memory : 8046.5625MB
% 0.23/0.48 % OS : Linux 6.8.0-71-generic
% 0.23/0.48 % CPULimit : 300
% 0.23/0.48 % WCLimit : 300
% 0.23/0.48 % DateTime : Sun Sep 27 14:20:32 UTC 2026
% 0.23/0.49 % CPUTime :
% 0.23/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.55 Running first-order theorem proving
% 0.28/0.55 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.40/3.84 % (1009394)Detected formulas, will run a generic FOF schedule.
% 13.40/3.84 % (1009400)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=2068077576:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 13.40/3.84 % (1009399)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=2643158341:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 13.40/3.84 % (1009401)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=3197035583:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 13.40/3.84 % (1009402)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=719453192:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 13.40/3.84 % (1009405)dis-21_1_sil=8000:lcm=predicate:random_seed=1886256168:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 13.40/3.84 % (1009404)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1786197663:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 13.40/3.84 % (1009403)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=471381866:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 13.40/3.84 % (1009402)Instruction limit reached!
% 13.40/3.84 % (1009402)------------------------------
% 13.40/3.84 % (1009402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009402)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009402)Termination reason: Instruction limit
% 13.40/3.84 % (1009402)Termination phase: Saturation
% 13.40/3.84 % (1009402)Time elapsed: 0.103 s
% 13.40/3.84 % (1009402)Peak memory usage: 92 MB
% 13.40/3.84 % (1009402)Instructions burned: 109 (million)
% 13.40/3.84 % (1009403)Instruction limit reached!
% 13.40/3.84 % (1009403)------------------------------
% 13.40/3.84 % (1009403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009403)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009403)Termination reason: Instruction limit
% 13.40/3.84 % (1009403)Termination phase: Saturation
% 13.40/3.84 % (1009403)Time elapsed: 0.123 s
% 13.40/3.84 % (1009403)Peak memory usage: 93 MB
% 13.40/3.84 % (1009403)Instructions burned: 119 (million)
% 13.40/3.84 % (1009405)Instruction limit reached!
% 13.40/3.84 % (1009405)------------------------------
% 13.40/3.84 % (1009405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009405)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009405)Termination reason: Instruction limit
% 13.40/3.84 % (1009405)Termination phase: Function definition elimination
% 13.40/3.84 % (1009405)Time elapsed: 0.129 s
% 13.40/3.84 % (1009405)Peak memory usage: 92 MB
% 13.40/3.84 % (1009405)Instructions burned: 130 (million)
% 13.40/3.84 % (1009404)Instruction limit reached!
% 13.40/3.84 % (1009404)------------------------------
% 13.40/3.84 % (1009404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009404)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009404)Termination reason: Instruction limit
% 13.40/3.84 % (1009404)Termination phase: Property scanning
% 13.40/3.84 % (1009404)Time elapsed: 0.144 s
% 13.40/3.84 % (1009404)Peak memory usage: 94 MB
% 13.40/3.84 % (1009404)Instructions burned: 140 (million)
% 13.40/3.84 % (1009413)lrs+10_1_sil=8000:sp=occurrence:random_seed=2432690619:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 13.40/3.84 % (1009414)lrs+10_1_sil=32000:urr=on:br=off:random_seed=320546316:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 13.40/3.84 % (1009415)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3885525432:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 13.40/3.84 % (1009416)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=4029363858:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 13.40/3.84 % (1009414)Instruction limit reached!
% 13.40/3.84 % (1009414)------------------------------
% 13.40/3.84 % (1009414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009414)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009414)Termination reason: Instruction limit
% 13.40/3.84 % (1009414)Termination phase: Saturation
% 13.40/3.84 % (1009414)Time elapsed: 0.150 s
% 13.40/3.84 % (1009414)Peak memory usage: 93 MB
% 13.40/3.84 % (1009414)Instructions burned: 158 (million)
% 13.40/3.84 % (1009416)Instruction limit reached!
% 13.40/3.84 % (1009416)------------------------------
% 13.40/3.84 % (1009416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009416)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009416)Termination reason: Instruction limit
% 13.40/3.84 % (1009416)Termination phase: Saturation
% 13.40/3.84 % (1009416)Time elapsed: 0.239 s
% 13.40/3.84 % (1009416)Peak memory usage: 97 MB
% 13.40/3.84 % (1009416)Instructions burned: 248 (million)
% 13.40/3.84 % (1009413)Instruction limit reached!
% 13.40/3.84 % (1009413)------------------------------
% 13.40/3.84 % (1009413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009413)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009413)Termination reason: Instruction limit
% 13.40/3.84 % (1009413)Termination phase: Saturation
% 13.40/3.84 % (1009413)Time elapsed: 0.325 s
% 13.40/3.84 % (1009413)Peak memory usage: 96 MB
% 13.40/3.84 % (1009413)Instructions burned: 285 (million)
% 13.40/3.84 % (1009415)Instruction limit reached!
% 13.40/3.84 % (1009415)------------------------------
% 13.40/3.84 % (1009415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009415)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009415)Termination reason: Instruction limit
% 13.40/3.84 % (1009415)Termination phase: Saturation
% 13.40/3.84 % (1009415)Time elapsed: 0.342 s
% 13.40/3.84 % (1009415)Peak memory usage: 94 MB
% 13.40/3.84 % (1009415)Instructions burned: 325 (million)
% 13.40/3.84 % (1009421)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3018681119:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 13.40/3.84 % (1009421)Instruction limit reached!
% 13.40/3.84 % (1009421)------------------------------
% 13.40/3.84 % (1009421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009421)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009421)Termination reason: Instruction limit
% 13.40/3.84 % (1009421)Termination phase: Saturation
% 13.40/3.84 % (1009421)Time elapsed: 0.148 s
% 13.40/3.84 % (1009421)Peak memory usage: 95 MB
% 13.40/3.84 % (1009421)Instructions burned: 295 (million)
% 13.40/3.84 % (1009422)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2109406095:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 13.40/3.84 % (1009423)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2710907248:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 13.40/3.84 % (1009424)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2663870935:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 13.40/3.84 % (1009423)Instruction limit reached!
% 13.40/3.84 % (1009423)------------------------------
% 13.40/3.84 % (1009423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009423)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009423)Termination reason: Instruction limit
% 13.40/3.84 % (1009423)Termination phase: Saturation
% 13.40/3.84 % (1009423)Time elapsed: 0.114 s
% 13.40/3.84 % (1009423)Peak memory usage: 93 MB
% 13.40/3.84 % (1009423)Instructions burned: 113 (million)
% 13.40/3.84 % (1009424)Instruction limit reached!
% 13.40/3.84 % (1009424)------------------------------
% 13.40/3.84 % (1009424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009424)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009424)Termination reason: Instruction limit
% 13.40/3.84 % (1009424)Termination phase: Property scanning
% 13.40/3.84 % (1009424)Time elapsed: 0.131 s
% 13.40/3.84 % (1009424)Peak memory usage: 94 MB
% 13.40/3.84 % (1009424)Instructions burned: 128 (million)
% 13.40/3.84 % (1009426)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3793610955:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 13.40/3.84 % (1009426)Instruction limit reached!
% 13.40/3.84 % (1009426)------------------------------
% 13.40/3.84 % (1009426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.40/3.84 % (1009426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.40/3.84 % (1009426)CaDiCaL version: 2.1.3
% 13.40/3.84 % (1009426)Termination reason: Instruction limit
% 13.40/3.84 % (1009426)Termination phase: Property scanning
% 13.40/3.84 % (1009426)Time elapsed: 0.057 s
% 13.40/3.84 % (1009426)Peak memory usage: 91 MB
% 13.40/3.84 % (1009426)Instructions burned: 115 (million)
% 13.40/3.84 % (1009430)lrs+10_1_sil=8000:sp=occurrence:random_seed=3533898312:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 13.40/3.84 % (1009431)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2876319339:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 13.40/3.84 % (1009400)First to succeed.
% 13.40/3.84 % (1009400)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1009394"
% 13.40/3.84 % (1009433)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1353339364:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 13.40/3.84 % (1009431)Also succeeded, but the first one will report.
% 13.40/3.84 % (1009400)Refutation found. Thanks to Tanya!
% 13.40/3.84 % SZS status Theorem for theBenchmark
% 13.40/3.84 % SZS output start Proof for theBenchmark
% See solution above
% 17.69/4.19 % (1009400)------------------------------
% 17.69/4.19 % (1009400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.69/4.19 % (1009400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.69/4.19 % (1009400)CaDiCaL version: 2.1.3
% 17.69/4.19 % (1009400)Termination reason: Refutation
% 17.69/4.19 % (1009400)Time elapsed: 1.609 s
% 17.69/4.19 % (1009400)Peak memory usage: 163 MB
% 17.69/4.19 % (1009400)Instructions burned: 2023 (million)
% 17.69/4.19 % (1009400)------------------------------
% 17.69/4.19 % (1009400)------------------------------
% 17.69/4.19 % (1009394)Success in time 2.528 s
% 17.69/4.19 % Vampire exiting
%------------------------------------------------------------------------------