%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU443+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 : n009.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:07 PM UTC 2026
% Result : Theorem 38.55s 16.77s
% Output : Refutation 78.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 47
% Syntax : Number of formulae : 265 ( 53 unt; 33 def)
% Number of atoms : 790 ( 72 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 979 ( 454 ~; 456 |; 19 &)
% ( 33 <=>; 16 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 29 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 9 con; 0-5 aty)
% Number of variables : 171 ( 1 sgn 159 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f70,axiom,
! [X0,X1,X2] :
( ( r1_tarski(X0,X1)
& r1_tarski(X1,X2) )
=> r1_tarski(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f907,axiom,
! [X0] :
( v1_relat_1(X0)
=> k4_relat_1(k4_relat_1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k4_relat_1) ).
fof(f1422,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f1481,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f1483,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(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(f1500,axiom,
! [X0,X1,X2] :
( m1_relset_1(X2,X0,X1)
=> k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_relset_1) ).
fof(f1508,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/sandbox/benchmark/theBenchmark.p',redefinition_k10_relset_1) ).
fof(f6128,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/sandbox/benchmark/theBenchmark.p',t21_funct_5) ).
fof(f71077,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/sandbox/benchmark/theBenchmark.p',dt_k9_relset_2) ).
fof(f71133,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/sandbox/benchmark/theBenchmark.p',t51_relset_2) ).
fof(f71136,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X0))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k1_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_relset_2) ).
fof(f71137,conjecture,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k2_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t55_relset_2) ).
fof(f71138,negated_conjecture,
~ ! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
=> ! [X3] :
( m2_relset_1(X3,X0,X1)
=> ( r1_tarski(X2,k2_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f71137]) ).
fof(f71154,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f71225,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,[],[f71077]) ).
fof(f71226,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,[],[f71225]) ).
fof(f71289,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,[],[f71133]) ).
fof(f71292,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( r1_tarski(X2,k1_funct_5(X3))
<=> r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) )
| ~ m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f71136]) ).
fof(f71293,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( r1_tarski(X2,k2_funct_5(X3))
<~> r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f71138]) ).
fof(f71394,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(f71395,plain,
! [X0,X1,X2] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f1422]) ).
fof(f71797,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f71798,plain,
! [X0,X1,X2] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(flattening,[],[f71797]) ).
fof(f71849,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,[],[f1508]) ).
fof(f72271,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(ennf_transformation,[],[f907]) ).
fof(f72296,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,[],[f6128]) ).
fof(f72305,plain,
! [X0,X1,X2] :
( k6_relset_1(X0,X1,X2) = k4_relat_1(X2)
| ~ m1_relset_1(X2,X0,X1) ),
inference(ennf_transformation,[],[f1500]) ).
fof(f72307,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(f72361,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( ( r1_tarski(X2,k1_funct_5(X3))
| ~ r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) )
& ( r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2))
| ~ r1_tarski(X2,k1_funct_5(X3)) ) )
| ~ m2_relset_1(X3,X0,X1) )
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f71292]) ).
fof(f72362,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ~ r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| ~ r1_tarski(X2,k2_funct_5(X3)) )
& ( r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| r1_tarski(X2,k2_funct_5(X3)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X1)) ),
inference(nnf_transformation,[],[f71293]) ).
fof(f72363,plain,
? [X0,X1,X2] :
( ? [X3] :
( ( ~ r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| ~ r1_tarski(X2,k2_funct_5(X3)) )
& ( r1_tarski(X2,k10_relset_1(X1,X1,k9_relset_2(X1,X0,X1,k6_relset_1(X0,X1,X3),X3),X2))
| r1_tarski(X2,k2_funct_5(X3)) )
& m2_relset_1(X3,X0,X1) )
& m1_subset_1(X2,k1_zfmisc_1(X1)) ),
inference(flattening,[],[f72362]) ).
fof(f72364,plain,
( ( ~ r1_tarski(sK29,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,k6_relset_1(sK27,sK28,sK30),sK30),sK29))
| ~ r1_tarski(sK29,k2_funct_5(sK30)) )
& ( r1_tarski(sK29,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,k6_relset_1(sK27,sK28,sK30),sK30),sK29))
| r1_tarski(sK29,k2_funct_5(sK30)) )
& m2_relset_1(sK30,sK27,sK28)
& m1_subset_1(sK29,k1_zfmisc_1(sK28)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29),skolemize(X3,sK30)],[f72363]) ).
fof(f72390,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(f72785,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| m2_relset_1(k9_relset_2(X0,X1,X2,X3,X4),X0,X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f71226]) ).
fof(f72866,plain,
! [X2,X0,X1] :
( k10_relset_1(X1,X0,X2,X1) = k2_funct_5(X2)
| ~ m2_relset_1(X2,X1,X0) ),
inference(cnf_transformation,[],[f71289]) ).
fof(f72867,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X1,X0)
| k1_funct_5(X2) = k10_relset_1(X0,X1,k6_relset_1(X1,X0,X2),X0) ),
inference(cnf_transformation,[],[f71289]) ).
fof(f72872,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ r1_tarski(X2,k1_funct_5(X3))
| ~ m2_relset_1(X3,X0,X1)
| r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2)) ),
inference(cnf_transformation,[],[f72361]) ).
fof(f72873,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(X3,X0,X1)
| ~ r1_tarski(X2,k10_relset_1(X0,X0,k9_relset_2(X0,X1,X0,X3,k6_relset_1(X0,X1,X3)),X2))
| r1_tarski(X2,k1_funct_5(X3))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f72361]) ).
fof(f72874,plain,
m1_subset_1(sK29,k1_zfmisc_1(sK28)),
inference(cnf_transformation,[],[f72364]) ).
fof(f72875,plain,
m2_relset_1(sK30,sK27,sK28),
inference(cnf_transformation,[],[f72364]) ).
fof(f72876,plain,
( r1_tarski(sK29,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,k6_relset_1(sK27,sK28,sK30),sK30),sK29))
| r1_tarski(sK29,k2_funct_5(sK30)) ),
inference(cnf_transformation,[],[f72364]) ).
fof(f72877,plain,
( ~ r1_tarski(sK29,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,k6_relset_1(sK27,sK28,sK30),sK30),sK29))
| ~ r1_tarski(sK29,k2_funct_5(sK30)) ),
inference(cnf_transformation,[],[f72364]) ).
fof(f73025,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f72390]) ).
fof(f73040,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71394]) ).
fof(f73041,plain,
! [X2,X0,X1] :
( v1_relat_1(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f71395]) ).
fof(f73640,plain,
! [X2,X0,X1] :
( r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X2) ),
inference(cnf_transformation,[],[f71798]) ).
fof(f73644,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f71154]) ).
fof(f73720,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k10_relset_1(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f71849]) ).
fof(f74355,plain,
! [X0] :
( k4_relat_1(k4_relat_1(X0)) = X0
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[],[f72271]) ).
fof(f74409,plain,
! [X0] :
( ~ v1_relat_1(X0)
| k1_relat_1(X0) = k1_funct_5(X0) ),
inference(cnf_transformation,[],[f72296]) ).
fof(f74450,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| k6_relset_1(X0,X1,X2) = k4_relat_1(X2) ),
inference(cnf_transformation,[],[f72305]) ).
fof(f74452,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(k6_relset_1(X0,X1,X2),X1,X0) ),
inference(cnf_transformation,[],[f72307]) ).
fof(f75250,definition,
sF304 = k6_relset_1(sK27,sK28,sK30),
introduced(definition,[new_symbols(definition,[sF304])],[function_definition]) ).
fof(f75251,plain,
k6_relset_1(sK27,sK28,sK30) = sF304,
inference(reorient_equations,[],[f75250]) ).
fof(f75252,definition,
sF305 = k9_relset_2(sK28,sK27,sK28,sF304,sK30),
introduced(definition,[new_symbols(definition,[sF305])],[function_definition]) ).
fof(f75253,plain,
k9_relset_2(sK28,sK27,sK28,sF304,sK30) = sF305,
inference(reorient_equations,[],[f75252]) ).
fof(f75254,definition,
sF306 = k10_relset_1(sK28,sK28,sF305,sK29),
introduced(definition,[new_symbols(definition,[sF306])],[function_definition]) ).
fof(f75255,plain,
k10_relset_1(sK28,sK28,sF305,sK29) = sF306,
inference(reorient_equations,[],[f75254]) ).
fof(f75256,definition,
sF307 = k2_funct_5(sK30),
introduced(definition,[new_symbols(definition,[sF307])],[function_definition]) ).
fof(f75257,plain,
k2_funct_5(sK30) = sF307,
inference(reorient_equations,[],[f75256]) ).
fof(f75258,plain,
( ~ r1_tarski(sK29,sF306)
| ~ r1_tarski(sK29,sF307) ),
inference(definition_folding,[],[f72877,f75257,f75255,f75253,f75251]) ).
fof(f75259,plain,
( r1_tarski(sK29,sF306)
| r1_tarski(sK29,sF307) ),
inference(definition_folding,[],[f72876,f75257,f75255,f75253,f75251]) ).
fof(f75260,definition,
sF308 = k1_zfmisc_1(sK28),
introduced(definition,[new_symbols(definition,[sF308])],[function_definition]) ).
fof(f75261,plain,
k1_zfmisc_1(sK28) = sF308,
inference(reorient_equations,[],[f75260]) ).
fof(f75262,plain,
m1_subset_1(sK29,sF308),
inference(definition_folding,[],[f72874,f75261]) ).
fof(f75597,definition,
( spl309_46
<=> m1_subset_1(sK29,sF308) ),
introduced(definition,[new_symbols(definition,[spl309_46])],[avatar_definition]) ).
fof(f75599,plain,
( m1_subset_1(sK29,sF308)
| ~ spl309_46 ),
inference(avatar_component_clause,[],[f75597]) ).
fof(f75600,plain,
spl309_46,
inference(avatar_split_clause,[],[f75262,f75597]) ).
fof(f75602,definition,
( spl309_47
<=> m2_relset_1(sK30,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_47])],[avatar_definition]) ).
fof(f75604,plain,
( m2_relset_1(sK30,sK27,sK28)
| ~ spl309_47 ),
inference(avatar_component_clause,[],[f75602]) ).
fof(f75605,plain,
spl309_47,
inference(avatar_split_clause,[],[f72875,f75602]) ).
fof(f75607,definition,
( spl309_48
<=> r1_tarski(sK29,sF307) ),
introduced(definition,[new_symbols(definition,[spl309_48])],[avatar_definition]) ).
fof(f75608,plain,
( ~ r1_tarski(sK29,sF307)
| spl309_48 ),
inference(avatar_component_clause,[],[f75607]) ).
fof(f75609,plain,
( r1_tarski(sK29,sF307)
| ~ spl309_48 ),
inference(avatar_component_clause,[],[f75607]) ).
fof(f75611,definition,
( spl309_49
<=> r1_tarski(sK29,sF306) ),
introduced(definition,[new_symbols(definition,[spl309_49])],[avatar_definition]) ).
fof(f75612,plain,
( ~ r1_tarski(sK29,sF306)
| spl309_49 ),
inference(avatar_component_clause,[],[f75611]) ).
fof(f75613,plain,
( r1_tarski(sK29,sF306)
| ~ spl309_49 ),
inference(avatar_component_clause,[],[f75611]) ).
fof(f75614,plain,
( spl309_48
| spl309_49 ),
inference(avatar_split_clause,[],[f75259,f75611,f75607]) ).
fof(f75615,plain,
( ~ spl309_48
| ~ spl309_49 ),
inference(avatar_split_clause,[],[f75258,f75611,f75607]) ).
fof(f75630,definition,
( spl309_51
<=> k6_relset_1(sK27,sK28,sK30) = sF304 ),
introduced(definition,[new_symbols(definition,[spl309_51])],[avatar_definition]) ).
fof(f75632,plain,
( k6_relset_1(sK27,sK28,sK30) = sF304
| ~ spl309_51 ),
inference(avatar_component_clause,[],[f75630]) ).
fof(f75633,plain,
spl309_51,
inference(avatar_split_clause,[],[f75251,f75630]) ).
fof(f75635,definition,
( spl309_52
<=> k9_relset_2(sK28,sK27,sK28,sF304,sK30) = sF305 ),
introduced(definition,[new_symbols(definition,[spl309_52])],[avatar_definition]) ).
fof(f75637,plain,
( k9_relset_2(sK28,sK27,sK28,sF304,sK30) = sF305
| ~ spl309_52 ),
inference(avatar_component_clause,[],[f75635]) ).
fof(f75638,plain,
spl309_52,
inference(avatar_split_clause,[],[f75253,f75635]) ).
fof(f75640,definition,
( spl309_53
<=> k10_relset_1(sK28,sK28,sF305,sK29) = sF306 ),
introduced(definition,[new_symbols(definition,[spl309_53])],[avatar_definition]) ).
fof(f75642,plain,
( k10_relset_1(sK28,sK28,sF305,sK29) = sF306
| ~ spl309_53 ),
inference(avatar_component_clause,[],[f75640]) ).
fof(f75643,plain,
spl309_53,
inference(avatar_split_clause,[],[f75255,f75640]) ).
fof(f75645,definition,
( spl309_54
<=> k2_funct_5(sK30) = sF307 ),
introduced(definition,[new_symbols(definition,[spl309_54])],[avatar_definition]) ).
fof(f75647,plain,
( k2_funct_5(sK30) = sF307
| ~ spl309_54 ),
inference(avatar_component_clause,[],[f75645]) ).
fof(f75648,plain,
spl309_54,
inference(avatar_split_clause,[],[f75257,f75645]) ).
fof(f75650,definition,
( spl309_55
<=> k1_zfmisc_1(sK28) = sF308 ),
introduced(definition,[new_symbols(definition,[spl309_55])],[avatar_definition]) ).
fof(f75652,plain,
( k1_zfmisc_1(sK28) = sF308
| ~ spl309_55 ),
inference(avatar_component_clause,[],[f75650]) ).
fof(f75653,plain,
spl309_55,
inference(avatar_split_clause,[],[f75261,f75650]) ).
fof(f75758,definition,
( spl309_61
<=> m2_relset_1(sF304,sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_61])],[avatar_definition]) ).
fof(f75759,plain,
( m2_relset_1(sF304,sK28,sK27)
| ~ spl309_61 ),
inference(avatar_component_clause,[],[f75758]) ).
fof(f75760,plain,
( ~ m2_relset_1(sF304,sK28,sK27)
| spl309_61 ),
inference(avatar_component_clause,[],[f75758]) ).
fof(f75771,plain,
( m1_subset_1(sK30,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_47 ),
inference(resolution,[],[f73040,f75604]) ).
fof(f75773,definition,
( spl309_63
<=> m1_subset_1(sK30,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28))) ),
introduced(definition,[new_symbols(definition,[spl309_63])],[avatar_definition]) ).
fof(f75775,plain,
( m1_subset_1(sK30,k1_zfmisc_1(k2_zfmisc_1(sK27,sK28)))
| ~ spl309_63 ),
inference(avatar_component_clause,[],[f75773]) ).
fof(f75776,plain,
( spl309_63
| ~ spl309_47 ),
inference(avatar_split_clause,[],[f75771,f75602,f75773]) ).
fof(f75800,plain,
( ! [X2,X0,X1] :
( ~ m2_relset_1(X1,sK28,X2)
| ~ r1_tarski(X0,k1_funct_5(X1))
| ~ m1_subset_1(X0,sF308)
| r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,X2,sK28,X1,k6_relset_1(sK28,X2,X1)),X0)) )
| ~ spl309_55 ),
inference(superposition,[],[f72872,f75652]) ).
fof(f75815,plain,
( v1_relat_1(sK30)
| ~ spl309_63 ),
inference(unit_resulting_resolution,[],[f73041,f75775]) ).
fof(f75817,definition,
( spl309_68
<=> v1_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_68])],[avatar_definition]) ).
fof(f75819,plain,
( v1_relat_1(sK30)
| ~ spl309_68 ),
inference(avatar_component_clause,[],[f75817]) ).
fof(f75820,plain,
( spl309_68
| ~ spl309_63 ),
inference(avatar_split_clause,[],[f75815,f75773,f75817]) ).
fof(f75913,plain,
( m1_relset_1(sK30,sK27,sK28)
| ~ spl309_47 ),
inference(resolution,[],[f73025,f75604]) ).
fof(f75915,definition,
( spl309_74
<=> m1_relset_1(sK30,sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_74])],[avatar_definition]) ).
fof(f75917,plain,
( m1_relset_1(sK30,sK27,sK28)
| ~ spl309_74 ),
inference(avatar_component_clause,[],[f75915]) ).
fof(f75918,plain,
( spl309_74
| ~ spl309_47 ),
inference(avatar_split_clause,[],[f75913,f75602,f75915]) ).
fof(f75921,plain,
( m2_relset_1(k6_relset_1(sK27,sK28,sK30),sK28,sK27)
| ~ spl309_74 ),
inference(unit_resulting_resolution,[],[f74452,f75917]) ).
fof(f75927,plain,
( k6_relset_1(sK27,sK28,sK30) = k4_relat_1(sK30)
| ~ spl309_74 ),
inference(resolution,[],[f75917,f74450]) ).
fof(f75930,plain,
( sF304 = k4_relat_1(sK30)
| ~ spl309_51
| ~ spl309_74 ),
inference(forward_demodulation,[],[f75927,f75632]) ).
fof(f75934,plain,
( m2_relset_1(sF304,sK28,sK27)
| ~ spl309_51
| ~ spl309_74 ),
inference(forward_demodulation,[],[f75921,f75632]) ).
fof(f75939,definition,
( spl309_75
<=> sF304 = k4_relat_1(sK30) ),
introduced(definition,[new_symbols(definition,[spl309_75])],[avatar_definition]) ).
fof(f75941,plain,
( sF304 = k4_relat_1(sK30)
| ~ spl309_75 ),
inference(avatar_component_clause,[],[f75939]) ).
fof(f75942,plain,
( spl309_75
| ~ spl309_51
| ~ spl309_74 ),
inference(avatar_split_clause,[],[f75930,f75915,f75630,f75939]) ).
fof(f75950,plain,
( $false
| ~ spl309_51
| spl309_61
| ~ spl309_74 ),
inference(forward_subsumption_resolution,[],[f75934,f75760]) ).
fof(f75951,plain,
( ~ spl309_51
| spl309_61
| ~ spl309_74 ),
inference(avatar_contradiction_clause,[],[f75950]) ).
fof(f75989,plain,
( m1_relset_1(sF304,sK28,sK27)
| ~ spl309_61 ),
inference(resolution,[],[f75759,f73025]) ).
fof(f75991,plain,
( k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sK27)
| ~ spl309_61 ),
inference(resolution,[],[f75759,f72867]) ).
fof(f75992,plain,
( m1_subset_1(sF304,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27)))
| ~ spl309_61 ),
inference(resolution,[],[f75759,f73040]) ).
fof(f75995,definition,
( spl309_79
<=> m1_subset_1(sF304,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27))) ),
introduced(definition,[new_symbols(definition,[spl309_79])],[avatar_definition]) ).
fof(f75997,plain,
( m1_subset_1(sF304,k1_zfmisc_1(k2_zfmisc_1(sK28,sK27)))
| ~ spl309_79 ),
inference(avatar_component_clause,[],[f75995]) ).
fof(f75998,plain,
( spl309_79
| ~ spl309_61 ),
inference(avatar_split_clause,[],[f75992,f75758,f75995]) ).
fof(f76000,definition,
( spl309_80
<=> k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sK27) ),
introduced(definition,[new_symbols(definition,[spl309_80])],[avatar_definition]) ).
fof(f76002,plain,
( k1_funct_5(sF304) = k10_relset_1(sK27,sK28,k6_relset_1(sK28,sK27,sF304),sK27)
| ~ spl309_80 ),
inference(avatar_component_clause,[],[f76000]) ).
fof(f76003,plain,
( spl309_80
| ~ spl309_61 ),
inference(avatar_split_clause,[],[f75991,f75758,f76000]) ).
fof(f76005,definition,
( spl309_81
<=> m1_relset_1(sF304,sK28,sK27) ),
introduced(definition,[new_symbols(definition,[spl309_81])],[avatar_definition]) ).
fof(f76007,plain,
( m1_relset_1(sF304,sK28,sK27)
| ~ spl309_81 ),
inference(avatar_component_clause,[],[f76005]) ).
fof(f76008,plain,
( spl309_81
| ~ spl309_61 ),
inference(avatar_split_clause,[],[f75989,f75758,f76005]) ).
fof(f76097,plain,
( m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28)
| ~ spl309_81 ),
inference(resolution,[],[f76007,f74452]) ).
fof(f76098,plain,
( k6_relset_1(sK28,sK27,sF304) = k4_relat_1(sF304)
| ~ spl309_81 ),
inference(resolution,[],[f76007,f74450]) ).
fof(f76101,definition,
( spl309_90
<=> k6_relset_1(sK28,sK27,sF304) = k4_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_90])],[avatar_definition]) ).
fof(f76103,plain,
( k6_relset_1(sK28,sK27,sF304) = k4_relat_1(sF304)
| ~ spl309_90 ),
inference(avatar_component_clause,[],[f76101]) ).
fof(f76104,plain,
( spl309_90
| ~ spl309_81 ),
inference(avatar_split_clause,[],[f76098,f76005,f76101]) ).
fof(f76106,definition,
( spl309_91
<=> m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_91])],[avatar_definition]) ).
fof(f76108,plain,
( m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28)
| ~ spl309_91 ),
inference(avatar_component_clause,[],[f76106]) ).
fof(f76109,plain,
( spl309_91
| ~ spl309_81 ),
inference(avatar_split_clause,[],[f76097,f76005,f76106]) ).
fof(f76115,plain,
( m2_relset_1(k4_relat_1(sF304),sK27,sK28)
| ~ spl309_90
| ~ spl309_91 ),
inference(forward_demodulation,[],[f76108,f76103]) ).
fof(f76118,definition,
( spl309_93
<=> m2_relset_1(k4_relat_1(sF304),sK27,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_93])],[avatar_definition]) ).
fof(f76120,plain,
( m2_relset_1(k4_relat_1(sF304),sK27,sK28)
| ~ spl309_93 ),
inference(avatar_component_clause,[],[f76118]) ).
fof(f76121,plain,
( spl309_93
| ~ spl309_90
| ~ spl309_91 ),
inference(avatar_split_clause,[],[f76115,f76106,f76101,f76118]) ).
fof(f76168,plain,
( v1_relat_1(sF304)
| ~ spl309_79 ),
inference(unit_resulting_resolution,[],[f73041,f75997]) ).
fof(f76170,plain,
( m2_relset_1(k9_relset_2(sK28,sK27,sK28,sF304,sK30),sK28,sK28)
| ~ spl309_63
| ~ spl309_79 ),
inference(unit_resulting_resolution,[],[f72785,f75775,f75997]) ).
fof(f76184,definition,
( spl309_98
<=> v1_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_98])],[avatar_definition]) ).
fof(f76186,plain,
( v1_relat_1(sF304)
| ~ spl309_98 ),
inference(avatar_component_clause,[],[f76184]) ).
fof(f76187,plain,
( spl309_98
| ~ spl309_79 ),
inference(avatar_split_clause,[],[f76168,f75995,f76184]) ).
fof(f76193,plain,
( m2_relset_1(sF305,sK28,sK28)
| ~ spl309_52
| ~ spl309_63
| ~ spl309_79 ),
inference(forward_demodulation,[],[f76170,f75637]) ).
fof(f76201,definition,
( spl309_101
<=> m2_relset_1(sF305,sK28,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_101])],[avatar_definition]) ).
fof(f76203,plain,
( m2_relset_1(sF305,sK28,sK28)
| ~ spl309_101 ),
inference(avatar_component_clause,[],[f76201]) ).
fof(f76204,plain,
( spl309_101
| ~ spl309_52
| ~ spl309_63
| ~ spl309_79 ),
inference(avatar_split_clause,[],[f76193,f75995,f75773,f75635,f76201]) ).
fof(f76232,plain,
( m1_relset_1(sF305,sK28,sK28)
| ~ spl309_101 ),
inference(resolution,[],[f76203,f73025]) ).
fof(f76248,definition,
( spl309_106
<=> m1_relset_1(sF305,sK28,sK28) ),
introduced(definition,[new_symbols(definition,[spl309_106])],[avatar_definition]) ).
fof(f76250,plain,
( m1_relset_1(sF305,sK28,sK28)
| ~ spl309_106 ),
inference(avatar_component_clause,[],[f76248]) ).
fof(f76251,plain,
( spl309_106
| ~ spl309_101 ),
inference(avatar_split_clause,[],[f76232,f76201,f76248]) ).
fof(f76346,plain,
( ! [X0] : k10_relset_1(sK28,sK28,sF305,X0) = k9_relat_1(sF305,X0)
| ~ spl309_106 ),
inference(resolution,[],[f76250,f73720]) ).
fof(f76383,plain,
( sF306 = k9_relat_1(sF305,sK29)
| ~ spl309_53
| ~ spl309_106 ),
inference(superposition,[],[f75642,f76346]) ).
fof(f76387,definition,
( spl309_125
<=> sF306 = k9_relat_1(sF305,sK29) ),
introduced(definition,[new_symbols(definition,[spl309_125])],[avatar_definition]) ).
fof(f76389,plain,
( sF306 = k9_relat_1(sF305,sK29)
| ~ spl309_125 ),
inference(avatar_component_clause,[],[f76387]) ).
fof(f76390,plain,
( spl309_125
| ~ spl309_53
| ~ spl309_106 ),
inference(avatar_split_clause,[],[f76383,f76248,f75640,f76387]) ).
fof(f76809,plain,
( k1_funct_5(sF304) = k2_funct_5(k6_relset_1(sK28,sK27,sF304))
| ~ m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28)
| ~ spl309_80 ),
inference(superposition,[],[f72866,f76002]) ).
fof(f76810,plain,
( k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304))
| ~ m2_relset_1(k6_relset_1(sK28,sK27,sF304),sK27,sK28)
| ~ spl309_80
| ~ spl309_90 ),
inference(forward_demodulation,[],[f76809,f76103]) ).
fof(f76817,plain,
( ~ m2_relset_1(k4_relat_1(sF304),sK27,sK28)
| k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304))
| ~ spl309_80
| ~ spl309_90 ),
inference(forward_demodulation,[],[f76810,f76103]) ).
fof(f76819,plain,
( k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304))
| ~ spl309_80
| ~ spl309_90
| ~ spl309_93 ),
inference(forward_subsumption_resolution,[],[f76817,f76120]) ).
fof(f76822,definition,
( spl309_161
<=> k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304)) ),
introduced(definition,[new_symbols(definition,[spl309_161])],[avatar_definition]) ).
fof(f76824,plain,
( k1_funct_5(sF304) = k2_funct_5(k4_relat_1(sF304))
| ~ spl309_161 ),
inference(avatar_component_clause,[],[f76822]) ).
fof(f76825,plain,
( spl309_161
| ~ spl309_80
| ~ spl309_90
| ~ spl309_93 ),
inference(avatar_split_clause,[],[f76819,f76118,f76101,f76000,f76822]) ).
fof(f77231,plain,
( ! [X0] :
( ~ r1_tarski(sK29,X0)
| ~ r1_tarski(X0,sF306) )
| spl309_49 ),
inference(resolution,[],[f75612,f73640]) ).
fof(f77971,plain,
( k1_funct_5(sF304) = k1_relat_1(sF304)
| ~ spl309_98 ),
inference(resolution,[],[f74409,f76186]) ).
fof(f77979,definition,
( spl309_251
<=> k1_funct_5(sF304) = k1_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_251])],[avatar_definition]) ).
fof(f77981,plain,
( k1_funct_5(sF304) = k1_relat_1(sF304)
| ~ spl309_251 ),
inference(avatar_component_clause,[],[f77979]) ).
fof(f77982,plain,
( spl309_251
| ~ spl309_98 ),
inference(avatar_split_clause,[],[f77971,f76184,f77979]) ).
fof(f78591,plain,
( sK30 = k4_relat_1(sF304)
| ~ v1_relat_1(sK30)
| ~ spl309_75 ),
inference(superposition,[],[f74355,f75941]) ).
fof(f78592,plain,
( sK30 = k4_relat_1(sF304)
| ~ spl309_68
| ~ spl309_75 ),
inference(forward_subsumption_resolution,[],[f78591,f75819]) ).
fof(f78605,definition,
( spl309_305
<=> sK30 = k4_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_305])],[avatar_definition]) ).
fof(f78607,plain,
( sK30 = k4_relat_1(sF304)
| ~ spl309_305 ),
inference(avatar_component_clause,[],[f78605]) ).
fof(f78608,plain,
( spl309_305
| ~ spl309_68
| ~ spl309_75 ),
inference(avatar_split_clause,[],[f78592,f75939,f75817,f78605]) ).
fof(f79075,plain,
( k2_funct_5(sK30) = k1_funct_5(sF304)
| ~ spl309_161
| ~ spl309_305 ),
inference(superposition,[],[f76824,f78607]) ).
fof(f79080,plain,
( k2_funct_5(sK30) = k1_relat_1(sF304)
| ~ spl309_161
| ~ spl309_251
| ~ spl309_305 ),
inference(forward_demodulation,[],[f79075,f77981]) ).
fof(f79083,plain,
( sF307 = k1_relat_1(sF304)
| ~ spl309_54
| ~ spl309_161
| ~ spl309_251
| ~ spl309_305 ),
inference(forward_demodulation,[],[f79080,f75647]) ).
fof(f79086,definition,
( spl309_342
<=> sF307 = k1_relat_1(sF304) ),
introduced(definition,[new_symbols(definition,[spl309_342])],[avatar_definition]) ).
fof(f79088,plain,
( sF307 = k1_relat_1(sF304)
| ~ spl309_342 ),
inference(avatar_component_clause,[],[f79086]) ).
fof(f79089,plain,
( spl309_342
| ~ spl309_54
| ~ spl309_161
| ~ spl309_251
| ~ spl309_305 ),
inference(avatar_split_clause,[],[f79083,f78605,f77979,f76822,f75645,f79086]) ).
fof(f79226,plain,
( ! [X0] :
( ~ r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,k6_relset_1(sK28,sK27,sF304)),X0))
| r1_tarski(X0,k1_funct_5(sF304))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_61 ),
inference(resolution,[],[f72873,f75759]) ).
fof(f79229,plain,
( ! [X0] :
( ~ r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304)),X0))
| r1_tarski(X0,k1_funct_5(sF304))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_61
| ~ spl309_90 ),
inference(forward_demodulation,[],[f79226,f76103]) ).
fof(f79233,plain,
( ! [X0] :
( ~ r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,sK30),X0))
| r1_tarski(X0,k1_funct_5(sF304))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_61
| ~ spl309_90
| ~ spl309_305 ),
inference(forward_demodulation,[],[f79229,f78607]) ).
fof(f79237,plain,
( ! [X0] :
( ~ r1_tarski(X0,k10_relset_1(sK28,sK28,sF305,X0))
| r1_tarski(X0,k1_funct_5(sF304))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_52
| ~ spl309_61
| ~ spl309_90
| ~ spl309_305 ),
inference(forward_demodulation,[],[f79233,f75637]) ).
fof(f79240,plain,
( ! [X0] :
( ~ r1_tarski(X0,k9_relat_1(sF305,X0))
| r1_tarski(X0,k1_funct_5(sF304))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_52
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_305 ),
inference(forward_demodulation,[],[f79237,f76346]) ).
fof(f79242,plain,
( ! [X0] :
( r1_tarski(X0,k1_relat_1(sF304))
| ~ r1_tarski(X0,k9_relat_1(sF305,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_52
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305 ),
inference(forward_demodulation,[],[f79240,f77981]) ).
fof(f79244,plain,
( ! [X0] :
( r1_tarski(X0,sF307)
| ~ r1_tarski(X0,k9_relat_1(sF305,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(sK28)) )
| ~ spl309_52
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79242,f79088]) ).
fof(f79245,plain,
( ! [X0] :
( r1_tarski(X0,sF307)
| ~ m1_subset_1(X0,sF308)
| ~ r1_tarski(X0,k9_relat_1(sF305,X0)) )
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79244,f75652]) ).
fof(f79840,plain,
( ! [X0] :
( ~ r1_tarski(X0,k1_funct_5(sF304))
| ~ m1_subset_1(X0,sF308)
| r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,k6_relset_1(sK28,sK27,sF304)),X0)) )
| ~ spl309_55
| ~ spl309_61 ),
inference(resolution,[],[f75800,f75759]) ).
fof(f79843,plain,
( ! [X0] :
( ~ r1_tarski(X0,k1_relat_1(sF304))
| ~ m1_subset_1(X0,sF308)
| r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,k6_relset_1(sK28,sK27,sF304)),X0)) )
| ~ spl309_55
| ~ spl309_61
| ~ spl309_251 ),
inference(forward_demodulation,[],[f79840,f77981]) ).
fof(f79845,plain,
( ! [X0] :
( ~ r1_tarski(X0,sF307)
| ~ m1_subset_1(X0,sF308)
| r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,k6_relset_1(sK28,sK27,sF304)),X0)) )
| ~ spl309_55
| ~ spl309_61
| ~ spl309_251
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79843,f79088]) ).
fof(f79846,plain,
( ! [X0] :
( r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,k4_relat_1(sF304)),X0))
| ~ r1_tarski(X0,sF307)
| ~ m1_subset_1(X0,sF308) )
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_251
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79845,f76103]) ).
fof(f79847,plain,
( ! [X0] :
( r1_tarski(X0,k10_relset_1(sK28,sK28,k9_relset_2(sK28,sK27,sK28,sF304,sK30),X0))
| ~ r1_tarski(X0,sF307)
| ~ m1_subset_1(X0,sF308) )
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79846,f78607]) ).
fof(f79848,plain,
( ! [X0] :
( r1_tarski(X0,k10_relset_1(sK28,sK28,sF305,X0))
| ~ r1_tarski(X0,sF307)
| ~ m1_subset_1(X0,sF308) )
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79847,f75637]) ).
fof(f79849,plain,
( ! [X0] :
( r1_tarski(X0,k9_relat_1(sF305,X0))
| ~ r1_tarski(X0,sF307)
| ~ m1_subset_1(X0,sF308) )
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79848,f76346]) ).
fof(f79859,plain,
( ~ r1_tarski(sK29,sF307)
| ~ m1_subset_1(sK29,sF308)
| ~ r1_tarski(k9_relat_1(sF305,sK29),sF306)
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(resolution,[],[f79849,f77231]) ).
fof(f79879,plain,
( ~ m1_subset_1(sK29,sF308)
| ~ r1_tarski(k9_relat_1(sF305,sK29),sF306)
| ~ spl309_48
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_subsumption_resolution,[],[f79859,f75609]) ).
fof(f79899,plain,
( ~ r1_tarski(k9_relat_1(sF305,sK29),sF306)
| ~ spl309_46
| ~ spl309_48
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_subsumption_resolution,[],[f79879,f75599]) ).
fof(f79904,plain,
( ~ r1_tarski(sF306,sF306)
| ~ spl309_46
| ~ spl309_48
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f79899,f76389]) ).
fof(f79905,plain,
( $false
| ~ spl309_46
| ~ spl309_48
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_subsumption_resolution,[],[f79904,f73644]) ).
fof(f79906,plain,
( ~ spl309_46
| ~ spl309_48
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(avatar_contradiction_clause,[],[f79905]) ).
fof(f80041,plain,
( ~ m1_subset_1(sK29,sF308)
| ~ r1_tarski(sK29,k9_relat_1(sF305,sK29))
| spl309_48
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(resolution,[],[f75608,f79245]) ).
fof(f80046,plain,
( ~ r1_tarski(sK29,k9_relat_1(sF305,sK29))
| ~ spl309_46
| spl309_48
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_subsumption_resolution,[],[f80041,f75599]) ).
fof(f80049,plain,
( ~ r1_tarski(sK29,sF306)
| ~ spl309_46
| spl309_48
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_demodulation,[],[f80046,f76389]) ).
fof(f80052,plain,
( $false
| ~ spl309_46
| spl309_48
| ~ spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(forward_subsumption_resolution,[],[f80049,f75613]) ).
fof(f80053,plain,
( ~ spl309_46
| spl309_48
| ~ spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(avatar_contradiction_clause,[],[f80052]) ).
cnf(s49,plain,
spl309_46,
inference(sat_conversion,[],[f75600]) ).
cnf(s50,plain,
spl309_47,
inference(sat_conversion,[],[f75605]) ).
cnf(s51,plain,
( spl309_48
| spl309_49 ),
inference(sat_conversion,[],[f75614]) ).
cnf(s52,plain,
( ~ spl309_48
| ~ spl309_49 ),
inference(sat_conversion,[],[f75615]) ).
cnf(s54,plain,
spl309_51,
inference(sat_conversion,[],[f75633]) ).
cnf(s55,plain,
spl309_52,
inference(sat_conversion,[],[f75638]) ).
cnf(s56,plain,
spl309_53,
inference(sat_conversion,[],[f75643]) ).
cnf(s57,plain,
spl309_54,
inference(sat_conversion,[],[f75648]) ).
cnf(s58,plain,
spl309_55,
inference(sat_conversion,[],[f75653]) ).
cnf(s66,plain,
( ~ spl309_47
| spl309_63 ),
inference(sat_conversion,[],[f75776]) ).
cnf(s73,plain,
( ~ spl309_63
| spl309_68 ),
inference(sat_conversion,[],[f75820]) ).
cnf(s82,plain,
( ~ spl309_47
| spl309_74 ),
inference(sat_conversion,[],[f75918]) ).
cnf(s84,plain,
( ~ spl309_51
| ~ spl309_74
| spl309_75 ),
inference(sat_conversion,[],[f75942]) ).
cnf(s88,plain,
( ~ spl309_51
| spl309_61
| ~ spl309_74 ),
inference(sat_conversion,[],[f75951]) ).
cnf(s96,plain,
( ~ spl309_61
| spl309_79 ),
inference(sat_conversion,[],[f75998]) ).
cnf(s97,plain,
( ~ spl309_61
| spl309_80 ),
inference(sat_conversion,[],[f76003]) ).
cnf(s98,plain,
( ~ spl309_61
| spl309_81 ),
inference(sat_conversion,[],[f76008]) ).
cnf(s116,plain,
( ~ spl309_81
| spl309_90 ),
inference(sat_conversion,[],[f76104]) ).
cnf(s117,plain,
( ~ spl309_81
| spl309_91 ),
inference(sat_conversion,[],[f76109]) ).
cnf(s122,plain,
( ~ spl309_90
| ~ spl309_91
| spl309_93 ),
inference(sat_conversion,[],[f76121]) ).
cnf(s132,plain,
( ~ spl309_79
| spl309_98 ),
inference(sat_conversion,[],[f76187]) ).
cnf(s136,plain,
( ~ spl309_52
| ~ spl309_63
| ~ spl309_79
| spl309_101 ),
inference(sat_conversion,[],[f76204]) ).
cnf(s141,plain,
( ~ spl309_101
| spl309_106 ),
inference(sat_conversion,[],[f76251]) ).
cnf(s169,plain,
( ~ spl309_53
| ~ spl309_106
| spl309_125 ),
inference(sat_conversion,[],[f76390]) ).
cnf(s219,plain,
( ~ spl309_80
| ~ spl309_90
| ~ spl309_93
| spl309_161 ),
inference(sat_conversion,[],[f76825]) ).
cnf(s349,plain,
( ~ spl309_98
| spl309_251 ),
inference(sat_conversion,[],[f77982]) ).
cnf(s425,plain,
( ~ spl309_68
| ~ spl309_75
| spl309_305 ),
inference(sat_conversion,[],[f78608]) ).
cnf(s466,plain,
( ~ spl309_54
| ~ spl309_161
| ~ spl309_251
| ~ spl309_305
| spl309_342 ),
inference(sat_conversion,[],[f79089]) ).
cnf(s554,plain,
( ~ spl309_46
| ~ spl309_48
| spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(sat_conversion,[],[f79906]) ).
cnf(s614,plain,
( ~ spl309_46
| spl309_48
| ~ spl309_49
| ~ spl309_52
| ~ spl309_55
| ~ spl309_61
| ~ spl309_90
| ~ spl309_106
| ~ spl309_125
| ~ spl309_251
| ~ spl309_305
| ~ spl309_342 ),
inference(sat_conversion,[],[f80053]) ).
cnf(s615,plain,
spl309_74,
inference(rat,[],[s82,s50]) ).
cnf(s617,plain,
spl309_63,
inference(rat,[],[s66,s50]) ).
cnf(s620,plain,
spl309_75,
inference(rat,[],[s84,s54,s615]) ).
cnf(s622,plain,
spl309_61,
inference(rat,[],[s88,s54,s615]) ).
cnf(s624,plain,
spl309_68,
inference(rat,[],[s73,s617]) ).
cnf(s627,plain,
spl309_81,
inference(rat,[],[s98,s622]) ).
cnf(s628,plain,
spl309_80,
inference(rat,[],[s97,s622]) ).
cnf(s629,plain,
spl309_79,
inference(rat,[],[s96,s622]) ).
cnf(s636,plain,
spl309_305,
inference(rat,[],[s425,s620,s624]) ).
cnf(s641,plain,
spl309_91,
inference(rat,[],[s117,s627]) ).
cnf(s642,plain,
spl309_90,
inference(rat,[],[s116,s627]) ).
cnf(s645,plain,
spl309_98,
inference(rat,[],[s132,s629]) ).
cnf(s648,plain,
spl309_101,
inference(rat,[],[s136,s617,s55,s629]) ).
cnf(s665,plain,
spl309_93,
inference(rat,[],[s122,s641,s642]) ).
cnf(s667,plain,
spl309_251,
inference(rat,[],[s349,s645]) ).
cnf(s679,plain,
spl309_106,
inference(rat,[],[s141,s648]) ).
cnf(s707,plain,
spl309_161,
inference(rat,[],[s219,s642,s628,s665]) ).
cnf(s718,plain,
spl309_125,
inference(rat,[],[s169,s56,s679]) ).
cnf(s734,plain,
spl309_342,
inference(rat,[],[s466,s667,s636,s57,s707]) ).
cnf(s816,plain,
spl309_48,
inference(rat,[],[s51,s614,s49,s55,s58,s622,s642,s679,s718,s667,s636,s734]) ).
cnf(s817,plain,
spl309_49,
inference(rat,[],[s554,s734,s636,s667,s718,s679,s642,s622,s58,s55,s49,s816]) ).
cnf(s829,plain,
$false,
inference(rat,[],[s52,s817,s816]) ).
fof(f80054,plain,
$false,
inference(avatar_sat_refutation,[],[s829]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU443+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n009.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 05:32:16 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 21.62/8.79 % (2724381)Detected formulas, will run a generic FOF schedule.
% 21.62/8.79 % (2727615)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=1493444635:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2944 on theBenchmark for (2944ds/134677Mi)
% 21.62/8.79 % (2727612)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=142065927:i=141193_2944 on theBenchmark for (2944ds/141193Mi)
% 21.62/8.79 % (2727619)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=4009517620:i=141695:sd=1:nm=32:gsp=on:ss=included_2944 on theBenchmark for (2944ds/141695Mi)
% 21.62/8.79 % (2727623)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1903045998:i=109:sd=1:ins=1:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/109Mi)
% 21.62/8.79 % (2727628)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4196067184:i=119:av=off:ss=axioms_2944 on theBenchmark for (2944ds/119Mi)
% 21.62/8.79 % (2727632)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=894218870:s2a=on:i=139:gtg=position_2944 on theBenchmark for (2944ds/139Mi)
% 21.62/8.79 % (2727636)dis-21_1_sil=8000:lcm=predicate:random_seed=207829564: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)
% 21.62/8.79 % (2727623)Instruction limit reached!
% 21.62/8.79 % (2727623)------------------------------
% 21.62/8.79 % (2727623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.62/8.79 % (2727623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.62/8.79 % (2727623)CaDiCaL version: 2.1.3
% 21.62/8.79 % (2727623)Termination reason: Instruction limit
% 21.62/8.79 % (2727623)Termination phase: SInE selection
% 21.62/8.79 % (2727623)Time elapsed: 0.085 s
% 21.62/8.79 % (2727623)Peak memory usage: 201 MB
% 21.62/8.79 % (2727623)Instructions burned: 110 (million)
% 21.62/8.79 % (2727632)Instruction limit reached!
% 21.62/8.79 % (2727632)------------------------------
% 21.62/8.79 % (2727632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.62/8.79 % (2727632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.62/8.79 % (2727632)CaDiCaL version: 2.1.3
% 21.62/8.79 % (2727632)Termination reason: Instruction limit
% 21.62/8.79 % (2727632)Termination phase: Property scanning
% 21.62/8.79 % (2727632)Time elapsed: 0.069 s
% 21.62/8.79 % (2727632)Peak memory usage: 201 MB
% 21.62/8.79 % (2727632)Instructions burned: 141 (million)
% 21.62/8.79 % (2727628)Instruction limit reached!
% 21.62/8.79 % (2727628)------------------------------
% 21.62/8.79 % (2727628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.62/8.79 % (2727628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.62/8.79 % (2727628)CaDiCaL version: 2.1.3
% 21.62/8.79 % (2727628)Termination reason: Instruction limit
% 21.62/8.79 % (2727628)Termination phase: SInE selection
% 21.62/8.79 % (2727628)Time elapsed: 0.092 s
% 21.62/8.79 % (2727628)Peak memory usage: 201 MB
% 21.62/8.79 % (2727628)Instructions burned: 119 (million)
% 21.62/8.79 % (2727636)Instruction limit reached!
% 21.62/8.79 % (2727636)------------------------------
% 21.62/8.79 % (2727636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.62/8.79 % (2727636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.62/8.79 % (2727636)CaDiCaL version: 2.1.3
% 21.62/8.79 % (2727636)Termination reason: Instruction limit
% 21.62/8.79 % (2727636)Termination phase: SInE selection
% 21.62/8.79 % (2727636)Time elapsed: 0.100 s
% 21.62/8.79 % (2727636)Peak memory usage: 201 MB
% 21.62/8.79 % (2727636)Instructions burned: 129 (million)
% 21.62/8.79 % (2727763)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3889998708:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2941 on theBenchmark for (2941ds/157Mi)
% 21.62/8.79 % (2727759)lrs+10_1_sil=8000:sp=occurrence:random_seed=3066779601:i=285:sd=3:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/285Mi)
% 21.62/8.79 % (2727767)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2997233375:i=325:sd=1:ss=axioms:sgt=32_2941 on theBenchmark for (2941ds/325Mi)
% 21.62/8.79 % (2727783)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=1889192318:s2a=on:i=248:s2at=1.23:gtg=position_2941 on theBenchmark for (2941ds/248Mi)
% 21.62/8.79 % (2727763)Instruction limit reached!
% 27.65/9.57 % (2727763)------------------------------
% 27.65/9.57 % (2727763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727763)CaDiCaL version: 2.1.3
% 27.65/9.57 % (2727763)Termination reason: Instruction limit
% 27.65/9.57 % (2727763)Termination phase: Property scanning
% 27.65/9.57 % (2727763)Time elapsed: 0.077 s
% 27.65/9.57 % (2727763)Peak memory usage: 201 MB
% 27.65/9.57 % (2727763)Instructions burned: 159 (million)
% 27.65/9.57 % (2727783)Instruction limit reached!
% 27.65/9.57 % (2727783)------------------------------
% 27.65/9.57 % (2727783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727783)CaDiCaL version: 2.1.3
% 27.65/9.57 % (2727783)Termination reason: Instruction limit
% 27.65/9.57 % (2727783)Termination phase: Property scanning
% 27.65/9.57 % (2727783)Time elapsed: 0.115 s
% 27.65/9.57 % (2727783)Peak memory usage: 201 MB
% 27.65/9.57 % (2727783)Instructions burned: 250 (million)
% 27.65/9.57 % (2727759)Instruction limit reached!
% 27.65/9.57 % (2727759)------------------------------
% 27.65/9.57 % (2727759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727759)CaDiCaL version: 2.1.3
% 27.65/9.57 % (2727759)Termination reason: Instruction limit
% 27.65/9.57 % (2727759)Termination phase: SInE selection
% 27.65/9.57 % (2727759)Time elapsed: 0.216 s
% 27.65/9.57 % (2727759)Peak memory usage: 201 MB
% 27.65/9.57 % (2727759)Instructions burned: 285 (million)
% 27.65/9.57 % (2727888)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2178171723:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2939 on theBenchmark for (2939ds/294Mi)
% 27.65/9.57 % (2727767)Instruction limit reached!
% 27.65/9.57 % (2727767)------------------------------
% 27.65/9.57 % (2727767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727767)CaDiCaL version: 2.1.3
% 27.65/9.57 % (2727767)Termination reason: Instruction limit
% 27.65/9.57 % (2727767)Termination phase: SInE selection
% 27.65/9.57 % (2727767)Time elapsed: 0.242 s
% 27.65/9.57 % (2727767)Peak memory usage: 201 MB
% 27.65/9.57 % (2727767)Instructions burned: 325 (million)
% 27.65/9.57 % (2727944)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=852436692:i=2350_2938 on theBenchmark for (2938ds/2350Mi)
% 27.65/9.57 % (2727970)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3828824066:cts=off:i=113:fsr=off:ss=included:sgt=4_2938 on theBenchmark for (2938ds/113Mi)
% 27.65/9.57 % (2727993)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1710961126:i=127:av=off:fsr=off:sup=off_2937 on theBenchmark for (2937ds/127Mi)
% 27.65/9.57 % (2727888)Instruction limit reached!
% 27.65/9.57 % (2727888)------------------------------
% 27.65/9.57 % (2727888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727888)CaDiCaL version: 2.1.3
% 27.65/9.57 % (2727888)Termination reason: Instruction limit
% 27.65/9.57 % (2727888)Termination phase: SInE selection
% 27.65/9.57 % (2727888)Time elapsed: 0.223 s
% 27.65/9.57 % (2727888)Peak memory usage: 201 MB
% 27.65/9.57 % (2727888)Instructions burned: 295 (million)
% 27.65/9.57 % (2727970)Instruction limit reached!
% 27.65/9.57 % (2727970)------------------------------
% 27.65/9.57 % (2727970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727970)CaDiCaL version: 2.1.3
% 27.65/9.57 % (2727970)Termination reason: Instruction limit
% 27.65/9.57 % (2727970)Termination phase: SInE selection
% 27.65/9.57 % (2727970)Time elapsed: 0.088 s
% 27.65/9.57 % (2727970)Peak memory usage: 201 MB
% 27.65/9.57 % (2727970)Instructions burned: 114 (million)
% 27.65/9.57 % (2727993)Instruction limit reached!
% 27.65/9.57 % (2727993)------------------------------
% 27.65/9.57 % (2727993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.65/9.57 % (2727993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.65/9.57 % (2727993)CaDiCaL version: 2.1.3
% 61.29/14.22 % (2727993)Termination reason: Instruction limit
% 61.29/14.22 % (2727993)Termination phase: Preprocessing 1
% 61.29/14.22 % (2727993)Time elapsed: 0.102 s
% 61.29/14.22 % (2727993)Peak memory usage: 202 MB
% 61.29/14.22 % (2727993)Instructions burned: 128 (million)
% 61.29/14.22 % (2728106)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1077841236:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2935 on theBenchmark for (2935ds/114Mi)
% 61.29/14.22 % (2728110)lrs+10_1_sil=8000:sp=occurrence:random_seed=2280339909:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2935 on theBenchmark for (2935ds/907Mi)
% 61.29/14.22 % (2728106)Instruction limit reached!
% 61.29/14.22 % (2728106)------------------------------
% 61.29/14.22 % (2728106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.29/14.22 % (2728106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.29/14.22 % (2728106)CaDiCaL version: 2.1.3
% 61.29/14.22 % (2728106)Termination reason: Instruction limit
% 61.29/14.22 % (2728106)Termination phase: Property scanning
% 61.29/14.22 % (2728106)Time elapsed: 0.059 s
% 61.29/14.22 % (2728106)Peak memory usage: 201 MB
% 61.29/14.22 % (2728106)Instructions burned: 116 (million)
% 61.29/14.22 % (2728149)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2127143762:i=437:sd=1:aac=none:ss=included_2935 on theBenchmark for (2935ds/437Mi)
% 61.29/14.22 % (2728227)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4262605240:i=5202:ss=axioms:sgt=16_2933 on theBenchmark for (2933ds/5202Mi)
% 61.29/14.22 % (2728149)Instruction limit reached!
% 61.29/14.22 % (2728149)------------------------------
% 61.29/14.22 % (2728149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.29/14.22 % (2728149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.29/14.22 % (2728149)CaDiCaL version: 2.1.3
% 61.29/14.22 % (2728149)Termination reason: Instruction limit
% 61.29/14.22 % (2728149)Termination phase: SInE selection
% 61.29/14.22 % (2728149)Time elapsed: 0.323 s
% 61.29/14.22 % (2728149)Peak memory usage: 202 MB
% 61.29/14.22 % (2728149)Instructions burned: 437 (million)
% 61.29/14.22 % (2728422)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1079914034:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2930 on theBenchmark for (2930ds/134Mi)
% 61.29/14.22 % (2728110)Instruction limit reached!
% 61.29/14.22 % (2728110)------------------------------
% 61.29/14.22 % (2728110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.29/14.22 % (2728110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.29/14.22 % (2728110)CaDiCaL version: 2.1.3
% 61.29/14.22 % (2728110)Termination reason: Instruction limit
% 61.29/14.22 % (2728110)Termination phase: Preprocessing 1
% 61.29/14.22 % (2728110)Time elapsed: 0.660 s
% 61.29/14.22 % (2728110)Peak memory usage: 204 MB
% 61.29/14.22 % (2728110)Instructions burned: 907 (million)
% 61.29/14.22 % (2728422)Instruction limit reached!
% 61.29/14.22 % (2728422)------------------------------
% 61.29/14.22 % (2728422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.29/14.22 % (2728422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.29/14.22 % (2728422)CaDiCaL version: 2.1.3
% 61.29/14.22 % (2728422)Termination reason: Instruction limit
% 61.29/14.22 % (2728422)Termination phase: SInE selection
% 61.29/14.22 % (2728422)Time elapsed: 0.107 s
% 61.29/14.22 % (2728422)Peak memory usage: 201 MB
% 61.29/14.22 % (2728422)Instructions burned: 134 (million)
% 61.29/14.22 % (2728565)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1054677358:st=8:i=592:sd=3:ep=RST:ss=axioms_2927 on theBenchmark for (2927ds/592Mi)
% 61.29/14.22 % (2728580)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1963082694:st=3:i=13193:sd=3:ss=axioms_2927 on theBenchmark for (2927ds/13193Mi)
% 61.29/14.22 % (2728565)Instruction limit reached!
% 61.29/14.22 % (2728565)------------------------------
% 61.29/14.22 % (2728565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.29/14.22 % (2728565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.29/14.22 % (2728565)CaDiCaL version: 2.1.3
% 61.29/14.22 % (2728565)Termination reason: Instruction limit
% 61.29/14.22 % (2728565)Termination phase: SInE selection
% 61.29/14.22 % (2728565)Time elapsed: 0.382 s
% 61.29/14.22 % (2728565)Peak memory usage: 203 MB
% 61.29/14.22 % (2728565)Instructions burned: 592 (million)
% 61.29/14.22 % (2728866)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=2105788434:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2922 on theBenchmark for (2922ds/125Mi)
% 38.55/16.77 % (2728866)Instruction limit reached!
% 38.55/16.77 % (2728866)------------------------------
% 38.55/16.77 % (2728866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2728866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2728866)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2728866)Termination reason: Instruction limit
% 38.55/16.77 % (2728866)Termination phase: Property scanning
% 38.55/16.77 % (2728866)Time elapsed: 0.062 s
% 38.55/16.77 % (2728866)Peak memory usage: 201 MB
% 38.55/16.77 % (2728866)Instructions burned: 126 (million)
% 38.55/16.77 % (2728988)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1131479354:i=134:gtgl=5:slsql=off:gtg=exists_sym_2919 on theBenchmark for (2919ds/134Mi)
% 38.55/16.77 % (2727944)Instruction limit reached!
% 38.55/16.77 % (2727944)------------------------------
% 38.55/16.77 % (2727944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2727944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2727944)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2727944)Termination reason: Instruction limit
% 38.55/16.77 % (2727944)Termination phase: Preprocessing 3
% 38.55/16.77 % (2727944)Time elapsed: 1.874 s
% 38.55/16.77 % (2727944)Peak memory usage: 305 MB
% 38.55/16.77 % (2727944)Instructions burned: 2350 (million)
% 38.55/16.77 % (2728988)Instruction limit reached!
% 38.55/16.77 % (2728988)------------------------------
% 38.55/16.77 % (2728988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2728988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2728988)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2728988)Termination reason: Instruction limit
% 38.55/16.77 % (2728988)Termination phase: Property scanning
% 38.55/16.77 % (2728988)Time elapsed: 0.038 s
% 38.55/16.77 % (2728988)Peak memory usage: 201 MB
% 38.55/16.77 % (2728988)Instructions burned: 137 (million)
% 38.55/16.77 % (2729026)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=516833007:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2918 on theBenchmark for (2918ds/431Mi)
% 38.55/16.77 % (2729025)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2566277410:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2918 on theBenchmark for (2918ds/141Mi)
% 38.55/16.77 % (2729025)Instruction limit reached!
% 38.55/16.77 % (2729025)------------------------------
% 38.55/16.77 % (2729025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729025)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729025)Termination reason: Instruction limit
% 38.55/16.77 % (2729025)Termination phase: SInE selection
% 38.55/16.77 % (2729025)Time elapsed: 0.110 s
% 38.55/16.77 % (2729025)Peak memory usage: 201 MB
% 38.55/16.77 % (2729025)Instructions burned: 142 (million)
% 38.55/16.77 % (2729026)Instruction limit reached!
% 38.55/16.77 % (2729026)------------------------------
% 38.55/16.77 % (2729026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729026)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729026)Termination reason: Instruction limit
% 38.55/16.77 % (2729026)Termination phase: SInE selection
% 38.55/16.77 % (2729026)Time elapsed: 0.199 s
% 38.55/16.77 % (2729026)Peak memory usage: 202 MB
% 38.55/16.77 % (2729026)Instructions burned: 432 (million)
% 38.55/16.77 % (2729029)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=3521198353:i=6060:aac=none:ins=25_2915 on theBenchmark for (2915ds/6060Mi)
% 38.55/16.77 % (2729048)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=373198290:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2914 on theBenchmark for (2914ds/150Mi)
% 38.55/16.77 % (2729048)Instruction limit reached!
% 38.55/16.77 % (2729048)------------------------------
% 38.55/16.77 % (2729048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729048)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729048)Termination reason: Instruction limit
% 38.55/16.77 % (2729048)Termination phase: SInE selection
% 38.55/16.77 % (2729048)Time elapsed: 0.074 s
% 38.55/16.77 % (2729048)Peak memory usage: 201 MB
% 38.55/16.77 % (2729048)Instructions burned: 152 (million)
% 38.55/16.77 % (2729115)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3176333628:i=14155:bd=all_2912 on theBenchmark for (2912ds/14155Mi)
% 38.55/16.77 % (2728227)Instruction limit reached!
% 38.55/16.77 % (2728227)------------------------------
% 38.55/16.77 % (2728227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2728227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2728227)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2728227)Termination reason: Instruction limit
% 38.55/16.77 % (2728227)Termination phase: Property scanning
% 38.55/16.77 % (2728227)Time elapsed: 3.763 s
% 38.55/16.77 % (2728227)Peak memory usage: 333 MB
% 38.55/16.77 % (2728227)Instructions burned: 5203 (million)
% 38.55/16.77 % (2729149)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3804886968:i=667:av=off:fsr=off_2894 on theBenchmark for (2894ds/667Mi)
% 38.55/16.77 % (2729149)Instruction limit reached!
% 38.55/16.77 % (2729149)------------------------------
% 38.55/16.77 % (2729149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729149)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729149)Termination reason: Instruction limit
% 38.55/16.77 % (2729149)Termination phase: Preprocessing 2
% 38.55/16.77 % (2729149)Time elapsed: 0.601 s
% 38.55/16.77 % (2729149)Peak memory usage: 218 MB
% 38.55/16.77 % (2729149)Instructions burned: 667 (million)
% 38.55/16.77 % (2729151)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=1802761704:s2a=on:i=185:s2at=1.8:fdi=4_2886 on theBenchmark for (2886ds/185Mi)
% 38.55/16.77 % (2729151)Instruction limit reached!
% 38.55/16.77 % (2729151)------------------------------
% 38.55/16.77 % (2729151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729151)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729151)Termination reason: Instruction limit
% 38.55/16.77 % (2729151)Termination phase: SInE selection
% 38.55/16.77 % (2729151)Time elapsed: 0.140 s
% 38.55/16.77 % (2729151)Peak memory usage: 201 MB
% 38.55/16.77 % (2729151)Instructions burned: 185 (million)
% 38.55/16.77 % (2729153)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2763261817:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2883 on theBenchmark for (2883ds/193Mi)
% 38.55/16.77 % (2729153)Instruction limit reached!
% 38.55/16.77 % (2729153)------------------------------
% 38.55/16.77 % (2729153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729153)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729153)Termination reason: Instruction limit
% 38.55/16.77 % (2729153)Termination phase: SInE selection
% 38.55/16.77 % (2729153)Time elapsed: 0.149 s
% 38.55/16.77 % (2729153)Peak memory usage: 201 MB
% 38.55/16.77 % (2729153)Instructions burned: 193 (million)
% 38.55/16.77 % (2729155)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3711214876:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2879 on theBenchmark for (2879ds/4850Mi)
% 38.55/16.77 % (2729115)Instruction limit reached!
% 38.55/16.77 % (2729115)------------------------------
% 38.55/16.77 % (2729115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729115)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729115)Termination reason: Instruction limit
% 38.55/16.77 % (2729115)Termination phase: Property scanning
% 38.55/16.77 % (2729115)Time elapsed: 3.944 s
% 38.55/16.77 % (2729115)Peak memory usage: 447 MB
% 38.55/16.77 % (2729115)Instructions burned: 14158 (million)
% 38.55/16.77 % (2729157)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3097017648:i=12111:sd=1:ss=included_2871 on theBenchmark for (2871ds/12111Mi)
% 38.55/16.77 % (2729029)Instruction limit reached!
% 38.55/16.77 % (2729029)------------------------------
% 38.55/16.77 % (2729029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729029)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729029)Termination reason: Instruction limit
% 38.55/16.77 % (2729029)Termination phase: NewCNF
% 38.55/16.77 % (2729029)Time elapsed: 4.750 s
% 38.55/16.77 % (2729029)Peak memory usage: 381 MB
% 38.55/16.77 % (2729029)Instructions burned: 6061 (million)
% 38.55/16.77 % (2729159)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4019163820:i=319:kws=precedence:fsr=off_2865 on theBenchmark for (2865ds/319Mi)
% 38.55/16.77 % (2729159)Instruction limit reached!
% 38.55/16.77 % (2729159)------------------------------
% 38.55/16.77 % (2729159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729159)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729159)Termination reason: Instruction limit
% 38.55/16.77 % (2729159)Termination phase: Preprocessing 1
% 38.55/16.77 % (2729159)Time elapsed: 0.226 s
% 38.55/16.77 % (2729159)Peak memory usage: 203 MB
% 38.55/16.77 % (2729159)Instructions burned: 319 (million)
% 38.55/16.77 % (2729161)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2656211723:i=2064:ep=RST_2861 on theBenchmark for (2861ds/2064Mi)
% 38.55/16.77 % (2729157)First to succeed.
% 38.55/16.77 % (2729157)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2724381"
% 38.55/16.77 % (2729161)Instruction limit reached!
% 38.55/16.77 % (2729161)------------------------------
% 38.55/16.77 % (2729161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729161)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729161)Termination reason: Instruction limit
% 38.55/16.77 % (2729161)Termination phase: Preprocessing 3
% 38.55/16.77 % (2729161)Time elapsed: 1.550 s
% 38.55/16.77 % (2729161)Peak memory usage: 317 MB
% 38.55/16.77 % (2729161)Instructions burned: 2064 (million)
% 38.55/16.77 % (2729155)Instruction limit reached!
% 38.55/16.77 % (2729155)------------------------------
% 38.55/16.77 % (2729155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2729155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2729155)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2729155)Termination reason: Instruction limit
% 38.55/16.77 % (2729155)Termination phase: Property scanning
% 38.55/16.77 % (2729155)Time elapsed: 3.352 s
% 38.55/16.77 % (2729155)Peak memory usage: 362 MB
% 38.55/16.77 % (2729155)Instructions burned: 4852 (million)
% 38.55/16.77 % (2728580)Instruction limit reached!
% 38.55/16.77 % (2728580)------------------------------
% 38.55/16.77 % (2728580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.55/16.77 % (2728580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.55/16.77 % (2728580)CaDiCaL version: 2.1.3
% 38.55/16.77 % (2728580)Termination reason: Instruction limit
% 38.55/16.77 % (2728580)Termination phase: Saturation
% 38.55/16.77 % (2728580)Time elapsed: 8.298 s
% 38.55/16.77 % (2728580)Peak memory usage: 620 MB
% 38.55/16.77 % (2728580)Instructions burned: 13197 (million)
% 38.55/16.77 % (2729157)Refutation found. Thanks to Tanya!
% 38.55/16.77 % SZS status Theorem for theBenchmark
% 38.55/16.77 % SZS output start Proof for theBenchmark
% See solution above
% 78.84/17.03 % (2729157)------------------------------
% 78.84/17.03 % (2729157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.84/17.03 % (2729157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.84/17.03 % (2729157)CaDiCaL version: 2.1.3
% 78.84/17.03 % (2729157)Termination reason: Refutation
% 78.84/17.03 % (2729157)Time elapsed: 2.343 s
% 78.84/17.03 % (2729157)Peak memory usage: 299 MB
% 78.84/17.03 % (2729157)Instructions burned: 3634 (million)
% 78.84/17.03 % (2729157)------------------------------
% 78.84/17.03 % (2729157)------------------------------
% 78.84/17.03 % (2724381)Success in time 15.915 s
% 78.84/17.03 % Vampire exiting
%------------------------------------------------------------------------------