%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : TOP038+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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 02:34:01 PM UTC 2026
% Result : Theorem 101.53s 19.47s
% Output : Refutation 120.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 46
% Syntax : Number of formulae : 240 ( 65 unt; 33 def)
% Number of atoms : 800 ( 77 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1006 ( 446 ~; 455 |; 58 &)
% ( 27 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 25 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-4 aty)
% Number of variables : 151 ( 0 sgn 143 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f568,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) = k4_subset_1(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k4_subset_1) ).
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/sandbox/benchmark/theBenchmark.p',redefinition_k4_subset_1) ).
fof(f862,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t153_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f18318,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f18324,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f18325,axiom,
! [X0,X1,X2,X3] :
( ( l1_struct_0(X0)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f34364,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
=> l1_pre_topc(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_tsp_1) ).
fof(f34366,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_tsp_1) ).
fof(f34374,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0)
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m1_pre_topc(X1,X0) )
=> ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_tsp_2) ).
fof(f34435,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) = k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_tsp_2) ).
fof(f34436,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) = k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34435]) ).
fof(f34567,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) != k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34436]) ).
fof(f34568,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),k4_subset_1(u1_struct_0(X0),X2,X3)) != k4_subset_1(u1_struct_0(X1),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X2),k4_pre_topc(X0,X1,k4_tsp_2(X0,X1),X3))
& m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X1)
& v2_tsp_2(X1,X0)
& m2_tsp_1(X1,X0) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f34567]) ).
fof(f34590,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(f34591,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,[],[f34590]) ).
fof(f34594,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f568]) ).
fof(f34595,plain,
! [X0,X1,X2] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f34594]) ).
fof(f34614,plain,
! [X0] :
( ! [X1] :
( m2_tsp_1(X1,X0)
<=> m1_pre_topc(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34366]) ).
fof(f34616,plain,
! [X0] :
( ! [X1] :
( l1_pre_topc(X1)
| ~ m2_tsp_1(X1,X0) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f34364]) ).
fof(f34670,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f18325]) ).
fof(f34671,plain,
! [X0,X1,X2,X3] :
( k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f34670]) ).
fof(f34672,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f18324]) ).
fof(f34673,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f34672]) ).
fof(f34682,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(ennf_transformation,[],[f34374]) ).
fof(f34683,plain,
! [X0,X1] :
( ( v1_funct_1(k4_tsp_2(X0,X1))
& v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
& v5_pre_topc(k4_tsp_2(X0,X1),X0,X1)
& m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1)) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(flattening,[],[f34682]) ).
fof(f35932,plain,
! [X0,X1,X2] :
( k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ v1_relat_1(X2) ),
inference(ennf_transformation,[],[f862]) ).
fof(f35987,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f18318]) ).
fof(f36345,plain,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1481]) ).
fof(f36346,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f38530,plain,
( k4_pre_topc(sK123,sK124,k4_tsp_2(sK123,sK124),k4_subset_1(u1_struct_0(sK123),sK125,sK126)) != k4_subset_1(u1_struct_0(sK124),k4_pre_topc(sK123,sK124,k4_tsp_2(sK123,sK124),sK125),k4_pre_topc(sK123,sK124,k4_tsp_2(sK123,sK124),sK126))
& m1_subset_1(sK126,k1_zfmisc_1(u1_struct_0(sK123)))
& m1_subset_1(sK125,k1_zfmisc_1(u1_struct_0(sK123)))
& ~ v3_struct_0(sK124)
& v2_tsp_2(sK124,sK123)
& m2_tsp_1(sK124,sK123)
& ~ v3_struct_0(sK123)
& v2_pre_topc(sK123)
& l1_pre_topc(sK123) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123,sK124,sK125,sK126]),skolemize(X0,sK123),skolemize(X1,sK124),skolemize(X2,sK125),skolemize(X3,sK126)],[f34568]) ).
fof(f38568,plain,
! [X0] :
( ! [X1] :
( ( m2_tsp_1(X1,X0)
| ~ m1_pre_topc(X1,X0) )
& ( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0) ) )
| ~ l1_pre_topc(X0) ),
inference(nnf_transformation,[],[f34614]) ).
fof(f39078,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(f40145,plain,
l1_pre_topc(sK123),
inference(cnf_transformation,[],[f38530]) ).
fof(f40146,plain,
v2_pre_topc(sK123),
inference(cnf_transformation,[],[f38530]) ).
fof(f40147,plain,
~ v3_struct_0(sK123),
inference(cnf_transformation,[],[f38530]) ).
fof(f40148,plain,
m2_tsp_1(sK124,sK123),
inference(cnf_transformation,[],[f38530]) ).
fof(f40149,plain,
v2_tsp_2(sK124,sK123),
inference(cnf_transformation,[],[f38530]) ).
fof(f40150,plain,
~ v3_struct_0(sK124),
inference(cnf_transformation,[],[f38530]) ).
fof(f40151,plain,
m1_subset_1(sK125,k1_zfmisc_1(u1_struct_0(sK123))),
inference(cnf_transformation,[],[f38530]) ).
fof(f40152,plain,
m1_subset_1(sK126,k1_zfmisc_1(u1_struct_0(sK123))),
inference(cnf_transformation,[],[f38530]) ).
fof(f40153,plain,
k4_pre_topc(sK123,sK124,k4_tsp_2(sK123,sK124),k4_subset_1(u1_struct_0(sK123),sK125,sK126)) != k4_subset_1(u1_struct_0(sK124),k4_pre_topc(sK123,sK124,k4_tsp_2(sK123,sK124),sK125),k4_pre_topc(sK123,sK124,k4_tsp_2(sK123,sK124),sK126)),
inference(cnf_transformation,[],[f38530]) ).
fof(f40182,plain,
! [X2,X0,X1] :
( k2_xboole_0(X1,X2) = k4_subset_1(X0,X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f34591]) ).
fof(f40184,plain,
! [X2,X0,X1] :
( k4_subset_1(X0,X1,X2) = k4_subset_1(X0,X2,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f34595]) ).
fof(f40219,plain,
! [X0,X1] :
( m1_pre_topc(X1,X0)
| ~ m2_tsp_1(X1,X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f38568]) ).
fof(f40222,plain,
! [X0,X1] :
( ~ m2_tsp_1(X1,X0)
| l1_pre_topc(X1)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f34616]) ).
fof(f40336,plain,
! [X2,X3,X0,X1] :
( k9_relat_1(X2,X3) = k4_pre_topc(X0,X1,X2,X3)
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f34671]) ).
fof(f40337,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_struct_0(X0)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f34673]) ).
fof(f40346,plain,
! [X0,X1] :
( m2_relset_1(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34683]) ).
fof(f40348,plain,
! [X0,X1] :
( v1_funct_2(k4_tsp_2(X0,X1),u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34683]) ).
fof(f40349,plain,
! [X0,X1] :
( v1_funct_1(k4_tsp_2(X0,X1))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0)
| v3_struct_0(X1)
| ~ v2_tsp_2(X1,X0)
| ~ m1_pre_topc(X1,X0) ),
inference(cnf_transformation,[],[f34683]) ).
fof(f42377,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| k9_relat_1(X2,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(cnf_transformation,[],[f35932]) ).
fof(f42419,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f39078]) ).
fof(f42484,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f35987]) ).
fof(f43031,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f36345]) ).
fof(f43032,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f36346]) ).
fof(f47413,definition,
sF961 = k4_tsp_2(sK123,sK124),
introduced(definition,[new_symbols(definition,[sF961])],[function_definition]) ).
fof(f47414,plain,
k4_tsp_2(sK123,sK124) = sF961,
inference(reorient_equations,[],[f47413]) ).
fof(f47415,definition,
sF962 = u1_struct_0(sK123),
introduced(definition,[new_symbols(definition,[sF962])],[function_definition]) ).
fof(f47416,plain,
u1_struct_0(sK123) = sF962,
inference(reorient_equations,[],[f47415]) ).
fof(f47417,definition,
sF963 = k4_subset_1(sF962,sK125,sK126),
introduced(definition,[new_symbols(definition,[sF963])],[function_definition]) ).
fof(f47418,plain,
k4_subset_1(sF962,sK125,sK126) = sF963,
inference(reorient_equations,[],[f47417]) ).
fof(f47419,definition,
sF964 = k4_pre_topc(sK123,sK124,sF961,sF963),
introduced(definition,[new_symbols(definition,[sF964])],[function_definition]) ).
fof(f47420,plain,
k4_pre_topc(sK123,sK124,sF961,sF963) = sF964,
inference(reorient_equations,[],[f47419]) ).
fof(f47421,definition,
sF965 = u1_struct_0(sK124),
introduced(definition,[new_symbols(definition,[sF965])],[function_definition]) ).
fof(f47422,plain,
u1_struct_0(sK124) = sF965,
inference(reorient_equations,[],[f47421]) ).
fof(f47423,definition,
sF966 = k4_pre_topc(sK123,sK124,sF961,sK125),
introduced(definition,[new_symbols(definition,[sF966])],[function_definition]) ).
fof(f47424,plain,
k4_pre_topc(sK123,sK124,sF961,sK125) = sF966,
inference(reorient_equations,[],[f47423]) ).
fof(f47425,definition,
sF967 = k4_pre_topc(sK123,sK124,sF961,sK126),
introduced(definition,[new_symbols(definition,[sF967])],[function_definition]) ).
fof(f47426,plain,
k4_pre_topc(sK123,sK124,sF961,sK126) = sF967,
inference(reorient_equations,[],[f47425]) ).
fof(f47427,definition,
sF968 = k4_subset_1(sF965,sF966,sF967),
introduced(definition,[new_symbols(definition,[sF968])],[function_definition]) ).
fof(f47428,plain,
k4_subset_1(sF965,sF966,sF967) = sF968,
inference(reorient_equations,[],[f47427]) ).
fof(f47429,plain,
sF964 != sF968,
inference(definition_folding,[],[f40153,f47428,f47426,f47414,f47424,f47414,f47422,f47420,f47418,f47416,f47414]) ).
fof(f47430,definition,
sF969 = k1_zfmisc_1(sF962),
introduced(definition,[new_symbols(definition,[sF969])],[function_definition]) ).
fof(f47431,plain,
k1_zfmisc_1(sF962) = sF969,
inference(reorient_equations,[],[f47430]) ).
fof(f47432,plain,
m1_subset_1(sK126,sF969),
inference(definition_folding,[],[f40152,f47431,f47416]) ).
fof(f47433,plain,
m1_subset_1(sK125,sF969),
inference(definition_folding,[],[f40151,f47431,f47416]) ).
fof(f47539,definition,
( spl970_18
<=> m1_subset_1(sF967,k1_zfmisc_1(sF965)) ),
introduced(definition,[new_symbols(definition,[spl970_18])],[avatar_definition]) ).
fof(f47543,definition,
( spl970_19
<=> m1_subset_1(sF966,k1_zfmisc_1(sF965)) ),
introduced(definition,[new_symbols(definition,[spl970_19])],[avatar_definition]) ).
fof(f47560,definition,
( spl970_22
<=> m1_subset_1(sK125,sF969) ),
introduced(definition,[new_symbols(definition,[spl970_22])],[avatar_definition]) ).
fof(f47564,definition,
( spl970_23
<=> m1_subset_1(sK126,sF969) ),
introduced(definition,[new_symbols(definition,[spl970_23])],[avatar_definition]) ).
fof(f47570,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_subset_1(X2,X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2))
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(superposition,[],[f40184,f40182]) ).
fof(f47575,plain,
! [X2,X0,X1] :
( k2_xboole_0(X0,X1) = k4_subset_1(X2,X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ m1_subset_1(X0,k1_zfmisc_1(X2)) ),
inference(duplicate_literal_removal,[],[f47570]) ).
fof(f47579,plain,
spl970_23,
inference(avatar_split_clause,[],[f47432,f47564]) ).
fof(f47582,plain,
spl970_22,
inference(avatar_split_clause,[],[f47433,f47560]) ).
fof(f47584,plain,
( m1_subset_1(sF966,k1_zfmisc_1(u1_struct_0(sK124)))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(superposition,[],[f40337,f47424]) ).
fof(f47585,plain,
( m1_subset_1(sF967,k1_zfmisc_1(u1_struct_0(sK124)))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(superposition,[],[f40337,f47426]) ).
fof(f47590,definition,
( spl970_24
<=> l1_struct_0(sK124) ),
introduced(definition,[new_symbols(definition,[spl970_24])],[avatar_definition]) ).
fof(f47592,plain,
( ~ l1_struct_0(sK124)
| spl970_24 ),
inference(avatar_component_clause,[],[f47590]) ).
fof(f47597,plain,
( m1_subset_1(sF967,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47585,f47422]) ).
fof(f47598,plain,
( m1_subset_1(sF966,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47584,f47422]) ).
fof(f47601,definition,
( spl970_26
<=> l1_struct_0(sK123) ),
introduced(definition,[new_symbols(definition,[spl970_26])],[avatar_definition]) ).
fof(f47603,plain,
( ~ l1_struct_0(sK123)
| spl970_26 ),
inference(avatar_component_clause,[],[f47601]) ).
fof(f47608,plain,
( ~ v1_funct_2(sF961,u1_struct_0(sK123),sF965)
| m1_subset_1(sF967,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47597,f47422]) ).
fof(f47609,plain,
( ~ v1_funct_2(sF961,u1_struct_0(sK123),sF965)
| m1_subset_1(sF966,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47598,f47422]) ).
fof(f47611,plain,
( ~ v1_funct_2(sF961,sF962,sF965)
| m1_subset_1(sF967,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47608,f47416]) ).
fof(f47612,plain,
( ~ v1_funct_2(sF961,sF962,sF965)
| m1_subset_1(sF966,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47609,f47416]) ).
fof(f47614,plain,
( ~ m1_relset_1(sF961,u1_struct_0(sK123),sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| m1_subset_1(sF967,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47611,f47422]) ).
fof(f47615,plain,
( ~ m1_relset_1(sF961,u1_struct_0(sK123),sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| m1_subset_1(sF966,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47612,f47422]) ).
fof(f47617,plain,
( ~ m1_relset_1(sF961,sF962,sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| m1_subset_1(sF967,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47614,f47416]) ).
fof(f47618,plain,
( ~ m1_relset_1(sF961,sF962,sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| m1_subset_1(sF966,k1_zfmisc_1(sF965))
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47615,f47416]) ).
fof(f47621,definition,
( spl970_28
<=> v1_funct_1(sF961) ),
introduced(definition,[new_symbols(definition,[spl970_28])],[avatar_definition]) ).
fof(f47625,definition,
( spl970_29
<=> v1_funct_2(sF961,sF962,sF965) ),
introduced(definition,[new_symbols(definition,[spl970_29])],[avatar_definition]) ).
fof(f47629,definition,
( spl970_30
<=> m1_relset_1(sF961,sF962,sF965) ),
introduced(definition,[new_symbols(definition,[spl970_30])],[avatar_definition]) ).
fof(f47631,plain,
( ~ m1_relset_1(sF961,sF962,sF965)
| spl970_30 ),
inference(avatar_component_clause,[],[f47629]) ).
fof(f47632,plain,
( ~ spl970_28
| ~ spl970_24
| ~ spl970_26
| spl970_18
| ~ spl970_29
| ~ spl970_30 ),
inference(avatar_split_clause,[],[f47617,f47629,f47625,f47539,f47601,f47590,f47621]) ).
fof(f47633,plain,
( ~ spl970_28
| ~ spl970_24
| ~ spl970_26
| spl970_19
| ~ spl970_29
| ~ spl970_30 ),
inference(avatar_split_clause,[],[f47618,f47629,f47625,f47543,f47601,f47590,f47621]) ).
fof(f47639,plain,
( v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(superposition,[],[f40348,f47414]) ).
fof(f47645,definition,
( spl970_32
<=> v3_struct_0(sK123) ),
introduced(definition,[new_symbols(definition,[spl970_32])],[avatar_definition]) ).
fof(f47653,definition,
( spl970_34
<=> v3_struct_0(sK124) ),
introduced(definition,[new_symbols(definition,[spl970_34])],[avatar_definition]) ).
fof(f47661,definition,
( spl970_36
<=> l1_pre_topc(sK123) ),
introduced(definition,[new_symbols(definition,[spl970_36])],[avatar_definition]) ).
fof(f47665,definition,
( spl970_37
<=> v2_pre_topc(sK123) ),
introduced(definition,[new_symbols(definition,[spl970_37])],[avatar_definition]) ).
fof(f47673,definition,
( spl970_39
<=> l1_pre_topc(sK124) ),
introduced(definition,[new_symbols(definition,[spl970_39])],[avatar_definition]) ).
fof(f47684,plain,
( v1_funct_2(sF961,u1_struct_0(sK123),sF965)
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(forward_demodulation,[],[f47639,f47422]) ).
fof(f47685,plain,
( v1_funct_2(sF961,sF962,sF965)
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(forward_demodulation,[],[f47684,f47416]) ).
fof(f47687,definition,
( spl970_42
<=> m1_pre_topc(sK124,sK123) ),
introduced(definition,[new_symbols(definition,[spl970_42])],[avatar_definition]) ).
fof(f47689,plain,
( ~ m1_pre_topc(sK124,sK123)
| spl970_42 ),
inference(avatar_component_clause,[],[f47687]) ).
fof(f47691,definition,
( spl970_43
<=> v2_tsp_2(sK124,sK123) ),
introduced(definition,[new_symbols(definition,[spl970_43])],[avatar_definition]) ).
fof(f47694,plain,
( ~ spl970_42
| ~ spl970_43
| spl970_34
| ~ spl970_36
| ~ spl970_37
| spl970_32
| spl970_29 ),
inference(avatar_split_clause,[],[f47685,f47625,f47645,f47665,f47661,f47653,f47691,f47687]) ).
fof(f47697,plain,
~ spl970_34,
inference(avatar_split_clause,[],[f40150,f47653]) ).
fof(f47700,plain,
~ spl970_32,
inference(avatar_split_clause,[],[f40147,f47645]) ).
fof(f47703,plain,
spl970_36,
inference(avatar_split_clause,[],[f40145,f47661]) ).
fof(f47706,plain,
spl970_37,
inference(avatar_split_clause,[],[f40146,f47665]) ).
fof(f47738,definition,
( spl970_46
<=> m2_tsp_1(sK124,sK123) ),
introduced(definition,[new_symbols(definition,[spl970_46])],[avatar_definition]) ).
fof(f47739,plain,
( m2_tsp_1(sK124,sK123)
| ~ spl970_46 ),
inference(avatar_component_clause,[],[f47738]) ).
fof(f47747,plain,
spl970_43,
inference(avatar_split_clause,[],[f40149,f47691]) ).
fof(f47750,plain,
spl970_46,
inference(avatar_split_clause,[],[f40148,f47738]) ).
fof(f47752,plain,
( m2_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(superposition,[],[f40346,f47414]) ).
fof(f47770,plain,
( sF966 = k9_relat_1(sF961,sK125)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(superposition,[],[f40336,f47424]) ).
fof(f47771,plain,
( sF967 = k9_relat_1(sF961,sK126)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(superposition,[],[f40336,f47426]) ).
fof(f47772,plain,
( sF964 = k9_relat_1(sF961,sF963)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ v1_funct_2(sF961,u1_struct_0(sK123),u1_struct_0(sK124))
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(superposition,[],[f40336,f47420]) ).
fof(f47785,plain,
( ~ v1_funct_2(sF961,u1_struct_0(sK123),sF965)
| sF964 = k9_relat_1(sF961,sF963)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47772,f47422]) ).
fof(f47786,plain,
( ~ v1_funct_2(sF961,u1_struct_0(sK123),sF965)
| sF967 = k9_relat_1(sF961,sK126)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47771,f47422]) ).
fof(f47787,plain,
( ~ v1_funct_2(sF961,u1_struct_0(sK123),sF965)
| sF966 = k9_relat_1(sF961,sK125)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47770,f47422]) ).
fof(f47793,plain,
( ~ v1_funct_2(sF961,sF962,sF965)
| sF964 = k9_relat_1(sF961,sF963)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47785,f47416]) ).
fof(f47794,plain,
( ~ v1_funct_2(sF961,sF962,sF965)
| sF967 = k9_relat_1(sF961,sK126)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47786,f47416]) ).
fof(f47795,plain,
( ~ v1_funct_2(sF961,sF962,sF965)
| sF966 = k9_relat_1(sF961,sK125)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961)
| ~ m1_relset_1(sF961,u1_struct_0(sK123),u1_struct_0(sK124)) ),
inference(forward_demodulation,[],[f47787,f47416]) ).
fof(f47801,plain,
( ~ m1_relset_1(sF961,u1_struct_0(sK123),sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| sF964 = k9_relat_1(sF961,sF963)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47793,f47422]) ).
fof(f47802,plain,
( ~ m1_relset_1(sF961,u1_struct_0(sK123),sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| sF967 = k9_relat_1(sF961,sK126)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47794,f47422]) ).
fof(f47803,plain,
( ~ m1_relset_1(sF961,u1_struct_0(sK123),sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| sF966 = k9_relat_1(sF961,sK125)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47795,f47422]) ).
fof(f47809,plain,
( ~ m1_relset_1(sF961,sF962,sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| sF964 = k9_relat_1(sF961,sF963)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47801,f47416]) ).
fof(f47810,plain,
( ~ m1_relset_1(sF961,sF962,sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| sF967 = k9_relat_1(sF961,sK126)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47802,f47416]) ).
fof(f47811,plain,
( ~ m1_relset_1(sF961,sF962,sF965)
| ~ v1_funct_2(sF961,sF962,sF965)
| sF966 = k9_relat_1(sF961,sK125)
| ~ l1_struct_0(sK123)
| ~ l1_struct_0(sK124)
| ~ v1_funct_1(sF961) ),
inference(forward_demodulation,[],[f47803,f47416]) ).
fof(f47814,definition,
( spl970_51
<=> sF964 = k9_relat_1(sF961,sF963) ),
introduced(definition,[new_symbols(definition,[spl970_51])],[avatar_definition]) ).
fof(f47816,plain,
( sF964 = k9_relat_1(sF961,sF963)
| ~ spl970_51 ),
inference(avatar_component_clause,[],[f47814]) ).
fof(f47819,definition,
( spl970_52
<=> sF967 = k9_relat_1(sF961,sK126) ),
introduced(definition,[new_symbols(definition,[spl970_52])],[avatar_definition]) ).
fof(f47821,plain,
( sF967 = k9_relat_1(sF961,sK126)
| ~ spl970_52 ),
inference(avatar_component_clause,[],[f47819]) ).
fof(f47824,definition,
( spl970_53
<=> sF966 = k9_relat_1(sF961,sK125) ),
introduced(definition,[new_symbols(definition,[spl970_53])],[avatar_definition]) ).
fof(f47826,plain,
( sF966 = k9_relat_1(sF961,sK125)
| ~ spl970_53 ),
inference(avatar_component_clause,[],[f47824]) ).
fof(f47832,plain,
( ~ spl970_28
| ~ spl970_24
| ~ spl970_26
| spl970_51
| ~ spl970_29
| ~ spl970_30 ),
inference(avatar_split_clause,[],[f47809,f47629,f47625,f47814,f47601,f47590,f47621]) ).
fof(f47833,plain,
( ~ spl970_28
| ~ spl970_24
| ~ spl970_26
| spl970_52
| ~ spl970_29
| ~ spl970_30 ),
inference(avatar_split_clause,[],[f47810,f47629,f47625,f47819,f47601,f47590,f47621]) ).
fof(f47834,plain,
( ~ spl970_28
| ~ spl970_24
| ~ spl970_26
| spl970_53
| ~ spl970_29
| ~ spl970_30 ),
inference(avatar_split_clause,[],[f47811,f47629,f47625,f47824,f47601,f47590,f47621]) ).
fof(f47836,plain,
( sF968 = k2_xboole_0(sF967,sF966)
| ~ m1_subset_1(sF966,k1_zfmisc_1(sF965))
| ~ m1_subset_1(sF967,k1_zfmisc_1(sF965)) ),
inference(superposition,[],[f47575,f47428]) ).
fof(f47837,plain,
( sF963 = k2_xboole_0(sK126,sK125)
| ~ m1_subset_1(sK125,k1_zfmisc_1(sF962))
| ~ m1_subset_1(sK126,k1_zfmisc_1(sF962)) ),
inference(superposition,[],[f47575,f47418]) ).
fof(f47855,plain,
( ~ m1_subset_1(sK125,sF969)
| sF963 = k2_xboole_0(sK126,sK125)
| ~ m1_subset_1(sK126,k1_zfmisc_1(sF962)) ),
inference(forward_demodulation,[],[f47837,f47431]) ).
fof(f47857,plain,
( ~ m1_subset_1(sK126,sF969)
| ~ m1_subset_1(sK125,sF969)
| sF963 = k2_xboole_0(sK126,sK125) ),
inference(forward_demodulation,[],[f47855,f47431]) ).
fof(f47859,definition,
( spl970_55
<=> sF963 = k2_xboole_0(sK126,sK125) ),
introduced(definition,[new_symbols(definition,[spl970_55])],[avatar_definition]) ).
fof(f47861,plain,
( sF963 = k2_xboole_0(sK126,sK125)
| ~ spl970_55 ),
inference(avatar_component_clause,[],[f47859]) ).
fof(f47863,plain,
( spl970_55
| ~ spl970_22
| ~ spl970_23 ),
inference(avatar_split_clause,[],[f47857,f47564,f47560,f47859]) ).
fof(f47864,plain,
( l1_pre_topc(sK124)
| ~ l1_pre_topc(sK123)
| ~ spl970_46 ),
inference(resolution,[],[f40222,f47739]) ).
fof(f47865,plain,
( ~ spl970_36
| spl970_39
| ~ spl970_46 ),
inference(avatar_split_clause,[],[f47864,f47738,f47673,f47661]) ).
fof(f47929,plain,
( ~ m2_tsp_1(sK124,sK123)
| ~ l1_pre_topc(sK123)
| spl970_42 ),
inference(resolution,[],[f40219,f47689]) ).
fof(f47930,plain,
( ~ spl970_36
| ~ spl970_46
| spl970_42 ),
inference(avatar_split_clause,[],[f47929,f47687,f47738,f47661]) ).
fof(f47931,plain,
( m2_relset_1(sF961,u1_struct_0(sK123),sF965)
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(forward_demodulation,[],[f47752,f47422]) ).
fof(f47937,plain,
( m2_relset_1(sF961,sF962,sF965)
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(forward_demodulation,[],[f47931,f47416]) ).
fof(f47939,definition,
( spl970_69
<=> m2_relset_1(sF961,sF962,sF965) ),
introduced(definition,[new_symbols(definition,[spl970_69])],[avatar_definition]) ).
fof(f47941,plain,
( m2_relset_1(sF961,sF962,sF965)
| ~ spl970_69 ),
inference(avatar_component_clause,[],[f47939]) ).
fof(f47942,plain,
( ~ spl970_42
| ~ spl970_43
| spl970_34
| ~ spl970_36
| ~ spl970_37
| spl970_32
| spl970_69 ),
inference(avatar_split_clause,[],[f47937,f47939,f47645,f47665,f47661,f47653,f47691,f47687]) ).
fof(f47943,plain,
( v1_funct_1(sF961)
| v3_struct_0(sK123)
| ~ v2_pre_topc(sK123)
| ~ l1_pre_topc(sK123)
| v3_struct_0(sK124)
| ~ v2_tsp_2(sK124,sK123)
| ~ m1_pre_topc(sK124,sK123) ),
inference(superposition,[],[f40349,f47414]) ).
fof(f47944,plain,
( ~ spl970_42
| ~ spl970_43
| spl970_34
| ~ spl970_36
| ~ spl970_37
| spl970_32
| spl970_28 ),
inference(avatar_split_clause,[],[f47943,f47621,f47645,f47665,f47661,f47653,f47691,f47687]) ).
fof(f48038,plain,
( ~ l1_pre_topc(sK123)
| spl970_26 ),
inference(resolution,[],[f42484,f47603]) ).
fof(f48039,plain,
( ~ l1_pre_topc(sK124)
| spl970_24 ),
inference(resolution,[],[f42484,f47592]) ).
fof(f48040,plain,
( ~ spl970_39
| spl970_24 ),
inference(avatar_split_clause,[],[f48039,f47590,f47673]) ).
fof(f48041,plain,
( ~ spl970_36
| spl970_26 ),
inference(avatar_split_clause,[],[f48038,f47601,f47661]) ).
fof(f48042,plain,
( ~ m2_relset_1(sF961,sF962,sF965)
| spl970_30 ),
inference(resolution,[],[f47631,f42419]) ).
fof(f48043,plain,
( ~ spl970_69
| spl970_30 ),
inference(avatar_split_clause,[],[f48042,f47629,f47939]) ).
fof(f48050,definition,
( spl970_80
<=> sF968 = k2_xboole_0(sF967,sF966) ),
introduced(definition,[new_symbols(definition,[spl970_80])],[avatar_definition]) ).
fof(f48052,plain,
( sF968 = k2_xboole_0(sF967,sF966)
| ~ spl970_80 ),
inference(avatar_component_clause,[],[f48050]) ).
fof(f48054,plain,
( ~ spl970_18
| ~ spl970_19
| spl970_80 ),
inference(avatar_split_clause,[],[f47836,f48050,f47543,f47539]) ).
fof(f48562,definition,
( spl970_138
<=> v1_relat_1(sF961) ),
introduced(definition,[new_symbols(definition,[spl970_138])],[avatar_definition]) ).
fof(f48563,plain,
( v1_relat_1(sF961)
| ~ spl970_138 ),
inference(avatar_component_clause,[],[f48562]) ).
fof(f48564,plain,
( ~ v1_relat_1(sF961)
| spl970_138 ),
inference(avatar_component_clause,[],[f48562]) ).
fof(f48950,plain,
! [X2,X0,X1] :
( v1_relat_1(X0)
| ~ m2_relset_1(X0,X1,X2) ),
inference(resolution,[],[f43031,f43032]) ).
fof(f52206,plain,
( ! [X0,X1] : ~ m2_relset_1(sF961,X0,X1)
| spl970_138 ),
inference(resolution,[],[f48950,f48564]) ).
fof(f52208,plain,
( $false
| ~ spl970_69
| spl970_138 ),
inference(backward_subsumption_resolution,[],[f47941,f52206]) ).
fof(f52210,plain,
( ~ spl970_69
| spl970_138 ),
inference(avatar_contradiction_clause,[],[f52208]) ).
fof(f58817,plain,
( ! [X0,X1] : k9_relat_1(sF961,k2_xboole_0(X0,X1)) = k2_xboole_0(k9_relat_1(sF961,X0),k9_relat_1(sF961,X1))
| ~ spl970_138 ),
inference(resolution,[],[f42377,f48563]) ).
fof(f58827,plain,
( ! [X0] : k2_xboole_0(sF967,k9_relat_1(sF961,X0)) = k9_relat_1(sF961,k2_xboole_0(sK126,X0))
| ~ spl970_52
| ~ spl970_138 ),
inference(superposition,[],[f58817,f47821]) ).
fof(f58886,plain,
( k9_relat_1(sF961,sF963) = k2_xboole_0(sF967,k9_relat_1(sF961,sK125))
| ~ spl970_52
| ~ spl970_55
| ~ spl970_138 ),
inference(superposition,[],[f58827,f47861]) ).
fof(f58910,plain,
( k9_relat_1(sF961,sF963) = k2_xboole_0(sF967,sF966)
| ~ spl970_52
| ~ spl970_53
| ~ spl970_55
| ~ spl970_138 ),
inference(forward_demodulation,[],[f58886,f47826]) ).
fof(f58911,plain,
( sF968 = k9_relat_1(sF961,sF963)
| ~ spl970_52
| ~ spl970_53
| ~ spl970_55
| ~ spl970_80
| ~ spl970_138 ),
inference(forward_demodulation,[],[f58910,f48052]) ).
fof(f58912,plain,
( sF964 = sF968
| ~ spl970_51
| ~ spl970_52
| ~ spl970_53
| ~ spl970_55
| ~ spl970_80
| ~ spl970_138 ),
inference(forward_demodulation,[],[f58911,f47816]) ).
fof(f58913,plain,
( $false
| ~ spl970_51
| ~ spl970_52
| ~ spl970_53
| ~ spl970_55
| ~ spl970_80
| ~ spl970_138 ),
inference(backward_subsumption_resolution,[],[f47429,f58912]) ).
fof(f58930,plain,
( ~ spl970_51
| ~ spl970_52
| ~ spl970_53
| ~ spl970_55
| ~ spl970_80
| ~ spl970_138 ),
inference(avatar_contradiction_clause,[],[f58913]) ).
cnf(s18,plain,
spl970_23,
inference(sat_conversion,[],[f47579]) ).
cnf(s20,plain,
spl970_22,
inference(sat_conversion,[],[f47582]) ).
cnf(s23,plain,
( spl970_18
| ~ spl970_24
| ~ spl970_26
| ~ spl970_28
| ~ spl970_29
| ~ spl970_30 ),
inference(sat_conversion,[],[f47632]) ).
cnf(s24,plain,
( spl970_19
| ~ spl970_24
| ~ spl970_26
| ~ spl970_28
| ~ spl970_29
| ~ spl970_30 ),
inference(sat_conversion,[],[f47633]) ).
cnf(s30,plain,
( spl970_29
| spl970_32
| spl970_34
| ~ spl970_36
| ~ spl970_37
| ~ spl970_42
| ~ spl970_43 ),
inference(sat_conversion,[],[f47694]) ).
cnf(s32,plain,
~ spl970_34,
inference(sat_conversion,[],[f47697]) ).
cnf(s34,plain,
~ spl970_32,
inference(sat_conversion,[],[f47700]) ).
cnf(s36,plain,
spl970_36,
inference(sat_conversion,[],[f47703]) ).
cnf(s38,plain,
spl970_37,
inference(sat_conversion,[],[f47706]) ).
cnf(s43,plain,
spl970_43,
inference(sat_conversion,[],[f47747]) ).
cnf(s45,plain,
spl970_46,
inference(sat_conversion,[],[f47750]) ).
cnf(s53,plain,
( ~ spl970_24
| ~ spl970_26
| ~ spl970_28
| ~ spl970_29
| ~ spl970_30
| spl970_51 ),
inference(sat_conversion,[],[f47832]) ).
cnf(s54,plain,
( ~ spl970_24
| ~ spl970_26
| ~ spl970_28
| ~ spl970_29
| ~ spl970_30
| spl970_52 ),
inference(sat_conversion,[],[f47833]) ).
cnf(s55,plain,
( ~ spl970_24
| ~ spl970_26
| ~ spl970_28
| ~ spl970_29
| ~ spl970_30
| spl970_53 ),
inference(sat_conversion,[],[f47834]) ).
cnf(s58,plain,
( ~ spl970_22
| ~ spl970_23
| spl970_55 ),
inference(sat_conversion,[],[f47863]) ).
cnf(s59,plain,
( ~ spl970_36
| spl970_39
| ~ spl970_46 ),
inference(sat_conversion,[],[f47865]) ).
cnf(s70,plain,
( ~ spl970_36
| spl970_42
| ~ spl970_46 ),
inference(sat_conversion,[],[f47930]) ).
cnf(s72,plain,
( spl970_32
| spl970_34
| ~ spl970_36
| ~ spl970_37
| ~ spl970_42
| ~ spl970_43
| spl970_69 ),
inference(sat_conversion,[],[f47942]) ).
cnf(s73,plain,
( spl970_28
| spl970_32
| spl970_34
| ~ spl970_36
| ~ spl970_37
| ~ spl970_42
| ~ spl970_43 ),
inference(sat_conversion,[],[f47944]) ).
cnf(s83,plain,
( spl970_24
| ~ spl970_39 ),
inference(sat_conversion,[],[f48040]) ).
cnf(s84,plain,
( spl970_26
| ~ spl970_36 ),
inference(sat_conversion,[],[f48041]) ).
cnf(s85,plain,
( spl970_30
| ~ spl970_69 ),
inference(sat_conversion,[],[f48043]) ).
cnf(s88,plain,
( ~ spl970_18
| ~ spl970_19
| spl970_80 ),
inference(sat_conversion,[],[f48054]) ).
cnf(s765,plain,
( ~ spl970_69
| spl970_138 ),
inference(sat_conversion,[],[f52210]) ).
cnf(s1657,plain,
( ~ spl970_51
| ~ spl970_52
| ~ spl970_53
| ~ spl970_55
| ~ spl970_80
| ~ spl970_138 ),
inference(sat_conversion,[],[f58930]) ).
cnf(s1686,plain,
spl970_26,
inference(rat,[],[s84,s36]) ).
cnf(s1687,plain,
spl970_42,
inference(rat,[],[s70,s45,s36]) ).
cnf(s1688,plain,
spl970_39,
inference(rat,[],[s59,s45,s36]) ).
cnf(s1691,plain,
spl970_24,
inference(rat,[],[s83,s1688]) ).
cnf(s1774,plain,
spl970_69,
inference(rat,[],[s72,s34,s43,s1687,s38,s36,s32]) ).
cnf(s1782,plain,
spl970_28,
inference(rat,[],[s73,s43,s1687,s38,s36,s34,s32]) ).
cnf(s1791,plain,
spl970_138,
inference(rat,[],[s765,s1774]) ).
cnf(s1792,plain,
spl970_30,
inference(rat,[],[s85,s1774]) ).
cnf(s1804,plain,
spl970_29,
inference(rat,[],[s30,s43,s1687,s38,s36,s32,s34]) ).
cnf(s1811,plain,
spl970_53,
inference(rat,[],[s55,s1782,s1792,s1691,s1686,s1804]) ).
cnf(s1812,plain,
spl970_52,
inference(rat,[],[s54,s1782,s1792,s1691,s1686,s1804]) ).
cnf(s1813,plain,
spl970_51,
inference(rat,[],[s53,s1782,s1792,s1691,s1686,s1804]) ).
cnf(s1855,plain,
spl970_19,
inference(rat,[],[s24,s1792,s1804,s1782,s1686,s1691]) ).
cnf(s1880,plain,
spl970_18,
inference(rat,[],[s23,s1792,s1804,s1782,s1686,s1691]) ).
cnf(s1891,plain,
spl970_80,
inference(rat,[],[s88,s1855,s1880]) ).
cnf(s1919,plain,
~ spl970_55,
inference(rat,[],[s1657,s1791,s1813,s1812,s1811,s1891]) ).
cnf(s1960,plain,
~ spl970_23,
inference(rat,[],[s58,s1919,s20]) ).
cnf(s1998,plain,
$false,
inference(rat,[],[s18,s1960]) ).
fof(f58932,plain,
$false,
inference(avatar_sat_refutation,[],[s1998]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP038+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n010.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:00:55 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.34/4.98 % (2214739)Detected formulas, will run a generic FOF schedule.
% 16.34/4.98 % (2214744)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=3972704049:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 16.34/4.98 % (2214746)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=1070105417:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 16.34/4.98 % (2214745)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=1625732210:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 16.34/4.98 % (2214748)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2204188245:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 16.34/4.98 % (2214749)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1650943309:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 16.34/4.98 % (2214747)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=727321012:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 16.34/4.98 % (2214750)dis-21_1_sil=8000:lcm=predicate:random_seed=4121963406:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 16.34/4.98 % (2214749)Instruction limit reached!
% 16.34/4.98 % (2214749)------------------------------
% 16.34/4.98 % (2214749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.34/4.98 % (2214749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.34/4.98 % (2214749)CaDiCaL version: 2.1.3
% 16.34/4.98 % (2214749)Termination reason: Instruction limit
% 16.34/4.98 % (2214749)Termination phase: Property scanning
% 16.34/4.98 % (2214749)Time elapsed: 0.061 s
% 16.34/4.98 % (2214749)Peak memory usage: 136 MB
% 16.34/4.98 % (2214749)Instructions burned: 140 (million)
% 16.34/4.98 % (2214747)Instruction limit reached!
% 16.34/4.98 % (2214747)------------------------------
% 16.34/4.98 % (2214747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.34/4.98 % (2214747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.34/4.98 % (2214747)CaDiCaL version: 2.1.3
% 16.34/4.98 % (2214747)Termination reason: Instruction limit
% 16.34/4.98 % (2214747)Termination phase: SInE selection
% 16.34/4.98 % (2214747)Time elapsed: 0.080 s
% 16.34/4.98 % (2214747)Peak memory usage: 135 MB
% 16.34/4.98 % (2214747)Instructions burned: 110 (million)
% 16.34/4.98 % (2214748)Instruction limit reached!
% 16.34/4.98 % (2214748)------------------------------
% 16.34/4.98 % (2214748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.34/4.98 % (2214748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.34/4.98 % (2214748)CaDiCaL version: 2.1.3
% 16.34/4.98 % (2214748)Termination reason: Instruction limit
% 16.34/4.98 % (2214748)Termination phase: SInE selection
% 16.34/4.98 % (2214748)Time elapsed: 0.087 s
% 16.34/4.98 % (2214748)Peak memory usage: 135 MB
% 16.34/4.98 % (2214748)Instructions burned: 120 (million)
% 16.34/4.98 % (2214750)Instruction limit reached!
% 16.34/4.98 % (2214750)------------------------------
% 16.34/4.98 % (2214750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.34/4.98 % (2214750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.34/4.98 % (2214750)CaDiCaL version: 2.1.3
% 16.34/4.98 % (2214750)Termination reason: Instruction limit
% 16.34/4.98 % (2214750)Termination phase: SInE selection
% 16.34/4.98 % (2214750)Time elapsed: 0.091 s
% 16.34/4.98 % (2214750)Peak memory usage: 136 MB
% 16.34/4.98 % (2214750)Instructions burned: 130 (million)
% 16.34/4.98 % (2214758)lrs+10_1_sil=8000:sp=occurrence:random_seed=1149650791:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 16.34/4.98 % (2214759)lrs+10_1_sil=32000:urr=on:br=off:random_seed=819993004:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/157Mi)
% 16.34/4.98 % (2214761)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=2067717956:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 16.34/4.98 % (2214760)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2515657447:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 16.34/4.98 % (2214759)Instruction limit reached!
% 23.81/5.93 % (2214759)------------------------------
% 23.81/5.93 % (2214759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214759)CaDiCaL version: 2.1.3
% 23.81/5.93 % (2214759)Termination reason: Instruction limit
% 23.81/5.93 % (2214759)Termination phase: Property scanning
% 23.81/5.93 % (2214759)Time elapsed: 0.068 s
% 23.81/5.93 % (2214759)Peak memory usage: 136 MB
% 23.81/5.93 % (2214759)Instructions burned: 157 (million)
% 23.81/5.93 % (2214761)Instruction limit reached!
% 23.81/5.93 % (2214761)------------------------------
% 23.81/5.93 % (2214761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214761)CaDiCaL version: 2.1.3
% 23.81/5.93 % (2214761)Termination reason: Instruction limit
% 23.81/5.93 % (2214761)Termination phase: Property scanning
% 23.81/5.93 % (2214761)Time elapsed: 0.106 s
% 23.81/5.93 % (2214761)Peak memory usage: 136 MB
% 23.81/5.93 % (2214761)Instructions burned: 248 (million)
% 23.81/5.93 % (2214766)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=592648813:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2974 on theBenchmark for (2974ds/294Mi)
% 23.81/5.93 % (2214758)Instruction limit reached!
% 23.81/5.93 % (2214758)------------------------------
% 23.81/5.93 % (2214758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214758)CaDiCaL version: 2.1.3
% 23.81/5.93 % (2214758)Termination reason: Instruction limit
% 23.81/5.93 % (2214758)Termination phase: Preprocessing 3
% 23.81/5.93 % (2214758)Time elapsed: 0.237 s
% 23.81/5.93 % (2214758)Peak memory usage: 140 MB
% 23.81/5.93 % (2214758)Instructions burned: 285 (million)
% 23.81/5.93 % (2214767)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4182035326:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 23.81/5.93 % (2214760)Instruction limit reached!
% 23.81/5.93 % (2214760)------------------------------
% 23.81/5.93 % (2214760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214760)CaDiCaL version: 2.1.3
% 23.81/5.93 % (2214760)Termination reason: Instruction limit
% 23.81/5.93 % (2214760)Termination phase: Saturation
% 23.81/5.93 % (2214760)Time elapsed: 0.252 s
% 23.81/5.93 % (2214760)Peak memory usage: 142 MB
% 23.81/5.93 % (2214760)Instructions burned: 326 (million)
% 23.81/5.93 % (2214769)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2547811157:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 23.81/5.93 % (2214766)Instruction limit reached!
% 23.81/5.93 % (2214766)------------------------------
% 23.81/5.93 % (2214766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214766)CaDiCaL version: 2.1.3
% 23.81/5.93 % (2214766)Termination reason: Instruction limit
% 23.81/5.93 % (2214766)Termination phase: SInE selection
% 23.81/5.93 % (2214766)Time elapsed: 0.184 s
% 23.81/5.93 % (2214766)Peak memory usage: 136 MB
% 23.81/5.93 % (2214766)Instructions burned: 295 (million)
% 23.81/5.93 % (2214771)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=214823906:i=127:av=off:fsr=off:sup=off_2972 on theBenchmark for (2972ds/127Mi)
% 23.81/5.93 % (2214769)Instruction limit reached!
% 23.81/5.93 % (2214769)------------------------------
% 23.81/5.93 % (2214769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214769)CaDiCaL version: 2.1.3
% 23.81/5.93 % (2214769)Termination reason: Instruction limit
% 23.81/5.93 % (2214769)Termination phase: SInE selection
% 23.81/5.93 % (2214769)Time elapsed: 0.086 s
% 23.81/5.93 % (2214769)Peak memory usage: 136 MB
% 23.81/5.93 % (2214769)Instructions burned: 114 (million)
% 23.81/5.93 % (2214771)Instruction limit reached!
% 23.81/5.93 % (2214771)------------------------------
% 23.81/5.93 % (2214771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.81/5.93 % (2214771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.81/5.93 % (2214771)CaDiCaL version: 2.1.3
% 49.56/9.53 % (2214771)Termination reason: Instruction limit
% 49.56/9.53 % (2214771)Termination phase: Preprocessing 1
% 49.56/9.53 % (2214771)Time elapsed: 0.099 s
% 49.56/9.53 % (2214771)Peak memory usage: 137 MB
% 49.56/9.53 % (2214771)Instructions burned: 128 (million)
% 49.56/9.53 % (2214773)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1799215006:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2970 on theBenchmark for (2970ds/114Mi)
% 49.56/9.53 % (2214773)Instruction limit reached!
% 49.56/9.53 % (2214773)------------------------------
% 49.56/9.53 % (2214773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.56/9.53 % (2214773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/9.53 % (2214773)CaDiCaL version: 2.1.3
% 49.56/9.53 % (2214773)Termination reason: Instruction limit
% 49.56/9.53 % (2214773)Termination phase: Property scanning
% 49.56/9.53 % (2214773)Time elapsed: 0.053 s
% 49.56/9.53 % (2214773)Peak memory usage: 136 MB
% 49.56/9.53 % (2214773)Instructions burned: 116 (million)
% 49.56/9.53 % (2214775)lrs+10_1_sil=8000:sp=occurrence:random_seed=3196400616:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2970 on theBenchmark for (2970ds/907Mi)
% 49.56/9.53 % (2214777)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=333679302:i=437:sd=1:aac=none:ss=included_2969 on theBenchmark for (2969ds/437Mi)
% 49.56/9.53 % (2214779)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2058115900:i=5202:ss=axioms:sgt=16_2968 on theBenchmark for (2968ds/5202Mi)
% 49.56/9.53 % (2214777)Instruction limit reached!
% 49.56/9.53 % (2214777)------------------------------
% 49.56/9.53 % (2214777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.56/9.53 % (2214777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/9.53 % (2214777)CaDiCaL version: 2.1.3
% 49.56/9.53 % (2214777)Termination reason: Instruction limit
% 49.56/9.53 % (2214777)Termination phase: Saturation
% 49.56/9.53 % (2214777)Time elapsed: 0.304 s
% 49.56/9.53 % (2214777)Peak memory usage: 144 MB
% 49.56/9.53 % (2214777)Instructions burned: 437 (million)
% 49.56/9.53 % (2214782)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3782478333:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2965 on theBenchmark for (2965ds/134Mi)
% 49.56/9.53 % (2214775)Instruction limit reached!
% 49.56/9.53 % (2214775)------------------------------
% 49.56/9.53 % (2214775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.56/9.53 % (2214775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/9.53 % (2214775)CaDiCaL version: 2.1.3
% 49.56/9.53 % (2214775)Termination reason: Instruction limit
% 49.56/9.53 % (2214775)Termination phase: Property scanning
% 49.56/9.53 % (2214775)Time elapsed: 0.590 s
% 49.56/9.53 % (2214775)Peak memory usage: 158 MB
% 49.56/9.53 % (2214775)Instructions burned: 907 (million)
% 49.56/9.53 % (2214782)Instruction limit reached!
% 49.56/9.53 % (2214782)------------------------------
% 49.56/9.53 % (2214782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.56/9.53 % (2214782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/9.53 % (2214782)CaDiCaL version: 2.1.3
% 49.56/9.53 % (2214782)Termination reason: Instruction limit
% 49.56/9.53 % (2214782)Termination phase: SInE selection
% 49.56/9.53 % (2214782)Time elapsed: 0.098 s
% 49.56/9.53 % (2214782)Peak memory usage: 136 MB
% 49.56/9.53 % (2214782)Instructions burned: 134 (million)
% 49.56/9.53 % (2214784)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=23555839:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 49.56/9.53 % (2214785)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=446040617:st=3:i=13193:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/13193Mi)
% 49.56/9.53 % (2214784)Instruction limit reached!
% 49.56/9.53 % (2214784)------------------------------
% 49.56/9.53 % (2214784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.56/9.53 % (2214784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/9.53 % (2214784)CaDiCaL version: 2.1.3
% 49.56/9.53 % (2214784)Termination reason: Instruction limit
% 49.56/9.53 % (2214784)Termination phase: Preprocessing 2
% 49.56/9.53 % (2214784)Time elapsed: 0.464 s
% 49.56/9.53 % (2214784)Peak memory usage: 147 MB
% 49.56/9.53 % (2214784)Instructions burned: 592 (million)
% 49.56/9.53 % (2214767)Instruction limit reached!
% 49.56/9.53 % (2214767)------------------------------
% 49.56/9.53 % (2214767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.44/16.02 % (2214767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.44/16.02 % (2214767)CaDiCaL version: 2.1.3
% 95.44/16.02 % (2214767)Termination reason: Instruction limit
% 95.44/16.02 % (2214767)Termination phase: Property scanning
% 95.44/16.02 % (2214767)Time elapsed: 1.545 s
% 95.44/16.02 % (2214767)Peak memory usage: 232 MB
% 95.44/16.02 % (2214767)Instructions burned: 2351 (million)
% 95.44/16.02 % (2214788)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=1911715783:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 95.44/16.02 % (2214789)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=898876356:i=134:gtgl=5:slsql=off:gtg=exists_sym_2956 on theBenchmark for (2956ds/134Mi)
% 95.44/16.02 % (2214788)Instruction limit reached!
% 95.44/16.02 % (2214788)------------------------------
% 95.44/16.02 % (2214788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.44/16.02 % (2214788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.44/16.02 % (2214788)CaDiCaL version: 2.1.3
% 95.44/16.02 % (2214788)Termination reason: Instruction limit
% 95.44/16.02 % (2214788)Termination phase: Property scanning
% 95.44/16.02 % (2214788)Time elapsed: 0.058 s
% 95.44/16.02 % (2214788)Peak memory usage: 136 MB
% 95.44/16.02 % (2214788)Instructions burned: 127 (million)
% 95.44/16.02 % (2214789)Instruction limit reached!
% 95.44/16.02 % (2214789)------------------------------
% 95.44/16.02 % (2214789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.44/16.02 % (2214789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.44/16.02 % (2214789)CaDiCaL version: 2.1.3
% 95.44/16.02 % (2214789)Termination reason: Instruction limit
% 95.44/16.02 % (2214789)Termination phase: Property scanning
% 95.44/16.02 % (2214789)Time elapsed: 0.061 s
% 95.44/16.02 % (2214789)Peak memory usage: 136 MB
% 95.44/16.02 % (2214789)Instructions burned: 135 (million)
% 95.44/16.02 % (2214792)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3939434045:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/141Mi)
% 95.44/16.02 % (2214793)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3862683655:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2954 on theBenchmark for (2954ds/431Mi)
% 95.44/16.02 % (2214792)Instruction limit reached!
% 95.44/16.02 % (2214792)------------------------------
% 95.44/16.02 % (2214792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.44/16.02 % (2214792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.44/16.02 % (2214792)CaDiCaL version: 2.1.3
% 95.44/16.02 % (2214792)Termination reason: Instruction limit
% 95.44/16.02 % (2214792)Termination phase: SInE selection
% 95.44/16.02 % (2214792)Time elapsed: 0.108 s
% 95.44/16.02 % (2214792)Peak memory usage: 136 MB
% 95.44/16.02 % (2214792)Instructions burned: 141 (million)
% 95.44/16.02 % (2214796)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=3888916024:i=6060:aac=none:ins=25_2952 on theBenchmark for (2952ds/6060Mi)
% 95.44/16.02 % (2214793)Instruction limit reached!
% 95.44/16.02 % (2214793)------------------------------
% 95.44/16.02 % (2214793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.44/16.02 % (2214793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.44/16.02 % (2214793)CaDiCaL version: 2.1.3
% 95.44/16.02 % (2214793)Termination reason: Instruction limit
% 95.44/16.02 % (2214793)Termination phase: Saturation
% 95.44/16.02 % (2214793)Time elapsed: 0.316 s
% 95.44/16.02 % (2214793)Peak memory usage: 144 MB
% 95.44/16.02 % (2214793)Instructions burned: 432 (million)
% 95.44/16.02 % (2214798)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=826738426:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2949 on theBenchmark for (2949ds/150Mi)
% 95.44/16.02 % (2214798)Instruction limit reached!
% 95.44/16.02 % (2214798)------------------------------
% 95.44/16.02 % (2214798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.44/16.02 % (2214798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.44/16.02 % (2214798)CaDiCaL version: 2.1.3
% 95.44/16.02 % (2214798)Termination reason: Instruction limit
% 112.41/18.38 % (2214798)Termination phase: SInE selection
% 112.41/18.38 % (2214798)Time elapsed: 0.114 s
% 112.41/18.38 % (2214798)Peak memory usage: 136 MB
% 112.41/18.38 % (2214798)Instructions burned: 150 (million)
% 112.41/18.38 % (2214800)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1061281991:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 112.41/18.38 % (2214779)Instruction limit reached!
% 112.41/18.38 % (2214779)------------------------------
% 112.41/18.38 % (2214779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.41/18.38 % (2214779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.41/18.38 % (2214779)CaDiCaL version: 2.1.3
% 112.41/18.38 % (2214779)Termination reason: Instruction limit
% 112.41/18.38 % (2214779)Termination phase: Saturation
% 112.41/18.38 % (2214779)Time elapsed: 3.873 s
% 112.41/18.38 % (2214779)Peak memory usage: 615 MB
% 112.41/18.38 % (2214779)Instructions burned: 5202 (million)
% 112.41/18.38 % (2214803)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=812616237:i=667:av=off:fsr=off_2928 on theBenchmark for (2928ds/667Mi)
% 112.41/18.38 % (2214803)Instruction limit reached!
% 112.41/18.38 % (2214803)------------------------------
% 112.41/18.38 % (2214803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.41/18.38 % (2214803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.41/18.38 % (2214803)CaDiCaL version: 2.1.3
% 112.41/18.38 % (2214803)Termination reason: Instruction limit
% 112.41/18.38 % (2214803)Termination phase: NewCNF
% 112.41/18.38 % (2214803)Time elapsed: 0.549 s
% 112.41/18.38 % (2214803)Peak memory usage: 185 MB
% 112.41/18.38 % (2214803)Instructions burned: 667 (million)
% 112.41/18.38 % (2214805)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1433974468:s2a=on:i=185:s2at=1.8:fdi=4_2921 on theBenchmark for (2921ds/185Mi)
% 112.41/18.38 % (2214805)Instruction limit reached!
% 112.41/18.38 % (2214805)------------------------------
% 112.41/18.38 % (2214805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.41/18.38 % (2214805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.41/18.38 % (2214805)CaDiCaL version: 2.1.3
% 112.41/18.38 % (2214805)Termination reason: Instruction limit
% 112.41/18.38 % (2214805)Termination phase: SInE selection
% 112.41/18.38 % (2214805)Time elapsed: 0.131 s
% 112.41/18.38 % (2214805)Peak memory usage: 136 MB
% 112.41/18.38 % (2214805)Instructions burned: 186 (million)
% 112.41/18.38 % (2214807)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=115136985:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2918 on theBenchmark for (2918ds/193Mi)
% 112.41/18.38 % (2214807)Instruction limit reached!
% 112.41/18.38 % (2214807)------------------------------
% 112.41/18.38 % (2214807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.41/18.38 % (2214807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.41/18.38 % (2214807)CaDiCaL version: 2.1.3
% 112.41/18.38 % (2214807)Termination reason: Instruction limit
% 112.41/18.38 % (2214807)Termination phase: SInE selection
% 112.41/18.38 % (2214807)Time elapsed: 0.151 s
% 112.41/18.38 % (2214807)Peak memory usage: 136 MB
% 112.41/18.38 % (2214807)Instructions burned: 193 (million)
% 112.41/18.38 % (2214809)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3678928632:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2915 on theBenchmark for (2915ds/4850Mi)
% 112.41/18.38 % (2214796)Instruction limit reached!
% 112.41/18.38 % (2214796)------------------------------
% 112.41/18.38 % (2214796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.41/18.38 % (2214796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.41/18.38 % (2214796)CaDiCaL version: 2.1.3
% 112.41/18.38 % (2214796)Termination reason: Instruction limit
% 112.41/18.38 % (2214796)Termination phase: Function definition elimination
% 112.41/18.38 % (2214796)Time elapsed: 3.836 s
% 112.41/18.38 % (2214796)Peak memory usage: 244 MB
% 112.41/18.38 % (2214796)Instructions burned: 6060 (million)
% 112.41/18.38 % (2214785)Instruction limit reached!
% 112.41/18.38 % (2214785)------------------------------
% 112.41/18.38 % (2214785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.41/18.38 % (2214785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.41/18.38 % (2214785)CaDiCaL version: 2.1.3
% 112.41/18.38 % (2214785)Termination reason: Instruction limit
% 101.53/19.46 % (2214785)Termination phase: Saturation
% 101.53/19.46 % (2214785)Time elapsed: 5.016 s
% 101.53/19.46 % (2214785)Peak memory usage: 366 MB
% 101.53/19.46 % (2214785)Instructions burned: 13194 (million)
% 101.53/19.46 % (2214811)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2309325916:i=12111:sd=1:ss=included_2912 on theBenchmark for (2912ds/12111Mi)
% 101.53/19.46 % (2214812)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=343818116:i=319:kws=precedence:fsr=off_2911 on theBenchmark for (2911ds/319Mi)
% 101.53/19.46 % (2214812)Instruction limit reached!
% 101.53/19.46 % (2214812)------------------------------
% 101.53/19.46 % (2214812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214812)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214812)Termination reason: Instruction limit
% 101.53/19.46 % (2214812)Termination phase: Unused predicate definition removal
% 101.53/19.46 % (2214812)Time elapsed: 0.154 s
% 101.53/19.46 % (2214812)Peak memory usage: 142 MB
% 101.53/19.46 % (2214812)Instructions burned: 319 (million)
% 101.53/19.46 % (2214815)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2627444921:i=2064:ep=RST_2908 on theBenchmark for (2908ds/2064Mi)
% 101.53/19.46 % (2214815)Instruction limit reached!
% 101.53/19.46 % (2214815)------------------------------
% 101.53/19.46 % (2214815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214815)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214815)Termination reason: Instruction limit
% 101.53/19.46 % (2214815)Termination phase: Property scanning
% 101.53/19.46 % (2214815)Time elapsed: 0.750 s
% 101.53/19.46 % (2214815)Peak memory usage: 231 MB
% 101.53/19.46 % (2214815)Instructions burned: 2064 (million)
% 101.53/19.46 % (2214817)dis-1011_128_sil=32000:random_seed=3117846955:i=3706:ep=RST:av=off_2899 on theBenchmark for (2899ds/3706Mi)
% 101.53/19.46 % (2214809)Instruction limit reached!
% 101.53/19.46 % (2214809)------------------------------
% 101.53/19.46 % (2214809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214809)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214809)Termination reason: Instruction limit
% 101.53/19.46 % (2214809)Termination phase: Property scanning
% 101.53/19.46 % (2214809)Time elapsed: 2.484 s
% 101.53/19.46 % (2214809)Peak memory usage: 217 MB
% 101.53/19.46 % (2214809)Instructions burned: 4851 (million)
% 101.53/19.46 % (2214819)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=641178621:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2889 on theBenchmark for (2889ds/757Mi)
% 101.53/19.46 % (2214817)Instruction limit reached!
% 101.53/19.46 % (2214817)------------------------------
% 101.53/19.46 % (2214817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214817)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214817)Termination reason: Instruction limit
% 101.53/19.46 % (2214817)Termination phase: Function definition elimination
% 101.53/19.46 % (2214817)Time elapsed: 1.140 s
% 101.53/19.46 % (2214817)Peak memory usage: 241 MB
% 101.53/19.46 % (2214817)Instructions burned: 3709 (million)
% 101.53/19.46 % (2214821)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3953892227:i=13913:ss=axioms:sgt=8_2887 on theBenchmark for (2887ds/13913Mi)
% 101.53/19.46 % (2214819)Instruction limit reached!
% 101.53/19.46 % (2214819)------------------------------
% 101.53/19.46 % (2214819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214819)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214819)Termination reason: Instruction limit
% 101.53/19.46 % (2214819)Termination phase: Saturation
% 101.53/19.46 % (2214819)Time elapsed: 0.570 s
% 101.53/19.46 % (2214819)Peak memory usage: 147 MB
% 101.53/19.46 % (2214819)Instructions burned: 757 (million)
% 101.53/19.46 % (2214823)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3418632522:i=9925:aac=none_2882 on theBenchmark for (2882ds/9925Mi)
% 101.53/19.46 % (2214800)Instruction limit reached!
% 101.53/19.46 % (2214800)------------------------------
% 101.53/19.46 % (2214800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214800)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214800)Termination reason: Instruction limit
% 101.53/19.46 % (2214800)Termination phase: Saturation
% 101.53/19.46 % (2214800)Time elapsed: 9.945 s
% 101.53/19.46 % (2214800)Peak memory usage: 1407 MB
% 101.53/19.46 % (2214800)Instructions burned: 14156 (million)
% 101.53/19.46 % (2214825)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3633073458:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2845 on theBenchmark for (2845ds/2479Mi)
% 101.53/19.46 % (2214821)Instruction limit reached!
% 101.53/19.46 % (2214821)------------------------------
% 101.53/19.46 % (2214821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.46 % (2214821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.46 % (2214821)CaDiCaL version: 2.1.3
% 101.53/19.46 % (2214821)Termination reason: Instruction limit
% 101.53/19.46 % (2214821)Termination phase: Saturation
% 101.53/19.47 % (2214821)Time elapsed: 4.776 s
% 101.53/19.47 % (2214821)Peak memory usage: 305 MB
% 101.53/19.47 % (2214821)Instructions burned: 13917 (million)
% 101.53/19.47 % (2214827)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1020506327:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2838 on theBenchmark for (2838ds/440Mi)
% 101.53/19.47 % (2214827)Instruction limit reached!
% 101.53/19.47 % (2214827)------------------------------
% 101.53/19.47 % (2214827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.47 % (2214827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.47 % (2214827)CaDiCaL version: 2.1.3
% 101.53/19.47 % (2214827)Termination reason: Instruction limit
% 101.53/19.47 % (2214827)Termination phase: Property scanning
% 101.53/19.47 % (2214827)Time elapsed: 0.103 s
% 101.53/19.47 % (2214827)Peak memory usage: 136 MB
% 101.53/19.47 % (2214827)Instructions burned: 443 (million)
% 101.53/19.47 % (2214829)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=526115431:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2836 on theBenchmark for (2836ds/11145Mi)
% 101.53/19.47 % (2214811)Instruction limit reached!
% 101.53/19.47 % (2214811)------------------------------
% 101.53/19.47 % (2214811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.47 % (2214811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.47 % (2214811)CaDiCaL version: 2.1.3
% 101.53/19.47 % (2214811)Termination reason: Instruction limit
% 101.53/19.47 % (2214811)Termination phase: Saturation
% 101.53/19.47 % (2214811)Time elapsed: 8.124 s
% 101.53/19.47 % (2214811)Peak memory usage: 302 MB
% 101.53/19.47 % (2214811)Instructions burned: 12111 (million)
% 101.53/19.47 % (2214825)Instruction limit reached!
% 101.53/19.47 % (2214825)------------------------------
% 101.53/19.47 % (2214825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.47 % (2214825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.47 % (2214825)CaDiCaL version: 2.1.3
% 101.53/19.47 % (2214825)Termination reason: Instruction limit
% 101.53/19.47 % (2214825)Termination phase: Saturation
% 101.53/19.47 % (2214825)Time elapsed: 1.547 s
% 101.53/19.47 % (2214825)Peak memory usage: 161 MB
% 101.53/19.47 % (2214825)Instructions burned: 2481 (million)
% 101.53/19.47 % (2214831)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1804937162:cts=off:i=3034:av=off:er=known:fsd=on_2829 on theBenchmark for (2829ds/3034Mi)
% 101.53/19.47 % (2214832)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1663654418:st=2:s2a=on:i=524:s2at=2:ss=axioms_2828 on theBenchmark for (2828ds/524Mi)
% 101.53/19.47 % (2214823)Instruction limit reached!
% 101.53/19.47 % (2214823)------------------------------
% 101.53/19.47 % (2214823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.47 % (2214823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.47 % (2214823)CaDiCaL version: 2.1.3
% 101.53/19.47 % (2214823)Termination reason: Instruction limit
% 101.53/19.47 % (2214823)Termination phase: Saturation
% 101.53/19.47 % (2214823)Time elapsed: 5.567 s
% 101.53/19.47 % (2214823)Peak memory usage: 663 MB
% 101.53/19.47 % (2214823)Instructions burned: 9928 (million)
% 101.53/19.47 % (2214835)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2111430784:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2824 on theBenchmark for (2824ds/1016Mi)
% 101.53/19.47 % (2214832)Instruction limit reached!
% 101.53/19.47 % (2214832)------------------------------
% 101.53/19.47 % (2214832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.47 % (2214832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.47 % (2214832)CaDiCaL version: 2.1.3
% 101.53/19.47 % (2214832)Termination reason: Instruction limit
% 101.53/19.47 % (2214832)Termination phase: SInE selection
% 101.53/19.47 % (2214832)Time elapsed: 0.404 s
% 101.53/19.47 % (2214832)Peak memory usage: 137 MB
% 101.53/19.47 % (2214832)Instructions burned: 524 (million)
% 101.53/19.47 % (2214837)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3350285916:i=14123:bd=preordered:ins=4_2822 on theBenchmark for (2822ds/14123Mi)
% 101.53/19.47 % (2214835)Instruction limit reached!
% 101.53/19.47 % (2214835)------------------------------
% 101.53/19.47 % (2214835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.53/19.47 % (2214835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.53/19.47 % (2214835)CaDiCaL version: 2.1.3
% 101.53/19.47 % (2214835)Termination reason: Instruction limit
% 101.53/19.47 % (2214835)Termination phase: Saturation
% 101.53/19.47 % (2214835)Time elapsed: 0.622 s
% 101.53/19.47 % (2214835)Peak memory usage: 153 MB
% 101.53/19.47 % (2214835)Instructions burned: 1017 (million)
% 101.53/19.47 % (2214829)First to succeed.
% 101.53/19.47 % (2214829)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2214739"
% 101.53/19.47 % (2214839)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=381040269:i=5781:kws=precedence:bd=all:rawr=on_2816 on theBenchmark for (2816ds/5781Mi)
% 101.53/19.47 % (2214829)Refutation found. Thanks to Tanya!
% 101.53/19.47 % SZS status Theorem for theBenchmark
% 101.53/19.47 % SZS output start Proof for theBenchmark
% See solution above
% 120.13/19.65 % (2214829)------------------------------
% 120.13/19.65 % (2214829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.13/19.65 % (2214829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.13/19.66 % (2214829)CaDiCaL version: 2.1.3
% 120.13/19.66 % (2214829)Termination reason: Refutation
% 120.13/19.66 % (2214829)Time elapsed: 1.991 s
% 120.13/19.66 % (2214829)Peak memory usage: 274 MB
% 120.13/19.66 % (2214829)Instructions burned: 5333 (million)
% 120.13/19.66 % (2214829)------------------------------
% 120.13/19.66 % (2214829)------------------------------
% 120.13/19.66 % (2214739)Success in time 18.806 s
% 120.13/19.66 % Vampire exiting
%------------------------------------------------------------------------------