%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU450+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 : 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:11 PM UTC 2026
% Result : Theorem 63.16s 14.79s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 49
% Syntax : Number of formulae : 265 ( 69 unt; 41 def)
% Number of atoms : 783 ( 59 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 980 ( 462 ~; 451 |; 17 &)
% ( 34 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 38 ( 36 usr; 33 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-4 aty)
% Number of variables : 154 ( 0 sgn 149 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
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(f1498,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relset_1) ).
fof(f71075,axiom,
! [X0,X1,X2,X3] :
( ( m1_subset_1(X2,k1_zfmisc_1(X0))
& m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
=> m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k8_relset_2) ).
fof(f71114,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X0))
=> ! [X4] :
( m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> ( r1_tarski(X2,X3)
=> r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_relset_2) ).
fof(f71145,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( r1_tarski(X2,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)))
& r1_tarski(X3,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_relset_2) ).
fof(f71146,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( k8_relset_2(X0,X1,X2,X4) = k8_relset_2(X0,X1,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)),X4)
& k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)) = k8_relset_2(X1,X0,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4),k6_relset_1(X0,X1,X4)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t64_relset_2) ).
fof(f71147,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(X1))
=> ! [X4] :
( m2_relset_1(X4,X0,X1)
=> ( k8_relset_2(X0,X1,X2,X4) = k8_relset_2(X0,X1,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)),X4)
& k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)) = k8_relset_2(X1,X0,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4),k6_relset_1(X0,X1,X4)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f71146]) ).
fof(f71229,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f71075]) ).
fof(f71230,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(flattening,[],[f71229]) ).
fof(f71272,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71114]) ).
fof(f71273,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4))
| ~ r1_tarski(X2,X3)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f71272]) ).
fof(f71309,plain,
! [X0,X1,X2] :
( ! [X3] :
( ! [X4] :
( ( r1_tarski(X2,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)))
& r1_tarski(X3,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4)) )
| ~ m2_relset_1(X4,X0,X1) )
| ~ m1_subset_1(X3,k1_zfmisc_1(X1)) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71145]) ).
fof(f71310,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ( k8_relset_2(X0,X1,X2,X4) != k8_relset_2(X0,X1,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)),X4)
| k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)) != k8_relset_2(X1,X0,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4),k6_relset_1(X0,X1,X4)) )
& m2_relset_1(X4,X0,X1) )
& m1_subset_1(X3,k1_zfmisc_1(X1)) )
& m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71147]) ).
fof(f71411,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(f72324,plain,
! [X0,X1,X2] :
( m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1498]) ).
fof(f72382,plain,
( ( k8_relset_2(sK27,sK28,sK29,sK31) != k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,sK29,sK31),k6_relset_1(sK27,sK28,sK31)),sK31)
| k8_relset_2(sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK31)) != k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK31)),sK31),k6_relset_1(sK27,sK28,sK31)) )
& m2_relset_1(sK31,sK27,sK28)
& m1_subset_1(sK30,k1_zfmisc_1(sK28))
& m1_subset_1(sK29,k1_zfmisc_1(sK27)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30,sK31]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29),skolemize(X3,sK30),skolemize(X4,sK31)],[f71310]) ).
fof(f72408,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(f72548,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f72549,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f72548]) ).
fof(f72801,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| m1_subset_1(k8_relset_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f71230]) ).
fof(f72855,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| ~ r1_tarski(X2,X3)
| r1_tarski(k8_relset_2(X0,X1,X3,X4),k8_relset_2(X0,X1,X2,X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71273]) ).
fof(f72904,plain,
! [X2,X3,X0,X1,X4] :
( r1_tarski(X3,k8_relset_2(X0,X1,k8_relset_2(X1,X0,X3,k6_relset_1(X0,X1,X4)),X4))
| ~ m2_relset_1(X4,X0,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71309]) ).
fof(f72905,plain,
! [X2,X3,X0,X1,X4] :
( ~ m2_relset_1(X4,X0,X1)
| r1_tarski(X2,k8_relset_2(X1,X0,k8_relset_2(X0,X1,X2,X4),k6_relset_1(X0,X1,X4)))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f71309]) ).
fof(f72906,plain,
m1_subset_1(sK29,k1_zfmisc_1(sK27)),
inference(cnf_transformation,[],[f72382]) ).
fof(f72907,plain,
m1_subset_1(sK30,k1_zfmisc_1(sK28)),
inference(cnf_transformation,[],[f72382]) ).
fof(f72908,plain,
m2_relset_1(sK31,sK27,sK28),
inference(cnf_transformation,[],[f72382]) ).
fof(f72909,plain,
( k8_relset_2(sK27,sK28,sK29,sK31) != k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,sK29,sK31),k6_relset_1(sK27,sK28,sK31)),sK31)
| k8_relset_2(sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK31)) != k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,sK30,k6_relset_1(sK27,sK28,sK31)),sK31),k6_relset_1(sK27,sK28,sK31)) ),
inference(cnf_transformation,[],[f72382]) ).
fof(f73057,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72408]) ).
fof(f73072,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,[],[f71411]) ).
fof(f73675,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| X0 = X1
| ~ r1_tarski(X1,X0) ),
inference(cnf_transformation,[],[f72549]) ).
fof(f74484,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f72324]) ).
fof(f75282,definition,
sF305 = k8_relset_2(sK27,sK28,sK29,sK31),
introduced(definition,[new_symbols(definition,[sF305])],[function_definition]) ).
fof(f75283,plain,
k8_relset_2(sK27,sK28,sK29,sK31) = sF305,
inference(reorient_equations,[],[f75282]) ).
fof(f75284,definition,
sF306 = k6_relset_1(sK27,sK28,sK31),
introduced(definition,[new_symbols(definition,[sF306])],[function_definition]) ).
fof(f75285,plain,
k6_relset_1(sK27,sK28,sK31) = sF306,
inference(reorient_equations,[],[f75284]) ).
fof(f75286,definition,
sF307 = k8_relset_2(sK28,sK27,sF305,sF306),
introduced(definition,[new_symbols(definition,[sF307])],[function_definition]) ).
fof(f75287,plain,
k8_relset_2(sK28,sK27,sF305,sF306) = sF307,
inference(reorient_equations,[],[f75286]) ).
fof(f75288,definition,
sF308 = k8_relset_2(sK27,sK28,sF307,sK31),
introduced(definition,[new_symbols(definition,[sF308])],[function_definition]) ).
fof(f75289,plain,
k8_relset_2(sK27,sK28,sF307,sK31) = sF308,
inference(reorient_equations,[],[f75288]) ).
fof(f75290,definition,
sF309 = k8_relset_2(sK28,sK27,sK30,sF306),
introduced(definition,[new_symbols(definition,[sF309])],[function_definition]) ).
fof(f75291,plain,
k8_relset_2(sK28,sK27,sK30,sF306) = sF309,
inference(reorient_equations,[],[f75290]) ).
fof(f75292,definition,
sF310 = k8_relset_2(sK27,sK28,sF309,sK31),
introduced(definition,[new_symbols(definition,[sF310])],[function_definition]) ).
fof(f75293,plain,
k8_relset_2(sK27,sK28,sF309,sK31) = sF310,
inference(reorient_equations,[],[f75292]) ).
fof(f75294,definition,
sF311 = k8_relset_2(sK28,sK27,sF310,sF306),
introduced(definition,[new_symbols(definition,[sF311])],[function_definition]) ).
fof(f75295,plain,
k8_relset_2(sK28,sK27,sF310,sF306) = sF311,
inference(reorient_equations,[],[f75294]) ).
fof(f75296,plain,
( sF305 != sF308
| sF309 != sF311 ),
inference(definition_folding,[],[f72909,f75295,f75285,f75293,f75291,f75285,f75291,f75285,f75289,f75287,f75285,f75283,f75283]) ).
fof(f75297,definition,
sF312 = k1_zfmisc_1(sK28),
introduced(definition,[new_symbols(definition,[sF312])],[function_definition]) ).
fof(f75298,plain,
k1_zfmisc_1(sK28) = sF312,
inference(reorient_equations,[],[f75297]) ).
fof(f75299,plain,
m1_subset_1(sK30,sF312),
inference(definition_folding,[],[f72907,f75298]) ).
fof(f75300,definition,
sF313 = k1_zfmisc_1(sK27),
introduced(definition,[new_symbols(definition,[sF313])],[function_definition]) ).
fof(f75301,plain,
k1_zfmisc_1(sK27) = sF313,
inference(reorient_equations,[],[f75300]) ).
fof(f75302,plain,
m1_subset_1(sK29,sF313),
inference(definition_folding,[],[f72906,f75301]) ).
fof(f75637,definition,
( spl314_46
<=> m1_subset_1(sK29,sF313) ),
introduced(definition,[new_symbols(definition,[spl314_46])],[avatar_definition]) ).
fof(f75639,plain,
( m1_subset_1(sK29,sF313)
| ~ spl314_46 ),
inference(avatar_component_clause,[],[f75637]) ).
fof(f75640,plain,
spl314_46,
inference(avatar_split_clause,[],[f75302,f75637]) ).
fof(f75642,definition,
( spl314_47
<=> m1_subset_1(sK30,sF312) ),
introduced(definition,[new_symbols(definition,[spl314_47])],[avatar_definition]) ).
fof(f75644,plain,
( m1_subset_1(sK30,sF312)
| ~ spl314_47 ),
inference(avatar_component_clause,[],[f75642]) ).
fof(f75645,plain,
spl314_47,
inference(avatar_split_clause,[],[f75299,f75642]) ).
fof(f75647,definition,
( spl314_48
<=> m2_relset_1(sK31,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl314_48])],[avatar_definition]) ).
fof(f75649,plain,
( m2_relset_1(sK31,sK27,sK28)
| ~ spl314_48 ),
inference(avatar_component_clause,[],[f75647]) ).
fof(f75650,plain,
spl314_48,
inference(avatar_split_clause,[],[f72908,f75647]) ).
fof(f75652,definition,
( spl314_49
<=> sF309 = sF311 ),
introduced(definition,[new_symbols(definition,[spl314_49])],[avatar_definition]) ).
fof(f75656,definition,
( spl314_50
<=> sF305 = sF308 ),
introduced(definition,[new_symbols(definition,[spl314_50])],[avatar_definition]) ).
fof(f75658,plain,
( sF305 != sF308
| spl314_50 ),
inference(avatar_component_clause,[],[f75656]) ).
fof(f75659,plain,
( ~ spl314_49
| ~ spl314_50 ),
inference(avatar_split_clause,[],[f75296,f75656,f75652]) ).
fof(f75674,definition,
( spl314_52
<=> k8_relset_2(sK27,sK28,sK29,sK31) = sF305 ),
introduced(definition,[new_symbols(definition,[spl314_52])],[avatar_definition]) ).
fof(f75676,plain,
( k8_relset_2(sK27,sK28,sK29,sK31) = sF305
| ~ spl314_52 ),
inference(avatar_component_clause,[],[f75674]) ).
fof(f75677,plain,
spl314_52,
inference(avatar_split_clause,[],[f75283,f75674]) ).
fof(f75679,definition,
( spl314_53
<=> k6_relset_1(sK27,sK28,sK31) = sF306 ),
introduced(definition,[new_symbols(definition,[spl314_53])],[avatar_definition]) ).
fof(f75681,plain,
( k6_relset_1(sK27,sK28,sK31) = sF306
| ~ spl314_53 ),
inference(avatar_component_clause,[],[f75679]) ).
fof(f75682,plain,
spl314_53,
inference(avatar_split_clause,[],[f75285,f75679]) ).
fof(f75684,definition,
( spl314_54
<=> k8_relset_2(sK28,sK27,sF305,sF306) = sF307 ),
introduced(definition,[new_symbols(definition,[spl314_54])],[avatar_definition]) ).
fof(f75686,plain,
( k8_relset_2(sK28,sK27,sF305,sF306) = sF307
| ~ spl314_54 ),
inference(avatar_component_clause,[],[f75684]) ).
fof(f75687,plain,
spl314_54,
inference(avatar_split_clause,[],[f75287,f75684]) ).
fof(f75689,definition,
( spl314_55
<=> k8_relset_2(sK27,sK28,sF307,sK31) = sF308 ),
introduced(definition,[new_symbols(definition,[spl314_55])],[avatar_definition]) ).
fof(f75691,plain,
( k8_relset_2(sK27,sK28,sF307,sK31) = sF308
| ~ spl314_55 ),
inference(avatar_component_clause,[],[f75689]) ).
fof(f75692,plain,
spl314_55,
inference(avatar_split_clause,[],[f75289,f75689]) ).
fof(f75694,definition,
( spl314_56
<=> k8_relset_2(sK28,sK27,sK30,sF306) = sF309 ),
introduced(definition,[new_symbols(definition,[spl314_56])],[avatar_definition]) ).
fof(f75696,plain,
( k8_relset_2(sK28,sK27,sK30,sF306) = sF309
| ~ spl314_56 ),
inference(avatar_component_clause,[],[f75694]) ).
fof(f75697,plain,
spl314_56,
inference(avatar_split_clause,[],[f75291,f75694]) ).
fof(f75699,definition,
( spl314_57
<=> k8_relset_2(sK27,sK28,sF309,sK31) = sF310 ),
introduced(definition,[new_symbols(definition,[spl314_57])],[avatar_definition]) ).
fof(f75701,plain,
( k8_relset_2(sK27,sK28,sF309,sK31) = sF310
| ~ spl314_57 ),
inference(avatar_component_clause,[],[f75699]) ).
fof(f75702,plain,
spl314_57,
inference(avatar_split_clause,[],[f75293,f75699]) ).
fof(f75704,definition,
( spl314_58
<=> k8_relset_2(sK28,sK27,sF310,sF306) = sF311 ),
introduced(definition,[new_symbols(definition,[spl314_58])],[avatar_definition]) ).
fof(f75706,plain,
( k8_relset_2(sK28,sK27,sF310,sF306) = sF311
| ~ spl314_58 ),
inference(avatar_component_clause,[],[f75704]) ).
fof(f75707,plain,
spl314_58,
inference(avatar_split_clause,[],[f75295,f75704]) ).
fof(f75709,definition,
( spl314_59
<=> k1_zfmisc_1(sK28) = sF312 ),
introduced(definition,[new_symbols(definition,[spl314_59])],[avatar_definition]) ).
fof(f75711,plain,
( k1_zfmisc_1(sK28) = sF312
| ~ spl314_59 ),
inference(avatar_component_clause,[],[f75709]) ).
fof(f75712,plain,
spl314_59,
inference(avatar_split_clause,[],[f75298,f75709]) ).
fof(f75714,definition,
( spl314_60
<=> k1_zfmisc_1(sK27) = sF313 ),
introduced(definition,[new_symbols(definition,[spl314_60])],[avatar_definition]) ).
fof(f75716,plain,
( k1_zfmisc_1(sK27) = sF313
| ~ spl314_60 ),
inference(avatar_component_clause,[],[f75714]) ).
fof(f75717,plain,
spl314_60,
inference(avatar_split_clause,[],[f75301,f75714]) ).
fof(f75811,plain,
( ! [X0,X1] :
( r1_tarski(X0,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,X0,sK31),k6_relset_1(sK27,sK28,sK31)))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK28))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK27)) )
| ~ spl314_48 ),
inference(resolution,[],[f72905,f75649]) ).
fof(f75812,plain,
( ! [X0,X1] :
( r1_tarski(X0,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,X0,sK31),sF306))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK28))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK27)) )
| ~ spl314_48
| ~ spl314_53 ),
inference(forward_demodulation,[],[f75811,f75681]) ).
fof(f75813,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF312)
| r1_tarski(X0,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,X0,sK31),sF306))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK27)) )
| ~ spl314_48
| ~ spl314_53
| ~ spl314_59 ),
inference(forward_demodulation,[],[f75812,f75711]) ).
fof(f75814,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF313)
| ~ m1_subset_1(X1,sF312)
| r1_tarski(X0,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,X0,sK31),sF306)) )
| ~ spl314_48
| ~ spl314_53
| ~ spl314_59
| ~ spl314_60 ),
inference(forward_demodulation,[],[f75813,f75716]) ).
fof(f75816,definition,
( spl314_65
<=> ! [X1] : ~ m1_subset_1(X1,sF312) ),
introduced(definition,[new_symbols(definition,[spl314_65])],[avatar_definition]) ).
fof(f75817,plain,
( ! [X1] : ~ m1_subset_1(X1,sF312)
| ~ spl314_65 ),
inference(avatar_component_clause,[],[f75816]) ).
fof(f75819,definition,
( spl314_66
<=> ! [X0] :
( ~ m1_subset_1(X0,sF313)
| r1_tarski(X0,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,X0,sK31),sF306)) ) ),
introduced(definition,[new_symbols(definition,[spl314_66])],[avatar_definition]) ).
fof(f75820,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF313)
| r1_tarski(X0,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,X0,sK31),sF306)) )
| ~ spl314_66 ),
inference(avatar_component_clause,[],[f75819]) ).
fof(f75821,plain,
( spl314_65
| spl314_66
| ~ spl314_48
| ~ spl314_53
| ~ spl314_59
| ~ spl314_60 ),
inference(avatar_split_clause,[],[f75814,f75714,f75709,f75679,f75647,f75819,f75816]) ).
fof(f75822,plain,
( $false
| ~ spl314_47
| ~ spl314_65 ),
inference(unit_resulting_resolution,[],[f75817,f75644]) ).
fof(f75825,plain,
( ~ spl314_47
| ~ spl314_65 ),
inference(avatar_contradiction_clause,[],[f75822]) ).
fof(f75826,plain,
( ! [X0,X1] :
( r1_tarski(X0,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,X0,sF306),sK31))
| ~ m2_relset_1(sK31,sK27,sK28)
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK27)) )
| ~ spl314_53 ),
inference(superposition,[],[f72904,f75681]) ).
fof(f75827,plain,
( ! [X0,X1] :
( r1_tarski(X0,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,X0,sF306),sK31))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK27)) )
| ~ spl314_48
| ~ spl314_53 ),
inference(forward_subsumption_resolution,[],[f75826,f75649]) ).
fof(f75828,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF312)
| r1_tarski(X0,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,X0,sF306),sK31))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK27)) )
| ~ spl314_48
| ~ spl314_53
| ~ spl314_59 ),
inference(forward_demodulation,[],[f75827,f75711]) ).
fof(f75829,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF313)
| ~ m1_subset_1(X0,sF312)
| r1_tarski(X0,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,X0,sF306),sK31)) )
| ~ spl314_48
| ~ spl314_53
| ~ spl314_59
| ~ spl314_60 ),
inference(forward_demodulation,[],[f75828,f75716]) ).
fof(f75831,definition,
( spl314_67
<=> ! [X0] :
( ~ m1_subset_1(X0,sF312)
| r1_tarski(X0,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,X0,sF306),sK31)) ) ),
introduced(definition,[new_symbols(definition,[spl314_67])],[avatar_definition]) ).
fof(f75832,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF312)
| r1_tarski(X0,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,X0,sF306),sK31)) )
| ~ spl314_67 ),
inference(avatar_component_clause,[],[f75831]) ).
fof(f75834,definition,
( spl314_68
<=> ! [X1] : ~ m1_subset_1(X1,sF313) ),
introduced(definition,[new_symbols(definition,[spl314_68])],[avatar_definition]) ).
fof(f75835,plain,
( ! [X1] : ~ m1_subset_1(X1,sF313)
| ~ spl314_68 ),
inference(avatar_component_clause,[],[f75834]) ).
fof(f75836,plain,
( spl314_67
| spl314_68
| ~ spl314_48
| ~ spl314_53
| ~ spl314_59
| ~ spl314_60 ),
inference(avatar_split_clause,[],[f75829,f75714,f75709,f75679,f75647,f75834,f75831]) ).
fof(f75837,plain,
( m1_subset_1(sK31,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl314_48 ),
inference(unit_resulting_resolution,[],[f73072,f75649]) ).
fof(f75838,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X0,X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| m1_subset_1(k8_relset_2(X1,X2,X3,X0),k1_zfmisc_1(X2)) ),
inference(resolution,[],[f73072,f72801]) ).
fof(f75840,definition,
( spl314_69
<=> m1_subset_1(sK31,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28))) ),
introduced(definition,[new_symbols(definition,[spl314_69])],[avatar_definition]) ).
fof(f75842,plain,
( m1_subset_1(sK31,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl314_69 ),
inference(avatar_component_clause,[],[f75840]) ).
fof(f75843,plain,
( spl314_69
| ~ spl314_48 ),
inference(avatar_split_clause,[],[f75837,f75647,f75840]) ).
fof(f75844,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK27))
| m1_subset_1(k8_relset_2(sK27,sK28,X0,sK31),k1_zfmisc_1(sK28)) )
| ~ spl314_48 ),
inference(resolution,[],[f75838,f75649]) ).
fof(f75845,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF313)
| m1_subset_1(k8_relset_2(sK27,sK28,X0,sK31),k1_zfmisc_1(sK28)) )
| ~ spl314_48
| ~ spl314_60 ),
inference(forward_demodulation,[],[f75844,f75716]) ).
fof(f75846,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF313)
| m1_subset_1(k8_relset_2(sK27,sK28,X0,sK31),sF312) )
| ~ spl314_48
| ~ spl314_59
| ~ spl314_60 ),
inference(forward_demodulation,[],[f75845,f75711]) ).
fof(f75851,plain,
( r1_tarski(sK29,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,sK29,sK31),sF306))
| ~ spl314_46
| ~ spl314_66 ),
inference(resolution,[],[f75820,f75639]) ).
fof(f75852,plain,
( r1_tarski(sK29,k8_relset_2(sK28,sK27,sF305,sF306))
| ~ spl314_46
| ~ spl314_52
| ~ spl314_66 ),
inference(forward_demodulation,[],[f75851,f75676]) ).
fof(f75854,plain,
( r1_tarski(sK29,sF307)
| ~ spl314_46
| ~ spl314_52
| ~ spl314_54
| ~ spl314_66 ),
inference(forward_demodulation,[],[f75852,f75686]) ).
fof(f75857,definition,
( spl314_70
<=> r1_tarski(sK29,sF307) ),
introduced(definition,[new_symbols(definition,[spl314_70])],[avatar_definition]) ).
fof(f75859,plain,
( r1_tarski(sK29,sF307)
| ~ spl314_70 ),
inference(avatar_component_clause,[],[f75857]) ).
fof(f75860,plain,
( spl314_70
| ~ spl314_46
| ~ spl314_52
| ~ spl314_54
| ~ spl314_66 ),
inference(avatar_split_clause,[],[f75854,f75819,f75684,f75674,f75637,f75857]) ).
fof(f75862,plain,
( m1_subset_1(k8_relset_2(sK27,sK28,sK29,sK31),sF312)
| ~ spl314_46
| ~ spl314_48
| ~ spl314_59
| ~ spl314_60 ),
inference(resolution,[],[f75846,f75639]) ).
fof(f75863,plain,
( m1_subset_1(sF305,sF312)
| ~ spl314_46
| ~ spl314_48
| ~ spl314_52
| ~ spl314_59
| ~ spl314_60 ),
inference(forward_demodulation,[],[f75862,f75676]) ).
fof(f75866,definition,
( spl314_71
<=> m1_subset_1(sF305,sF312) ),
introduced(definition,[new_symbols(definition,[spl314_71])],[avatar_definition]) ).
fof(f75868,plain,
( m1_subset_1(sF305,sF312)
| ~ spl314_71 ),
inference(avatar_component_clause,[],[f75866]) ).
fof(f75869,plain,
( spl314_71
| ~ spl314_46
| ~ spl314_48
| ~ spl314_52
| ~ spl314_59
| ~ spl314_60 ),
inference(avatar_split_clause,[],[f75863,f75714,f75709,f75674,f75647,f75637,f75866]) ).
fof(f75872,plain,
( r1_tarski(sK30,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,sK30,sF306),sK31))
| ~ spl314_47
| ~ spl314_67 ),
inference(resolution,[],[f75832,f75644]) ).
fof(f75873,plain,
( r1_tarski(sF305,k8_relset_2(sK27,sK28,k8_relset_2(sK28,sK27,sF305,sF306),sK31))
| ~ spl314_67
| ~ spl314_71 ),
inference(resolution,[],[f75832,f75868]) ).
fof(f75874,plain,
( r1_tarski(sF305,k8_relset_2(sK27,sK28,sF307,sK31))
| ~ spl314_54
| ~ spl314_67
| ~ spl314_71 ),
inference(forward_demodulation,[],[f75873,f75686]) ).
fof(f75875,plain,
( r1_tarski(sK30,k8_relset_2(sK27,sK28,sF309,sK31))
| ~ spl314_47
| ~ spl314_56
| ~ spl314_67 ),
inference(forward_demodulation,[],[f75872,f75696]) ).
fof(f75878,plain,
( r1_tarski(sF305,sF308)
| ~ spl314_54
| ~ spl314_55
| ~ spl314_67
| ~ spl314_71 ),
inference(forward_demodulation,[],[f75874,f75691]) ).
fof(f75879,plain,
( r1_tarski(sK30,sF310)
| ~ spl314_47
| ~ spl314_56
| ~ spl314_57
| ~ spl314_67 ),
inference(forward_demodulation,[],[f75875,f75701]) ).
fof(f75883,definition,
( spl314_72
<=> r1_tarski(sF305,sF308) ),
introduced(definition,[new_symbols(definition,[spl314_72])],[avatar_definition]) ).
fof(f75885,plain,
( r1_tarski(sF305,sF308)
| ~ spl314_72 ),
inference(avatar_component_clause,[],[f75883]) ).
fof(f75886,plain,
( spl314_72
| ~ spl314_54
| ~ spl314_55
| ~ spl314_67
| ~ spl314_71 ),
inference(avatar_split_clause,[],[f75878,f75866,f75831,f75689,f75684,f75883]) ).
fof(f75888,definition,
( spl314_73
<=> r1_tarski(sK30,sF310) ),
introduced(definition,[new_symbols(definition,[spl314_73])],[avatar_definition]) ).
fof(f75890,plain,
( r1_tarski(sK30,sF310)
| ~ spl314_73 ),
inference(avatar_component_clause,[],[f75888]) ).
fof(f75891,plain,
( spl314_73
| ~ spl314_47
| ~ spl314_56
| ~ spl314_57
| ~ spl314_67 ),
inference(avatar_split_clause,[],[f75879,f75831,f75699,f75694,f75642,f75888]) ).
fof(f75892,plain,
( $false
| ~ spl314_46
| ~ spl314_68 ),
inference(unit_resulting_resolution,[],[f75835,f75639]) ).
fof(f75895,plain,
( ~ spl314_46
| ~ spl314_68 ),
inference(avatar_contradiction_clause,[],[f75892]) ).
fof(f75947,plain,
( ! [X0,X1] :
( ~ r1_tarski(X0,X1)
| r1_tarski(k8_relset_2(sK27,sK28,X1,sK31),k8_relset_2(sK27,sK28,X0,sK31))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK27))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK27)) )
| ~ spl314_69 ),
inference(resolution,[],[f72855,f75842]) ).
fof(f75948,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF313)
| ~ r1_tarski(X0,X1)
| r1_tarski(k8_relset_2(sK27,sK28,X1,sK31),k8_relset_2(sK27,sK28,X0,sK31))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK27)) )
| ~ spl314_60
| ~ spl314_69 ),
inference(forward_demodulation,[],[f75947,f75716]) ).
fof(f75949,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF313)
| ~ m1_subset_1(X1,sF313)
| ~ r1_tarski(X0,X1)
| r1_tarski(k8_relset_2(sK27,sK28,X1,sK31),k8_relset_2(sK27,sK28,X0,sK31)) )
| ~ spl314_60
| ~ spl314_69 ),
inference(forward_demodulation,[],[f75948,f75716]) ).
fof(f75950,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF313)
| ~ r1_tarski(sK29,X0)
| r1_tarski(k8_relset_2(sK27,sK28,X0,sK31),k8_relset_2(sK27,sK28,sK29,sK31)) )
| ~ spl314_46
| ~ spl314_60
| ~ spl314_69 ),
inference(resolution,[],[f75949,f75639]) ).
fof(f75951,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF313)
| r1_tarski(k8_relset_2(sK27,sK28,X0,sK31),sF305)
| ~ r1_tarski(sK29,X0) )
| ~ spl314_46
| ~ spl314_52
| ~ spl314_60
| ~ spl314_69 ),
inference(forward_demodulation,[],[f75950,f75676]) ).
fof(f75956,plain,
( m1_relset_1(sK31,sK27,sK28)
| ~ spl314_48 ),
inference(resolution,[],[f73057,f75649]) ).
fof(f75958,definition,
( spl314_76
<=> m1_relset_1(sK31,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl314_76])],[avatar_definition]) ).
fof(f75960,plain,
( m1_relset_1(sK31,sK27,sK28)
| ~ spl314_76 ),
inference(avatar_component_clause,[],[f75958]) ).
fof(f75961,plain,
( spl314_76
| ~ spl314_48 ),
inference(avatar_split_clause,[],[f75956,f75647,f75958]) ).
fof(f75966,plain,
( m2_relset_1(k6_relset_1(sK27,sK28,sK31),sK28,sK27)
| ~ spl314_76 ),
inference(resolution,[],[f75960,f74484]) ).
fof(f75969,plain,
( m2_relset_1(sF306,sK28,sK27)
| ~ spl314_53
| ~ spl314_76 ),
inference(forward_demodulation,[],[f75966,f75681]) ).
fof(f75980,definition,
( spl314_78
<=> m2_relset_1(sF306,sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl314_78])],[avatar_definition]) ).
fof(f75982,plain,
( m2_relset_1(sF306,sK28,sK27)
| ~ spl314_78 ),
inference(avatar_component_clause,[],[f75980]) ).
fof(f75983,plain,
( spl314_78
| ~ spl314_53
| ~ spl314_76 ),
inference(avatar_split_clause,[],[f75969,f75958,f75679,f75980]) ).
fof(f75991,plain,
( m1_subset_1(sF306,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27)))
| ~ spl314_78 ),
inference(unit_resulting_resolution,[],[f73072,f75982]) ).
fof(f75994,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sK28))
| m1_subset_1(k8_relset_2(sK28,sK27,X0,sF306),k1_zfmisc_1(sK27)) )
| ~ spl314_78 ),
inference(resolution,[],[f75982,f75838]) ).
fof(f75997,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF312)
| m1_subset_1(k8_relset_2(sK28,sK27,X0,sF306),k1_zfmisc_1(sK27)) )
| ~ spl314_59
| ~ spl314_78 ),
inference(forward_demodulation,[],[f75994,f75711]) ).
fof(f76010,definition,
( spl314_82
<=> m1_subset_1(sF306,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27))) ),
introduced(definition,[new_symbols(definition,[spl314_82])],[avatar_definition]) ).
fof(f76012,plain,
( m1_subset_1(sF306,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27)))
| ~ spl314_82 ),
inference(avatar_component_clause,[],[f76010]) ).
fof(f76013,plain,
( spl314_82
| ~ spl314_78 ),
inference(avatar_split_clause,[],[f75991,f75980,f76010]) ).
fof(f76015,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF312)
| m1_subset_1(k8_relset_2(sK28,sK27,X0,sF306),sF313) )
| ~ spl314_59
| ~ spl314_60
| ~ spl314_78 ),
inference(forward_demodulation,[],[f75997,f75716]) ).
fof(f76073,plain,
( ! [X0,X1] :
( ~ r1_tarski(X0,X1)
| r1_tarski(k8_relset_2(sK28,sK27,X1,sF306),k8_relset_2(sK28,sK27,X0,sF306))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK28))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl314_82 ),
inference(resolution,[],[f76012,f72855]) ).
fof(f76076,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF312)
| ~ r1_tarski(X0,X1)
| r1_tarski(k8_relset_2(sK28,sK27,X1,sF306),k8_relset_2(sK28,sK27,X0,sF306))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl314_59
| ~ spl314_82 ),
inference(forward_demodulation,[],[f76073,f75711]) ).
fof(f76083,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF312)
| ~ m1_subset_1(X1,sF312)
| ~ r1_tarski(X0,X1)
| r1_tarski(k8_relset_2(sK28,sK27,X1,sF306),k8_relset_2(sK28,sK27,X0,sF306)) )
| ~ spl314_59
| ~ spl314_82 ),
inference(forward_demodulation,[],[f76076,f75711]) ).
fof(f76098,plain,
( m1_subset_1(k8_relset_2(sK28,sK27,sK30,sF306),sF313)
| ~ spl314_47
| ~ spl314_59
| ~ spl314_60
| ~ spl314_78 ),
inference(resolution,[],[f76015,f75644]) ).
fof(f76099,plain,
( m1_subset_1(k8_relset_2(sK28,sK27,sF305,sF306),sF313)
| ~ spl314_59
| ~ spl314_60
| ~ spl314_71
| ~ spl314_78 ),
inference(resolution,[],[f76015,f75868]) ).
fof(f76100,plain,
( m1_subset_1(sF307,sF313)
| ~ spl314_54
| ~ spl314_59
| ~ spl314_60
| ~ spl314_71
| ~ spl314_78 ),
inference(forward_demodulation,[],[f76099,f75686]) ).
fof(f76101,plain,
( m1_subset_1(sF309,sF313)
| ~ spl314_47
| ~ spl314_56
| ~ spl314_59
| ~ spl314_60
| ~ spl314_78 ),
inference(forward_demodulation,[],[f76098,f75696]) ).
fof(f76105,definition,
( spl314_94
<=> m1_subset_1(sF307,sF313) ),
introduced(definition,[new_symbols(definition,[spl314_94])],[avatar_definition]) ).
fof(f76107,plain,
( m1_subset_1(sF307,sF313)
| ~ spl314_94 ),
inference(avatar_component_clause,[],[f76105]) ).
fof(f76108,plain,
( spl314_94
| ~ spl314_54
| ~ spl314_59
| ~ spl314_60
| ~ spl314_71
| ~ spl314_78 ),
inference(avatar_split_clause,[],[f76100,f75980,f75866,f75714,f75709,f75684,f76105]) ).
fof(f76110,definition,
( spl314_95
<=> m1_subset_1(sF309,sF313) ),
introduced(definition,[new_symbols(definition,[spl314_95])],[avatar_definition]) ).
fof(f76112,plain,
( m1_subset_1(sF309,sF313)
| ~ spl314_95 ),
inference(avatar_component_clause,[],[f76110]) ).
fof(f76113,plain,
( spl314_95
| ~ spl314_47
| ~ spl314_56
| ~ spl314_59
| ~ spl314_60
| ~ spl314_78 ),
inference(avatar_split_clause,[],[f76101,f75980,f75714,f75709,f75694,f75642,f76110]) ).
fof(f76120,plain,
( m1_subset_1(k8_relset_2(sK27,sK28,sF309,sK31),sF312)
| ~ spl314_48
| ~ spl314_59
| ~ spl314_60
| ~ spl314_95 ),
inference(resolution,[],[f76112,f75846]) ).
fof(f76121,plain,
( r1_tarski(sF309,k8_relset_2(sK28,sK27,k8_relset_2(sK27,sK28,sF309,sK31),sF306))
| ~ spl314_66
| ~ spl314_95 ),
inference(resolution,[],[f76112,f75820]) ).
fof(f76122,plain,
( r1_tarski(sF309,k8_relset_2(sK28,sK27,sF310,sF306))
| ~ spl314_57
| ~ spl314_66
| ~ spl314_95 ),
inference(forward_demodulation,[],[f76121,f75701]) ).
fof(f76123,plain,
( m1_subset_1(sF310,sF312)
| ~ spl314_48
| ~ spl314_57
| ~ spl314_59
| ~ spl314_60
| ~ spl314_95 ),
inference(forward_demodulation,[],[f76120,f75701]) ).
fof(f76130,plain,
( r1_tarski(sF309,sF311)
| ~ spl314_57
| ~ spl314_58
| ~ spl314_66
| ~ spl314_95 ),
inference(forward_demodulation,[],[f76122,f75706]) ).
fof(f76132,definition,
( spl314_96
<=> m1_subset_1(sF310,sF312) ),
introduced(definition,[new_symbols(definition,[spl314_96])],[avatar_definition]) ).
fof(f76134,plain,
( m1_subset_1(sF310,sF312)
| ~ spl314_96 ),
inference(avatar_component_clause,[],[f76132]) ).
fof(f76135,plain,
( spl314_96
| ~ spl314_48
| ~ spl314_57
| ~ spl314_59
| ~ spl314_60
| ~ spl314_95 ),
inference(avatar_split_clause,[],[f76123,f76110,f75714,f75709,f75699,f75647,f76132]) ).
fof(f76147,definition,
( spl314_99
<=> r1_tarski(sF309,sF311) ),
introduced(definition,[new_symbols(definition,[spl314_99])],[avatar_definition]) ).
fof(f76149,plain,
( r1_tarski(sF309,sF311)
| ~ spl314_99 ),
inference(avatar_component_clause,[],[f76147]) ).
fof(f76150,plain,
( spl314_99
| ~ spl314_57
| ~ spl314_58
| ~ spl314_66
| ~ spl314_95 ),
inference(avatar_split_clause,[],[f76130,f76110,f75819,f75704,f75699,f76147]) ).
fof(f76206,plain,
( r1_tarski(k8_relset_2(sK27,sK28,sF307,sK31),sF305)
| ~ spl314_46
| ~ spl314_52
| ~ spl314_60
| ~ spl314_69
| ~ spl314_70
| ~ spl314_94 ),
inference(unit_resulting_resolution,[],[f75951,f75859,f76107]) ).
fof(f76222,plain,
( r1_tarski(sF308,sF305)
| ~ spl314_46
| ~ spl314_52
| ~ spl314_55
| ~ spl314_60
| ~ spl314_69
| ~ spl314_70
| ~ spl314_94 ),
inference(forward_demodulation,[],[f76206,f75691]) ).
fof(f76236,definition,
( spl314_109
<=> r1_tarski(sF308,sF305) ),
introduced(definition,[new_symbols(definition,[spl314_109])],[avatar_definition]) ).
fof(f76238,plain,
( r1_tarski(sF308,sF305)
| ~ spl314_109 ),
inference(avatar_component_clause,[],[f76236]) ).
fof(f76239,plain,
( spl314_109
| ~ spl314_46
| ~ spl314_52
| ~ spl314_55
| ~ spl314_60
| ~ spl314_69
| ~ spl314_70
| ~ spl314_94 ),
inference(avatar_split_clause,[],[f76222,f76105,f75857,f75840,f75714,f75689,f75674,f75637,f76236]) ).
fof(f76296,plain,
( sF305 = sF308
| ~ r1_tarski(sF308,sF305)
| ~ spl314_72 ),
inference(resolution,[],[f73675,f75885]) ).
fof(f76299,plain,
( sF309 = sF311
| ~ r1_tarski(sF311,sF309)
| ~ spl314_99 ),
inference(resolution,[],[f73675,f76149]) ).
fof(f76305,definition,
( spl314_113
<=> r1_tarski(sF311,sF309) ),
introduced(definition,[new_symbols(definition,[spl314_113])],[avatar_definition]) ).
fof(f76307,plain,
( ~ r1_tarski(sF311,sF309)
| spl314_113 ),
inference(avatar_component_clause,[],[f76305]) ).
fof(f76308,plain,
( ~ spl314_113
| spl314_49
| ~ spl314_99 ),
inference(avatar_split_clause,[],[f76299,f76147,f75652,f76305]) ).
fof(f76319,plain,
( ~ r1_tarski(sF308,sF305)
| spl314_50
| ~ spl314_72 ),
inference(forward_subsumption_resolution,[],[f76296,f75658]) ).
fof(f76357,plain,
( $false
| spl314_50
| ~ spl314_72
| ~ spl314_109 ),
inference(forward_subsumption_resolution,[],[f76319,f76238]) ).
fof(f76358,plain,
( spl314_50
| ~ spl314_72
| ~ spl314_109 ),
inference(avatar_contradiction_clause,[],[f76357]) ).
fof(f76799,plain,
( r1_tarski(k8_relset_2(sK28,sK27,sF310,sF306),k8_relset_2(sK28,sK27,sK30,sF306))
| ~ spl314_47
| ~ spl314_59
| ~ spl314_73
| ~ spl314_82
| ~ spl314_96 ),
inference(unit_resulting_resolution,[],[f76083,f75644,f75890,f76134]) ).
fof(f76810,plain,
( r1_tarski(k8_relset_2(sK28,sK27,sF310,sF306),sF309)
| ~ spl314_47
| ~ spl314_56
| ~ spl314_59
| ~ spl314_73
| ~ spl314_82
| ~ spl314_96 ),
inference(forward_demodulation,[],[f76799,f75696]) ).
fof(f76813,plain,
( r1_tarski(sF311,sF309)
| ~ spl314_47
| ~ spl314_56
| ~ spl314_58
| ~ spl314_59
| ~ spl314_73
| ~ spl314_82
| ~ spl314_96 ),
inference(forward_demodulation,[],[f76810,f75706]) ).
fof(f76816,plain,
( $false
| ~ spl314_47
| ~ spl314_56
| ~ spl314_58
| ~ spl314_59
| ~ spl314_73
| ~ spl314_82
| ~ spl314_96
| spl314_113 ),
inference(forward_subsumption_resolution,[],[f76813,f76307]) ).
fof(f76817,plain,
( ~ spl314_47
| ~ spl314_56
| ~ spl314_58
| ~ spl314_59
| ~ spl314_73
| ~ spl314_82
| ~ spl314_96
| spl314_113 ),
inference(avatar_contradiction_clause,[],[f76816]) ).
cnf(s49,plain,
spl314_46,
inference(sat_conversion,[],[f75640]) ).
cnf(s50,plain,
spl314_47,
inference(sat_conversion,[],[f75645]) ).
cnf(s51,plain,
spl314_48,
inference(sat_conversion,[],[f75650]) ).
cnf(s52,plain,
( ~ spl314_49
| ~ spl314_50 ),
inference(sat_conversion,[],[f75659]) ).
cnf(s54,plain,
spl314_52,
inference(sat_conversion,[],[f75677]) ).
cnf(s55,plain,
spl314_53,
inference(sat_conversion,[],[f75682]) ).
cnf(s56,plain,
spl314_54,
inference(sat_conversion,[],[f75687]) ).
cnf(s57,plain,
spl314_55,
inference(sat_conversion,[],[f75692]) ).
cnf(s58,plain,
spl314_56,
inference(sat_conversion,[],[f75697]) ).
cnf(s59,plain,
spl314_57,
inference(sat_conversion,[],[f75702]) ).
cnf(s60,plain,
spl314_58,
inference(sat_conversion,[],[f75707]) ).
cnf(s61,plain,
spl314_59,
inference(sat_conversion,[],[f75712]) ).
cnf(s62,plain,
spl314_60,
inference(sat_conversion,[],[f75717]) ).
cnf(s68,plain,
( ~ spl314_48
| ~ spl314_53
| ~ spl314_59
| ~ spl314_60
| spl314_65
| spl314_66 ),
inference(sat_conversion,[],[f75821]) ).
cnf(s70,plain,
( ~ spl314_47
| ~ spl314_65 ),
inference(sat_conversion,[],[f75825]) ).
cnf(s71,plain,
( ~ spl314_48
| ~ spl314_53
| ~ spl314_59
| ~ spl314_60
| spl314_67
| spl314_68 ),
inference(sat_conversion,[],[f75836]) ).
cnf(s72,plain,
( ~ spl314_48
| spl314_69 ),
inference(sat_conversion,[],[f75843]) ).
cnf(s73,plain,
( ~ spl314_46
| ~ spl314_52
| ~ spl314_54
| ~ spl314_66
| spl314_70 ),
inference(sat_conversion,[],[f75860]) ).
cnf(s75,plain,
( ~ spl314_46
| ~ spl314_48
| ~ spl314_52
| ~ spl314_59
| ~ spl314_60
| spl314_71 ),
inference(sat_conversion,[],[f75869]) ).
cnf(s77,plain,
( ~ spl314_54
| ~ spl314_55
| ~ spl314_67
| ~ spl314_71
| spl314_72 ),
inference(sat_conversion,[],[f75886]) ).
cnf(s78,plain,
( ~ spl314_47
| ~ spl314_56
| ~ spl314_57
| ~ spl314_67
| spl314_73 ),
inference(sat_conversion,[],[f75891]) ).
cnf(s82,plain,
( ~ spl314_46
| ~ spl314_68 ),
inference(sat_conversion,[],[f75895]) ).
cnf(s89,plain,
( ~ spl314_48
| spl314_76 ),
inference(sat_conversion,[],[f75961]) ).
cnf(s92,plain,
( ~ spl314_53
| ~ spl314_76
| spl314_78 ),
inference(sat_conversion,[],[f75983]) ).
cnf(s100,plain,
( ~ spl314_78
| spl314_82 ),
inference(sat_conversion,[],[f76013]) ).
cnf(s114,plain,
( ~ spl314_54
| ~ spl314_59
| ~ spl314_60
| ~ spl314_71
| ~ spl314_78
| spl314_94 ),
inference(sat_conversion,[],[f76108]) ).
cnf(s115,plain,
( ~ spl314_47
| ~ spl314_56
| ~ spl314_59
| ~ spl314_60
| ~ spl314_78
| spl314_95 ),
inference(sat_conversion,[],[f76113]) ).
cnf(s118,plain,
( ~ spl314_48
| ~ spl314_57
| ~ spl314_59
| ~ spl314_60
| ~ spl314_95
| spl314_96 ),
inference(sat_conversion,[],[f76135]) ).
cnf(s121,plain,
( ~ spl314_57
| ~ spl314_58
| ~ spl314_66
| ~ spl314_95
| spl314_99 ),
inference(sat_conversion,[],[f76150]) ).
cnf(s137,plain,
( ~ spl314_46
| ~ spl314_52
| ~ spl314_55
| ~ spl314_60
| ~ spl314_69
| ~ spl314_70
| ~ spl314_94
| spl314_109 ),
inference(sat_conversion,[],[f76239]) ).
cnf(s147,plain,
( spl314_49
| ~ spl314_99
| ~ spl314_113 ),
inference(sat_conversion,[],[f76308]) ).
cnf(s159,plain,
( spl314_50
| ~ spl314_72
| ~ spl314_109 ),
inference(sat_conversion,[],[f76358]) ).
cnf(s214,plain,
( ~ spl314_47
| ~ spl314_56
| ~ spl314_58
| ~ spl314_59
| ~ spl314_73
| ~ spl314_82
| ~ spl314_96
| spl314_113 ),
inference(sat_conversion,[],[f76817]) ).
cnf(s215,plain,
spl314_76,
inference(rat,[],[s89,s51]) ).
cnf(s217,plain,
spl314_69,
inference(rat,[],[s72,s51]) ).
cnf(s220,plain,
spl314_78,
inference(rat,[],[s92,s55,s215]) ).
cnf(s224,plain,
spl314_82,
inference(rat,[],[s100,s220]) ).
cnf(s243,plain,
spl314_95,
inference(rat,[],[s115,s220,s58,s62,s61,s50]) ).
cnf(s244,plain,
~ spl314_65,
inference(rat,[],[s70,s50]) ).
cnf(s246,plain,
spl314_96,
inference(rat,[],[s118,s51,s59,s62,s61,s243]) ).
cnf(s248,plain,
spl314_66,
inference(rat,[],[s68,s51,s55,s62,s61,s244]) ).
cnf(s251,plain,
spl314_99,
inference(rat,[],[s121,s243,s59,s60,s248]) ).
cnf(s257,plain,
~ spl314_68,
inference(rat,[],[s82,s49]) ).
cnf(s258,plain,
spl314_71,
inference(rat,[],[s75,s51,s62,s61,s54,s49]) ).
cnf(s259,plain,
spl314_70,
inference(rat,[],[s73,s248,s54,s56,s49]) ).
cnf(s262,plain,
spl314_67,
inference(rat,[],[s71,s51,s55,s62,s61,s257]) ).
cnf(s264,plain,
spl314_94,
inference(rat,[],[s114,s220,s56,s61,s62,s258]) ).
cnf(s266,plain,
spl314_73,
inference(rat,[],[s78,s50,s58,s59,s262]) ).
cnf(s267,plain,
spl314_72,
inference(rat,[],[s77,s258,s56,s57,s262]) ).
cnf(s271,plain,
spl314_109,
inference(rat,[],[s137,s259,s49,s217,s54,s62,s57,s264]) ).
cnf(s273,plain,
spl314_113,
inference(rat,[],[s214,s246,s50,s224,s58,s61,s60,s266]) ).
cnf(s274,plain,
spl314_50,
inference(rat,[],[s159,s271,s267]) ).
cnf(s278,plain,
spl314_49,
inference(rat,[],[s147,s251,s273]) ).
cnf(s282,plain,
$false,
inference(rat,[],[s52,s274,s278]) ).
fof(f76818,plain,
$false,
inference(avatar_sat_refutation,[],[s282]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU450+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.10/0.35 % Computer : n002.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 28 05:39:49 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 Running first-order theorem proving
% 0.13/0.38 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
% 22.42/8.86 % (60769)Detected formulas, will run a generic FOF schedule.
% 22.42/8.86 % (60777)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2917727976:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 22.42/8.86 % (60774)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=1719503071:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 22.42/8.86 % (60776)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=1114659332:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 22.42/8.86 % (60775)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=2708628762:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 22.42/8.86 % (60780)dis-21_1_sil=8000:lcm=predicate:random_seed=1219794906:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2944 on theBenchmark for (2944ds/129Mi)
% 22.42/8.86 % (60779)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=446850395:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 22.42/8.86 % (60778)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3325413699:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 22.42/8.86 % (60777)Instruction limit reached!
% 22.42/8.86 % (60777)------------------------------
% 22.42/8.86 % (60777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/8.86 % (60777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/8.86 % (60777)CaDiCaL version: 2.1.3
% 22.42/8.86 % (60777)Termination reason: Instruction limit
% 22.42/8.86 % (60777)Termination phase: SInE selection
% 22.42/8.86 % (60777)Time elapsed: 0.052 s
% 22.42/8.86 % (60777)Peak memory usage: 201 MB
% 22.42/8.86 % (60777)Instructions burned: 110 (million)
% 22.42/8.86 % (60779)Instruction limit reached!
% 22.42/8.86 % (60779)------------------------------
% 22.42/8.86 % (60779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/8.86 % (60779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/8.86 % (60779)CaDiCaL version: 2.1.3
% 22.42/8.86 % (60779)Termination reason: Instruction limit
% 22.42/8.86 % (60779)Termination phase: Property scanning
% 22.42/8.86 % (60779)Time elapsed: 0.068 s
% 22.42/8.86 % (60779)Peak memory usage: 201 MB
% 22.42/8.86 % (60779)Instructions burned: 139 (million)
% 22.42/8.86 % (60778)Instruction limit reached!
% 22.42/8.86 % (60778)------------------------------
% 22.42/8.86 % (60778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/8.86 % (60778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/8.86 % (60778)CaDiCaL version: 2.1.3
% 22.42/8.86 % (60778)Termination reason: Instruction limit
% 22.42/8.86 % (60778)Termination phase: SInE selection
% 22.42/8.86 % (60778)Time elapsed: 0.091 s
% 22.42/8.86 % (60778)Peak memory usage: 201 MB
% 22.42/8.86 % (60778)Instructions burned: 119 (million)
% 22.42/8.86 % (60780)Instruction limit reached!
% 22.42/8.86 % (60780)------------------------------
% 22.42/8.86 % (60780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.42/8.86 % (60780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.42/8.86 % (60780)CaDiCaL version: 2.1.3
% 22.42/8.86 % (60780)Termination reason: Instruction limit
% 22.42/8.86 % (60780)Termination phase: SInE selection
% 22.42/8.86 % (60780)Time elapsed: 0.099 s
% 22.42/8.86 % (60780)Peak memory usage: 201 MB
% 22.42/8.86 % (60780)Instructions burned: 130 (million)
% 22.42/8.86 % (60788)lrs+10_1_sil=8000:sp=occurrence:random_seed=1732061985:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 22.42/8.86 % (60789)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1686035848:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/157Mi)
% 22.42/8.86 % (60790)lrs+1011_1_sil=32000:sp=occurrence:random_seed=132327864:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 22.42/8.86 % (60791)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=2194283702:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 22.42/8.86 % (60788)Instruction limit reached!
% 22.42/8.86 % (60788)------------------------------
% 22.42/8.86 % (60788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60788)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60788)Termination reason: Instruction limit
% 28.96/9.75 % (60788)Termination phase: SInE selection
% 28.96/9.75 % (60788)Time elapsed: 0.132 s
% 28.96/9.75 % (60788)Peak memory usage: 201 MB
% 28.96/9.75 % (60788)Instructions burned: 288 (million)
% 28.96/9.75 % (60789)Instruction limit reached!
% 28.96/9.75 % (60789)------------------------------
% 28.96/9.75 % (60789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60789)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60789)Termination reason: Instruction limit
% 28.96/9.75 % (60789)Termination phase: Property scanning
% 28.96/9.75 % (60789)Time elapsed: 0.076 s
% 28.96/9.75 % (60789)Peak memory usage: 201 MB
% 28.96/9.75 % (60789)Instructions burned: 159 (million)
% 28.96/9.75 % (60791)Instruction limit reached!
% 28.96/9.75 % (60791)------------------------------
% 28.96/9.75 % (60791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60791)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60791)Termination reason: Instruction limit
% 28.96/9.75 % (60791)Termination phase: Property scanning
% 28.96/9.75 % (60791)Time elapsed: 0.112 s
% 28.96/9.75 % (60791)Peak memory usage: 201 MB
% 28.96/9.75 % (60791)Instructions burned: 250 (million)
% 28.96/9.75 % (60796)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=386508404:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 28.96/9.75 % (60797)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3027430862:i=2350_2939 on theBenchmark for (2939ds/2350Mi)
% 28.96/9.75 % (60790)Instruction limit reached!
% 28.96/9.75 % (60790)------------------------------
% 28.96/9.75 % (60790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60790)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60790)Termination reason: Instruction limit
% 28.96/9.75 % (60790)Termination phase: SInE selection
% 28.96/9.75 % (60790)Time elapsed: 0.236 s
% 28.96/9.75 % (60790)Peak memory usage: 201 MB
% 28.96/9.75 % (60790)Instructions burned: 325 (million)
% 28.96/9.75 % (60798)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3666314968:cts=off:i=113:fsr=off:ss=included:sgt=4_2939 on theBenchmark for (2939ds/113Mi)
% 28.96/9.75 % (60798)Instruction limit reached!
% 28.96/9.75 % (60798)------------------------------
% 28.96/9.75 % (60798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60798)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60798)Termination reason: Instruction limit
% 28.96/9.75 % (60798)Termination phase: SInE selection
% 28.96/9.75 % (60798)Time elapsed: 0.053 s
% 28.96/9.75 % (60798)Peak memory usage: 201 MB
% 28.96/9.75 % (60798)Instructions burned: 113 (million)
% 28.96/9.75 % (60801)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=576781184:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 28.96/9.75 % (60796)Instruction limit reached!
% 28.96/9.75 % (60796)------------------------------
% 28.96/9.75 % (60796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60796)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60796)Termination reason: Instruction limit
% 28.96/9.75 % (60796)Termination phase: SInE selection
% 28.96/9.75 % (60796)Time elapsed: 0.226 s
% 28.96/9.75 % (60796)Peak memory usage: 201 MB
% 28.96/9.75 % (60796)Instructions burned: 295 (million)
% 28.96/9.75 % (60803)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2217011892:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2936 on theBenchmark for (2936ds/114Mi)
% 28.96/9.75 % (60801)Instruction limit reached!
% 28.96/9.75 % (60801)------------------------------
% 28.96/9.75 % (60801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.96/9.75 % (60801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.96/9.75 % (60801)CaDiCaL version: 2.1.3
% 28.96/9.75 % (60801)Termination reason: Instruction limit
% 28.96/9.75 % (60801)Termination phase: Preprocessing 1
% 63.58/14.52 % (60801)Time elapsed: 0.100 s
% 63.58/14.52 % (60801)Peak memory usage: 202 MB
% 63.58/14.52 % (60801)Instructions burned: 127 (million)
% 63.58/14.52 % (60803)Instruction limit reached!
% 63.58/14.52 % (60803)------------------------------
% 63.58/14.52 % (60803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.58/14.52 % (60803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/14.52 % (60803)CaDiCaL version: 2.1.3
% 63.58/14.52 % (60803)Termination reason: Instruction limit
% 63.58/14.52 % (60803)Termination phase: Property scanning
% 63.58/14.52 % (60803)Time elapsed: 0.032 s
% 63.58/14.52 % (60803)Peak memory usage: 201 MB
% 63.58/14.52 % (60803)Instructions burned: 117 (million)
% 63.58/14.52 % (60805)lrs+10_1_sil=8000:sp=occurrence:random_seed=2533463252:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2936 on theBenchmark for (2936ds/907Mi)
% 63.58/14.52 % (60808)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2581702191:i=5202:ss=axioms:sgt=16_2935 on theBenchmark for (2935ds/5202Mi)
% 63.58/14.52 % (60807)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4128255807:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 63.58/14.52 % (60807)Instruction limit reached!
% 63.58/14.52 % (60807)------------------------------
% 63.58/14.52 % (60807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.58/14.52 % (60807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/14.52 % (60807)CaDiCaL version: 2.1.3
% 63.58/14.52 % (60807)Termination reason: Instruction limit
% 63.58/14.52 % (60807)Termination phase: SInE selection
% 63.58/14.52 % (60807)Time elapsed: 0.318 s
% 63.58/14.52 % (60807)Peak memory usage: 202 MB
% 63.58/14.52 % (60807)Instructions burned: 438 (million)
% 63.58/14.52 % (60812)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=605230114:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2930 on theBenchmark for (2930ds/134Mi)
% 63.58/14.52 % (60812)Instruction limit reached!
% 63.58/14.52 % (60812)------------------------------
% 63.58/14.52 % (60812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.58/14.52 % (60812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/14.52 % (60812)CaDiCaL version: 2.1.3
% 63.58/14.52 % (60812)Termination reason: Instruction limit
% 63.58/14.52 % (60812)Termination phase: SInE selection
% 63.58/14.52 % (60812)Time elapsed: 0.102 s
% 63.58/14.52 % (60812)Peak memory usage: 201 MB
% 63.58/14.52 % (60812)Instructions burned: 134 (million)
% 63.58/14.52 % (60805)Instruction limit reached!
% 63.58/14.52 % (60805)------------------------------
% 63.58/14.52 % (60805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.58/14.52 % (60805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/14.52 % (60805)CaDiCaL version: 2.1.3
% 63.58/14.52 % (60805)Termination reason: Instruction limit
% 63.58/14.52 % (60805)Termination phase: Preprocessing 1
% 63.58/14.52 % (60805)Time elapsed: 0.679 s
% 63.58/14.52 % (60805)Peak memory usage: 204 MB
% 63.58/14.52 % (60805)Instructions burned: 907 (million)
% 63.58/14.52 % (60814)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4192381207:st=8:i=592:sd=3:ep=RST:ss=axioms_2927 on theBenchmark for (2927ds/592Mi)
% 63.58/14.52 % (60815)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2942408540:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 63.58/14.52 % (60814)Instruction limit reached!
% 63.58/14.52 % (60814)------------------------------
% 63.58/14.52 % (60814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.58/14.52 % (60814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.58/14.52 % (60814)CaDiCaL version: 2.1.3
% 63.58/14.52 % (60814)Termination reason: Instruction limit
% 63.58/14.52 % (60814)Termination phase: SInE selection
% 63.58/14.52 % (60814)Time elapsed: 0.383 s
% 63.58/14.52 % (60814)Peak memory usage: 203 MB
% 63.58/14.52 % (60814)Instructions burned: 593 (million)
% 63.58/14.52 % (60818)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=517027199:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2922 on theBenchmark for (2922ds/125Mi)
% 63.58/14.52 % (60818)Instruction limit reached!
% 63.58/14.52 % (60818)------------------------------
% 63.58/14.52 % (60818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.58/14.52 % (60818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60818)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60818)Termination reason: Instruction limit
% 63.16/14.79 % (60818)Termination phase: Property scanning
% 63.16/14.79 % (60818)Time elapsed: 0.062 s
% 63.16/14.79 % (60818)Peak memory usage: 201 MB
% 63.16/14.79 % (60818)Instructions burned: 125 (million)
% 63.16/14.79 % (60797)Instruction limit reached!
% 63.16/14.79 % (60797)------------------------------
% 63.16/14.79 % (60797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60797)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60797)Termination reason: Instruction limit
% 63.16/14.79 % (60797)Termination phase: Preprocessing 3
% 63.16/14.79 % (60797)Time elapsed: 1.863 s
% 63.16/14.79 % (60797)Peak memory usage: 305 MB
% 63.16/14.79 % (60797)Instructions burned: 2351 (million)
% 63.16/14.79 % (60820)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3968291062:i=134:gtgl=5:slsql=off:gtg=exists_sym_2919 on theBenchmark for (2919ds/134Mi)
% 63.16/14.79 % (60821)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1616140195:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2919 on theBenchmark for (2919ds/141Mi)
% 63.16/14.79 % (60820)Instruction limit reached!
% 63.16/14.79 % (60820)------------------------------
% 63.16/14.79 % (60820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60820)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60820)Termination reason: Instruction limit
% 63.16/14.79 % (60820)Termination phase: Property scanning
% 63.16/14.79 % (60820)Time elapsed: 0.067 s
% 63.16/14.79 % (60820)Peak memory usage: 201 MB
% 63.16/14.79 % (60820)Instructions burned: 136 (million)
% 63.16/14.79 % (60821)Instruction limit reached!
% 63.16/14.79 % (60821)------------------------------
% 63.16/14.79 % (60821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60821)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60821)Termination reason: Instruction limit
% 63.16/14.79 % (60821)Termination phase: SInE selection
% 63.16/14.79 % (60821)Time elapsed: 0.111 s
% 63.16/14.79 % (60821)Peak memory usage: 201 MB
% 63.16/14.79 % (60821)Instructions burned: 141 (million)
% 63.16/14.79 % (60824)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2355739657:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2917 on theBenchmark for (2917ds/431Mi)
% 63.16/14.79 % (60825)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=491127735:i=6060:aac=none:ins=25_2916 on theBenchmark for (2916ds/6060Mi)
% 63.16/14.79 % (60808)Instruction limit reached!
% 63.16/14.79 % (60808)------------------------------
% 63.16/14.79 % (60808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60808)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60808)Termination reason: Instruction limit
% 63.16/14.79 % (60808)Termination phase: Saturation
% 63.16/14.79 % (60808)Time elapsed: 2.078 s
% 63.16/14.79 % (60808)Peak memory usage: 415 MB
% 63.16/14.79 % (60808)Instructions burned: 5204 (million)
% 63.16/14.79 % (60824)Instruction limit reached!
% 63.16/14.79 % (60824)------------------------------
% 63.16/14.79 % (60824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60824)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60824)Termination reason: Instruction limit
% 63.16/14.79 % (60824)Termination phase: SInE selection
% 63.16/14.79 % (60824)Time elapsed: 0.314 s
% 63.16/14.79 % (60824)Peak memory usage: 202 MB
% 63.16/14.79 % (60824)Instructions burned: 432 (million)
% 63.16/14.79 % (60828)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=1077954674:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2912 on theBenchmark for (2912ds/150Mi)
% 63.16/14.79 % (60828)Instruction limit reached!
% 63.16/14.79 % (60828)------------------------------
% 63.16/14.79 % (60828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60828)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60828)Termination reason: Instruction limit
% 63.16/14.79 % (60828)Termination phase: SInE selection
% 63.16/14.79 % (60828)Time elapsed: 0.071 s
% 63.16/14.79 % (60828)Peak memory usage: 201 MB
% 63.16/14.79 % (60828)Instructions burned: 152 (million)
% 63.16/14.79 % (60829)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1525894796:i=14155:bd=all_2912 on theBenchmark for (2912ds/14155Mi)
% 63.16/14.79 % (60831)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3586319846:i=667:av=off:fsr=off_2910 on theBenchmark for (2910ds/667Mi)
% 63.16/14.79 % (60831)Instruction limit reached!
% 63.16/14.79 % (60831)------------------------------
% 63.16/14.79 % (60831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60831)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60831)Termination reason: Instruction limit
% 63.16/14.79 % (60831)Termination phase: Preprocessing 2
% 63.16/14.79 % (60831)Time elapsed: 0.395 s
% 63.16/14.79 % (60831)Peak memory usage: 218 MB
% 63.16/14.79 % (60831)Instructions burned: 667 (million)
% 63.16/14.79 % (60834)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=3452968796:s2a=on:i=185:s2at=1.8:fdi=4_2905 on theBenchmark for (2905ds/185Mi)
% 63.16/14.79 % (60834)Instruction limit reached!
% 63.16/14.79 % (60834)------------------------------
% 63.16/14.79 % (60834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60834)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60834)Termination reason: Instruction limit
% 63.16/14.79 % (60834)Termination phase: SInE selection
% 63.16/14.79 % (60834)Time elapsed: 0.088 s
% 63.16/14.79 % (60834)Peak memory usage: 201 MB
% 63.16/14.79 % (60834)Instructions burned: 187 (million)
% 63.16/14.79 % (60836)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=554364955:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2902 on theBenchmark for (2902ds/193Mi)
% 63.16/14.79 % (60836)Instruction limit reached!
% 63.16/14.79 % (60836)------------------------------
% 63.16/14.79 % (60836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60836)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60836)Termination reason: Instruction limit
% 63.16/14.79 % (60836)Termination phase: SInE selection
% 63.16/14.79 % (60836)Time elapsed: 0.094 s
% 63.16/14.79 % (60836)Peak memory usage: 201 MB
% 63.16/14.79 % (60836)Instructions burned: 193 (million)
% 63.16/14.79 % (60838)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2704416829:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2900 on theBenchmark for (2900ds/4850Mi)
% 63.16/14.79 % (60838)Instruction limit reached!
% 63.16/14.79 % (60838)------------------------------
% 63.16/14.79 % (60838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60838)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60838)Termination reason: Instruction limit
% 63.16/14.79 % (60838)Termination phase: Property scanning
% 63.16/14.79 % (60838)Time elapsed: 2.089 s
% 63.16/14.79 % (60838)Peak memory usage: 362 MB
% 63.16/14.79 % (60838)Instructions burned: 4854 (million)
% 63.16/14.79 % (60840)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3953210112:i=12111:sd=1:ss=included_2877 on theBenchmark for (2877ds/12111Mi)
% 63.16/14.79 % (60825)Instruction limit reached!
% 63.16/14.79 % (60825)------------------------------
% 63.16/14.79 % (60825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.16/14.79 % (60825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.16/14.79 % (60825)CaDiCaL version: 2.1.3
% 63.16/14.79 % (60825)Termination reason: Instruction limit
% 63.16/14.79 % (60825)Termination phase: NewCNF
% 63.16/14.79 % (60825)Time elapsed: 4.926 s
% 63.16/14.79 % (60825)Peak memory usage: 381 MB
% 63.16/14.79 % (60825)Instructions burned: 6060 (million)
% 63.16/14.79 % (60840)First to succeed.
% 63.16/14.79 % (60842)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2980235535:i=319:kws=precedence:fsr=off_2864 on theBenchmark for (2864ds/319Mi)
% 63.16/14.79 % (60840)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-60769"
% 63.16/14.79 % (60840)Refutation found. Thanks to Tanya!
% 63.16/14.79 % SZS status Theorem for theBenchmark
% 63.16/14.79 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/14.91 % (60840)------------------------------
% 0.15/14.91 % (60840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/14.91 % (60840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/14.91 % (60840)CaDiCaL version: 2.1.3
% 0.15/14.91 % (60840)Termination reason: Refutation
% 0.15/14.91 % (60840)Time elapsed: 1.338 s
% 0.15/14.91 % (60840)Peak memory usage: 298 MB
% 0.15/14.91 % (60840)Instructions burned: 3326 (million)
% 0.15/14.91 % (60840)------------------------------
% 0.15/14.91 % (60840)------------------------------
% 0.15/14.91 % (60769)Success in time 13.963 s
% 0.15/14.91 % Vampire exiting
%------------------------------------------------------------------------------