%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU221+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:52:27 PM UTC 2026
% Result : Theorem 82.72s 29.04s
% Output : Refutation 82.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 12
% Syntax : Number of formulae : 108 ( 14 unt; 4 def)
% Number of atoms : 370 ( 59 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 461 ( 199 ~; 203 |; 38 &)
% ( 7 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 5 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-2 aty)
% Number of variables : 55 ( 0 sgn 49 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ( one_to_one(X0)
<=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
& in(X2,relation_dom(X0))
& apply(X0,X1) = apply(X0,X2) )
=> X1 = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_funct_1) ).
fof(f43,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ( one_to_one(X0)
=> function_inverse(X0) = relation_inverse(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_funct_1) ).
fof(f51,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ( relation(function_inverse(X0))
& function(function_inverse(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_funct_1) ).
fof(f61,axiom,
! [X0] :
( relation(X0)
=> relation(relation_inverse(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_relat_1) ).
fof(f100,axiom,
! [X0] :
( relation(X0)
=> relation_inverse(relation_inverse(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k4_relat_1) ).
fof(f175,axiom,
! [X0] :
( relation(X0)
=> ( relation_rng(X0) = relation_dom(relation_inverse(X0))
& relation_dom(X0) = relation_rng(relation_inverse(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_relat_1) ).
fof(f205,axiom,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ( ( one_to_one(X1)
& in(X0,relation_rng(X1)) )
=> ( X0 = apply(X1,apply(function_inverse(X1),X0))
& X0 = apply(relation_composition(function_inverse(X1),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t57_funct_1) ).
fof(f209,conjecture,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ( one_to_one(X0)
=> one_to_one(function_inverse(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_funct_1) ).
fof(f210,negated_conjecture,
~ ! [X0] :
( ( relation(X0)
& function(X0) )
=> ( one_to_one(X0)
=> one_to_one(function_inverse(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f209]) ).
fof(f273,plain,
! [X0] :
( ( one_to_one(X0)
<=> ! [X1,X2] :
( X1 = X2
| ~ in(X1,relation_dom(X0))
| ~ in(X2,relation_dom(X0))
| apply(X0,X1) != apply(X0,X2) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f274,plain,
! [X0] :
( ( one_to_one(X0)
<=> ! [X1,X2] :
( X1 = X2
| ~ in(X1,relation_dom(X0))
| ~ in(X2,relation_dom(X0))
| apply(X0,X1) != apply(X0,X2) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f273]) ).
fof(f279,plain,
! [X0] :
( function_inverse(X0) = relation_inverse(X0)
| ~ one_to_one(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f280,plain,
! [X0] :
( function_inverse(X0) = relation_inverse(X0)
| ~ one_to_one(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f279]) ).
fof(f281,plain,
! [X0] :
( ( relation(function_inverse(X0))
& function(function_inverse(X0)) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f282,plain,
! [X0] :
( ( relation(function_inverse(X0))
& function(function_inverse(X0)) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f281]) ).
fof(f284,plain,
! [X0] :
( relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f318,plain,
! [X0] :
( relation_inverse(relation_inverse(X0)) = X0
| ~ relation(X0) ),
inference(ennf_transformation,[],[f100]) ).
fof(f386,plain,
! [X0] :
( ( relation_rng(X0) = relation_dom(relation_inverse(X0))
& relation_dom(X0) = relation_rng(relation_inverse(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f175]) ).
fof(f417,plain,
! [X0,X1] :
( ( X0 = apply(X1,apply(function_inverse(X1),X0))
& X0 = apply(relation_composition(function_inverse(X1),X1),X0) )
| ~ one_to_one(X1)
| ~ in(X0,relation_rng(X1))
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f205]) ).
fof(f418,plain,
! [X0,X1] :
( ( X0 = apply(X1,apply(function_inverse(X1),X0))
& X0 = apply(relation_composition(function_inverse(X1),X1),X0) )
| ~ one_to_one(X1)
| ~ in(X0,relation_rng(X1))
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f417]) ).
fof(f421,plain,
? [X0] :
( ~ one_to_one(function_inverse(X0))
& one_to_one(X0)
& relation(X0)
& function(X0) ),
inference(ennf_transformation,[],[f210]) ).
fof(f422,plain,
? [X0] :
( ~ one_to_one(function_inverse(X0))
& one_to_one(X0)
& relation(X0)
& function(X0) ),
inference(flattening,[],[f421]) ).
fof(f527,plain,
! [X0] :
( ( ( one_to_one(X0)
| ? [X1,X2] :
( X1 != X2
& in(X1,relation_dom(X0))
& in(X2,relation_dom(X0))
& apply(X0,X1) = apply(X0,X2) ) )
& ( ! [X1,X2] :
( X1 = X2
| ~ in(X1,relation_dom(X0))
| ~ in(X2,relation_dom(X0))
| apply(X0,X1) != apply(X0,X2) )
| ~ one_to_one(X0) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f274]) ).
fof(f528,plain,
! [X0] :
( ( ( one_to_one(X0)
| ? [X1,X2] :
( X1 != X2
& in(X1,relation_dom(X0))
& in(X2,relation_dom(X0))
& apply(X0,X1) = apply(X0,X2) ) )
& ( ! [X3,X4] :
( X3 = X4
| ~ in(X3,relation_dom(X0))
| ~ in(X4,relation_dom(X0))
| apply(X0,X3) != apply(X0,X4) )
| ~ one_to_one(X0) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(rectify,[],[f527]) ).
fof(f529,plain,
! [X0] :
( ( ( one_to_one(X0)
| ( sK47(X0) != sK48(X0)
& in(sK47(X0),relation_dom(X0))
& in(sK48(X0),relation_dom(X0))
& apply(X0,sK47(X0)) = apply(X0,sK48(X0)) ) )
& ( ! [X3,X4] :
( X3 = X4
| ~ in(X3,relation_dom(X0))
| ~ in(X4,relation_dom(X0))
| apply(X0,X3) != apply(X0,X4) )
| ~ one_to_one(X0) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47,sK48]),skolemize(X1,sK47(X0)),skolemize(X2,sK48(X0))],[f528]) ).
fof(f592,plain,
( ~ one_to_one(function_inverse(sK77))
& one_to_one(sK77)
& relation(sK77)
& function(sK77) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77]),skolemize(X0,sK77)],[f422]) ).
fof(f742,plain,
! [X0] :
( one_to_one(X0)
| apply(X0,sK47(X0)) = apply(X0,sK48(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f529]) ).
fof(f743,plain,
! [X0] :
( in(sK48(X0),relation_dom(X0))
| one_to_one(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f529]) ).
fof(f744,plain,
! [X0] :
( in(sK47(X0),relation_dom(X0))
| one_to_one(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f529]) ).
fof(f745,plain,
! [X0] :
( sK47(X0) != sK48(X0)
| one_to_one(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f529]) ).
fof(f758,plain,
! [X0] :
( ~ one_to_one(X0)
| relation_inverse(X0) = function_inverse(X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f280]) ).
fof(f759,plain,
! [X0] :
( function(function_inverse(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f282]) ).
fof(f763,plain,
! [X0] :
( relation(relation_inverse(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f284]) ).
fof(f808,plain,
! [X0] :
( ~ relation(X0)
| relation_inverse(relation_inverse(X0)) = X0 ),
inference(cnf_transformation,[],[f318]) ).
fof(f922,plain,
! [X0] :
( ~ relation(X0)
| relation_dom(X0) = relation_rng(relation_inverse(X0)) ),
inference(cnf_transformation,[],[f386]) ).
fof(f977,plain,
! [X0,X1] :
( ~ in(X0,relation_rng(X1))
| ~ one_to_one(X1)
| apply(X1,apply(function_inverse(X1),X0)) = X0
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f418]) ).
fof(f982,plain,
function(sK77),
inference(cnf_transformation,[],[f592]) ).
fof(f983,plain,
relation(sK77),
inference(cnf_transformation,[],[f592]) ).
fof(f984,plain,
one_to_one(sK77),
inference(cnf_transformation,[],[f592]) ).
fof(f985,plain,
~ one_to_one(function_inverse(sK77)),
inference(cnf_transformation,[],[f592]) ).
fof(f1490,plain,
sK77 = relation_inverse(relation_inverse(sK77)),
inference(resolution,[],[f808,f983]) ).
fof(f2043,definition,
( spl80_9
<=> relation(relation_inverse(sK77)) ),
introduced(definition,[new_symbols(definition,[spl80_9])],[avatar_definition]) ).
fof(f2044,plain,
( relation(relation_inverse(sK77))
| ~ spl80_9 ),
inference(avatar_component_clause,[],[f2043]) ).
fof(f2045,plain,
( ~ relation(relation_inverse(sK77))
| spl80_9 ),
inference(avatar_component_clause,[],[f2043]) ).
fof(f2056,plain,
( ~ relation(sK77)
| spl80_9 ),
inference(resolution,[],[f2045,f763]) ).
fof(f2059,plain,
( $false
| spl80_9 ),
inference(forward_subsumption_resolution,[],[f2056,f983]) ).
fof(f2060,plain,
spl80_9,
inference(avatar_contradiction_clause,[],[f2059]) ).
fof(f2061,plain,
( relation_dom(relation_inverse(sK77)) = relation_rng(relation_inverse(relation_inverse(sK77)))
| ~ spl80_9 ),
inference(resolution,[],[f2044,f922]) ).
fof(f2063,plain,
( relation_dom(relation_inverse(sK77)) = relation_rng(sK77)
| ~ spl80_9 ),
inference(forward_demodulation,[],[f2061,f1490]) ).
fof(f12290,plain,
( in(sK48(relation_inverse(sK77)),relation_rng(sK77))
| one_to_one(relation_inverse(sK77))
| ~ relation(relation_inverse(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(superposition,[],[f743,f2063]) ).
fof(f12294,plain,
( in(sK48(relation_inverse(sK77)),relation_rng(sK77))
| one_to_one(relation_inverse(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_subsumption_resolution,[],[f12290,f2044]) ).
fof(f12505,plain,
( in(sK47(relation_inverse(sK77)),relation_rng(sK77))
| one_to_one(relation_inverse(sK77))
| ~ relation(relation_inverse(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(superposition,[],[f744,f2063]) ).
fof(f12509,plain,
( in(sK47(relation_inverse(sK77)),relation_rng(sK77))
| one_to_one(relation_inverse(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_subsumption_resolution,[],[f12505,f2044]) ).
fof(f12788,plain,
( function_inverse(sK77) = relation_inverse(sK77)
| ~ relation(sK77)
| ~ function(sK77) ),
inference(resolution,[],[f758,f984]) ).
fof(f12790,plain,
( function_inverse(sK77) = relation_inverse(sK77)
| ~ function(sK77) ),
inference(forward_subsumption_resolution,[],[f12788,f983]) ).
fof(f12794,plain,
function_inverse(sK77) = relation_inverse(sK77),
inference(forward_subsumption_resolution,[],[f12790,f982]) ).
fof(f13894,plain,
( in(sK48(function_inverse(sK77)),relation_rng(sK77))
| one_to_one(relation_inverse(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_demodulation,[],[f12294,f12794]) ).
fof(f13895,plain,
( in(sK47(function_inverse(sK77)),relation_rng(sK77))
| one_to_one(relation_inverse(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_demodulation,[],[f12509,f12794]) ).
fof(f13956,plain,
( one_to_one(function_inverse(sK77))
| in(sK48(function_inverse(sK77)),relation_rng(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_demodulation,[],[f13894,f12794]) ).
fof(f13957,plain,
( one_to_one(function_inverse(sK77))
| in(sK47(function_inverse(sK77)),relation_rng(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_demodulation,[],[f13895,f12794]) ).
fof(f13960,plain,
( in(sK48(function_inverse(sK77)),relation_rng(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_subsumption_resolution,[],[f13956,f985]) ).
fof(f13961,plain,
( in(sK47(function_inverse(sK77)),relation_rng(sK77))
| ~ function(relation_inverse(sK77))
| ~ spl80_9 ),
inference(forward_subsumption_resolution,[],[f13957,f985]) ).
fof(f13964,plain,
( ~ function(function_inverse(sK77))
| in(sK48(function_inverse(sK77)),relation_rng(sK77))
| ~ spl80_9 ),
inference(forward_demodulation,[],[f13960,f12794]) ).
fof(f13965,plain,
( ~ function(function_inverse(sK77))
| in(sK47(function_inverse(sK77)),relation_rng(sK77))
| ~ spl80_9 ),
inference(forward_demodulation,[],[f13961,f12794]) ).
fof(f13968,definition,
( spl80_127
<=> in(sK48(function_inverse(sK77)),relation_rng(sK77)) ),
introduced(definition,[new_symbols(definition,[spl80_127])],[avatar_definition]) ).
fof(f13970,plain,
( in(sK48(function_inverse(sK77)),relation_rng(sK77))
| ~ spl80_127 ),
inference(avatar_component_clause,[],[f13968]) ).
fof(f13972,definition,
( spl80_128
<=> function(function_inverse(sK77)) ),
introduced(definition,[new_symbols(definition,[spl80_128])],[avatar_definition]) ).
fof(f13973,plain,
( function(function_inverse(sK77))
| ~ spl80_128 ),
inference(avatar_component_clause,[],[f13972]) ).
fof(f13974,plain,
( ~ function(function_inverse(sK77))
| spl80_128 ),
inference(avatar_component_clause,[],[f13972]) ).
fof(f13975,plain,
( spl80_127
| ~ spl80_128
| ~ spl80_9 ),
inference(avatar_split_clause,[],[f13964,f2043,f13972,f13968]) ).
fof(f13977,definition,
( spl80_129
<=> in(sK47(function_inverse(sK77)),relation_rng(sK77)) ),
introduced(definition,[new_symbols(definition,[spl80_129])],[avatar_definition]) ).
fof(f13979,plain,
( in(sK47(function_inverse(sK77)),relation_rng(sK77))
| ~ spl80_129 ),
inference(avatar_component_clause,[],[f13977]) ).
fof(f13980,plain,
( spl80_129
| ~ spl80_128
| ~ spl80_9 ),
inference(avatar_split_clause,[],[f13965,f2043,f13972,f13977]) ).
fof(f13997,plain,
( ~ relation(sK77)
| ~ function(sK77)
| spl80_128 ),
inference(resolution,[],[f13974,f759]) ).
fof(f13999,plain,
( ~ function(sK77)
| spl80_128 ),
inference(forward_subsumption_resolution,[],[f13997,f983]) ).
fof(f14000,plain,
( $false
| spl80_128 ),
inference(forward_subsumption_resolution,[],[f13999,f982]) ).
fof(f14001,plain,
spl80_128,
inference(avatar_contradiction_clause,[],[f14000]) ).
fof(f14449,plain,
( relation(function_inverse(sK77))
| ~ spl80_9 ),
inference(superposition,[],[f2044,f12794]) ).
fof(f22473,plain,
( apply(function_inverse(sK77),sK47(function_inverse(sK77))) = apply(function_inverse(sK77),sK48(function_inverse(sK77)))
| ~ relation(function_inverse(sK77))
| ~ function(function_inverse(sK77)) ),
inference(resolution,[],[f742,f985]) ).
fof(f22496,plain,
( apply(function_inverse(sK77),sK47(function_inverse(sK77))) = apply(function_inverse(sK77),sK48(function_inverse(sK77)))
| ~ function(function_inverse(sK77))
| ~ spl80_9 ),
inference(forward_subsumption_resolution,[],[f22473,f14449]) ).
fof(f22502,plain,
( apply(function_inverse(sK77),sK47(function_inverse(sK77))) = apply(function_inverse(sK77),sK48(function_inverse(sK77)))
| ~ spl80_9
| ~ spl80_128 ),
inference(forward_subsumption_resolution,[],[f22496,f13973]) ).
fof(f26742,plain,
( ~ one_to_one(sK77)
| sK47(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK47(function_inverse(sK77))))
| ~ relation(sK77)
| ~ function(sK77)
| ~ spl80_129 ),
inference(resolution,[],[f977,f13979]) ).
fof(f26743,plain,
( ~ one_to_one(sK77)
| sK48(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK48(function_inverse(sK77))))
| ~ relation(sK77)
| ~ function(sK77)
| ~ spl80_127 ),
inference(resolution,[],[f977,f13970]) ).
fof(f26770,plain,
( sK48(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK48(function_inverse(sK77))))
| ~ relation(sK77)
| ~ function(sK77)
| ~ spl80_127 ),
inference(forward_subsumption_resolution,[],[f26743,f984]) ).
fof(f26771,plain,
( sK47(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK47(function_inverse(sK77))))
| ~ relation(sK77)
| ~ function(sK77)
| ~ spl80_129 ),
inference(forward_subsumption_resolution,[],[f26742,f984]) ).
fof(f26780,plain,
( sK48(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK48(function_inverse(sK77))))
| ~ function(sK77)
| ~ spl80_127 ),
inference(forward_subsumption_resolution,[],[f26770,f983]) ).
fof(f26781,plain,
( sK47(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK47(function_inverse(sK77))))
| ~ function(sK77)
| ~ spl80_129 ),
inference(forward_subsumption_resolution,[],[f26771,f983]) ).
fof(f26786,plain,
( sK48(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK48(function_inverse(sK77))))
| ~ spl80_127 ),
inference(forward_subsumption_resolution,[],[f26780,f982]) ).
fof(f26787,plain,
( sK47(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK47(function_inverse(sK77))))
| ~ spl80_129 ),
inference(forward_subsumption_resolution,[],[f26781,f982]) ).
fof(f26791,plain,
( sK48(function_inverse(sK77)) = apply(sK77,apply(function_inverse(sK77),sK47(function_inverse(sK77))))
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128 ),
inference(forward_demodulation,[],[f26786,f22502]) ).
fof(f26829,plain,
( sK48(function_inverse(sK77)) = sK47(function_inverse(sK77))
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(forward_demodulation,[],[f26791,f26787]) ).
fof(f26856,plain,
( sK47(function_inverse(sK77)) != sK47(function_inverse(sK77))
| one_to_one(function_inverse(sK77))
| ~ relation(function_inverse(sK77))
| ~ function(function_inverse(sK77))
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(superposition,[],[f745,f26829]) ).
fof(f26858,plain,
( one_to_one(function_inverse(sK77))
| ~ relation(function_inverse(sK77))
| ~ function(function_inverse(sK77))
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(trivial_inequality_removal,[],[f26856]) ).
fof(f26859,plain,
( ~ relation(function_inverse(sK77))
| ~ function(function_inverse(sK77))
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(forward_subsumption_resolution,[],[f26858,f985]) ).
fof(f26860,plain,
( ~ function(function_inverse(sK77))
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(forward_subsumption_resolution,[],[f26859,f14449]) ).
fof(f26861,plain,
( $false
| ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(forward_subsumption_resolution,[],[f26860,f13973]) ).
fof(f26862,plain,
( ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(avatar_contradiction_clause,[],[f26861]) ).
cnf(s11,plain,
spl80_9,
inference(sat_conversion,[],[f2060]) ).
cnf(s141,plain,
( ~ spl80_9
| spl80_127
| ~ spl80_128 ),
inference(sat_conversion,[],[f13975]) ).
cnf(s142,plain,
( ~ spl80_9
| ~ spl80_128
| spl80_129 ),
inference(sat_conversion,[],[f13980]) ).
cnf(s145,plain,
spl80_128,
inference(sat_conversion,[],[f14001]) ).
cnf(s256,plain,
( ~ spl80_9
| ~ spl80_127
| ~ spl80_128
| ~ spl80_129 ),
inference(sat_conversion,[],[f26862]) ).
cnf(s277,plain,
( ~ spl80_9
| spl80_129 ),
inference(rat,[],[s142,s145]) ).
cnf(s278,plain,
( ~ spl80_9
| spl80_127 ),
inference(rat,[],[s141,s145]) ).
cnf(s308,plain,
spl80_129,
inference(rat,[],[s277,s11]) ).
cnf(s309,plain,
spl80_127,
inference(rat,[],[s278,s11]) ).
cnf(s311,plain,
$false,
inference(rat,[],[s256,s11,s145,s308,s309]) ).
fof(f26863,plain,
$false,
inference(avatar_sat_refutation,[],[s311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU221+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n009.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.40 % DateTime : Mon Sep 28 04:08:46 UTC 2026
% 0.10/0.40 % CPUTime :
% 0.10/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.43 Running first-order model finding
% 0.10/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.51/2.55 % (2650573)Will run a generic schedule for satisfiability detection.
% 14.51/2.55 % (2650584)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2729104497:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.51/2.55 % (2650579)% WARNING: option uhcvi not known.
% 14.51/2.55 % (2650578)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2498225503_2999 on theBenchmark for (2999ds/0Mi)
% 14.51/2.55 % (2650579)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1316570647:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.51/2.55 % (2650580)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=488905301:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.51/2.55 % (2650582)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2934381195:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.51/2.55 % (2650581)dis+10_1_sil=32000:sp=arity:random_seed=3421429073:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.51/2.55 % (2650583)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=578288915:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.51/2.55 % (2650584)Instruction limit reached!
% 14.51/2.55 % (2650584)------------------------------
% 14.51/2.55 % (2650584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.51/2.55 % (2650584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.55 % (2650584)CaDiCaL version: 2.1.3
% 14.51/2.55 % (2650584)Termination reason: Instruction limit
% 14.51/2.55 % (2650584)Termination phase: Saturation
% 14.51/2.55 % (2650584)Time elapsed: 0.056 s
% 14.51/2.55 % (2650584)Peak memory usage: 14 MB
% 14.51/2.55 % (2650584)Instructions burned: 160 (million)
% 14.51/2.55 % TRYING [1]
% 14.51/2.55 % TRYING [2]
% 14.51/2.55 % (2650592)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3298591286:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.51/2.55 % (2650583)Instruction limit reached!
% 14.51/2.55 % (2650583)------------------------------
% 14.51/2.55 % (2650583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.51/2.55 % (2650583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.55 % (2650583)CaDiCaL version: 2.1.3
% 14.51/2.55 % (2650583)Termination reason: Instruction limit
% 14.51/2.55 % (2650583)Termination phase: Saturation
% 14.51/2.55 % (2650583)Time elapsed: 0.066 s
% 14.51/2.55 % (2650583)Peak memory usage: 13 MB
% 14.51/2.55 % (2650583)Instructions burned: 132 (million)
% 14.51/2.55 % (2650582)Instruction limit reached!
% 14.51/2.55 % (2650582)------------------------------
% 14.51/2.55 % (2650582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.51/2.55 % (2650582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.55 % (2650582)CaDiCaL version: 2.1.3
% 14.51/2.55 % (2650582)Termination reason: Instruction limit
% 14.51/2.55 % (2650582)Termination phase: Saturation
% 14.51/2.55 % (2650582)Time elapsed: 0.069 s
% 14.51/2.55 % (2650582)Peak memory usage: 13 MB
% 14.51/2.55 % (2650582)Instructions burned: 117 (million)
% 14.51/2.55 % (2650581)Instruction limit reached!
% 14.51/2.55 % (2650581)------------------------------
% 14.51/2.55 % (2650581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.51/2.55 % (2650581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.51/2.55 % (2650581)CaDiCaL version: 2.1.3
% 14.51/2.55 % (2650581)Termination reason: Instruction limit
% 14.51/2.55 % (2650581)Termination phase: Saturation
% 14.51/2.55 % (2650581)Time elapsed: 0.075 s
% 14.51/2.55 % (2650581)Peak memory usage: 13 MB
% 14.51/2.55 % (2650581)Instructions burned: 104 (million)
% 14.51/2.55 % TRYING [3]
% 14.51/2.55 % TRYING [1]
% 14.51/2.55 % TRYING [2]
% 14.51/2.55 % (2650594)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4106986882:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.51/2.55 % (2650595)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1855733352:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.51/2.55 % (2650596)ott-21_1_sil=16000:fs=off:random_seed=3416024418:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.51/2.55 % TRYING [3]
% 14.51/2.55 % TRYING [4]
% 14.51/2.55 % (2650594)Instruction limit reached!
% 14.51/2.55 % (2650594)------------------------------
% 14.51/2.55 % (2650594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.51/2.55 % (2650594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650594)CaDiCaL version: 2.1.3
% 42.88/6.59 % (2650594)Termination reason: Instruction limit
% 42.88/6.59 % (2650594)Termination phase: Saturation
% 42.88/6.59 % (2650594)Time elapsed: 0.072 s
% 42.88/6.59 % (2650594)Peak memory usage: 14 MB
% 42.88/6.59 % (2650594)Instructions burned: 131 (million)
% 42.88/6.59 % (2650600)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2284719445:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.88/6.59 % (2650596)Instruction limit reached!
% 42.88/6.59 % (2650596)------------------------------
% 42.88/6.59 % (2650596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.88/6.59 % (2650596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650596)CaDiCaL version: 2.1.3
% 42.88/6.59 % (2650596)Termination reason: Instruction limit
% 42.88/6.59 % (2650596)Termination phase: Saturation
% 42.88/6.59 % (2650596)Time elapsed: 0.102 s
% 42.88/6.59 % (2650596)Peak memory usage: 14 MB
% 42.88/6.59 % (2650596)Instructions burned: 181 (million)
% 42.88/6.59 % (2650592)Instruction limit reached!
% 42.88/6.59 % (2650592)------------------------------
% 42.88/6.59 % (2650592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.88/6.59 % (2650592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650592)CaDiCaL version: 2.1.3
% 42.88/6.59 % (2650592)Termination reason: Instruction limit
% 42.88/6.59 % (2650592)Termination phase: Finite model building constraint generation
% 42.88/6.59 % (2650592)Time elapsed: 0.141 s
% 42.88/6.59 % (2650592)Peak memory usage: 32 MB
% 42.88/6.59 % (2650592)Instructions burned: 716 (million)
% 42.88/6.59 % (2650603)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1702582192:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 42.88/6.59 % (2650602)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4172442883:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.88/6.59 % TRYING [4]
% 42.88/6.59 % TRYING [1]
% 42.88/6.59 % TRYING [2]
% 42.88/6.59 % TRYING [3]
% 42.88/6.59 % (2650595)Instruction limit reached!
% 42.88/6.59 % (2650595)------------------------------
% 42.88/6.59 % (2650595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.88/6.59 % (2650595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650595)CaDiCaL version: 2.1.3
% 42.88/6.59 % (2650595)Termination reason: Instruction limit
% 42.88/6.59 % (2650595)Termination phase: Saturation
% 42.88/6.59 % (2650595)Time elapsed: 0.368 s
% 42.88/6.59 % (2650595)Peak memory usage: 15 MB
% 42.88/6.59 % (2650595)Instructions burned: 684 (million)
% 42.88/6.59 % (2650606)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1858050800:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.88/6.59 % (2650600)Instruction limit reached!
% 42.88/6.59 % (2650600)------------------------------
% 42.88/6.59 % (2650600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.88/6.59 % (2650600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650600)CaDiCaL version: 2.1.3
% 42.88/6.59 % (2650600)Termination reason: Instruction limit
% 42.88/6.59 % (2650600)Termination phase: Saturation
% 42.88/6.59 % (2650600)Time elapsed: 0.334 s
% 42.88/6.59 % (2650600)Peak memory usage: 15 MB
% 42.88/6.59 % (2650600)Instructions burned: 477 (million)
% 42.88/6.59 % (2650608)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2141819372:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 42.88/6.59 % (2650603)Instruction limit reached!
% 42.88/6.59 % (2650603)------------------------------
% 42.88/6.59 % (2650603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.88/6.59 % (2650603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650603)CaDiCaL version: 2.1.3
% 42.88/6.59 % (2650603)Termination reason: Instruction limit
% 42.88/6.59 % (2650603)Termination phase: Saturation
% 42.88/6.59 % (2650603)Time elapsed: 0.385 s
% 42.88/6.59 % (2650603)Peak memory usage: 25 MB
% 42.88/6.59 % (2650603)Instructions burned: 1182 (million)
% 42.88/6.59 % (2650602)Instruction limit reached!
% 42.88/6.59 % (2650602)------------------------------
% 42.88/6.59 % (2650602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.88/6.59 % (2650602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.88/6.59 % (2650602)CaDiCaL version: 2.1.3
% 92.54/13.57 % (2650602)Termination reason: Instruction limit
% 92.54/13.57 % (2650602)Termination phase: Finite model building SAT solving
% 92.54/13.57 % (2650602)Time elapsed: 0.387 s
% 92.54/13.57 % (2650602)Peak memory usage: 34 MB
% 92.54/13.57 % (2650602)Instructions burned: 866 (million)
% 92.54/13.57 % (2650610)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2645793532:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 92.54/13.57 % (2650611)fmb+10_1_sil=64000:random_seed=2406968975:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 92.54/13.57 % TRYING [1]
% 92.54/13.57 % TRYING [2]
% 92.54/13.57 % TRYING [3]
% 92.54/13.57 % TRYING [5]
% 92.54/13.57 % (2650608)Instruction limit reached!
% 92.54/13.57 % (2650608)------------------------------
% 92.54/13.57 % (2650608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.54/13.57 % (2650608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.54/13.57 % (2650608)CaDiCaL version: 2.1.3
% 92.54/13.57 % (2650608)Termination reason: Instruction limit
% 92.54/13.57 % (2650608)Termination phase: Saturation
% 92.54/13.57 % (2650608)Time elapsed: 0.351 s
% 92.54/13.57 % (2650608)Peak memory usage: 19 MB
% 92.54/13.57 % (2650608)Instructions burned: 692 (million)
% 92.54/13.57 % (2650610)Instruction limit reached!
% 92.54/13.57 % (2650610)------------------------------
% 92.54/13.57 % (2650610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.54/13.57 % (2650610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.54/13.57 % (2650610)CaDiCaL version: 2.1.3
% 92.54/13.57 % (2650610)Termination reason: Instruction limit
% 92.54/13.57 % (2650610)Termination phase: Saturation
% 92.54/13.57 % (2650610)Time elapsed: 0.274 s
% 92.54/13.57 % (2650610)Peak memory usage: 21 MB
% 92.54/13.57 % (2650610)Instructions burned: 880 (million)
% 92.54/13.57 % (2650606)Instruction limit reached!
% 92.54/13.57 % (2650606)------------------------------
% 92.54/13.57 % (2650606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.54/13.57 % (2650606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.54/13.57 % (2650606)CaDiCaL version: 2.1.3
% 92.54/13.57 % (2650606)Termination reason: Instruction limit
% 92.54/13.57 % (2650606)Termination phase: Finite model building constraint generation
% 92.54/13.57 % (2650606)Time elapsed: 0.411 s
% 92.54/13.57 % (2650606)Peak memory usage: 102 MB
% 92.54/13.57 % (2650606)Instructions burned: 890 (million)
% 92.54/13.57 % (2650614)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2808880726:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 92.54/13.57 % (2650615)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2495807611:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 92.54/13.57 % (2650617)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4115602884:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 92.54/13.57 % TRYING [20]
% 92.54/13.57 % TRYING [8]
% 92.54/13.57 % TRYING [4]
% 92.54/13.57 % (2650615)Instruction limit reached!
% 92.54/13.57 % (2650615)------------------------------
% 92.54/13.57 % (2650615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.54/13.57 % (2650615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.54/13.57 % (2650615)CaDiCaL version: 2.1.3
% 92.54/13.57 % (2650615)Termination reason: Instruction limit
% 92.54/13.57 % (2650615)Termination phase: Finite model building constraint generation
% 92.54/13.57 % (2650615)Time elapsed: 0.320 s
% 92.54/13.57 % (2650615)Peak memory usage: 60 MB
% 92.54/13.57 % (2650615)Instructions burned: 921 (million)
% 92.54/13.57 % (2650620)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2394504267:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 92.54/13.57 % (2650620)Instruction limit reached!
% 92.54/13.57 % (2650620)------------------------------
% 92.54/13.57 % (2650620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 92.54/13.57 % (2650620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.54/13.57 % (2650620)CaDiCaL version: 2.1.3
% 92.54/13.57 % (2650620)Termination reason: Instruction limit
% 92.54/13.57 % (2650620)Termination phase: Saturation
% 92.54/13.57 % (2650620)Time elapsed: 0.739 s
% 92.54/13.57 % (2650620)Peak memory usage: 25 MB
% 92.54/13.57 % (2650620)Instructions burned: 1472 (million)
% 92.54/13.57 % (2650622)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1794418029:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 92.54/13.57 % (2650622)Cannot represent all propositional literals internally
% 92.54/13.57 % (2650622)Refutation not found, incomplete strategy
% 193.24/27.75 % (2650622)------------------------------
% 193.24/27.75 % (2650622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 193.24/27.75 % (2650622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.24/27.75 % (2650622)CaDiCaL version: 2.1.3
% 193.24/27.75 % (2650622)Termination reason: Refutation not found, incomplete strategy
% 193.24/27.75 % (2650622)Time elapsed: 0.050 s
% 193.24/27.75 % (2650622)Peak memory usage: 13 MB
% 193.24/27.75 % (2650622)Instructions burned: 101 (million)
% 193.24/27.75 % (2650622)------------------------------
% 193.24/27.75 % (2650622)------------------------------
% 193.24/27.75 % (2650624)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1382718587:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 193.24/27.75 % TRYING [16]
% 193.24/27.75 % TRYING [5]
% 193.24/27.75 % (2650614)Instruction limit reached!
% 193.24/27.75 % (2650614)------------------------------
% 193.24/27.75 % (2650614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 193.24/27.75 % (2650614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.24/27.75 % (2650614)CaDiCaL version: 2.1.3
% 193.24/27.75 % (2650614)Termination reason: Instruction limit
% 193.24/27.75 % (2650614)Termination phase: Finite model building constraint generation
% 193.24/27.75 % (2650614)Time elapsed: 1.870 s
% 193.24/27.75 % (2650614)Peak memory usage: 614 MB
% 193.24/27.75 % (2650614)Instructions burned: 9517 (million)
% 193.24/27.75 % (2650626)ott-2_1_sil=16000:newcnf=on:random_seed=1454518343:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 193.24/27.75 % (2650624)Instruction limit reached!
% 193.24/27.75 % (2650624)------------------------------
% 193.24/27.75 % (2650624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 193.24/27.75 % (2650624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.24/27.75 % (2650624)CaDiCaL version: 2.1.3
% 193.24/27.75 % (2650624)Termination reason: Instruction limit
% 193.24/27.75 % (2650624)Termination phase: Finite model building constraint generation
% 193.24/27.75 % (2650624)Time elapsed: 0.825 s
% 193.24/27.75 % (2650624)Peak memory usage: 117 MB
% 193.24/27.75 % (2650624)Instructions burned: 2174 (million)
% 193.24/27.75 % (2650628)ott+10_1_sil=32000:tgt=ground:random_seed=1360916953:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 193.24/27.75 % TRYING [6]
% 193.24/27.75 % (2650626)Instruction limit reached!
% 193.24/27.75 % (2650626)------------------------------
% 193.24/27.75 % (2650626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 193.24/27.75 % (2650626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.24/27.75 % (2650626)CaDiCaL version: 2.1.3
% 193.24/27.75 % (2650626)Termination reason: Instruction limit
% 193.24/27.75 % (2650626)Termination phase: Saturation
% 193.24/27.75 % (2650626)Time elapsed: 0.284 s
% 193.24/27.75 % (2650626)Peak memory usage: 21 MB
% 193.24/27.75 % (2650626)Instructions burned: 869 (million)
% 193.24/27.75 % (2650630)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1198155459:i=54282_2968 on theBenchmark for (2968ds/54282Mi)
% 193.24/27.75 % TRYING [1]
% 193.24/27.75 % TRYING [2]
% 193.24/27.75 % TRYING [3]
% 193.24/27.75 % TRYING [4]
% 193.24/27.75 % TRYING [5]
% 193.24/27.75 % (2650617)Instruction limit reached!
% 193.24/27.75 % (2650617)------------------------------
% 193.24/27.75 % (2650617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 193.24/27.75 % (2650617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.24/27.75 % (2650617)CaDiCaL version: 2.1.3
% 193.24/27.75 % (2650617)Termination reason: Instruction limit
% 193.24/27.75 % (2650617)Termination phase: Saturation
% 193.24/27.75 % (2650617)Time elapsed: 3.0000 s
% 193.24/27.75 % (2650617)Peak memory usage: 45 MB
% 193.24/27.75 % (2650617)Instructions burned: 5131 (million)
% 193.24/27.75 % (2650632)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1241329983:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 193.24/27.75 % TRYING [6]
% 193.24/27.75 % TRYING [6]
% 193.24/27.75 % (2650632)Instruction limit reached!
% 193.24/27.75 % (2650632)------------------------------
% 193.24/27.75 % (2650632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 193.24/27.75 % (2650632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.24/27.75 % (2650632)CaDiCaL version: 2.1.3
% 193.24/27.75 % (2650632)Termination reason: Instruction limit
% 193.24/27.75 % (2650632)Termination phase: Saturation
% 193.24/27.75 % (2650632)Time elapsed: 2.137 s
% 193.24/27.75 % (2650632)Peak memory usage: 36 MB
% 193.24/27.75 % (2650632)Instructions burned: 3512 (million)
% 193.24/27.75 % (2650634)dis+21_1_sil=32000:sas=cadical:random_seed=1203883863:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 82.72/29.04 % (2650628)Instruction limit reached!
% 82.72/29.04 % (2650628)------------------------------
% 82.72/29.04 % (2650628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650628)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650628)Termination reason: Instruction limit
% 82.72/29.04 % (2650628)Termination phase: Saturation
% 82.72/29.04 % (2650628)Time elapsed: 3.235 s
% 82.72/29.04 % (2650628)Peak memory usage: 62 MB
% 82.72/29.04 % (2650628)Instructions burned: 5115 (million)
% 82.72/29.04 % (2650636)ott+11_1_sil=16000:gs=on:random_seed=576053379:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 82.72/29.04 % (2650636)Instruction limit reached!
% 82.72/29.04 % (2650636)------------------------------
% 82.72/29.04 % (2650636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650636)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650636)Termination reason: Instruction limit
% 82.72/29.04 % (2650636)Termination phase: Saturation
% 82.72/29.04 % (2650636)Time elapsed: 1.199 s
% 82.72/29.04 % (2650636)Peak memory usage: 25 MB
% 82.72/29.04 % (2650636)Instructions burned: 2253 (million)
% 82.72/29.04 % (2650638)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3412096467:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi)
% 82.72/29.04 % TRYING [7]
% 82.72/29.04 % TRYING [7]
% 82.72/29.04 % (2650634)Instruction limit reached!
% 82.72/29.04 % (2650634)------------------------------
% 82.72/29.04 % (2650634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650634)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650634)Termination reason: Instruction limit
% 82.72/29.04 % (2650634)Termination phase: Saturation
% 82.72/29.04 % (2650634)Time elapsed: 2.271 s
% 82.72/29.04 % (2650634)Peak memory usage: 44 MB
% 82.72/29.04 % (2650634)Instructions burned: 3773 (million)
% 82.72/29.04 % (2650640)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3141788814:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi)
% 82.72/29.04 % TRYING [7]
% 82.72/29.04 % (2650611)Instruction limit reached!
% 82.72/29.04 % (2650611)------------------------------
% 82.72/29.04 % (2650611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650611)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650611)Termination reason: Instruction limit
% 82.72/29.04 % (2650611)Termination phase: Finite model building SAT solving
% 82.72/29.04 % (2650611)Time elapsed: 9.566 s
% 82.72/29.04 % (2650611)Peak memory usage: 411 MB
% 82.72/29.04 % (2650611)Instructions burned: 22061 (million)
% 82.72/29.04 % (2650642)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=619417661:i=29340_2896 on theBenchmark for (2896ds/29340Mi)
% 82.72/29.04 % (2650640)Instruction limit reached!
% 82.72/29.04 % (2650640)------------------------------
% 82.72/29.04 % (2650640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650640)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650640)Termination reason: Instruction limit
% 82.72/29.04 % (2650640)Termination phase: Saturation
% 82.72/29.04 % (2650640)Time elapsed: 2.108 s
% 82.72/29.04 % (2650640)Peak memory usage: 39 MB
% 82.72/29.04 % (2650640)Instructions burned: 4592 (million)
% 82.72/29.04 % (2650644)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3581118890:i=5211_2894 on theBenchmark for (2894ds/5211Mi)
% 82.72/29.04 % (2650644)Instruction limit reached!
% 82.72/29.04 % (2650644)------------------------------
% 82.72/29.04 % (2650644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650644)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650644)Termination reason: Instruction limit
% 82.72/29.04 % (2650644)Termination phase: Saturation
% 82.72/29.04 % (2650644)Time elapsed: 2.520 s
% 82.72/29.04 % (2650644)Peak memory usage: 46 MB
% 82.72/29.04 % (2650644)Instructions burned: 5213 (million)
% 82.72/29.04 % (2650646)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1891115131:i=5497:nm=2_2868 on theBenchmark for (2868ds/5497Mi)
% 82.72/29.04 % TRYING [17]
% 82.72/29.04 % (2650630)Instruction limit reached!
% 82.72/29.04 % (2650630)------------------------------
% 82.72/29.04 % (2650630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650630)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650630)Termination reason: Instruction limit
% 82.72/29.04 % (2650630)Termination phase: Finite model building constraint generation
% 82.72/29.04 % (2650630)Time elapsed: 10.954 s
% 82.72/29.04 % (2650630)Peak memory usage: 1724 MB
% 82.72/29.04 % (2650630)Instructions burned: 54286 (million)
% 82.72/29.04 % (2650648)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2417137757:fmbsr=2:i=46332_2857 on theBenchmark for (2857ds/46332Mi)
% 82.72/29.04 % TRYING [15]
% 82.72/29.04 % (2650646)Instruction limit reached!
% 82.72/29.04 % (2650646)------------------------------
% 82.72/29.04 % (2650646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650646)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650646)Termination reason: Instruction limit
% 82.72/29.04 % (2650646)Termination phase: Finite model building constraint generation
% 82.72/29.04 % (2650646)Time elapsed: 1.937 s
% 82.72/29.04 % (2650646)Peak memory usage: 346 MB
% 82.72/29.04 % (2650646)Instructions burned: 5499 (million)
% 82.72/29.04 % (2650650)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1385005215:i=14071_2848 on theBenchmark for (2848ds/14071Mi)
% 82.72/29.04 % TRYING [12]
% 82.72/29.04 % (2650650)Instruction limit reached!
% 82.72/29.04 % (2650650)------------------------------
% 82.72/29.04 % (2650650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650650)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650650)Termination reason: Instruction limit
% 82.72/29.04 % (2650650)Termination phase: Finite model building constraint generation
% 82.72/29.04 % (2650650)Time elapsed: 4.824 s
% 82.72/29.04 % (2650650)Peak memory usage: 760 MB
% 82.72/29.04 % (2650650)Instructions burned: 14071 (million)
% 82.72/29.04 % (2650652)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=726466121:i=22565:add=on:rawr=on_2799 on theBenchmark for (2799ds/22565Mi)
% 82.72/29.04 % (2650648)Instruction limit reached!
% 82.72/29.04 % (2650648)------------------------------
% 82.72/29.04 % (2650648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650648)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650648)Termination reason: Instruction limit
% 82.72/29.04 % (2650648)Termination phase: Finite model building constraint generation
% 82.72/29.04 % (2650648)Time elapsed: 8.500 s
% 82.72/29.04 % (2650648)Peak memory usage: 2212 MB
% 82.72/29.04 % (2650648)Instructions burned: 46336 (million)
% 82.72/29.04 % (2650654)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=178762893:i=8173:av=off_2770 on theBenchmark for (2770ds/8173Mi)
% 82.72/29.04 % TRYING [8]
% 82.72/29.04 % (2650654)Instruction limit reached!
% 82.72/29.04 % (2650654)------------------------------
% 82.72/29.04 % (2650654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650654)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650654)Termination reason: Instruction limit
% 82.72/29.04 % (2650654)Termination phase: Saturation
% 82.72/29.04 % (2650654)Time elapsed: 2.628 s
% 82.72/29.04 % (2650654)Peak memory usage: 88 MB
% 82.72/29.04 % (2650654)Instructions burned: 8175 (million)
% 82.72/29.04 % (2650656)dis+10_16:1_sil=16000:random_seed=3397554242:i=9155:fsr=off_2744 on theBenchmark for (2744ds/9155Mi)
% 82.72/29.04 % (2650642)Instruction limit reached!
% 82.72/29.04 % (2650642)------------------------------
% 82.72/29.04 % (2650642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650642)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650642)Termination reason: Instruction limit
% 82.72/29.04 % (2650642)Termination phase: Saturation
% 82.72/29.04 % (2650642)Time elapsed: 16.994 s
% 82.72/29.04 % (2650642)Peak memory usage: 649 MB
% 82.72/29.04 % (2650642)Instructions burned: 29342 (million)
% 82.72/29.04 % (2650658)ott-3_8_sil=64000:random_seed=4191609311:i=20139:bs=on_2725 on theBenchmark for (2725ds/20139Mi)
% 82.72/29.04 % (2650658) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2650573-2650658"...
% 82.72/29.04 % (2650658)...printing done.
% 82.72/29.04 % (2650658)Refutation found. Thanks to Tanya!
% 82.72/29.04 % SZS status Theorem for theBenchmark
% 82.72/29.04 % SZS output start Proof for theBenchmark
% See solution above
% 82.72/29.04 % (2650658)------------------------------
% 82.72/29.04 % (2650658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.72/29.04 % (2650658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.72/29.04 % (2650658)CaDiCaL version: 2.1.3
% 82.72/29.04 % (2650658)Termination reason: Refutation
% 82.72/29.04 % (2650658)Time elapsed: 0.888 s
% 82.72/29.04 % (2650658)Peak memory usage: 25 MB
% 82.72/29.04 % (2650658)Instructions burned: 1297 (million)
% 82.72/29.04 % (2650573)Success in time 28.602 s
% 82.72/29.04 % Vampire exiting
%------------------------------------------------------------------------------