%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV029-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 10:59:01 AM UTC 2026
% Result : Unsatisfiable 14.69s 2.54s
% Output : Refutation 14.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 33
% Syntax : Number of formulae : 174 ( 20 unt; 12 def)
% Number of atoms : 548 ( 90 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 587 ( 213 ~; 362 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 13 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 38 ( 0 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0] : fwork_DOTfifo_DOTrtl_DOTlevel_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(X0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_5) ).
fof(f6,axiom,
! [X0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) != fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_6) ).
fof(f7,plain,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ != fwork_DOTfifo_DOTrtl_DOTint__level_(X0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0)) ),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X0] :
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_7) ).
fof(f9,plain,
! [X0] :
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(X0))
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(X0) ),
inference(reorient_equations,[],[f8]) ).
fof(f16,axiom,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = n0
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_12) ).
fof(f17,plain,
! [X0] :
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) ),
inference(reorient_equations,[],[f16]) ).
fof(f23,axiom,
! [X0] :
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_18) ).
fof(f29,axiom,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X0)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_23) ).
fof(f30,plain,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
inference(reorient_equations,[],[f29]) ).
fof(f38,axiom,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X0)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_31) ).
fof(f39,plain,
! [X0] :
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
inference(reorient_equations,[],[f38]) ).
fof(f44,axiom,
! [X0] :
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_36) ).
fof(f52,axiom,
! [X0] :
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_43) ).
fof(f56,axiom,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X0)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_47) ).
fof(f57,plain,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
inference(reorient_equations,[],[f56]) ).
fof(f61,axiom,
! [X0] :
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(X0)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_51) ).
fof(f62,plain,
! [X0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
inference(reorient_equations,[],[f61]) ).
fof(f73,axiom,
! [X0] :
( p_LES_EQU_(X0,n0)
| ~ p_LES_EQU_(X0,f_SUB_(X0,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_61) ).
fof(f80,axiom,
! [X0,X1] :
( p_LES_EQU_(f_ADD_(X1,n1),X0)
| ~ p_LES_EQU_(X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_68) ).
fof(f82,axiom,
! [X0,X1] :
( ~ p_LES_EQU_(X1,X0)
| ~ p_LES_EQU_(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_70) ).
fof(f83,axiom,
! [X2,X0,X1] :
( p_LES_EQU_(X2,X1)
| ~ p_LES_EQU_(X0,X1)
| p_LES_EQU_(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_71) ).
fof(f85,axiom,
! [X0] :
( ~ p_LES_EQU_(X0,n0)
| X0 = n0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_73) ).
fof(f86,plain,
! [X0] :
( ~ p_LES_EQU_(X0,n0)
| n0 = X0 ),
inference(reorient_equations,[],[f85]) ).
fof(f89,axiom,
! [X0] : p_LES_EQU_(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_75) ).
fof(f91,axiom,
! [X0] : f_ADD_(n0,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV004-0.ax',axiom_77) ).
fof(f152,negated_conjecture,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f153,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f154,negated_conjecture,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
fof(f155,plain,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
inference(definition_unfolding,[],[f152,f5]) ).
fof(f156,plain,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)),fwork_DOTfifo_DOTrtl_DOTfifo__length_),
inference(definition_unfolding,[],[f153,f5]) ).
fof(f182,plain,
! [X0] :
( ~ p_LES_EQU_(X0,f_SUB_(X0,n1))
| n0 = X0 ),
inference(resolution,[],[f73,f86]) ).
fof(f244,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(resolution,[],[f82,f155]) ).
fof(f250,definition,
( spl0_3
<=> fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f251,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ != fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_3 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f252,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl0_4
<=> p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f256,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))
| spl0_4 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f257,plain,
( spl0_3
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f244,f254,f250]) ).
fof(f264,plain,
! [X0] :
( p_LES_EQU_(X0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ p_LES_EQU_(X0,n0) ),
inference(resolution,[],[f83,f154]) ).
fof(f269,plain,
! [X0] :
( p_LES_EQU_(X0,fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)))
| ~ p_LES_EQU_(X0,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
inference(resolution,[],[f83,f156]) ).
fof(f277,plain,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)),n0),
inference(resolution,[],[f264,f156]) ).
fof(f359,plain,
! [X0] :
( p_LES_EQU_(n1,X0)
| ~ p_LES_EQU_(n0,X0)
| n0 = X0 ),
inference(superposition,[],[f80,f91]) ).
fof(f507,definition,
( spl0_6
<=> n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f508,plain,
( n0 != fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_6 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,definition,
( spl0_7
<=> p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f512,plain,
( ~ p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| spl0_7 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f552,plain,
( p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ spl0_6 ),
inference(superposition,[],[f155,f509]) ).
fof(f554,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ != n0
| p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(t_206))
| ~ spl0_6 ),
inference(superposition,[],[f7,f509]) ).
fof(f583,definition,
( spl0_8
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(t_206)) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f585,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTfull_(t_206))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f587,definition,
( spl0_9
<=> fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f589,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ != n0
| spl0_9 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f590,plain,
( spl0_8
| ~ spl0_9
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f554,f507,f587,f583]) ).
fof(f865,plain,
! [X0] :
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
inference(forward_subsumption_resolution,[],[f30,f62]) ).
fof(f922,plain,
! [X0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = n0 ),
inference(resolution,[],[f39,f86]) ).
fof(f962,plain,
! [X0] :
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n0)
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0)) ),
inference(forward_subsumption_resolution,[],[f57,f62]) ).
fof(f971,plain,
( ~ p_LES_EQU_(n0,n0)
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_6 ),
inference(superposition,[],[f962,f509]) ).
fof(f973,plain,
( ~ p_LES_EQU_(n0,n0)
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f971,f17]) ).
fof(f974,plain,
( n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f973,f89]) ).
fof(f976,definition,
( spl0_15
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f977,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| spl0_15 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f978,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f980,definition,
( spl0_16
<=> n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f981,plain,
( n0 != fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| spl0_16 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f982,plain,
( n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f983,plain,
( spl0_15
| spl0_16
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f974,f507,f980,f976]) ).
fof(f997,definition,
( spl0_17
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f998,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| spl0_17 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f999,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f1026,plain,
( ~ p_LES_EQU_(n0,n0)
| f_ADD_(n0,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_6 ),
inference(superposition,[],[f44,f509]) ).
fof(f1028,plain,
( f_ADD_(n0,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1026,f89]) ).
fof(f1029,plain,
( f_ADD_(n0,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_6
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1028,f978]) ).
fof(f1030,plain,
( n1 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_6
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1029,f91]) ).
fof(f1049,plain,
! [X0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(X0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(X0,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(X0),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(X0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(X0) = n0 ),
inference(resolution,[],[f52,f86]) ).
fof(f1158,definition,
( spl0_21
<=> p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1159,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| spl0_21 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1160,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1162,definition,
( spl0_22
<=> n1 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1164,plain,
( n1 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1177,plain,
( n1 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_6
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1030,f1160]) ).
fof(f1179,plain,
( spl0_17
| spl0_22
| ~ spl0_6
| ~ spl0_15
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1177,f1158,f976,f507,f1162,f997]) ).
fof(f1183,plain,
( ~ p_LES_EQU_(n1,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ spl0_22 ),
inference(superposition,[],[f156,f1164]) ).
fof(f1217,plain,
( ~ spl0_7
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1183,f1162,f511]) ).
fof(f1818,plain,
( ~ p_LES_EQU_(n0,n0)
| ~ spl0_16 ),
inference(superposition,[],[f277,f982]) ).
fof(f1857,plain,
( $false
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1818,f89]) ).
fof(f1858,plain,
~ spl0_16,
inference(avatar_contradiction_clause,[],[f1857]) ).
fof(f1942,plain,
( n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ spl0_17 ),
inference(resolution,[],[f999,f17]) ).
fof(f2017,plain,
( $false
| spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1942,f981]) ).
fof(f2018,plain,
( spl0_16
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2017]) ).
fof(f2705,plain,
( ~ p_LES_EQU_(n0,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0
| spl0_7 ),
inference(resolution,[],[f359,f512]) ).
fof(f2741,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0
| ~ spl0_6
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f2705,f552]) ).
fof(f2745,plain,
( $false
| ~ spl0_6
| spl0_7
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f2741,f589]) ).
fof(f2746,plain,
( ~ spl0_6
| spl0_7
| spl0_9 ),
inference(avatar_contradiction_clause,[],[f2745]) ).
fof(f2773,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| ~ spl0_8 ),
inference(resolution,[],[f585,f9]) ).
fof(f3871,plain,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_3 ),
inference(superposition,[],[f39,f252]) ).
fof(f3875,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_3 ),
inference(superposition,[],[f865,f252]) ).
fof(f3892,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3871,f154]) ).
fof(f9994,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_17 ),
inference(resolution,[],[f922,f998]) ).
fof(f10814,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3875,f89]) ).
fof(f10821,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ spl0_3
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f10814,f998]) ).
fof(f10891,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ spl0_3
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f10821,f1159]) ).
fof(f10914,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ spl0_3
| spl0_17
| spl0_21 ),
inference(superposition,[],[f156,f10891]) ).
fof(f10958,plain,
( $false
| ~ spl0_3
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f10914,f89]) ).
fof(f10959,plain,
( ~ spl0_3
| spl0_17
| spl0_21 ),
inference(avatar_contradiction_clause,[],[f10958]) ).
fof(f10966,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| spl0_6
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f9994,f508]) ).
fof(f10970,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| ~ spl0_3
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f3892,f998]) ).
fof(f13538,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| ~ spl0_3
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f10970,f1160]) ).
fof(f13539,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ spl0_3
| ~ spl0_15
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f13538,f978]) ).
fof(f13552,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ spl0_3
| ~ spl0_15
| spl0_17
| ~ spl0_21 ),
inference(superposition,[],[f156,f13539]) ).
fof(f13602,plain,
( $false
| ~ spl0_3
| ~ spl0_15
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f13552,f89]) ).
fof(f13603,plain,
( ~ spl0_3
| ~ spl0_15
| spl0_17
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f13602]) ).
fof(f13619,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| spl0_6
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f10966,f1160]) ).
fof(f13648,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| spl0_4 ),
inference(resolution,[],[f256,f23]) ).
fof(f13697,plain,
( $false
| spl0_3
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f2773,f251]) ).
fof(f13698,plain,
( spl0_3
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f13697]) ).
fof(f31085,definition,
( spl0_102
<=> fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f31086,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) != fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| spl0_102 ),
inference(avatar_component_clause,[],[f31085]) ).
fof(f31087,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f31085]) ).
fof(f31088,plain,
( spl0_102
| ~ spl0_15
| spl0_6
| spl0_17
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f13619,f1158,f997,f507,f976,f31085]) ).
fof(f31096,plain,
( ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_15 ),
inference(resolution,[],[f977,f1049]) ).
fof(f31104,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_15
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f31096,f1160]) ).
fof(f31112,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f31104,f998]) ).
fof(f31115,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_SUB_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f31112,f508]) ).
fof(f31168,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)))
| n0 = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(superposition,[],[f182,f31115]) ).
fof(f31172,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)))
| spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f31168,f508]) ).
fof(f31196,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(resolution,[],[f31172,f269]) ).
fof(f31219,plain,
( $false
| spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f31196,f155]) ).
fof(f31220,plain,
( spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f31219]) ).
fof(f31250,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| ~ spl0_102 ),
inference(superposition,[],[f156,f31087]) ).
fof(f31303,plain,
( $false
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f31250,f155]) ).
fof(f31304,plain,
~ spl0_102,
inference(avatar_contradiction_clause,[],[f31303]) ).
fof(f31312,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| spl0_4
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f13648,f978]) ).
fof(f31317,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| spl0_4
| ~ spl0_15
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f31312,f998]) ).
fof(f31343,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f31317,f1159]) ).
fof(f31344,plain,
( ~ p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(superposition,[],[f156,f31343]) ).
fof(f31407,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(resolution,[],[f31344,f80]) ).
fof(f31422,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f31407,f155]) ).
fof(f31429,plain,
( $false
| spl0_3
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f31422,f251]) ).
fof(f31430,plain,
( spl0_3
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(avatar_contradiction_clause,[],[f31429]) ).
fof(f31450,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| spl0_15 ),
inference(resolution,[],[f977,f62]) ).
fof(f31467,plain,
( fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| spl0_15
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f31450,f1159]) ).
fof(f31476,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| spl0_15
| spl0_21
| spl0_102 ),
inference(forward_subsumption_resolution,[],[f31467,f31086]) ).
fof(f31480,plain,
( $false
| spl0_15
| spl0_17
| spl0_21
| spl0_102 ),
inference(forward_subsumption_resolution,[],[f31476,f998]) ).
fof(f31481,plain,
( spl0_15
| spl0_17
| spl0_21
| spl0_102 ),
inference(avatar_contradiction_clause,[],[f31480]) ).
cnf(s2,plain,
( spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f257]) ).
cnf(s5,plain,
( ~ spl0_6
| spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f590]) ).
cnf(s10,plain,
( ~ spl0_6
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f983]) ).
cnf(s14,plain,
( ~ spl0_6
| ~ spl0_15
| spl0_17
| ~ spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s15,plain,
( ~ spl0_7
| ~ spl0_22 ),
inference(sat_conversion,[],[f1217]) ).
cnf(s20,plain,
~ spl0_16,
inference(sat_conversion,[],[f1858]) ).
cnf(s22,plain,
( spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s34,plain,
( ~ spl0_6
| spl0_7
| spl0_9 ),
inference(sat_conversion,[],[f2746]) ).
cnf(s72,plain,
( ~ spl0_3
| spl0_17
| spl0_21 ),
inference(sat_conversion,[],[f10959]) ).
cnf(s85,plain,
( ~ spl0_3
| ~ spl0_15
| spl0_17
| ~ spl0_21 ),
inference(sat_conversion,[],[f13603]) ).
cnf(s86,plain,
( spl0_3
| ~ spl0_8 ),
inference(sat_conversion,[],[f13698]) ).
cnf(s126,plain,
( spl0_6
| ~ spl0_15
| spl0_17
| ~ spl0_21
| spl0_102 ),
inference(sat_conversion,[],[f31088]) ).
cnf(s129,plain,
( spl0_6
| spl0_15
| spl0_17
| ~ spl0_21 ),
inference(sat_conversion,[],[f31220]) ).
cnf(s132,plain,
~ spl0_102,
inference(sat_conversion,[],[f31304]) ).
cnf(s134,plain,
( spl0_3
| spl0_4
| ~ spl0_15
| spl0_17
| spl0_21 ),
inference(sat_conversion,[],[f31430]) ).
cnf(s138,plain,
( spl0_15
| spl0_17
| spl0_21
| spl0_102 ),
inference(sat_conversion,[],[f31481]) ).
cnf(s139,plain,
( spl0_6
| ~ spl0_15
| spl0_17
| ~ spl0_21 ),
inference(rat,[],[s126,s132]) ).
cnf(s140,plain,
~ spl0_17,
inference(rat,[],[s22,s20]) ).
cnf(s142,plain,
( ~ spl0_6
| ~ spl0_15
| ~ spl0_21
| spl0_22 ),
inference(rat,[],[s14,s140]) ).
cnf(s145,plain,
( ~ spl0_6
| spl0_15 ),
inference(rat,[],[s10,s20]) ).
cnf(s146,plain,
( ~ spl0_6
| spl0_3 ),
inference(rat,[],[s15,s142,s34,s134,s5,s145,s86,s2,s140]) ).
cnf(s147,plain,
( ~ spl0_15
| spl0_3 ),
inference(rat,[],[s139,s134,s2,s146,s140]) ).
cnf(s148,plain,
spl0_3,
inference(rat,[],[s129,s138,s147,s146,s140,s132]) ).
cnf(s149,plain,
spl0_21,
inference(rat,[],[s72,s140,s148]) ).
cnf(s150,plain,
~ spl0_15,
inference(rat,[],[s85,s148,s140,s149]) ).
cnf(s151,plain,
spl0_6,
inference(rat,[],[s129,s149,s140,s150]) ).
cnf(s153,plain,
$false,
inference(rat,[],[s145,s150,s151]) ).
fof(f31485,plain,
$false,
inference(avatar_sat_refutation,[],[s153]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV029-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 10:59:10 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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.69/2.54 % (1051052)Will run a generic schedule for satisfiability detection.
% 14.69/2.54 % (1051059)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1558520828:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.69/2.54 % (1051058)% WARNING: option uhcvi not known.
% 14.69/2.54 % (1051057)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=987868883_2999 on theBenchmark for (2999ds/0Mi)
% 14.69/2.54 % (1051058)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3298434074:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.69/2.54 % (1051060)dis+10_1_sil=32000:sp=arity:random_seed=541801144:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.69/2.54 % (1051061)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=156473309:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.69/2.54 % (1051062)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=704765915:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.69/2.54 % (1051063)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2915228030:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.69/2.54 % TRYING [1]
% 14.69/2.54 % TRYING [2]
% 14.69/2.54 % TRYING [3]
% 14.69/2.54 % TRYING [4]
% 14.69/2.54 % (1051060)Instruction limit reached!
% 14.69/2.54 % (1051060)------------------------------
% 14.69/2.54 % (1051060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051060)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051060)Termination reason: Instruction limit
% 14.69/2.54 % (1051060)Termination phase: Saturation
% 14.69/2.54 % (1051060)Time elapsed: 0.065 s
% 14.69/2.54 % (1051060)Peak memory usage: 12 MB
% 14.69/2.54 % (1051060)Instructions burned: 104 (million)
% 14.69/2.54 % (1051061)Instruction limit reached!
% 14.69/2.54 % (1051061)------------------------------
% 14.69/2.54 % (1051061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051061)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051061)Termination reason: Instruction limit
% 14.69/2.54 % (1051061)Termination phase: Saturation
% 14.69/2.54 % (1051061)Time elapsed: 0.070 s
% 14.69/2.54 % (1051061)Peak memory usage: 12 MB
% 14.69/2.54 % (1051061)Instructions burned: 116 (million)
% 14.69/2.54 % (1051062)Instruction limit reached!
% 14.69/2.54 % (1051062)------------------------------
% 14.69/2.54 % (1051062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051062)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051062)Termination reason: Instruction limit
% 14.69/2.54 % (1051062)Termination phase: Saturation
% 14.69/2.54 % (1051062)Time elapsed: 0.079 s
% 14.69/2.54 % (1051062)Peak memory usage: 13 MB
% 14.69/2.54 % (1051062)Instructions burned: 131 (million)
% 14.69/2.54 % (1051071)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1577071611:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.69/2.54 % (1051072)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3350078648:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.69/2.54 % (1051063)Instruction limit reached!
% 14.69/2.54 % (1051063)------------------------------
% 14.69/2.54 % (1051063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051063)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051063)Termination reason: Instruction limit
% 14.69/2.54 % (1051063)Termination phase: Saturation
% 14.69/2.54 % (1051063)Time elapsed: 0.094 s
% 14.69/2.54 % (1051063)Peak memory usage: 13 MB
% 14.69/2.54 % (1051063)Instructions burned: 159 (million)
% 14.69/2.54 % (1051073)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=2686866075:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.69/2.54 % TRYING [1]
% 14.69/2.54 % TRYING [2]
% 14.69/2.54 % TRYING [3]
% 14.69/2.54 % (1051076)ott-21_1_sil=16000:fs=off:random_seed=291450310:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.69/2.54 % TRYING [5]
% 14.69/2.54 % TRYING [4]
% 14.69/2.54 % (1051072)Instruction limit reached!
% 14.69/2.54 % (1051072)------------------------------
% 14.69/2.54 % (1051072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051072)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051072)Termination reason: Instruction limit
% 14.69/2.54 % (1051072)Termination phase: Saturation
% 14.69/2.54 % (1051072)Time elapsed: 0.078 s
% 14.69/2.54 % (1051072)Peak memory usage: 12 MB
% 14.69/2.54 % (1051072)Instructions burned: 133 (million)
% 14.69/2.54 % (1051079)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3279568322:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 14.69/2.54 % TRYING [5]
% 14.69/2.54 % (1051076)Instruction limit reached!
% 14.69/2.54 % (1051076)------------------------------
% 14.69/2.54 % (1051076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051076)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051076)Termination reason: Instruction limit
% 14.69/2.54 % (1051076)Termination phase: Saturation
% 14.69/2.54 % (1051076)Time elapsed: 0.097 s
% 14.69/2.54 % (1051076)Peak memory usage: 13 MB
% 14.69/2.54 % (1051076)Instructions burned: 182 (million)
% 14.69/2.54 % (1051081)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3494634538:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 14.69/2.54 % TRYING [1]
% 14.69/2.54 % TRYING [2]
% 14.69/2.54 % TRYING [3]
% 14.69/2.54 % TRYING [6]
% 14.69/2.54 % TRYING [4]
% 14.69/2.54 % (1051071)Instruction limit reached!
% 14.69/2.54 % (1051071)------------------------------
% 14.69/2.54 % (1051071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051071)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051071)Termination reason: Instruction limit
% 14.69/2.54 % (1051071)Termination phase: Finite model building constraint generation
% 14.69/2.54 % (1051071)Time elapsed: 0.268 s
% 14.69/2.54 % (1051071)Peak memory usage: 38 MB
% 14.69/2.54 % (1051071)Instructions burned: 716 (million)
% 14.69/2.54 % (1051083)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3062491617:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 14.69/2.54 % (1051073)Instruction limit reached!
% 14.69/2.54 % (1051073)------------------------------
% 14.69/2.54 % (1051073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051073)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051073)Termination reason: Instruction limit
% 14.69/2.54 % (1051073)Termination phase: Saturation
% 14.69/2.54 % (1051073)Time elapsed: 0.374 s
% 14.69/2.54 % (1051073)Peak memory usage: 18 MB
% 14.69/2.54 % (1051073)Instructions burned: 684 (million)
% 14.69/2.54 % (1051079)Instruction limit reached!
% 14.69/2.54 % (1051079)------------------------------
% 14.69/2.54 % (1051079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051079)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051079)Termination reason: Instruction limit
% 14.69/2.54 % (1051079)Termination phase: Saturation
% 14.69/2.54 % (1051079)Time elapsed: 0.297 s
% 14.69/2.54 % (1051079)Peak memory usage: 13 MB
% 14.69/2.54 % (1051079)Instructions burned: 478 (million)
% 14.69/2.54 % (1051085)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1775237755:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 14.69/2.54 % (1051086)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=646132702: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)
% 14.69/2.54 % TRYING [5]
% 14.69/2.54 % (1051081)Instruction limit reached!
% 14.69/2.54 % (1051081)------------------------------
% 14.69/2.54 % (1051081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051081)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051081)Termination reason: Instruction limit
% 14.69/2.54 % (1051081)Termination phase: Finite model building constraint generation
% 14.69/2.54 % (1051081)Time elapsed: 0.317 s
% 14.69/2.54 % (1051081)Peak memory usage: 24 MB
% 14.69/2.54 % (1051081)Instructions burned: 865 (million)
% 14.69/2.54 % (1051089)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=383984898:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 14.69/2.54 % TRYING [7]
% 14.69/2.54 % TRYING [14]
% 14.69/2.54 % (1051086)Instruction limit reached!
% 14.69/2.54 % (1051086)------------------------------
% 14.69/2.54 % (1051086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051086)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051086)Termination reason: Instruction limit
% 14.69/2.54 % (1051086)Termination phase: Saturation
% 14.69/2.54 % (1051086)Time elapsed: 0.370 s
% 14.69/2.54 % (1051086)Peak memory usage: 20 MB
% 14.69/2.54 % (1051086)Instructions burned: 693 (million)
% 14.69/2.54 % (1051085)Instruction limit reached!
% 14.69/2.54 % (1051085)------------------------------
% 14.69/2.54 % (1051085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051085)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051085)Termination reason: Instruction limit
% 14.69/2.54 % (1051085)Termination phase: Finite model building constraint generation
% 14.69/2.54 % (1051085)Time elapsed: 0.389 s
% 14.69/2.54 % (1051085)Peak memory usage: 99 MB
% 14.69/2.54 % (1051085)Instructions burned: 891 (million)
% 14.69/2.54 % (1051091)fmb+10_1_sil=64000:random_seed=3997972957:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 14.69/2.54 % (1051092)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1135216345:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 14.69/2.54 % TRYING [1]
% 14.69/2.54 % TRYING [2]
% 14.69/2.54 % TRYING [20]
% 14.69/2.54 % TRYING [3]
% 14.69/2.54 % TRYING [4]
% 14.69/2.54 % (1051083)Instruction limit reached!
% 14.69/2.54 % (1051083)------------------------------
% 14.69/2.54 % (1051083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051083)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051083)Termination reason: Instruction limit
% 14.69/2.54 % (1051083)Termination phase: Saturation
% 14.69/2.54 % (1051083)Time elapsed: 0.674 s
% 14.69/2.54 % (1051083)Peak memory usage: 19 MB
% 14.69/2.54 % (1051083)Instructions burned: 1180 (million)
% 14.69/2.54 % (1051095)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3562192034:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 14.69/2.54 % (1051089)Instruction limit reached!
% 14.69/2.54 % (1051089)------------------------------
% 14.69/2.54 % (1051089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051089)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051089)Termination reason: Instruction limit
% 14.69/2.54 % (1051089)Termination phase: Saturation
% 14.69/2.54 % (1051089)Time elapsed: 0.504 s
% 14.69/2.54 % (1051089)Peak memory usage: 20 MB
% 14.69/2.54 % (1051089)Instructions burned: 880 (million)
% 14.69/2.54 % TRYING [8]
% 14.69/2.54 % (1051097)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=60122051:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 14.69/2.54 % TRYING [5]
% 14.69/2.54 % (1051095)Instruction limit reached!
% 14.69/2.54 % (1051095)------------------------------
% 14.69/2.54 % (1051095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051095)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051095)Termination reason: Instruction limit
% 14.69/2.54 % (1051095)Termination phase: Finite model building constraint generation
% 14.69/2.54 % (1051095)Time elapsed: 0.329 s
% 14.69/2.54 % (1051095)Peak memory usage: 74 MB
% 14.69/2.54 % (1051095)Instructions burned: 920 (million)
% 14.69/2.54 % (1051099)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4007633857:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 14.69/2.54 % TRYING [6]
% 14.69/2.54 % (1051097) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1051052-1051097"...
% 14.69/2.54 % (1051097)...printing done.
% 14.69/2.54 % (1051097)Refutation found. Thanks to Tanya!
% 14.69/2.54 % SZS status Unsatisfiable for theBenchmark
% 14.69/2.54 % SZS output start Proof for theBenchmark
% See solution above
% 14.69/2.54 % (1051097)------------------------------
% 14.69/2.54 % (1051097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.69/2.54 % (1051097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.69/2.54 % (1051097)CaDiCaL version: 2.1.3
% 14.69/2.54 % (1051097)Termination reason: Refutation
% 14.69/2.54 % (1051097)Time elapsed: 0.954 s
% 14.69/2.54 % (1051097)Peak memory usage: 24 MB
% 14.69/2.54 % (1051097)Instructions burned: 1675 (million)
% 14.69/2.54 % (1051052)Success in time 2.12 s
% 14.69/2.54 % Vampire exiting
%------------------------------------------------------------------------------