%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU445+3 : 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 : n002.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 12:49:08 PM UTC 2026
% Result : Theorem 13.14s 5.22s
% Output : Refutation 24.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 30
% Syntax : Number of formulae : 182 ( 21 unt; 15 def)
% Number of atoms : 460 ( 100 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 510 ( 232 ~; 228 |; 18 &)
% ( 16 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 16 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-5 aty)
% Number of variables : 161 ( 0 sgn 158 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1333,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1358,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( k4_relset_1(X1,X0,k6_relset_1(X0,X1,X2)) = k5_relset_1(X0,X1,X2)
& k5_relset_1(X1,X0,k6_relset_1(X0,X1,X2)) = k4_relset_1(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_relset_1) ).
fof(f1372,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> ( k10_relset_1(X0,X1,X2,X0) = k5_relset_1(X0,X1,X2)
& k11_relset_1(X0,X1,X2,X1) = k4_relset_1(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_relset_1) ).
fof(f1373,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> ( k10_relset_1(X1,X0,X2,k11_relset_1(X1,X0,X2,X0)) = k5_relset_1(X1,X0,X2)
& k11_relset_1(X1,X0,X2,k10_relset_1(X1,X0,X2,X1)) = k4_relset_1(X1,X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_relset_1) ).
fof(f1392,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1394,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1409,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f1411,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_relset_1) ).
fof(f1419,axiom,
! [X0,X1,X2,X3] :
( m1_relset_1(X2,X0,X1)
=> k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f4077,axiom,
! [X0] :
( v1_relat_1(X0)
=> ( k1_funct_5(X0) = k1_relat_1(X0)
& k2_funct_5(X0) = k2_relat_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_funct_5) ).
fof(f19066,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
& m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) )
=> m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_relset_2) ).
fof(f19122,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_relset_2) ).
fof(f19124,axiom,
! [X0,X1,X2,X3] :
( m2_relset_1(X3,X0,X1)
=> ! [X4] :
( m2_relset_1(X4,X1,X2)
=> ( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
& r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_relset_2) ).
fof(f19127,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k10_relset_1(X1,X0,X2,X1)) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k2_funct_5(X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t56_relset_2) ).
fof(f19128,conjecture,
! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) = k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,X2,k6_relset_1(X1,X0,X2)),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t57_relset_2) ).
fof(f19129,negated_conjecture,
~ ! [X0,X1,X2] :
( m2_relset_1(X2,X1,X0)
=> k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) = k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,X2,k6_relset_1(X1,X0,X2)),X1) ),
inference(negated_conjecture,[status(cth)],[f19128]) ).
fof(f19217,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(ennf_transformation,[],[f19066]) ).
fof(f19218,plain,
! [X0,X1,X2,X3,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(flattening,[],[f19217]) ).
fof(f19281,plain,
! [X0,X1,X2] :
( ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k2_funct_5(X2) = k10_relset_1(X1,X0,X2,X1) )
| ~ m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f19122]) ).
fof(f19283,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( ( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
& r1_tarski(k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)),k2_funct_5(X4)) )
| ~ m2_relset_1(X4,X1,X2) )
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f19124]) ).
fof(f19286,plain,
! [X0,X1,X2] :
( ( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
& k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k10_relset_1(X1,X0,X2,X1)) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),k2_funct_5(X2)) )
| ~ m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f19127]) ).
fof(f19287,plain,
? [X0,X1,X2] :
( k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) != k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,X2,k6_relset_1(X1,X0,X2)),X1)
& m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f19129]) ).
fof(f19318,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,[],[f1392]) ).
fof(f19319,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1333]) ).
fof(f19641,plain,
! [X0,X1,X2,X3] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1419]) ).
fof(f19700,plain,
! [X0,X1,X2] :
( ( k10_relset_1(X1,X0,X2,k11_relset_1(X1,X0,X2,X0)) = k5_relset_1(X1,X0,X2)
& k11_relset_1(X1,X0,X2,k10_relset_1(X1,X0,X2,X1)) = k4_relset_1(X1,X0,X2) )
| ~ m2_relset_1(X2,X1,X0) ),
inference(ennf_transformation,[],[f1373]) ).
fof(f19701,plain,
! [X0,X1,X2] :
( ( k10_relset_1(X0,X1,X2,X0) = k5_relset_1(X0,X1,X2)
& k11_relset_1(X0,X1,X2,X1) = k4_relset_1(X0,X1,X2) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1372]) ).
fof(f19970,plain,
! [X0] :
( ( k1_funct_5(X0) = k1_relat_1(X0)
& k2_funct_5(X0) = k2_relat_1(X0) )
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f4077]) ).
fof(f19979,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1411]) ).
fof(f19981,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1409]) ).
fof(f19982,plain,
! [X0,X1,X2] :
( ( k4_relset_1(X1,X0,k6_relset_1(X0,X1,X2)) = k5_relset_1(X0,X1,X2)
& k5_relset_1(X1,X0,k6_relset_1(X0,X1,X2)) = k4_relset_1(X0,X1,X2) )
| ~ m2_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1358]) ).
fof(f20007,plain,
( k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) != k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9)
& m2_relset_1(sK10,sK9,sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10)],[f19287]) ).
fof(f20018,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,[],[f1394]) ).
fof(f20279,plain,
! [X2,X3,X0,X1,X4] :
( m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f19218]) ).
fof(f20360,plain,
! [X2,X0,X1] :
( k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f19281]) ).
fof(f20365,plain,
! [X2,X3,X0,X1,X4] :
( k2_funct_5(k9_relset_2(X0,X1,X2,X3,X4)) = k10_relset_1(X1,X2,X4,k2_funct_5(X3))
| ~ m2_relset_1(X4,X1,X2)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f19283]) ).
fof(f20371,plain,
! [X2,X0,X1] :
( k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f19286]) ).
fof(f20372,plain,
m2_relset_1(sK10,sK9,sK8),
inference(cnf_transformation,[],[f20007]) ).
fof(f20373,plain,
k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) != k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9),
inference(cnf_transformation,[],[f20007]) ).
fof(f20428,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20018]) ).
fof(f20434,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,[],[f19318]) ).
fof(f20435,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f19319]) ).
fof(f20901,plain,
! [X2,X3,X0,X1] :
( k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19641]) ).
fof(f21038,plain,
! [X2,X0,X1] :
( k5_relset_1(X1,X0,X2) = k10_relset_1(X1,X0,X2,k11_relset_1(X1,X0,X2,X0))
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f19700]) ).
fof(f21039,plain,
! [X2,X0,X1] :
( k4_relset_1(X0,X1,X2) = k11_relset_1(X0,X1,X2,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19701]) ).
fof(f21040,plain,
! [X2,X0,X1] :
( k5_relset_1(X0,X1,X2) = k10_relset_1(X0,X1,X2,X0)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19701]) ).
fof(f21417,plain,
! [X0] :
( k2_relat_1(X0) = k2_funct_5(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19970]) ).
fof(f21418,plain,
! [X0] :
( k1_relat_1(X0) = k1_funct_5(X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f19970]) ).
fof(f21459,plain,
! [X2,X0,X1] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19979]) ).
fof(f21461,plain,
! [X2,X0,X1] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19981]) ).
fof(f21462,plain,
! [X2,X0,X1] :
( k5_relset_1(X1,X0,k6_relset_1(X0,X1,X2)) = k4_relset_1(X0,X1,X2)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19982]) ).
fof(f21463,plain,
! [X2,X0,X1] :
( k5_relset_1(X0,X1,X2) = k4_relset_1(X1,X0,k6_relset_1(X0,X1,X2))
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f19982]) ).
fof(f21992,definition,
( spl337_1
<=> m2_relset_1(sK10,sK9,sK8) ),
introduced(definition,[new_symbols(definition,[spl337_1])],[avatar_definition]) ).
fof(f21994,plain,
( m2_relset_1(sK10,sK9,sK8)
| ~ spl337_1 ),
inference(avatar_component_clause,[],[f21992]) ).
fof(f21995,plain,
spl337_1,
inference(avatar_split_clause,[],[f20372,f21992]) ).
fof(f22017,plain,
( k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) = k1_funct_5(sK10)
| ~ spl337_1 ),
inference(resolution,[],[f21994,f20371]) ).
fof(f22018,plain,
( m1_relset_1(sK10,sK9,sK8)
| ~ spl337_1 ),
inference(resolution,[],[f21994,f20428]) ).
fof(f22019,plain,
( m1_subset_1(sK10,k1_zfmisc_1(k2_zfmisc_1(sK9,sK8)))
| ~ spl337_1 ),
inference(resolution,[],[f21994,f20434]) ).
fof(f22065,plain,
( k4_relset_1(sK9,sK8,sK10) = k5_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10))
| ~ spl337_1 ),
inference(resolution,[],[f21994,f21462]) ).
fof(f22086,definition,
( spl337_2
<=> k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) = k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9) ),
introduced(definition,[new_symbols(definition,[spl337_2])],[avatar_definition]) ).
fof(f22088,plain,
( k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) != k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9)
| spl337_2 ),
inference(avatar_component_clause,[],[f22086]) ).
fof(f22089,plain,
~ spl337_2,
inference(avatar_split_clause,[],[f20373,f22086]) ).
fof(f22090,plain,
( k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9) != k1_funct_5(sK10)
| ~ spl337_1
| spl337_2 ),
inference(forward_demodulation,[],[f22088,f22017]) ).
fof(f22092,definition,
( spl337_3
<=> k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9) = k1_funct_5(sK10) ),
introduced(definition,[new_symbols(definition,[spl337_3])],[avatar_definition]) ).
fof(f22094,plain,
( k10_relset_1(sK9,sK9,k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9) != k1_funct_5(sK10)
| spl337_3 ),
inference(avatar_component_clause,[],[f22092]) ).
fof(f22095,plain,
( ~ spl337_3
| ~ spl337_1
| spl337_2 ),
inference(avatar_split_clause,[],[f22090,f22086,f21992,f22092]) ).
fof(f22099,plain,
( k1_funct_5(sK10) != k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)))
| ~ m2_relset_1(k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9,sK9)
| spl337_3 ),
inference(superposition,[],[f22094,f20360]) ).
fof(f22122,definition,
( spl337_6
<=> m1_subset_1(k6_relset_1(sK9,sK8,sK10),k1_zfmisc_1(k2_zfmisc_1(sK8,sK9))) ),
introduced(definition,[new_symbols(definition,[spl337_6])],[avatar_definition]) ).
fof(f22123,plain,
( m1_subset_1(k6_relset_1(sK9,sK8,sK10),k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl337_6 ),
inference(avatar_component_clause,[],[f22122]) ).
fof(f22124,plain,
( ~ m1_subset_1(k6_relset_1(sK9,sK8,sK10),k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| spl337_6 ),
inference(avatar_component_clause,[],[f22122]) ).
fof(f22130,plain,
( ~ m2_relset_1(k6_relset_1(sK9,sK8,sK10),sK8,sK9)
| spl337_6 ),
inference(resolution,[],[f22124,f20434]) ).
fof(f22156,definition,
( spl337_8
<=> m2_relset_1(k6_relset_1(sK9,sK8,sK10),sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl337_8])],[avatar_definition]) ).
fof(f22157,plain,
( m2_relset_1(k6_relset_1(sK9,sK8,sK10),sK8,sK9)
| ~ spl337_8 ),
inference(avatar_component_clause,[],[f22156]) ).
fof(f22158,plain,
( ~ m2_relset_1(k6_relset_1(sK9,sK8,sK10),sK8,sK9)
| spl337_8 ),
inference(avatar_component_clause,[],[f22156]) ).
fof(f22159,plain,
( ~ spl337_8
| spl337_6 ),
inference(avatar_split_clause,[],[f22130,f22122,f22156]) ).
fof(f22160,plain,
( ~ m1_relset_1(sK10,sK9,sK8)
| spl337_8 ),
inference(resolution,[],[f22158,f21461]) ).
fof(f22181,plain,
( $false
| ~ spl337_1
| spl337_8 ),
inference(forward_subsumption_resolution,[],[f22160,f22018]) ).
fof(f22182,plain,
( ~ spl337_1
| spl337_8 ),
inference(avatar_contradiction_clause,[],[f22181]) ).
fof(f22238,plain,
( k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) = k5_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10))
| ~ spl337_8 ),
inference(resolution,[],[f22157,f21040]) ).
fof(f22269,plain,
( m2_relset_1(k4_relat_1(sK10),sK8,sK9)
| ~ m1_relset_1(sK10,sK9,sK8)
| ~ spl337_8 ),
inference(superposition,[],[f22157,f21459]) ).
fof(f22270,plain,
( m2_relset_1(k4_relat_1(sK10),sK8,sK9)
| ~ spl337_1
| ~ spl337_8 ),
inference(forward_subsumption_resolution,[],[f22269,f22018]) ).
fof(f22273,plain,
( k10_relset_1(sK8,sK9,k6_relset_1(sK9,sK8,sK10),sK8) = k4_relset_1(sK9,sK8,sK10)
| ~ spl337_1
| ~ spl337_8 ),
inference(forward_demodulation,[],[f22238,f22065]) ).
fof(f22279,plain,
( k1_funct_5(sK10) = k4_relset_1(sK9,sK8,sK10)
| ~ spl337_1
| ~ spl337_8 ),
inference(forward_demodulation,[],[f22273,f22017]) ).
fof(f22758,definition,
( spl337_11
<=> m2_relset_1(k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9,sK9) ),
introduced(definition,[new_symbols(definition,[spl337_11])],[avatar_definition]) ).
fof(f22760,plain,
( ~ m2_relset_1(k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)),sK9,sK9)
| spl337_11 ),
inference(avatar_component_clause,[],[f22758]) ).
fof(f22762,definition,
( spl337_12
<=> k1_funct_5(sK10) = k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10))) ),
introduced(definition,[new_symbols(definition,[spl337_12])],[avatar_definition]) ).
fof(f22764,plain,
( k1_funct_5(sK10) != k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k6_relset_1(sK9,sK8,sK10)))
| spl337_12 ),
inference(avatar_component_clause,[],[f22762]) ).
fof(f22765,plain,
( ~ spl337_11
| ~ spl337_12
| spl337_3 ),
inference(avatar_split_clause,[],[f22099,f22092,f22762,f22758]) ).
fof(f22766,plain,
( ~ m1_subset_1(sK10,k1_zfmisc_1(k2_zfmisc_1(sK9,sK8)))
| ~ m1_subset_1(k6_relset_1(sK9,sK8,sK10),k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| spl337_11 ),
inference(resolution,[],[f22760,f20279]) ).
fof(f22789,plain,
( ~ m1_subset_1(k6_relset_1(sK9,sK8,sK10),k1_zfmisc_1(k2_zfmisc_1(sK8,sK9)))
| ~ spl337_1
| spl337_11 ),
inference(forward_subsumption_resolution,[],[f22766,f22019]) ).
fof(f22791,plain,
( $false
| ~ spl337_1
| ~ spl337_6
| spl337_11 ),
inference(forward_subsumption_resolution,[],[f22789,f22123]) ).
fof(f22792,plain,
( ~ spl337_1
| ~ spl337_6
| spl337_11 ),
inference(avatar_contradiction_clause,[],[f22791]) ).
fof(f22794,plain,
( k1_funct_5(sK10) != k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k4_relat_1(sK10)))
| ~ m1_relset_1(sK10,sK9,sK8)
| spl337_12 ),
inference(superposition,[],[f22764,f21459]) ).
fof(f22805,plain,
( k1_funct_5(sK10) != k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k4_relat_1(sK10)))
| ~ spl337_1
| spl337_12 ),
inference(forward_subsumption_resolution,[],[f22794,f22018]) ).
fof(f22810,definition,
( spl337_13
<=> k1_funct_5(sK10) = k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k4_relat_1(sK10))) ),
introduced(definition,[new_symbols(definition,[spl337_13])],[avatar_definition]) ).
fof(f22812,plain,
( k1_funct_5(sK10) != k2_funct_5(k9_relset_2(sK9,sK8,sK9,sK10,k4_relat_1(sK10)))
| spl337_13 ),
inference(avatar_component_clause,[],[f22810]) ).
fof(f22813,plain,
( ~ spl337_13
| ~ spl337_1
| spl337_12 ),
inference(avatar_split_clause,[],[f22805,f22762,f21992,f22810]) ).
fof(f22818,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_funct_5(sK10))
| ~ m2_relset_1(k4_relat_1(sK10),sK8,sK9)
| ~ m2_relset_1(sK10,sK9,sK8)
| spl337_13 ),
inference(superposition,[],[f22812,f20365]) ).
fof(f22825,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_funct_5(sK10))
| ~ m2_relset_1(sK10,sK9,sK8)
| ~ spl337_1
| ~ spl337_8
| spl337_13 ),
inference(forward_subsumption_resolution,[],[f22818,f22270]) ).
fof(f22827,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_funct_5(sK10))
| ~ spl337_1
| ~ spl337_8
| spl337_13 ),
inference(forward_subsumption_resolution,[],[f22825,f21994]) ).
fof(f23112,definition,
( spl337_21
<=> k1_funct_5(sK10) = k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_funct_5(sK10)) ),
introduced(definition,[new_symbols(definition,[spl337_21])],[avatar_definition]) ).
fof(f23114,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_funct_5(sK10))
| spl337_21 ),
inference(avatar_component_clause,[],[f23112]) ).
fof(f23115,plain,
( ~ spl337_21
| ~ spl337_1
| ~ spl337_8
| spl337_13 ),
inference(avatar_split_clause,[],[f22827,f22810,f22156,f21992,f23112]) ).
fof(f23123,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_relat_1(sK10))
| ~ v1_relat_1(sK10)
| spl337_21 ),
inference(superposition,[],[f23114,f21417]) ).
fof(f23290,definition,
( spl337_23
<=> v1_relat_1(sK10) ),
introduced(definition,[new_symbols(definition,[spl337_23])],[avatar_definition]) ).
fof(f23291,plain,
( v1_relat_1(sK10)
| ~ spl337_23 ),
inference(avatar_component_clause,[],[f23290]) ).
fof(f23292,plain,
( ~ v1_relat_1(sK10)
| spl337_23 ),
inference(avatar_component_clause,[],[f23290]) ).
fof(f23298,plain,
( ! [X0,X1] : ~ m1_subset_1(sK10,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| spl337_23 ),
inference(resolution,[],[f23292,f20435]) ).
fof(f23310,plain,
( $false
| ~ spl337_1
| spl337_23 ),
inference(backward_subsumption_resolution,[],[f22019,f23298]) ).
fof(f23311,plain,
( ~ spl337_1
| spl337_23 ),
inference(avatar_contradiction_clause,[],[f23310]) ).
fof(f23380,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_relat_1(sK10))
| spl337_21
| ~ spl337_23 ),
inference(backward_subsumption_resolution,[],[f23123,f23291]) ).
fof(f23740,plain,
( k2_funct_5(sK10) = k2_relat_1(sK10)
| ~ spl337_23 ),
inference(resolution,[],[f23291,f21417]) ).
fof(f23741,plain,
( k1_funct_5(sK10) = k1_relat_1(sK10)
| ~ spl337_23 ),
inference(resolution,[],[f23291,f21418]) ).
fof(f24035,definition,
( spl337_31
<=> m1_relset_1(sK10,sK9,sK8) ),
introduced(definition,[new_symbols(definition,[spl337_31])],[avatar_definition]) ).
fof(f24037,plain,
( m1_relset_1(sK10,sK9,sK8)
| ~ spl337_31 ),
inference(avatar_component_clause,[],[f24035]) ).
fof(f24038,plain,
( spl337_31
| ~ spl337_1 ),
inference(avatar_split_clause,[],[f22018,f21992,f24035]) ).
fof(f24172,plain,
( ! [X0] : k10_relset_1(sK9,sK8,sK10,X0) = k9_relat_1(sK10,X0)
| ~ spl337_31 ),
inference(resolution,[],[f24037,f20901]) ).
fof(f24176,plain,
( k6_relset_1(sK9,sK8,sK10) = k4_relat_1(sK10)
| ~ spl337_31 ),
inference(resolution,[],[f24037,f21459]) ).
fof(f24181,definition,
( spl337_39
<=> ! [X0] : k10_relset_1(sK9,sK8,sK10,X0) = k9_relat_1(sK10,X0) ),
introduced(definition,[new_symbols(definition,[spl337_39])],[avatar_definition]) ).
fof(f24182,plain,
( ! [X0] : k10_relset_1(sK9,sK8,sK10,X0) = k9_relat_1(sK10,X0)
| ~ spl337_39 ),
inference(avatar_component_clause,[],[f24181]) ).
fof(f24183,plain,
( spl337_39
| ~ spl337_31 ),
inference(avatar_split_clause,[],[f24172,f24035,f24181]) ).
fof(f24188,plain,
( k9_relat_1(sK10,sK9) = k5_relset_1(sK9,sK8,sK10)
| ~ m2_relset_1(sK10,sK9,sK8)
| ~ spl337_39 ),
inference(superposition,[],[f21040,f24182]) ).
fof(f24191,plain,
( k2_funct_5(sK10) = k9_relat_1(sK10,sK9)
| ~ m2_relset_1(sK10,sK9,sK8)
| ~ spl337_39 ),
inference(superposition,[],[f20360,f24182]) ).
fof(f24206,plain,
( k2_funct_5(sK10) = k9_relat_1(sK10,sK9)
| ~ spl337_1
| ~ spl337_39 ),
inference(forward_subsumption_resolution,[],[f24191,f21994]) ).
fof(f24209,plain,
( k9_relat_1(sK10,sK9) = k5_relset_1(sK9,sK8,sK10)
| ~ spl337_1
| ~ spl337_39 ),
inference(forward_subsumption_resolution,[],[f24188,f21994]) ).
fof(f24215,plain,
( k2_relat_1(sK10) = k9_relat_1(sK10,sK9)
| ~ spl337_1
| ~ spl337_23
| ~ spl337_39 ),
inference(forward_demodulation,[],[f24206,f23740]) ).
fof(f24231,definition,
( spl337_40
<=> k6_relset_1(sK9,sK8,sK10) = k4_relat_1(sK10) ),
introduced(definition,[new_symbols(definition,[spl337_40])],[avatar_definition]) ).
fof(f24233,plain,
( k6_relset_1(sK9,sK8,sK10) = k4_relat_1(sK10)
| ~ spl337_40 ),
inference(avatar_component_clause,[],[f24231]) ).
fof(f24234,plain,
( spl337_40
| ~ spl337_31 ),
inference(avatar_split_clause,[],[f24176,f24035,f24231]) ).
fof(f24261,plain,
( k4_relset_1(sK9,sK8,sK10) = k5_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ m2_relset_1(sK10,sK9,sK8)
| ~ spl337_40 ),
inference(superposition,[],[f21462,f24233]) ).
fof(f24262,plain,
( k5_relset_1(sK9,sK8,sK10) = k4_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ m2_relset_1(sK10,sK9,sK8)
| ~ spl337_40 ),
inference(superposition,[],[f21463,f24233]) ).
fof(f24263,plain,
( k5_relset_1(sK9,sK8,sK10) = k4_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ spl337_1
| ~ spl337_40 ),
inference(forward_subsumption_resolution,[],[f24262,f21994]) ).
fof(f24264,plain,
( k4_relset_1(sK9,sK8,sK10) = k5_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ spl337_1
| ~ spl337_40 ),
inference(forward_subsumption_resolution,[],[f24261,f21994]) ).
fof(f24275,plain,
( k9_relat_1(sK10,sK9) = k4_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ spl337_1
| ~ spl337_39
| ~ spl337_40 ),
inference(forward_demodulation,[],[f24263,f24209]) ).
fof(f24276,plain,
( k1_funct_5(sK10) = k5_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ spl337_1
| ~ spl337_8
| ~ spl337_40 ),
inference(forward_demodulation,[],[f24264,f22279]) ).
fof(f24284,plain,
( k2_relat_1(sK10) = k4_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ spl337_1
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40 ),
inference(forward_demodulation,[],[f24275,f24215]) ).
fof(f24285,plain,
( k1_relat_1(sK10) = k5_relset_1(sK8,sK9,k4_relat_1(sK10))
| ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_40 ),
inference(forward_demodulation,[],[f24276,f23741]) ).
fof(f24453,definition,
( spl337_45
<=> m2_relset_1(k4_relat_1(sK10),sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl337_45])],[avatar_definition]) ).
fof(f24455,plain,
( m2_relset_1(k4_relat_1(sK10),sK8,sK9)
| ~ spl337_45 ),
inference(avatar_component_clause,[],[f24453]) ).
fof(f24456,plain,
( spl337_45
| ~ spl337_1
| ~ spl337_8 ),
inference(avatar_split_clause,[],[f22270,f22156,f21992,f24453]) ).
fof(f24510,plain,
( k5_relset_1(sK8,sK9,k4_relat_1(sK10)) = k10_relset_1(sK8,sK9,k4_relat_1(sK10),k11_relset_1(sK8,sK9,k4_relat_1(sK10),sK9))
| ~ spl337_45 ),
inference(resolution,[],[f24455,f21038]) ).
fof(f24511,plain,
( k4_relset_1(sK8,sK9,k4_relat_1(sK10)) = k11_relset_1(sK8,sK9,k4_relat_1(sK10),sK9)
| ~ spl337_45 ),
inference(resolution,[],[f24455,f21039]) ).
fof(f24556,plain,
( k2_relat_1(sK10) = k11_relset_1(sK8,sK9,k4_relat_1(sK10),sK9)
| ~ spl337_1
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40
| ~ spl337_45 ),
inference(forward_demodulation,[],[f24511,f24284]) ).
fof(f24557,plain,
( k1_relat_1(sK10) = k10_relset_1(sK8,sK9,k4_relat_1(sK10),k11_relset_1(sK8,sK9,k4_relat_1(sK10),sK9))
| ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_40
| ~ spl337_45 ),
inference(forward_demodulation,[],[f24510,f24285]) ).
fof(f24567,plain,
( k1_relat_1(sK10) = k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_relat_1(sK10))
| ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40
| ~ spl337_45 ),
inference(forward_demodulation,[],[f24557,f24556]) ).
fof(f24861,definition,
( spl337_53
<=> k1_funct_5(sK10) = k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_relat_1(sK10)) ),
introduced(definition,[new_symbols(definition,[spl337_53])],[avatar_definition]) ).
fof(f24863,plain,
( k1_funct_5(sK10) != k10_relset_1(sK8,sK9,k4_relat_1(sK10),k2_relat_1(sK10))
| spl337_53 ),
inference(avatar_component_clause,[],[f24861]) ).
fof(f24864,plain,
( ~ spl337_53
| spl337_21
| ~ spl337_23 ),
inference(avatar_split_clause,[],[f23380,f23290,f23112,f24861]) ).
fof(f24865,plain,
( k1_funct_5(sK10) != k1_relat_1(sK10)
| ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40
| ~ spl337_45
| spl337_53 ),
inference(forward_demodulation,[],[f24863,f24567]) ).
fof(f24866,plain,
( $false
| ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40
| ~ spl337_45
| spl337_53 ),
inference(forward_subsumption_resolution,[],[f24865,f23741]) ).
fof(f24867,plain,
( ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40
| ~ spl337_45
| spl337_53 ),
inference(avatar_contradiction_clause,[],[f24866]) ).
cnf(s1,plain,
spl337_1,
inference(sat_conversion,[],[f21995]) ).
cnf(s2,plain,
~ spl337_2,
inference(sat_conversion,[],[f22089]) ).
cnf(s3,plain,
( ~ spl337_1
| spl337_2
| ~ spl337_3 ),
inference(sat_conversion,[],[f22095]) ).
cnf(s7,plain,
( spl337_6
| ~ spl337_8 ),
inference(sat_conversion,[],[f22159]) ).
cnf(s8,plain,
( ~ spl337_1
| spl337_8 ),
inference(sat_conversion,[],[f22182]) ).
cnf(s11,plain,
( spl337_3
| ~ spl337_11
| ~ spl337_12 ),
inference(sat_conversion,[],[f22765]) ).
cnf(s12,plain,
( ~ spl337_1
| ~ spl337_6
| spl337_11 ),
inference(sat_conversion,[],[f22792]) ).
cnf(s13,plain,
( ~ spl337_1
| spl337_12
| ~ spl337_13 ),
inference(sat_conversion,[],[f22813]) ).
cnf(s21,plain,
( ~ spl337_1
| ~ spl337_8
| spl337_13
| ~ spl337_21 ),
inference(sat_conversion,[],[f23115]) ).
cnf(s24,plain,
( ~ spl337_1
| spl337_23 ),
inference(sat_conversion,[],[f23311]) ).
cnf(s31,plain,
( ~ spl337_1
| spl337_31 ),
inference(sat_conversion,[],[f24038]) ).
cnf(s39,plain,
( ~ spl337_31
| spl337_39 ),
inference(sat_conversion,[],[f24183]) ).
cnf(s40,plain,
( ~ spl337_31
| spl337_40 ),
inference(sat_conversion,[],[f24234]) ).
cnf(s45,plain,
( ~ spl337_1
| ~ spl337_8
| spl337_45 ),
inference(sat_conversion,[],[f24456]) ).
cnf(s52,plain,
( spl337_21
| ~ spl337_23
| ~ spl337_53 ),
inference(sat_conversion,[],[f24864]) ).
cnf(s53,plain,
( ~ spl337_1
| ~ spl337_8
| ~ spl337_23
| ~ spl337_39
| ~ spl337_40
| ~ spl337_45
| spl337_53 ),
inference(sat_conversion,[],[f24867]) ).
cnf(s57,plain,
spl337_31,
inference(rat,[],[s31,s1]) ).
cnf(s58,plain,
spl337_23,
inference(rat,[],[s24,s1]) ).
cnf(s59,plain,
spl337_8,
inference(rat,[],[s8,s1]) ).
cnf(s61,plain,
~ spl337_3,
inference(rat,[],[s3,s2,s1]) ).
cnf(s64,plain,
spl337_40,
inference(rat,[],[s40,s57]) ).
cnf(s65,plain,
spl337_39,
inference(rat,[],[s39,s57]) ).
cnf(s69,plain,
spl337_45,
inference(rat,[],[s45,s1,s59]) ).
cnf(s71,plain,
spl337_6,
inference(rat,[],[s7,s59]) ).
cnf(s75,plain,
spl337_53,
inference(rat,[],[s53,s59,s58,s64,s65,s1,s69]) ).
cnf(s78,plain,
spl337_11,
inference(rat,[],[s12,s1,s71]) ).
cnf(s80,plain,
spl337_21,
inference(rat,[],[s52,s58,s75]) ).
cnf(s86,plain,
~ spl337_12,
inference(rat,[],[s11,s61,s78]) ).
cnf(s91,plain,
spl337_13,
inference(rat,[],[s21,s59,s1,s80]) ).
cnf(s95,plain,
$false,
inference(rat,[],[s13,s1,s91,s86]) ).
fof(f24868,plain,
$false,
inference(avatar_sat_refutation,[],[s95]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU445+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n002.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 05:38:49 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.14/5.21 % (51954)Detected formulas, will run a generic FOF schedule.
% 13.14/5.21 % (52613)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=3707509103:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 13.14/5.21 % (52618)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=613640874:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 13.14/5.21 % (52617)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=62831107:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 13.14/5.21 % (52616)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3129138202:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 13.14/5.21 % (52619)dis-21_1_sil=8000:lcm=predicate:random_seed=3320799165:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 13.14/5.21 % (52614)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=3904330114:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 13.14/5.21 % (52615)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=68782655:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 13.14/5.21 % (52618)Instruction limit reached!
% 13.14/5.21 % (52618)------------------------------
% 13.14/5.21 % (52618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.21 % (52618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.21 % (52618)CaDiCaL version: 2.1.3
% 13.14/5.21 % (52618)Termination reason: Instruction limit
% 13.14/5.21 % (52618)Termination phase: Property scanning
% 13.14/5.21 % (52618)Time elapsed: 0.109 s
% 13.14/5.21 % (52618)Peak memory usage: 112 MB
% 13.14/5.21 % (52618)Instructions burned: 139 (million)
% 13.14/5.21 % (52616)Instruction limit reached!
% 13.14/5.21 % (52616)------------------------------
% 13.14/5.21 % (52616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.21 % (52616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.21 % (52616)CaDiCaL version: 2.1.3
% 13.14/5.21 % (52616)Termination reason: Instruction limit
% 13.14/5.21 % (52616)Termination phase: SInE selection
% 13.14/5.21 % (52616)Time elapsed: 0.119 s
% 13.14/5.21 % (52616)Peak memory usage: 112 MB
% 13.14/5.21 % (52616)Instructions burned: 110 (million)
% 13.14/5.21 % (52619)Instruction limit reached!
% 13.14/5.21 % (52619)------------------------------
% 13.14/5.21 % (52619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.21 % (52619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.21 % (52619)CaDiCaL version: 2.1.3
% 13.14/5.21 % (52619)Termination reason: Instruction limit
% 13.14/5.21 % (52619)Termination phase: SInE selection
% 13.14/5.21 % (52619)Time elapsed: 0.128 s
% 13.14/5.21 % (52619)Peak memory usage: 112 MB
% 13.14/5.21 % (52619)Instructions burned: 129 (million)
% 13.14/5.21 % (52617)Instruction limit reached!
% 13.14/5.21 % (52617)------------------------------
% 13.14/5.21 % (52617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.21 % (52617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.21 % (52617)CaDiCaL version: 2.1.3
% 13.14/5.21 % (52617)Termination reason: Instruction limit
% 13.14/5.21 % (52617)Termination phase: Preprocessing 1
% 13.14/5.21 % (52617)Time elapsed: 0.142 s
% 13.14/5.21 % (52617)Peak memory usage: 113 MB
% 13.14/5.21 % (52617)Instructions burned: 119 (million)
% 13.14/5.21 % (52659)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3398934854:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 13.14/5.21 % (52661)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=3955897077:s2a=on:i=248:s2at=1.23:gtg=position_2985 on theBenchmark for (2985ds/248Mi)
% 13.14/5.21 % (52660)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4094003086:i=325:sd=1:ss=axioms:sgt=32_2985 on theBenchmark for (2985ds/325Mi)
% 13.14/5.21 % (52658)lrs+10_1_sil=8000:sp=occurrence:random_seed=1305588425:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 13.14/5.21 % (52659)Instruction limit reached!
% 13.14/5.21 % (52659)------------------------------
% 13.14/5.21 % (52659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52659)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52659)Termination reason: Instruction limit
% 13.14/5.22 % (52659)Termination phase: Property scanning
% 13.14/5.22 % (52659)Time elapsed: 0.132 s
% 13.14/5.22 % (52659)Peak memory usage: 112 MB
% 13.14/5.22 % (52659)Instructions burned: 158 (million)
% 13.14/5.22 % (52660)Refutation not found, incomplete strategy
% 13.14/5.22 % (52660)------------------------------
% 13.14/5.22 % (52660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52660)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52660)Termination reason: Refutation not found, incomplete strategy
% 13.14/5.22 % (52660)Time elapsed: 0.159 s
% 13.14/5.22 % (52660)Peak memory usage: 118 MB
% 13.14/5.22 % (52660)Instructions burned: 122 (million)
% 13.14/5.22 % (52661)Instruction limit reached!
% 13.14/5.22 % (52661)------------------------------
% 13.14/5.22 % (52661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52661)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52661)Termination reason: Instruction limit
% 13.14/5.22 % (52661)Termination phase: Property scanning
% 13.14/5.22 % (52661)Time elapsed: 0.205 s
% 13.14/5.22 % (52661)Peak memory usage: 112 MB
% 13.14/5.22 % (52661)Instructions burned: 248 (million)
% 13.14/5.22 % (52658)Instruction limit reached!
% 13.14/5.22 % (52658)------------------------------
% 13.14/5.22 % (52658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52658)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52658)Termination reason: Instruction limit
% 13.14/5.22 % (52658)Termination phase: Saturation
% 13.14/5.22 % (52658)Time elapsed: 0.322 s
% 13.14/5.22 % (52658)Peak memory usage: 119 MB
% 13.14/5.22 % (52658)Instructions burned: 286 (million)
% 13.14/5.22 % (52666)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2310054695:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2981 on theBenchmark for (2981ds/294Mi)
% 13.14/5.22 % (52667)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3196610220:i=2350_2980 on theBenchmark for (2980ds/2350Mi)
% 13.14/5.22 % (52660)------------------------------
% 13.14/5.22 % (52660)------------------------------
% 13.14/5.22 % (52668)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2161248749:cts=off:i=113:fsr=off:ss=included:sgt=4_2979 on theBenchmark for (2979ds/113Mi)
% 13.14/5.22 % (52666)Instruction limit reached!
% 13.14/5.22 % (52666)------------------------------
% 13.14/5.22 % (52666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52666)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52666)Termination reason: Instruction limit
% 13.14/5.22 % (52666)Termination phase: Saturation
% 13.14/5.22 % (52666)Time elapsed: 0.328 s
% 13.14/5.22 % (52666)Peak memory usage: 119 MB
% 13.14/5.22 % (52666)Instructions burned: 294 (million)
% 13.14/5.22 % (52668)Instruction limit reached!
% 13.14/5.22 % (52668)------------------------------
% 13.14/5.22 % (52668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52668)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52668)Termination reason: Instruction limit
% 13.14/5.22 % (52668)Termination phase: SInE selection
% 13.14/5.22 % (52668)Time elapsed: 0.143 s
% 13.14/5.22 % (52668)Peak memory usage: 112 MB
% 13.14/5.22 % (52668)Instructions burned: 116 (million)
% 13.14/5.22 % (52671)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=954240856:i=127:av=off:fsr=off:sup=off_2976 on theBenchmark for (2976ds/127Mi)
% 13.14/5.22 % (52671)Instruction limit reached!
% 13.14/5.22 % (52671)------------------------------
% 13.14/5.22 % (52671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52671)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52671)Termination reason: Instruction limit
% 13.14/5.22 % (52671)Termination phase: Preprocessing 1
% 13.14/5.22 % (52671)Time elapsed: 0.149 s
% 13.14/5.22 % (52671)Peak memory usage: 113 MB
% 13.14/5.22 % (52671)Instructions burned: 127 (million)
% 13.14/5.22 % (52673)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=527221944:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2975 on theBenchmark for (2975ds/114Mi)
% 13.14/5.22 % (52674)lrs+10_1_sil=8000:sp=occurrence:random_seed=3970868031:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 13.14/5.22 % (52673)Instruction limit reached!
% 13.14/5.22 % (52673)------------------------------
% 13.14/5.22 % (52673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52673)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52673)Termination reason: Instruction limit
% 13.14/5.22 % (52673)Termination phase: Property scanning
% 13.14/5.22 % (52673)Time elapsed: 0.096 s
% 13.14/5.22 % (52673)Peak memory usage: 112 MB
% 13.14/5.22 % (52673)Instructions burned: 114 (million)
% 13.14/5.22 % (52677)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2118813740:i=437:sd=1:aac=none:ss=included_2972 on theBenchmark for (2972ds/437Mi)
% 13.14/5.22 % (52679)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2021727896:i=5202:ss=axioms:sgt=16_2971 on theBenchmark for (2971ds/5202Mi)
% 13.14/5.22 % (52677)Instruction limit reached!
% 13.14/5.22 % (52677)------------------------------
% 13.14/5.22 % (52677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52677)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52677)Termination reason: Instruction limit
% 13.14/5.22 % (52677)Termination phase: Saturation
% 13.14/5.22 % (52677)Time elapsed: 0.518 s
% 13.14/5.22 % (52677)Peak memory usage: 121 MB
% 13.14/5.22 % (52677)Instructions burned: 438 (million)
% 13.14/5.22 % (52674)Instruction limit reached!
% 13.14/5.22 % (52674)------------------------------
% 13.14/5.22 % (52674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52674)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52674)Termination reason: Instruction limit
% 13.14/5.22 % (52674)Termination phase: Saturation
% 13.14/5.22 % (52674)Time elapsed: 0.908 s
% 13.14/5.22 % (52674)Peak memory usage: 132 MB
% 13.14/5.22 % (52674)Instructions burned: 908 (million)
% 13.14/5.22 % (52615)First to succeed.
% 13.14/5.22 % (52615)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-51954"
% 13.14/5.22 % (52682)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=952899614:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2963 on theBenchmark for (2963ds/134Mi)
% 13.14/5.22 % (52683)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2956759236:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 13.14/5.22 % (52682)Instruction limit reached!
% 13.14/5.22 % (52682)------------------------------
% 13.14/5.22 % (52682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/5.22 % (52682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/5.22 % (52682)CaDiCaL version: 2.1.3
% 13.14/5.22 % (52682)Termination reason: Instruction limit
% 13.14/5.22 % (52682)Termination phase: NewCNF
% 13.14/5.22 % (52682)Time elapsed: 0.185 s
% 13.14/5.22 % (52682)Peak memory usage: 114 MB
% 13.14/5.22 % (52682)Instructions burned: 134 (million)
% 13.14/5.22 % (52615)Refutation found. Thanks to Tanya!
% 13.14/5.22 % SZS status Theorem for theBenchmark
% 13.14/5.22 % SZS output start Proof for theBenchmark
% See solution above
% 24.50/5.58 % (52615)------------------------------
% 24.50/5.58 % (52615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.50/5.58 % (52615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.50/5.58 % (52615)CaDiCaL version: 2.1.3
% 24.50/5.58 % (52615)Termination reason: Refutation
% 24.50/5.58 % (52615)Time elapsed: 2.567 s
% 24.50/5.58 % (52615)Peak memory usage: 178 MB
% 24.50/5.58 % (52615)Instructions burned: 2310 (million)
% 24.50/5.58 % (52615)------------------------------
% 24.50/5.58 % (52615)------------------------------
% 24.50/5.58 % (51954)Success in time 4.346 s
% 24.50/5.58 % Vampire exiting
%------------------------------------------------------------------------------