%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV031-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 5.91s 1.39s
% Output : Refutation 5.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 70
% Syntax : Number of formulae : 483 ( 52 unt; 41 def)
% Number of atoms : 1488 ( 233 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1676 ( 671 ~; 969 |; 0 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 37 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 88 ( 0 sgn 88 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : plus(X0,n1) != n0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_1) ).
fof(f2,axiom,
! [X0] : gt(plus(X0,n1),n0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_2) ).
fof(f4,axiom,
! [X2,X0,X1] :
( minus(X0,X1) != X2
| plus(X2,X1) = X0
| def_10(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_4) ).
fof(f5,axiom,
! [X2,X0,X1] :
( minus(X0,X1) = X2
| plus(X2,X1) != X0
| def_10(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ def_10(X0,X1)
| ~ gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_6) ).
fof(f7,axiom,
! [X0,X1] :
( ~ def_10(X0,X1)
| X1 != X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_7) ).
fof(f8,plain,
! [X0,X1] :
( ~ def_10(X0,X1)
| X0 != X1 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X0,X1] :
( gt(plus(X0,n1),plus(X1,n1))
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_8) ).
fof(f10,axiom,
! [X0,X1] :
( ~ gt(plus(X0,n1),plus(X1,n1))
| gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_9) ).
fof(f13,axiom,
! [X0,X1] :
( ~ gt(plus(X0,n1),X1)
| gt(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_11) ).
fof(f14,axiom,
! [X0,X1] :
( gt(X0,X1)
| X1 = X0
| gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_12) ).
fof(f15,plain,
! [X0,X1] :
( gt(X1,X0)
| gt(X0,X1)
| X0 = X1 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X2,X0,X1] :
( ~ gt(X1,X2)
| gt(X0,X2)
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_13) ).
fof(f17,axiom,
! [X0,X1] :
( gt(X0,plus(X1,n1))
| plus(X1,n1) = X0
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_14) ).
fof(f18,axiom,
! [X0] :
( X0 = n0
| gt(X0,n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_15) ).
fof(f19,plain,
! [X0] :
( gt(X0,n0)
| n0 = X0 ),
inference(reorient_equations,[],[f18]) ).
fof(f20,axiom,
! [X0] :
( X0 = n0
| X0 = plus(y_27(X0),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_16) ).
fof(f21,plain,
! [X0] :
( plus(y_27(X0),n1) = X0
| n0 = X0 ),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_17) ).
fof(f23,axiom,
! [X0,X1] :
( plus(X0,n1) != plus(X1,n1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_18) ).
fof(f24,axiom,
! [X0] : plus(n0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_19) ).
fof(f25,axiom,
n1 = plus(n0,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_20) ).
fof(f35,axiom,
! [X0] :
( ~ p_Reset(X0)
| wr_level(plus(X0,n1)) = n0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_27) ).
fof(f36,plain,
! [X0] :
( ~ p_Reset(X0)
| n0 = wr_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,axiom,
! [X0] :
( ~ p_Reset(X0)
| rd_level(plus(X0,n1)) = n0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_28) ).
fof(f38,plain,
! [X0] :
( ~ p_Reset(X0)
| n0 = rd_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f37]) ).
fof(f52,axiom,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| ~ gt(fifo_length,int_level(X0))
| ~ gt(minus(fifo_length,n1),wr_level(X0))
| wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_40) ).
fof(f53,axiom,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| ~ gt(fifo_length,int_level(X0))
| gt(minus(fifo_length,n1),wr_level(X0))
| wr_level(plus(X0,n1)) = n0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_41) ).
fof(f54,plain,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| ~ gt(fifo_length,int_level(X0))
| gt(minus(fifo_length,n1),wr_level(X0))
| n0 = wr_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f53]) ).
fof(f56,axiom,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| gt(fifo_length,int_level(X0))
| wr_level(plus(X0,n1)) = wr_level(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_43) ).
fof(f85,axiom,
! [X0] :
( ~ gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| p_Reset(X0)
| wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_67) ).
fof(f86,axiom,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| gt(minus(fifo_length,n1),wr_level(X0))
| wr_level(plus(X0,n1)) = n0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_68) ).
fof(f87,plain,
! [X0] :
( gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| p_Reset(X0)
| n0 = wr_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,axiom,
! [X0] :
( p_Wr(X0)
| p_Reset(X0)
| wr_level(plus(X0,n1)) = wr_level(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_69) ).
fof(f113,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_1) ).
fof(f114,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_2) ).
fof(f115,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_3) ).
fof(f116,plain,
! [X0,X1] :
( def_10(X1,X0)
| plus(minus(X0,X1),X1) = X0 ),
inference(equality_resolution,[],[f4]) ).
fof(f117,plain,
! [X2,X1] :
( def_10(X1,plus(X2,X1))
| minus(plus(X2,X1),X1) = X2 ),
inference(equality_resolution,[],[f5]) ).
fof(f118,plain,
! [X1] : ~ def_10(X1,X1),
inference(equality_resolution,[],[f8]) ).
fof(f119,definition,
sF0 = wr_level(x_139),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f120,plain,
wr_level(x_139) = sF0,
inference(reorient_equations,[],[f119]) ).
fof(f121,definition,
sF1 = plus(sF0,n1),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f122,plain,
plus(sF0,n1) = sF1,
inference(reorient_equations,[],[f121]) ).
fof(f123,plain,
~ gt(sF1,fifo_length),
inference(definition_folding,[],[f113,f122,f120]) ).
fof(f124,definition,
sF2 = plus(x_139,n1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f125,plain,
plus(x_139,n1) = sF2,
inference(reorient_equations,[],[f124]) ).
fof(f126,definition,
sF3 = wr_level(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f127,plain,
wr_level(sF2) = sF3,
inference(reorient_equations,[],[f126]) ).
fof(f128,definition,
sF4 = plus(sF3,n1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f129,plain,
plus(sF3,n1) = sF4,
inference(reorient_equations,[],[f128]) ).
fof(f130,plain,
gt(sF4,fifo_length),
inference(definition_folding,[],[f114,f129,f127,f125]) ).
fof(f150,plain,
! [X0] :
( gt(fifo_length,int_level(X0))
| p_Rd(X0)
| p_Reset(X0)
| wr_level(plus(X0,n1)) = wr_level(X0) ),
inference(forward_subsumption_resolution,[],[f56,f88]) ).
fof(f151,plain,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0))
| gt(minus(fifo_length,n1),wr_level(X0))
| n0 = wr_level(plus(X0,n1)) ),
inference(forward_subsumption_resolution,[],[f54,f87]) ).
fof(f152,plain,
! [X0] :
( ~ gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0))
| p_Reset(X0)
| wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) ),
inference(forward_subsumption_resolution,[],[f52,f85]) ).
fof(f167,plain,
! [X0] :
( gt(minus(fifo_length,n1),wr_level(X0))
| ~ gt(fifo_length,int_level(X0))
| ~ p_Wr(X0)
| n0 = wr_level(plus(X0,n1)) ),
inference(forward_subsumption_resolution,[],[f151,f36]) ).
fof(f173,plain,
gt(n1,n0),
inference(superposition,[],[f2,f24]) ).
fof(f174,plain,
n1 != n0,
inference(superposition,[],[f1,f24]) ).
fof(f178,plain,
n0 != sF1,
inference(superposition,[],[f1,f122]) ).
fof(f180,plain,
n0 != sF2,
inference(superposition,[],[f1,f125]) ).
fof(f208,definition,
( spl5_5
<=> p_Reset(x_139) ),
introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition]) ).
fof(f209,plain,
( p_Reset(x_139)
| ~ spl5_5 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( ~ p_Reset(x_139)
| spl5_5 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f295,definition,
( spl5_18
<=> p_Rd(x_139) ),
introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition]) ).
fof(f296,plain,
( ~ p_Rd(x_139)
| spl5_18 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f297,plain,
( p_Rd(x_139)
| ~ spl5_18 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f309,plain,
( gt(fifo_length,sF1)
| fifo_length = sF1 ),
inference(resolution,[],[f15,f123]) ).
fof(f315,definition,
( spl5_21
<=> fifo_length = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_21])],[avatar_definition]) ).
fof(f317,plain,
( fifo_length = sF1
| ~ spl5_21 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl5_22
<=> gt(fifo_length,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_22])],[avatar_definition]) ).
fof(f321,plain,
( gt(fifo_length,sF1)
| ~ spl5_22 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f323,plain,
( spl5_21
| spl5_22 ),
inference(avatar_split_clause,[],[f309,f319,f315]) ).
fof(f327,plain,
! [X0,X1] :
( ~ gt(X0,X1)
| gt(X0,n0)
| n0 = X1 ),
inference(resolution,[],[f16,f19]) ).
fof(f332,plain,
! [X0] :
( ~ gt(X0,fifo_length)
| gt(X0,n0) ),
inference(resolution,[],[f16,f115]) ).
fof(f347,plain,
! [X0] :
( gt(fifo_length,X0)
| gt(X0,n0)
| fifo_length = X0 ),
inference(resolution,[],[f332,f15]) ).
fof(f361,plain,
! [X0] :
( gt(plus(X0,n1),sF1)
| ~ gt(X0,sF0) ),
inference(superposition,[],[f9,f122]) ).
fof(f371,plain,
! [X0] :
( ~ gt(n1,plus(X0,n1))
| gt(n0,X0) ),
inference(superposition,[],[f10,f24]) ).
fof(f374,plain,
! [X0] :
( ~ gt(sF1,plus(X0,n1))
| gt(sF0,X0) ),
inference(superposition,[],[f10,f122]) ).
fof(f375,plain,
! [X0] :
( ~ gt(sF4,plus(X0,n1))
| gt(sF3,X0) ),
inference(superposition,[],[f10,f129]) ).
fof(f380,plain,
! [X0] :
( ~ gt(plus(X0,n1),sF1)
| gt(X0,sF0) ),
inference(superposition,[],[f10,f122]) ).
fof(f381,plain,
! [X0] :
( ~ gt(plus(X0,n1),sF4)
| gt(X0,sF3) ),
inference(superposition,[],[f10,f129]) ).
fof(f402,definition,
( spl5_25
<=> gt(n0,sF0) ),
introduced(definition,[new_symbols(definition,[spl5_25])],[avatar_definition]) ).
fof(f403,plain,
( gt(n0,sF0)
| ~ spl5_25 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( ~ gt(n0,sF0)
| spl5_25 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f422,plain,
! [X0] :
( plus(X0,n1) != sF4
| sF3 = X0 ),
inference(superposition,[],[f23,f129]) ).
fof(f471,plain,
( ! [X0] :
( ~ gt(X0,fifo_length)
| gt(X0,sF1) )
| ~ spl5_22 ),
inference(resolution,[],[f321,f16]) ).
fof(f473,plain,
! [X0] : plus(minus(X0,X0),X0) = X0,
inference(resolution,[],[f116,f118]) ).
fof(f479,plain,
( gt(sF4,sF1)
| ~ spl5_22 ),
inference(resolution,[],[f471,f130]) ).
fof(f524,plain,
! [X0,X1] :
( gt(X1,plus(X0,n1))
| gt(X0,X1)
| X0 = X1
| plus(X0,n1) = X1 ),
inference(resolution,[],[f13,f15]) ).
fof(f527,plain,
! [X0,X1] :
( gt(y_27(X0),X1)
| ~ gt(X0,X1)
| y_27(X0) = X1
| n0 = X0 ),
inference(superposition,[],[f13,f21]) ).
fof(f530,plain,
! [X0] :
( ~ gt(sF4,X0)
| gt(sF3,X0)
| sF3 = X0 ),
inference(superposition,[],[f13,f129]) ).
fof(f579,plain,
! [X0,X1] :
( ~ gt(plus(X0,X1),X1)
| minus(plus(X0,X1),X1) = X0 ),
inference(resolution,[],[f117,f6]) ).
fof(f580,plain,
! [X0] :
( def_10(X0,X0)
| n0 = minus(X0,X0) ),
inference(superposition,[],[f117,f24]) ).
fof(f581,plain,
( def_10(n1,n1)
| n0 = minus(n1,n1) ),
inference(superposition,[],[f117,f25]) ).
fof(f582,plain,
! [X0] :
( def_10(n1,X0)
| minus(X0,n1) = y_27(X0)
| n0 = X0 ),
inference(superposition,[],[f117,f21]) ).
fof(f583,plain,
( def_10(n1,sF2)
| x_139 = minus(sF2,n1) ),
inference(superposition,[],[f117,f125]) ).
fof(f584,plain,
( def_10(n1,sF1)
| sF0 = minus(sF1,n1) ),
inference(superposition,[],[f117,f122]) ).
fof(f596,definition,
( spl5_41
<=> sF0 = minus(sF1,n1) ),
introduced(definition,[new_symbols(definition,[spl5_41])],[avatar_definition]) ).
fof(f598,plain,
( sF0 = minus(sF1,n1)
| ~ spl5_41 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f600,definition,
( spl5_42
<=> def_10(n1,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_42])],[avatar_definition]) ).
fof(f602,plain,
( def_10(n1,sF1)
| ~ spl5_42 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,plain,
( spl5_41
| spl5_42 ),
inference(avatar_split_clause,[],[f584,f600,f596]) ).
fof(f605,plain,
n0 = minus(n1,n1),
inference(forward_subsumption_resolution,[],[f581,f118]) ).
fof(f606,plain,
! [X0] : n0 = minus(X0,X0),
inference(forward_subsumption_resolution,[],[f580,f118]) ).
fof(f608,definition,
( spl5_43
<=> def_10(n1,sF2) ),
introduced(definition,[new_symbols(definition,[spl5_43])],[avatar_definition]) ).
fof(f609,plain,
( ~ def_10(n1,sF2)
| spl5_43 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( def_10(n1,sF2)
| ~ spl5_43 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f617,definition,
( spl5_45
<=> x_139 = minus(sF2,n1) ),
introduced(definition,[new_symbols(definition,[spl5_45])],[avatar_definition]) ).
fof(f619,plain,
( x_139 = minus(sF2,n1)
| ~ spl5_45 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f620,plain,
( spl5_45
| spl5_43 ),
inference(avatar_split_clause,[],[f583,f608,f617]) ).
fof(f621,plain,
( ~ gt(sF2,n1)
| ~ spl5_43 ),
inference(resolution,[],[f610,f6]) ).
fof(f640,plain,
! [X0] :
( gt(X0,n1)
| n1 = X0
| ~ gt(X0,n0) ),
inference(superposition,[],[f17,f24]) ).
fof(f644,plain,
! [X0] :
( ~ gt(X0,sF3)
| sF4 = X0
| gt(X0,sF4) ),
inference(superposition,[],[f17,f129]) ).
fof(f646,plain,
! [X0] :
( ~ gt(X0,minus(n1,n1))
| gt(X0,n1)
| n1 = X0 ),
inference(forward_demodulation,[],[f640,f605]) ).
fof(f676,definition,
( spl5_51
<=> gt(sF0,minus(n1,n1)) ),
introduced(definition,[new_symbols(definition,[spl5_51])],[avatar_definition]) ).
fof(f677,plain,
( ~ gt(sF0,minus(n1,n1))
| spl5_51 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f678,plain,
( gt(sF0,minus(n1,n1))
| ~ spl5_51 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f742,definition,
( spl5_53
<=> p_Wr(x_139) ),
introduced(definition,[new_symbols(definition,[spl5_53])],[avatar_definition]) ).
fof(f743,plain,
( ~ p_Wr(x_139)
| spl5_53 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f744,plain,
( p_Wr(x_139)
| ~ spl5_53 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f1179,plain,
( gt(minus(fifo_length,n1),sF0)
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| n0 = wr_level(plus(x_139,n1)) ),
inference(superposition,[],[f87,f120]) ).
fof(f1192,definition,
( spl5_70
<=> gt(minus(fifo_length,n1),sF0) ),
introduced(definition,[new_symbols(definition,[spl5_70])],[avatar_definition]) ).
fof(f1193,plain,
( ~ gt(minus(fifo_length,n1),sF0)
| spl5_70 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1194,plain,
( gt(minus(fifo_length,n1),sF0)
| ~ spl5_70 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1196,definition,
( spl5_71
<=> sF3 = minus(n1,n1) ),
introduced(definition,[new_symbols(definition,[spl5_71])],[avatar_definition]) ).
fof(f1197,plain,
( sF3 != minus(n1,n1)
| spl5_71 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1198,plain,
( sF3 = minus(n1,n1)
| ~ spl5_71 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1334,plain,
( gt(minus(fifo_length,n1),sF0)
| ~ gt(fifo_length,int_level(x_139))
| ~ p_Wr(x_139)
| n0 = wr_level(plus(x_139,n1)) ),
inference(superposition,[],[f167,f120]) ).
fof(f1446,definition,
( spl5_72
<=> n1 = sF2 ),
introduced(definition,[new_symbols(definition,[spl5_72])],[avatar_definition]) ).
fof(f1447,plain,
( n1 != sF2
| spl5_72 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1448,plain,
( n1 = sF2
| ~ spl5_72 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1450,definition,
( spl5_73
<=> gt(sF2,n1) ),
introduced(definition,[new_symbols(definition,[spl5_73])],[avatar_definition]) ).
fof(f1451,plain,
( ~ gt(sF2,n1)
| spl5_73 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1711,plain,
( ~ gt(minus(fifo_length,n1),sF0)
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1) ),
inference(superposition,[],[f85,f120]) ).
fof(f1870,plain,
( ~ gt(minus(fifo_length,n1),sF0)
| ~ p_Wr(x_139)
| ~ gt(fifo_length,int_level(x_139))
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1) ),
inference(superposition,[],[f152,f120]) ).
fof(f1974,definition,
( spl5_76
<=> fifo_length = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_76])],[avatar_definition]) ).
fof(f1975,plain,
( fifo_length != sF3
| spl5_76 ),
inference(avatar_component_clause,[],[f1974]) ).
fof(f1976,plain,
( fifo_length = sF3
| ~ spl5_76 ),
inference(avatar_component_clause,[],[f1974]) ).
fof(f2210,definition,
( spl5_78
<=> minus(fifo_length,n1) = sF0 ),
introduced(definition,[new_symbols(definition,[spl5_78])],[avatar_definition]) ).
fof(f2211,plain,
( minus(fifo_length,n1) != sF0
| spl5_78 ),
inference(avatar_component_clause,[],[f2210]) ).
fof(f2212,plain,
( minus(fifo_length,n1) = sF0
| ~ spl5_78 ),
inference(avatar_component_clause,[],[f2210]) ).
fof(f2233,plain,
( gt(sF0,sF0)
| ~ spl5_70
| ~ spl5_78 ),
inference(forward_demodulation,[],[f1194,f2212]) ).
fof(f2243,plain,
( $false
| ~ spl5_70
| ~ spl5_78 ),
inference(forward_subsumption_resolution,[],[f2233,f22]) ).
fof(f2244,plain,
( ~ spl5_70
| ~ spl5_78 ),
inference(avatar_contradiction_clause,[],[f2243]) ).
fof(f2334,definition,
( spl5_84
<=> sF0 = rd_level(sF2) ),
introduced(definition,[new_symbols(definition,[spl5_84])],[avatar_definition]) ).
fof(f2336,plain,
( sF0 = rd_level(sF2)
| ~ spl5_84 ),
inference(avatar_component_clause,[],[f2334]) ).
fof(f2407,definition,
( spl5_86
<=> gt(sF0,n1) ),
introduced(definition,[new_symbols(definition,[spl5_86])],[avatar_definition]) ).
fof(f2408,plain,
( ~ gt(sF0,n1)
| spl5_86 ),
inference(avatar_component_clause,[],[f2407]) ).
fof(f2409,plain,
( gt(sF0,n1)
| ~ spl5_86 ),
inference(avatar_component_clause,[],[f2407]) ).
fof(f2632,plain,
! [X0] : sF2 != minus(X0,X0),
inference(superposition,[],[f180,f606]) ).
fof(f2959,plain,
( gt(n1,sF1)
| ~ gt(minus(n1,n1),sF0) ),
inference(superposition,[],[f361,f473]) ).
fof(f3039,plain,
( ~ gt(n1,sF1)
| gt(n0,sF0) ),
inference(superposition,[],[f371,f122]) ).
fof(f3042,plain,
( ~ gt(n1,sF1)
| spl5_25 ),
inference(forward_subsumption_resolution,[],[f3039,f404]) ).
fof(f3095,plain,
( ~ gt(sF1,n1)
| gt(sF0,minus(n1,n1)) ),
inference(superposition,[],[f374,f473]) ).
fof(f3142,plain,
( ~ gt(sF4,sF1)
| gt(sF3,sF0) ),
inference(superposition,[],[f375,f122]) ).
fof(f3373,plain,
( ~ gt(sF4,sF1)
| gt(sF3,sF0) ),
inference(superposition,[],[f380,f129]) ).
fof(f3404,plain,
( ~ gt(n1,sF4)
| gt(n0,sF3) ),
inference(superposition,[],[f381,f25]) ).
fof(f3479,plain,
( n1 != sF4
| sF3 = minus(n1,n1) ),
inference(superposition,[],[f422,f473]) ).
fof(f3763,plain,
( gt(sF3,fifo_length)
| fifo_length = sF3 ),
inference(resolution,[],[f530,f130]) ).
fof(f3783,plain,
( gt(sF3,fifo_length)
| spl5_76 ),
inference(forward_subsumption_resolution,[],[f3763,f1975]) ).
fof(f3866,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_70 ),
inference(forward_subsumption_resolution,[],[f1711,f1194]) ).
fof(f3927,plain,
( ~ p_Wr(x_139)
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_18
| ~ spl5_70 ),
inference(forward_subsumption_resolution,[],[f3866,f297]) ).
fof(f4169,plain,
( gt(sF3,sF1)
| ~ spl5_22
| spl5_76 ),
inference(resolution,[],[f3783,f471]) ).
fof(f4254,plain,
( gt(sF3,sF0)
| ~ spl5_22 ),
inference(forward_subsumption_resolution,[],[f3142,f479]) ).
fof(f4300,plain,
( p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_subsumption_resolution,[],[f3927,f744]) ).
fof(f4303,definition,
( spl5_127
<=> gt(fifo_length,int_level(x_139)) ),
introduced(definition,[new_symbols(definition,[spl5_127])],[avatar_definition]) ).
fof(f4304,plain,
( gt(fifo_length,int_level(x_139))
| ~ spl5_127 ),
inference(avatar_component_clause,[],[f4303]) ).
fof(f4305,plain,
( ~ gt(fifo_length,int_level(x_139))
| spl5_127 ),
inference(avatar_component_clause,[],[f4303]) ).
fof(f4382,plain,
( wr_level(plus(x_139,n1)) = plus(sF0,n1)
| spl5_5
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_subsumption_resolution,[],[f4300,f210]) ).
fof(f4437,plain,
( wr_level(plus(x_139,n1)) = sF1
| spl5_5
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_demodulation,[],[f4382,f122]) ).
fof(f4457,plain,
( sF1 = wr_level(sF2)
| spl5_5
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_demodulation,[],[f4437,f125]) ).
fof(f4463,plain,
( sF1 = sF3
| spl5_5
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_demodulation,[],[f4457,f127]) ).
fof(f4697,definition,
( spl5_146
<=> sF0 = minus(n1,n1) ),
introduced(definition,[new_symbols(definition,[spl5_146])],[avatar_definition]) ).
fof(f4698,plain,
( sF0 != minus(n1,n1)
| spl5_146 ),
inference(avatar_component_clause,[],[f4697]) ).
fof(f4699,plain,
( sF0 = minus(n1,n1)
| ~ spl5_146 ),
inference(avatar_component_clause,[],[f4697]) ).
fof(f4701,definition,
( spl5_147
<=> n1 = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_147])],[avatar_definition]) ).
fof(f4702,plain,
( n1 = sF1
| ~ spl5_147 ),
inference(avatar_component_clause,[],[f4701]) ).
fof(f4703,plain,
( n1 != sF1
| spl5_147 ),
inference(avatar_component_clause,[],[f4701]) ).
fof(f4768,definition,
( spl5_150
<=> sF1 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_150])],[avatar_definition]) ).
fof(f4769,plain,
( sF1 = sF4
| ~ spl5_150 ),
inference(avatar_component_clause,[],[f4768]) ).
fof(f4798,definition,
( spl5_152
<=> gt(n1,sF4) ),
introduced(definition,[new_symbols(definition,[spl5_152])],[avatar_definition]) ).
fof(f4799,plain,
( ~ gt(n1,sF4)
| spl5_152 ),
inference(avatar_component_clause,[],[f4798]) ).
fof(f4800,plain,
( gt(n1,sF4)
| ~ spl5_152 ),
inference(avatar_component_clause,[],[f4798]) ).
fof(f4802,definition,
( spl5_153
<=> gt(minus(n1,n1),sF2) ),
introduced(definition,[new_symbols(definition,[spl5_153])],[avatar_definition]) ).
fof(f4803,plain,
( gt(minus(n1,n1),sF2)
| ~ spl5_153 ),
inference(avatar_component_clause,[],[f4802]) ).
fof(f4804,plain,
( ~ gt(minus(n1,n1),sF2)
| spl5_153 ),
inference(avatar_component_clause,[],[f4802]) ).
fof(f4940,plain,
( ~ gt(sF1,n1)
| spl5_51 ),
inference(forward_subsumption_resolution,[],[f3095,f677]) ).
fof(f5938,definition,
( spl5_195
<=> gt(minus(n1,n1),sF1) ),
introduced(definition,[new_symbols(definition,[spl5_195])],[avatar_definition]) ).
fof(f5939,plain,
( ~ gt(minus(n1,n1),sF1)
| spl5_195 ),
inference(avatar_component_clause,[],[f5938]) ).
fof(f5940,plain,
( gt(minus(n1,n1),sF1)
| ~ spl5_195 ),
inference(avatar_component_clause,[],[f5938]) ).
fof(f6003,plain,
( gt(n1,sF1)
| n1 = sF1
| spl5_51 ),
inference(resolution,[],[f4940,f15]) ).
fof(f6006,plain,
( n1 = sF1
| spl5_25
| spl5_51 ),
inference(forward_subsumption_resolution,[],[f6003,f3042]) ).
fof(f6009,plain,
( $false
| spl5_25
| spl5_51
| spl5_147 ),
inference(forward_subsumption_resolution,[],[f6006,f4703]) ).
fof(f6010,plain,
( spl5_25
| spl5_51
| spl5_147 ),
inference(avatar_contradiction_clause,[],[f6009]) ).
fof(f6637,plain,
( def_10(sF2,sF2)
| ~ spl5_43
| ~ spl5_72 ),
inference(superposition,[],[f610,f1448]) ).
fof(f6652,plain,
( $false
| ~ spl5_43
| ~ spl5_72 ),
inference(forward_subsumption_resolution,[],[f6637,f118]) ).
fof(f6653,plain,
( ~ spl5_43
| ~ spl5_72 ),
inference(avatar_contradiction_clause,[],[f6652]) ).
fof(f6994,definition,
( spl5_209
<=> gt(minus(n1,n1),sF0) ),
introduced(definition,[new_symbols(definition,[spl5_209])],[avatar_definition]) ).
fof(f6996,plain,
( ~ gt(minus(n1,n1),sF0)
| spl5_209 ),
inference(avatar_component_clause,[],[f6994]) ).
fof(f6998,definition,
( spl5_210
<=> gt(n1,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_210])],[avatar_definition]) ).
fof(f7000,plain,
( gt(n1,sF1)
| ~ spl5_210 ),
inference(avatar_component_clause,[],[f6998]) ).
fof(f7001,plain,
( ~ spl5_209
| spl5_210 ),
inference(avatar_split_clause,[],[f2959,f6998,f6994]) ).
fof(f7377,plain,
( sF2 = plus(minus(sF2,n1),n1)
| spl5_43 ),
inference(resolution,[],[f609,f116]) ).
fof(f7454,plain,
( ~ gt(fifo_length,int_level(minus(sF2,n1)))
| ~ spl5_45
| spl5_127 ),
inference(forward_demodulation,[],[f4305,f619]) ).
fof(f7688,plain,
( sF0 = wr_level(minus(sF2,n1))
| ~ spl5_45 ),
inference(superposition,[],[f120,f619]) ).
fof(f7690,plain,
( ~ p_Reset(minus(sF2,n1))
| spl5_5
| ~ spl5_45 ),
inference(superposition,[],[f210,f619]) ).
fof(f7691,plain,
( ~ p_Rd(minus(sF2,n1))
| spl5_18
| ~ spl5_45 ),
inference(superposition,[],[f296,f619]) ).
fof(f7697,plain,
( p_Wr(minus(sF2,n1))
| ~ spl5_45
| ~ spl5_53 ),
inference(superposition,[],[f744,f619]) ).
fof(f7723,plain,
( p_Rd(minus(sF2,n1))
| p_Reset(minus(sF2,n1))
| wr_level(minus(sF2,n1)) = wr_level(plus(minus(sF2,n1),n1))
| ~ spl5_45
| spl5_127 ),
inference(resolution,[],[f7454,f150]) ).
fof(f7789,plain,
( ~ p_Wr(minus(sF2,n1))
| ~ spl5_45
| spl5_53 ),
inference(forward_demodulation,[],[f743,f619]) ).
fof(f7890,plain,
( p_Reset(minus(sF2,n1))
| ~ spl5_5
| ~ spl5_45 ),
inference(forward_demodulation,[],[f209,f619]) ).
fof(f8725,plain,
( gt(fifo_length,n1)
| n1 = fifo_length
| gt(minus(n1,n1),n0)
| fifo_length = minus(n1,n1) ),
inference(resolution,[],[f646,f347]) ).
fof(f8744,plain,
( gt(sF0,n0)
| n1 = n0
| ~ spl5_86 ),
inference(resolution,[],[f2409,f327]) ).
fof(f8746,plain,
( gt(sF0,n0)
| ~ spl5_86 ),
inference(forward_subsumption_resolution,[],[f8744,f174]) ).
fof(f8747,plain,
( gt(sF0,minus(n1,n1))
| ~ spl5_86 ),
inference(forward_demodulation,[],[f8746,f605]) ).
fof(f8748,plain,
( $false
| spl5_51
| ~ spl5_86 ),
inference(forward_subsumption_resolution,[],[f8747,f677]) ).
fof(f8749,plain,
( spl5_51
| ~ spl5_86 ),
inference(avatar_contradiction_clause,[],[f8748]) ).
fof(f8756,plain,
( p_Reset(minus(sF2,n1))
| wr_level(minus(sF2,n1)) = wr_level(plus(minus(sF2,n1),n1))
| spl5_18
| ~ spl5_45
| spl5_127 ),
inference(forward_subsumption_resolution,[],[f7723,f7691]) ).
fof(f8800,plain,
( p_Reset(minus(sF2,n1))
| wr_level(minus(sF2,n1)) = wr_level(plus(minus(sF2,n1),n1))
| ~ spl5_45
| spl5_53 ),
inference(resolution,[],[f7789,f88]) ).
fof(f8801,plain,
( n0 = rd_level(plus(minus(sF2,n1),n1))
| ~ spl5_5
| ~ spl5_45 ),
inference(resolution,[],[f7890,f38]) ).
fof(f8802,plain,
( n0 = wr_level(plus(minus(sF2,n1),n1))
| ~ spl5_5
| ~ spl5_45 ),
inference(resolution,[],[f7890,f36]) ).
fof(f8805,plain,
( n0 = wr_level(sF2)
| ~ spl5_5
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f8802,f7377]) ).
fof(f8806,plain,
( n0 = rd_level(sF2)
| ~ spl5_5
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f8801,f7377]) ).
fof(f8808,plain,
( n0 = sF3
| ~ spl5_5
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f8805,f127]) ).
fof(f8817,plain,
( wr_level(minus(sF2,n1)) = wr_level(plus(minus(sF2,n1),n1))
| spl5_5
| spl5_18
| ~ spl5_45
| spl5_127 ),
inference(forward_subsumption_resolution,[],[f8756,f7690]) ).
fof(f8822,plain,
( wr_level(minus(sF2,n1)) = wr_level(plus(minus(sF2,n1),n1))
| spl5_5
| ~ spl5_45
| spl5_53 ),
inference(forward_subsumption_resolution,[],[f8800,f7690]) ).
fof(f8826,plain,
( wr_level(sF2) = wr_level(minus(sF2,n1))
| spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(forward_demodulation,[],[f8817,f7377]) ).
fof(f8831,plain,
( wr_level(sF2) = wr_level(minus(sF2,n1))
| spl5_5
| spl5_43
| ~ spl5_45
| spl5_53 ),
inference(forward_demodulation,[],[f8822,f7377]) ).
fof(f8834,plain,
( sF0 = wr_level(sF2)
| spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(forward_demodulation,[],[f8826,f7688]) ).
fof(f8837,plain,
( sF0 = wr_level(sF2)
| spl5_5
| spl5_43
| ~ spl5_45
| spl5_53 ),
inference(forward_demodulation,[],[f8831,f7688]) ).
fof(f8855,plain,
( sF0 = sF3
| spl5_5
| spl5_43
| ~ spl5_45
| spl5_53 ),
inference(superposition,[],[f127,f8837]) ).
fof(f8958,plain,
( sF0 = sF3
| spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(superposition,[],[f127,f8834]) ).
fof(f9001,plain,
( gt(sF0,sF0)
| ~ spl5_51
| ~ spl5_146 ),
inference(forward_demodulation,[],[f678,f4699]) ).
fof(f9034,plain,
( $false
| ~ spl5_51
| ~ spl5_146 ),
inference(forward_subsumption_resolution,[],[f9001,f22]) ).
fof(f9035,plain,
( ~ spl5_51
| ~ spl5_146 ),
inference(avatar_contradiction_clause,[],[f9034]) ).
fof(f9150,plain,
( plus(sF0,n1) = sF4
| spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(superposition,[],[f129,f8958]) ).
fof(f9164,plain,
( sF1 = sF4
| spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(forward_demodulation,[],[f9150,f122]) ).
fof(f9170,plain,
( p_Rd(minus(sF2,n1))
| ~ spl5_18
| ~ spl5_45 ),
inference(forward_demodulation,[],[f297,f619]) ).
fof(f9205,plain,
( plus(sF0,n1) = sF4
| spl5_5
| spl5_43
| ~ spl5_45
| spl5_53 ),
inference(superposition,[],[f129,f8855]) ).
fof(f9219,plain,
( sF1 = sF4
| spl5_5
| spl5_43
| ~ spl5_45
| spl5_53 ),
inference(forward_demodulation,[],[f9205,f122]) ).
fof(f9240,plain,
( gt(minus(fifo_length,n1),sF0)
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1)) ),
inference(forward_subsumption_resolution,[],[f1179,f36]) ).
fof(f9341,plain,
( spl5_150
| spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(avatar_split_clause,[],[f9164,f4303,f617,f608,f295,f208,f4768]) ).
fof(f9605,plain,
( gt(sF1,fifo_length)
| ~ spl5_150 ),
inference(superposition,[],[f130,f4769]) ).
fof(f9664,plain,
( $false
| ~ spl5_150 ),
inference(forward_subsumption_resolution,[],[f9605,f123]) ).
fof(f9665,plain,
~ spl5_150,
inference(avatar_contradiction_clause,[],[f9664]) ).
fof(f9685,plain,
( spl5_150
| spl5_5
| spl5_43
| ~ spl5_45
| spl5_53 ),
inference(avatar_split_clause,[],[f9219,f742,f617,f608,f208,f4768]) ).
fof(f10941,plain,
( ~ gt(sF1,n1)
| sF0 = minus(sF1,n1) ),
inference(superposition,[],[f579,f122]) ).
fof(f11058,plain,
( minus(sF2,n1) = y_27(sF2)
| n0 = sF2
| spl5_43 ),
inference(resolution,[],[f582,f609]) ).
fof(f11059,plain,
( minus(n1,n1) = y_27(n1)
| n1 = n0 ),
inference(resolution,[],[f582,f118]) ).
fof(f11062,plain,
minus(n1,n1) = y_27(n1),
inference(forward_subsumption_resolution,[],[f11059,f174]) ).
fof(f11063,plain,
( minus(sF2,n1) = y_27(sF2)
| spl5_43 ),
inference(forward_subsumption_resolution,[],[f11058,f180]) ).
fof(f11443,plain,
( gt(minus(n1,n1),n0)
| n0 = sF1
| ~ spl5_195 ),
inference(resolution,[],[f5940,f327]) ).
fof(f11449,plain,
( gt(minus(n1,n1),n0)
| ~ spl5_195 ),
inference(forward_subsumption_resolution,[],[f11443,f178]) ).
fof(f11453,plain,
( gt(minus(n1,n1),minus(n1,n1))
| ~ spl5_195 ),
inference(forward_demodulation,[],[f11449,f605]) ).
fof(f11456,plain,
( $false
| ~ spl5_195 ),
inference(forward_subsumption_resolution,[],[f11453,f22]) ).
fof(f11457,plain,
~ spl5_195,
inference(avatar_contradiction_clause,[],[f11456]) ).
fof(f11511,plain,
( gt(sF2,plus(minus(n1,n1),n1))
| sF2 = minus(n1,n1)
| sF2 = plus(minus(n1,n1),n1)
| spl5_153 ),
inference(resolution,[],[f524,f4804]) ).
fof(f11564,plain,
( gt(sF2,plus(minus(n1,n1),n1))
| sF2 = plus(minus(n1,n1),n1)
| spl5_153 ),
inference(forward_subsumption_resolution,[],[f11511,f2632]) ).
fof(f11617,plain,
( gt(sF2,n1)
| sF2 = plus(minus(n1,n1),n1)
| spl5_153 ),
inference(forward_demodulation,[],[f11564,f473]) ).
fof(f12425,plain,
( gt(fifo_length,int_level(minus(sF2,n1)))
| ~ spl5_45
| ~ spl5_127 ),
inference(forward_demodulation,[],[f4304,f619]) ).
fof(f12497,plain,
( gt(minus(n1,n1),minus(n1,n1))
| gt(fifo_length,n1)
| n1 = fifo_length
| fifo_length = minus(n1,n1) ),
inference(forward_demodulation,[],[f8725,f605]) ).
fof(f12499,definition,
( spl5_304
<=> n1 = fifo_length ),
introduced(definition,[new_symbols(definition,[spl5_304])],[avatar_definition]) ).
fof(f12501,plain,
( n1 = fifo_length
| ~ spl5_304 ),
inference(avatar_component_clause,[],[f12499]) ).
fof(f12503,definition,
( spl5_305
<=> gt(fifo_length,n1) ),
introduced(definition,[new_symbols(definition,[spl5_305])],[avatar_definition]) ).
fof(f12507,plain,
( ~ gt(fifo_length,int_level(minus(sF2,n1)))
| gt(minus(fifo_length,n1),sF0)
| ~ p_Wr(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl5_45 ),
inference(forward_demodulation,[],[f1334,f619]) ).
fof(f12508,plain,
( ~ p_Wr(minus(sF2,n1))
| ~ gt(minus(fifo_length,n1),sF0)
| ~ gt(fifo_length,int_level(x_139))
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_45 ),
inference(forward_demodulation,[],[f1870,f619]) ).
fof(f12511,plain,
( ~ p_Wr(minus(sF2,n1))
| gt(minus(fifo_length,n1),sF0)
| ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl5_45 ),
inference(forward_demodulation,[],[f9240,f619]) ).
fof(f12565,plain,
( ~ gt(sF4,fifo_length)
| gt(sF3,sF0)
| ~ spl5_21 ),
inference(forward_demodulation,[],[f3373,f317]) ).
fof(f12576,plain,
( minus(fifo_length,n1) = sF0
| ~ spl5_21
| ~ spl5_41 ),
inference(forward_demodulation,[],[f598,f317]) ).
fof(f12600,plain,
( ~ gt(fifo_length,n1)
| sF0 = minus(sF1,n1)
| ~ spl5_21 ),
inference(forward_demodulation,[],[f10941,f317]) ).
fof(f12614,plain,
( gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_127 ),
inference(forward_demodulation,[],[f12425,f11063]) ).
fof(f12641,plain,
( gt(fifo_length,n1)
| n1 = fifo_length
| fifo_length = minus(n1,n1) ),
inference(forward_subsumption_resolution,[],[f12497,f22]) ).
fof(f12642,plain,
( ~ gt(minus(fifo_length,n1),sF0)
| ~ gt(fifo_length,int_level(x_139))
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_45
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f12508,f7697]) ).
fof(f12690,plain,
( gt(sF3,sF0)
| ~ spl5_21 ),
inference(forward_subsumption_resolution,[],[f12565,f130]) ).
fof(f12704,plain,
( minus(fifo_length,n1) = sF0
| ~ gt(fifo_length,n1)
| ~ spl5_21 ),
inference(forward_demodulation,[],[f12600,f317]) ).
fof(f12733,plain,
( fifo_length = y_27(n1)
| gt(fifo_length,n1)
| n1 = fifo_length ),
inference(forward_demodulation,[],[f12641,f11062]) ).
fof(f12734,plain,
( ~ gt(fifo_length,int_level(x_139))
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_subsumption_resolution,[],[f12642,f1194]) ).
fof(f12768,plain,
( ~ gt(fifo_length,n1)
| ~ spl5_21
| spl5_78 ),
inference(forward_subsumption_resolution,[],[f12704,f2211]) ).
fof(f12790,plain,
( ~ gt(fifo_length,int_level(minus(sF2,n1)))
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_demodulation,[],[f12734,f619]) ).
fof(f12797,plain,
( ~ spl5_305
| ~ spl5_21
| spl5_78 ),
inference(avatar_split_clause,[],[f12768,f2210,f315,f12503]) ).
fof(f12804,plain,
( ~ gt(fifo_length,int_level(y_27(sF2)))
| p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70 ),
inference(forward_demodulation,[],[f12790,f11063]) ).
fof(f12823,plain,
( p_Reset(x_139)
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(forward_subsumption_resolution,[],[f12804,f12614]) ).
fof(f12824,plain,
( p_Reset(minus(sF2,n1))
| wr_level(plus(x_139,n1)) = plus(sF0,n1)
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(forward_demodulation,[],[f12823,f619]) ).
fof(f12825,plain,
( wr_level(plus(x_139,n1)) = plus(sF0,n1)
| spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(forward_subsumption_resolution,[],[f12824,f7690]) ).
fof(f12826,plain,
( wr_level(plus(x_139,n1)) = sF1
| spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(forward_demodulation,[],[f12825,f122]) ).
fof(f12961,plain,
( ~ gt(y_27(n1),sF1)
| spl5_195 ),
inference(forward_demodulation,[],[f5939,f11062]) ).
fof(f12962,plain,
( sF1 = wr_level(sF2)
| spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(forward_demodulation,[],[f12826,f125]) ).
fof(f12978,plain,
( sF1 = sF3
| spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(forward_demodulation,[],[f12962,f127]) ).
fof(f12985,plain,
( p_Rd(y_27(sF2))
| ~ spl5_18
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f9170,f11063]) ).
fof(f13003,plain,
( ~ gt(fifo_length,int_level(y_27(sF2)))
| gt(minus(fifo_length,n1),sF0)
| ~ p_Wr(x_139)
| n0 = wr_level(plus(x_139,n1))
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f12507,f11063]) ).
fof(f13004,plain,
( gt(minus(fifo_length,n1),sF0)
| ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl5_45
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f12511,f7697]) ).
fof(f13084,plain,
( ~ gt(fifo_length,int_level(y_27(sF2)))
| ~ p_Wr(x_139)
| n0 = wr_level(plus(x_139,n1))
| spl5_43
| ~ spl5_45
| spl5_70 ),
inference(forward_subsumption_resolution,[],[f13003,f1193]) ).
fof(f13085,plain,
( ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_subsumption_resolution,[],[f13004,f1193]) ).
fof(f13087,definition,
( spl5_329
<=> fifo_length = y_27(n1) ),
introduced(definition,[new_symbols(definition,[spl5_329])],[avatar_definition]) ).
fof(f13092,plain,
( ~ p_Wr(minus(sF2,n1))
| ~ gt(fifo_length,int_level(y_27(sF2)))
| n0 = wr_level(plus(x_139,n1))
| spl5_43
| ~ spl5_45
| spl5_70 ),
inference(forward_demodulation,[],[f13084,f619]) ).
fof(f13093,plain,
( ~ p_Rd(minus(sF2,n1))
| n0 = wr_level(plus(x_139,n1))
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13085,f619]) ).
fof(f13094,plain,
( ~ gt(fifo_length,int_level(y_27(sF2)))
| n0 = wr_level(plus(x_139,n1))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_subsumption_resolution,[],[f13092,f7697]) ).
fof(f13095,plain,
( ~ p_Rd(y_27(sF2))
| n0 = wr_level(plus(x_139,n1))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13093,f11063]) ).
fof(f13096,plain,
( n0 = wr_level(sF2)
| ~ gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13094,f125]) ).
fof(f13097,plain,
( n0 = wr_level(plus(x_139,n1))
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_subsumption_resolution,[],[f13095,f12985]) ).
fof(f13098,plain,
( n0 = sF3
| ~ gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13096,f127]) ).
fof(f13099,plain,
( n0 = wr_level(sF2)
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13097,f125]) ).
fof(f13101,plain,
( n0 = sF3
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13099,f127]) ).
fof(f13141,definition,
( spl5_332
<=> gt(sF3,sF0) ),
introduced(definition,[new_symbols(definition,[spl5_332])],[avatar_definition]) ).
fof(f13142,plain,
( ~ gt(sF3,sF0)
| spl5_332 ),
inference(avatar_component_clause,[],[f13141]) ).
fof(f13143,plain,
( gt(sF3,sF0)
| ~ spl5_332 ),
inference(avatar_component_clause,[],[f13141]) ).
fof(f13151,plain,
( sF3 = y_27(n1)
| n1 != sF4 ),
inference(forward_demodulation,[],[f3479,f11062]) ).
fof(f13152,plain,
( sF3 != y_27(n1)
| spl5_71 ),
inference(forward_demodulation,[],[f1197,f11062]) ).
fof(f13212,plain,
( spl5_332
| ~ spl5_22 ),
inference(avatar_split_clause,[],[f4254,f319,f13141]) ).
fof(f13225,definition,
( spl5_339
<=> n1 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_339])],[avatar_definition]) ).
fof(f13229,definition,
( spl5_340
<=> sF3 = y_27(n1) ),
introduced(definition,[new_symbols(definition,[spl5_340])],[avatar_definition]) ).
fof(f13230,plain,
( sF3 != y_27(n1)
| spl5_340 ),
inference(avatar_component_clause,[],[f13229]) ).
fof(f13231,plain,
( sF3 = y_27(n1)
| ~ spl5_340 ),
inference(avatar_component_clause,[],[f13229]) ).
fof(f13232,plain,
( ~ spl5_339
| spl5_340 ),
inference(avatar_split_clause,[],[f13151,f13229,f13225]) ).
fof(f13233,plain,
( ~ spl5_340
| spl5_71 ),
inference(avatar_split_clause,[],[f13152,f1196,f13229]) ).
fof(f13394,plain,
( gt(n1,sF3)
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(superposition,[],[f173,f13101]) ).
fof(f13405,plain,
( ! [X0] : sF3 = minus(X0,X0)
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(superposition,[],[f606,f13101]) ).
fof(f13630,plain,
( n1 = sF4
| gt(n1,sF4)
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(resolution,[],[f13394,f644]) ).
fof(f13636,plain,
( n1 = sF4
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| spl5_152 ),
inference(forward_subsumption_resolution,[],[f13630,f4799]) ).
fof(f13637,plain,
( spl5_339
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| spl5_152 ),
inference(avatar_split_clause,[],[f13636,f4798,f1192,f742,f617,f608,f295,f13225]) ).
fof(f13679,plain,
( gt(n0,sF3)
| ~ spl5_152 ),
inference(forward_subsumption_resolution,[],[f3404,f4800]) ).
fof(f13690,plain,
( gt(minus(n1,n1),sF3)
| ~ spl5_152 ),
inference(forward_demodulation,[],[f13679,f605]) ).
fof(f13702,plain,
( gt(sF3,sF3)
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_152 ),
inference(forward_demodulation,[],[f13690,f13405]) ).
fof(f13709,plain,
( $false
| ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_152 ),
inference(forward_subsumption_resolution,[],[f13702,f22]) ).
fof(f13710,plain,
( ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_152 ),
inference(avatar_contradiction_clause,[],[f13709]) ).
fof(f13915,plain,
( sF3 = minus(n1,n1)
| ~ gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13098,f605]) ).
fof(f13945,plain,
( sF3 = y_27(n1)
| ~ gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70 ),
inference(forward_demodulation,[],[f13915,f11062]) ).
fof(f13956,plain,
( ~ gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| spl5_340 ),
inference(forward_subsumption_resolution,[],[f13945,f13230]) ).
fof(f14091,definition,
( spl5_364
<=> sF1 = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_364])],[avatar_definition]) ).
fof(f14093,plain,
( sF1 = sF3
| ~ spl5_364 ),
inference(avatar_component_clause,[],[f14091]) ).
fof(f14095,definition,
( spl5_365
<=> gt(sF3,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_365])],[avatar_definition]) ).
fof(f14096,plain,
( ~ gt(sF3,sF1)
| spl5_365 ),
inference(avatar_component_clause,[],[f14095]) ).
fof(f14097,plain,
( gt(sF3,sF1)
| ~ spl5_365 ),
inference(avatar_component_clause,[],[f14095]) ).
fof(f16499,plain,
( ~ gt(n1,sF1)
| sF1 = y_27(n1)
| n1 = n0
| spl5_195 ),
inference(resolution,[],[f12961,f527]) ).
fof(f16500,plain,
( sF1 = y_27(n1)
| n1 = n0
| spl5_195
| ~ spl5_210 ),
inference(forward_subsumption_resolution,[],[f16499,f7000]) ).
fof(f16501,plain,
( sF1 = y_27(n1)
| spl5_195
| ~ spl5_210 ),
inference(forward_subsumption_resolution,[],[f16500,f174]) ).
fof(f16502,plain,
( sF1 = sF3
| spl5_195
| ~ spl5_210
| ~ spl5_340 ),
inference(forward_demodulation,[],[f16501,f13231]) ).
fof(f16744,plain,
( spl5_364
| spl5_195
| ~ spl5_210
| ~ spl5_340 ),
inference(avatar_split_clause,[],[f16502,f13229,f6998,f5938,f14091]) ).
fof(f17308,plain,
( n0 != sF3
| ~ spl5_364 ),
inference(superposition,[],[f178,f14093]) ).
fof(f17312,plain,
( gt(fifo_length,sF3)
| ~ spl5_22
| ~ spl5_364 ),
inference(superposition,[],[f321,f14093]) ).
fof(f17329,plain,
( gt(sF3,sF3)
| ~ spl5_364
| ~ spl5_365 ),
inference(superposition,[],[f14097,f14093]) ).
fof(f17331,plain,
( $false
| ~ spl5_364
| ~ spl5_365 ),
inference(forward_subsumption_resolution,[],[f17329,f22]) ).
fof(f17332,plain,
( ~ spl5_364
| ~ spl5_365 ),
inference(avatar_contradiction_clause,[],[f17331]) ).
fof(f17403,plain,
( gt(sF3,sF3)
| ~ spl5_22
| ~ spl5_76
| ~ spl5_364 ),
inference(forward_demodulation,[],[f17312,f1976]) ).
fof(f17404,plain,
( sF3 != minus(n1,n1)
| ~ spl5_364 ),
inference(forward_demodulation,[],[f17308,f605]) ).
fof(f17439,plain,
( $false
| ~ spl5_22
| ~ spl5_76
| ~ spl5_364 ),
inference(forward_subsumption_resolution,[],[f17403,f22]) ).
fof(f17440,plain,
( ~ spl5_22
| ~ spl5_76
| ~ spl5_364 ),
inference(avatar_contradiction_clause,[],[f17439]) ).
fof(f17441,plain,
( $false
| ~ spl5_71
| ~ spl5_364 ),
inference(forward_subsumption_resolution,[],[f17404,f1198]) ).
fof(f17442,plain,
( ~ spl5_71
| ~ spl5_364 ),
inference(avatar_contradiction_clause,[],[f17441]) ).
fof(f17531,plain,
( ~ gt(y_27(n1),sF0)
| spl5_209 ),
inference(forward_demodulation,[],[f6996,f11062]) ).
fof(f17544,plain,
( gt(sF3,n1)
| ~ spl5_147
| ~ spl5_365 ),
inference(forward_demodulation,[],[f14097,f4702]) ).
fof(f17575,plain,
( ~ gt(sF3,sF0)
| spl5_209
| ~ spl5_340 ),
inference(forward_demodulation,[],[f17531,f13231]) ).
fof(f17601,plain,
( $false
| spl5_209
| ~ spl5_332
| ~ spl5_340 ),
inference(forward_subsumption_resolution,[],[f17575,f13143]) ).
fof(f17602,plain,
( spl5_209
| ~ spl5_332
| ~ spl5_340 ),
inference(avatar_contradiction_clause,[],[f17601]) ).
fof(f17652,plain,
( $false
| ~ spl5_21
| spl5_332 ),
inference(forward_subsumption_resolution,[],[f12690,f13142]) ).
fof(f17653,plain,
( ~ spl5_21
| spl5_332 ),
inference(avatar_contradiction_clause,[],[f17652]) ).
fof(f19767,plain,
( sF3 = rd_level(sF2)
| ~ spl5_5
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f8808,f8806]) ).
fof(f20711,plain,
( gt(sF3,n0)
| n0 = sF0
| ~ spl5_332 ),
inference(resolution,[],[f13143,f327]) ).
fof(f20714,plain,
( gt(sF3,minus(n1,n1))
| n0 = sF0
| ~ spl5_332 ),
inference(forward_demodulation,[],[f20711,f605]) ).
fof(f20919,plain,
( gt(fifo_length,rd_level(sF2))
| ~ spl5_5
| spl5_43
| ~ spl5_45 ),
inference(superposition,[],[f115,f8806]) ).
fof(f20936,plain,
( ! [X0] : minus(X0,X0) = rd_level(sF2)
| ~ spl5_5
| spl5_43
| ~ spl5_45 ),
inference(superposition,[],[f606,f8806]) ).
fof(f20943,plain,
( gt(sF3,rd_level(sF2))
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_76 ),
inference(forward_demodulation,[],[f20919,f1976]) ).
fof(f20952,plain,
( gt(rd_level(sF2),rd_level(sF2))
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_76 ),
inference(forward_demodulation,[],[f20943,f19767]) ).
fof(f20960,plain,
( $false
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_76 ),
inference(forward_subsumption_resolution,[],[f20952,f22]) ).
fof(f20961,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_76 ),
inference(avatar_contradiction_clause,[],[f20960]) ).
fof(f20965,plain,
( gt(rd_level(sF2),fifo_length)
| ~ spl5_5
| spl5_43
| ~ spl5_45
| spl5_76 ),
inference(forward_demodulation,[],[f3783,f19767]) ).
fof(f20968,plain,
( ~ gt(rd_level(sF2),sF1)
| ~ spl5_5
| spl5_43
| ~ spl5_45
| spl5_365 ),
inference(forward_demodulation,[],[f14096,f19767]) ).
fof(f20993,plain,
( spl5_78
| ~ spl5_21
| ~ spl5_41 ),
inference(avatar_split_clause,[],[f12576,f596,f315,f2210]) ).
fof(f21018,plain,
( gt(sF3,rd_level(sF2))
| n0 = sF0
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_332 ),
inference(forward_demodulation,[],[f20714,f20936]) ).
fof(f21036,plain,
( ~ gt(rd_level(sF2),fifo_length)
| ~ spl5_5
| ~ spl5_21
| spl5_43
| ~ spl5_45
| spl5_365 ),
inference(forward_demodulation,[],[f20968,f317]) ).
fof(f21067,plain,
( gt(rd_level(sF2),rd_level(sF2))
| n0 = sF0
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_332 ),
inference(forward_demodulation,[],[f21018,f19767]) ).
fof(f21071,plain,
( $false
| ~ spl5_5
| ~ spl5_21
| spl5_43
| ~ spl5_45
| spl5_76
| spl5_365 ),
inference(forward_subsumption_resolution,[],[f21036,f20965]) ).
fof(f21072,plain,
( ~ spl5_5
| ~ spl5_21
| spl5_43
| ~ spl5_45
| spl5_76
| spl5_365 ),
inference(avatar_contradiction_clause,[],[f21071]) ).
fof(f21088,plain,
( n0 = sF0
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_332 ),
inference(forward_subsumption_resolution,[],[f21067,f22]) ).
fof(f21184,plain,
( n0 != fifo_length
| ~ spl5_21 ),
inference(superposition,[],[f178,f317]) ).
fof(f21204,plain,
( fifo_length != minus(n1,n1)
| ~ spl5_21 ),
inference(forward_demodulation,[],[f21184,f605]) ).
fof(f21780,plain,
( ! [X0] : sF0 = minus(X0,X0)
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_332 ),
inference(superposition,[],[f606,f21088]) ).
fof(f21781,plain,
( sF0 = rd_level(sF2)
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_332 ),
inference(superposition,[],[f8806,f21088]) ).
fof(f21782,plain,
( spl5_84
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_332 ),
inference(avatar_split_clause,[],[f21781,f13141,f617,f608,f208,f2334]) ).
fof(f21871,plain,
( gt(rd_level(sF2),n1)
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_147
| ~ spl5_365 ),
inference(forward_demodulation,[],[f17544,f19767]) ).
fof(f21911,plain,
( gt(sF0,n1)
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_84
| ~ spl5_147
| ~ spl5_365 ),
inference(forward_demodulation,[],[f21871,f2336]) ).
fof(f21950,plain,
( $false
| ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_84
| spl5_86
| ~ spl5_147
| ~ spl5_365 ),
inference(forward_subsumption_resolution,[],[f21911,f2408]) ).
fof(f21951,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_84
| spl5_86
| ~ spl5_147
| ~ spl5_365 ),
inference(avatar_contradiction_clause,[],[f21950]) ).
fof(f22026,plain,
( gt(minus(n1,n1),sF0)
| ~ spl5_25 ),
inference(forward_demodulation,[],[f403,f605]) ).
fof(f22032,plain,
( $false
| ~ spl5_5
| spl5_43
| ~ spl5_45
| spl5_146
| ~ spl5_332 ),
inference(forward_subsumption_resolution,[],[f4698,f21780]) ).
fof(f22033,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| spl5_146
| ~ spl5_332 ),
inference(avatar_contradiction_clause,[],[f22032]) ).
fof(f22089,plain,
( gt(rd_level(sF2),sF0)
| ~ spl5_5
| ~ spl5_25
| spl5_43
| ~ spl5_45 ),
inference(forward_demodulation,[],[f22026,f20936]) ).
fof(f22137,plain,
( gt(sF0,sF0)
| ~ spl5_5
| ~ spl5_25
| spl5_43
| ~ spl5_45
| ~ spl5_84 ),
inference(forward_demodulation,[],[f22089,f2336]) ).
fof(f22172,plain,
( $false
| ~ spl5_5
| ~ spl5_25
| spl5_43
| ~ spl5_45
| ~ spl5_84 ),
inference(forward_subsumption_resolution,[],[f22137,f22]) ).
fof(f22173,plain,
( ~ spl5_5
| ~ spl5_25
| spl5_43
| ~ spl5_45
| ~ spl5_84 ),
inference(avatar_contradiction_clause,[],[f22172]) ).
fof(f22403,plain,
( gt(fifo_length,int_level(minus(sF2,n1)))
| ~ spl5_45
| ~ spl5_127 ),
inference(forward_demodulation,[],[f4304,f619]) ).
fof(f22516,plain,
( fifo_length != y_27(n1)
| ~ spl5_21 ),
inference(forward_demodulation,[],[f21204,f11062]) ).
fof(f22643,plain,
( gt(fifo_length,int_level(y_27(sF2)))
| spl5_43
| ~ spl5_45
| ~ spl5_127 ),
inference(forward_demodulation,[],[f22403,f11063]) ).
fof(f22812,plain,
( $false
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_127
| spl5_340 ),
inference(forward_subsumption_resolution,[],[f22643,f13956]) ).
fof(f22813,plain,
( spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_127
| spl5_340 ),
inference(avatar_contradiction_clause,[],[f22812]) ).
fof(f23391,plain,
( def_10(n1,fifo_length)
| ~ spl5_21
| ~ spl5_42 ),
inference(forward_demodulation,[],[f602,f317]) ).
fof(f23393,plain,
( spl5_364
| spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127 ),
inference(avatar_split_clause,[],[f12978,f4303,f1192,f742,f617,f608,f208,f14091]) ).
fof(f23406,plain,
( spl5_304
| spl5_305
| spl5_329 ),
inference(avatar_split_clause,[],[f12733,f13087,f12503,f12499]) ).
fof(f23430,plain,
( ~ spl5_329
| ~ spl5_21 ),
inference(avatar_split_clause,[],[f22516,f315,f13087]) ).
fof(f23561,plain,
( def_10(n1,n1)
| ~ spl5_21
| ~ spl5_42
| ~ spl5_304 ),
inference(forward_demodulation,[],[f23391,f12501]) ).
fof(f23675,plain,
( $false
| ~ spl5_21
| ~ spl5_42
| ~ spl5_304 ),
inference(forward_subsumption_resolution,[],[f23561,f118]) ).
fof(f23676,plain,
( ~ spl5_21
| ~ spl5_42
| ~ spl5_304 ),
inference(avatar_contradiction_clause,[],[f23675]) ).
fof(f23986,plain,
( spl5_365
| ~ spl5_22
| spl5_76 ),
inference(avatar_split_clause,[],[f4169,f1974,f319,f14095]) ).
fof(f24117,plain,
( spl5_364
| spl5_5
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70 ),
inference(avatar_split_clause,[],[f4463,f1192,f742,f295,f208,f14091]) ).
fof(f24268,plain,
( ~ spl5_73
| ~ spl5_43 ),
inference(avatar_split_clause,[],[f621,f608,f1450]) ).
fof(f24276,plain,
( sF2 = plus(minus(n1,n1),n1)
| spl5_73
| spl5_153 ),
inference(forward_subsumption_resolution,[],[f11617,f1451]) ).
fof(f24314,plain,
( n1 = sF2
| spl5_73
| spl5_153 ),
inference(forward_demodulation,[],[f24276,f473]) ).
fof(f24343,plain,
( $false
| spl5_72
| spl5_73
| spl5_153 ),
inference(forward_subsumption_resolution,[],[f24314,f1447]) ).
fof(f24344,plain,
( spl5_72
| spl5_73
| spl5_153 ),
inference(avatar_contradiction_clause,[],[f24343]) ).
fof(f24417,plain,
( gt(y_27(n1),sF2)
| ~ spl5_153 ),
inference(forward_demodulation,[],[f4803,f11062]) ).
fof(f25865,plain,
( gt(y_27(n1),n0)
| n0 = sF2
| ~ spl5_153 ),
inference(resolution,[],[f24417,f327]) ).
fof(f25868,plain,
( gt(y_27(n1),n0)
| ~ spl5_153 ),
inference(forward_subsumption_resolution,[],[f25865,f180]) ).
fof(f25873,plain,
( gt(y_27(n1),minus(n1,n1))
| ~ spl5_153 ),
inference(forward_demodulation,[],[f25868,f605]) ).
fof(f25876,plain,
( gt(y_27(n1),y_27(n1))
| ~ spl5_153 ),
inference(forward_demodulation,[],[f25873,f11062]) ).
fof(f25877,plain,
( $false
| ~ spl5_153 ),
inference(forward_subsumption_resolution,[],[f25876,f22]) ).
fof(f25878,plain,
~ spl5_153,
inference(avatar_contradiction_clause,[],[f25877]) ).
cnf(s15,plain,
( spl5_21
| spl5_22 ),
inference(sat_conversion,[],[f323]) ).
cnf(s31,plain,
( spl5_41
| spl5_42 ),
inference(sat_conversion,[],[f603]) ).
cnf(s33,plain,
( spl5_43
| spl5_45 ),
inference(sat_conversion,[],[f620]) ).
cnf(s68,plain,
( ~ spl5_70
| ~ spl5_78 ),
inference(sat_conversion,[],[f2244]) ).
cnf(s287,plain,
( spl5_25
| spl5_51
| spl5_147 ),
inference(sat_conversion,[],[f6010]) ).
cnf(s314,plain,
( ~ spl5_43
| ~ spl5_72 ),
inference(sat_conversion,[],[f6653]) ).
cnf(s322,plain,
( ~ spl5_209
| spl5_210 ),
inference(sat_conversion,[],[f7001]) ).
cnf(s442,plain,
( spl5_51
| ~ spl5_86 ),
inference(sat_conversion,[],[f8749]) ).
cnf(s469,plain,
( ~ spl5_51
| ~ spl5_146 ),
inference(sat_conversion,[],[f9035]) ).
cnf(s506,plain,
( spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127
| spl5_150 ),
inference(sat_conversion,[],[f9341]) ).
cnf(s544,plain,
~ spl5_150,
inference(sat_conversion,[],[f9665]) ).
cnf(s547,plain,
( spl5_5
| spl5_43
| ~ spl5_45
| spl5_53
| spl5_150 ),
inference(sat_conversion,[],[f9685]) ).
cnf(s632,plain,
~ spl5_195,
inference(sat_conversion,[],[f11457]) ).
cnf(s679,plain,
( ~ spl5_21
| spl5_78
| ~ spl5_305 ),
inference(sat_conversion,[],[f12797]) ).
cnf(s719,plain,
( ~ spl5_22
| spl5_332 ),
inference(sat_conversion,[],[f13212]) ).
cnf(s723,plain,
( ~ spl5_339
| spl5_340 ),
inference(sat_conversion,[],[f13232]) ).
cnf(s724,plain,
( spl5_71
| ~ spl5_340 ),
inference(sat_conversion,[],[f13233]) ).
cnf(s755,plain,
( ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| spl5_152
| spl5_339 ),
inference(sat_conversion,[],[f13637]) ).
cnf(s763,plain,
( ~ spl5_18
| spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_152 ),
inference(sat_conversion,[],[f13710]) ).
cnf(s872,plain,
( spl5_195
| ~ spl5_210
| ~ spl5_340
| spl5_364 ),
inference(sat_conversion,[],[f16744]) ).
cnf(s911,plain,
( ~ spl5_364
| ~ spl5_365 ),
inference(sat_conversion,[],[f17332]) ).
cnf(s921,plain,
( ~ spl5_22
| ~ spl5_76
| ~ spl5_364 ),
inference(sat_conversion,[],[f17440]) ).
cnf(s922,plain,
( ~ spl5_71
| ~ spl5_364 ),
inference(sat_conversion,[],[f17442]) ).
cnf(s946,plain,
( spl5_209
| ~ spl5_332
| ~ spl5_340 ),
inference(sat_conversion,[],[f17602]) ).
cnf(s954,plain,
( ~ spl5_21
| spl5_332 ),
inference(sat_conversion,[],[f17653]) ).
cnf(s1066,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_76 ),
inference(sat_conversion,[],[f20961]) ).
cnf(s1079,plain,
( ~ spl5_21
| ~ spl5_41
| spl5_78 ),
inference(sat_conversion,[],[f20993]) ).
cnf(s1083,plain,
( ~ spl5_5
| ~ spl5_21
| spl5_43
| ~ spl5_45
| spl5_76
| spl5_365 ),
inference(sat_conversion,[],[f21072]) ).
cnf(s1109,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| spl5_84
| ~ spl5_332 ),
inference(sat_conversion,[],[f21782]) ).
cnf(s1126,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_84
| spl5_86
| ~ spl5_147
| ~ spl5_365 ),
inference(sat_conversion,[],[f21951]) ).
cnf(s1133,plain,
( ~ spl5_5
| spl5_43
| ~ spl5_45
| spl5_146
| ~ spl5_332 ),
inference(sat_conversion,[],[f22033]) ).
cnf(s1139,plain,
( ~ spl5_5
| ~ spl5_25
| spl5_43
| ~ spl5_45
| ~ spl5_84 ),
inference(sat_conversion,[],[f22173]) ).
cnf(s1148,plain,
( spl5_43
| ~ spl5_45
| ~ spl5_53
| spl5_70
| ~ spl5_127
| spl5_340 ),
inference(sat_conversion,[],[f22813]) ).
cnf(s1154,plain,
( spl5_5
| spl5_43
| ~ spl5_45
| ~ spl5_53
| ~ spl5_70
| ~ spl5_127
| spl5_364 ),
inference(sat_conversion,[],[f23393]) ).
cnf(s1160,plain,
( spl5_304
| spl5_305
| spl5_329 ),
inference(sat_conversion,[],[f23406]) ).
cnf(s1164,plain,
( ~ spl5_21
| ~ spl5_329 ),
inference(sat_conversion,[],[f23430]) ).
cnf(s1169,plain,
( ~ spl5_21
| ~ spl5_42
| ~ spl5_304 ),
inference(sat_conversion,[],[f23676]) ).
cnf(s1178,plain,
( ~ spl5_22
| spl5_76
| spl5_365 ),
inference(sat_conversion,[],[f23986]) ).
cnf(s1201,plain,
( spl5_5
| ~ spl5_18
| ~ spl5_53
| ~ spl5_70
| spl5_364 ),
inference(sat_conversion,[],[f24117]) ).
cnf(s1215,plain,
( ~ spl5_43
| ~ spl5_73 ),
inference(sat_conversion,[],[f24268]) ).
cnf(s1221,plain,
( spl5_72
| spl5_73
| spl5_153 ),
inference(sat_conversion,[],[f24344]) ).
cnf(s1320,plain,
~ spl5_153,
inference(sat_conversion,[],[f25878]) ).
cnf(s1321,plain,
( spl5_72
| spl5_73 ),
inference(rat,[],[s1221,s1320]) ).
cnf(s1322,plain,
( spl5_5
| spl5_18
| spl5_43
| ~ spl5_45
| spl5_127 ),
inference(rat,[],[s506,s544]) ).
cnf(s1340,plain,
( spl5_43
| spl5_70
| spl5_340
| spl5_18
| spl5_5 ),
inference(rat,[],[s1148,s1322,s547,s33,s544]) ).
cnf(s1341,plain,
~ spl5_43,
inference(rat,[],[s1321,s314,s1215]) ).
cnf(s1342,plain,
spl5_45,
inference(rat,[],[s33,s1341]) ).
cnf(s1344,plain,
( ~ spl5_364
| ~ spl5_22 ),
inference(rat,[],[s1178,s921,s911]) ).
cnf(s1345,plain,
( ~ spl5_22
| spl5_18
| spl5_5 ),
inference(rat,[],[s322,s946,s872,s1340,s1154,s1344,s719,s547,s1322,s632,s1341,s1342,s544]) ).
cnf(s1346,plain,
( ~ spl5_340
| ~ spl5_332 ),
inference(rat,[],[s872,s322,s922,s946,s724,s632]) ).
cnf(s1347,plain,
( spl5_18
| spl5_5 ),
inference(rat,[],[s1169,s31,s1160,s1079,s679,s68,s1340,s1346,s954,s1164,s15,s1345,s1341]) ).
cnf(s1348,plain,
( ~ spl5_22
| spl5_5 ),
inference(rat,[],[s755,s763,s723,s1201,s1346,s1344,s719,s547,s1347,s1341,s1342,s544]) ).
cnf(s1349,plain,
( spl5_70
| spl5_5 ),
inference(rat,[],[s755,s763,s547,s1347,s723,s1346,s954,s15,s1348,s1341,s1342,s544]) ).
cnf(s1350,plain,
spl5_5,
inference(rat,[],[s1169,s31,s1160,s1079,s679,s68,s1349,s1164,s15,s1348]) ).
cnf(s1353,plain,
~ spl5_76,
inference(rat,[],[s1066,s1342,s1341,s1350]) ).
cnf(s1358,plain,
~ spl5_22,
inference(rat,[],[s1126,s287,s442,s469,s1139,s1133,s1109,s1178,s719,s1341,s1342,s1350,s1353]) ).
cnf(s1359,plain,
spl5_21,
inference(rat,[],[s15,s1358]) ).
cnf(s1362,plain,
spl5_332,
inference(rat,[],[s954,s1359]) ).
cnf(s1364,plain,
spl5_365,
inference(rat,[],[s1083,s1353,s1342,s1341,s1350,s1359]) ).
cnf(s1369,plain,
spl5_84,
inference(rat,[],[s1109,s1350,s1342,s1341,s1362]) ).
cnf(s1370,plain,
spl5_146,
inference(rat,[],[s1133,s1350,s1342,s1341,s1362]) ).
cnf(s1373,plain,
~ spl5_25,
inference(rat,[],[s1139,s1342,s1341,s1350,s1369]) ).
cnf(s1374,plain,
~ spl5_51,
inference(rat,[],[s469,s1370]) ).
cnf(s1381,plain,
~ spl5_86,
inference(rat,[],[s442,s1374]) ).
cnf(s1382,plain,
spl5_147,
inference(rat,[],[s287,s1373,s1374]) ).
cnf(s1387,plain,
$false,
inference(rat,[],[s1126,s1364,s1369,s1350,s1342,s1341,s1382,s1381]) ).
fof(f25879,plain,
$false,
inference(avatar_sat_refutation,[],[s1387]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV031-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:59:07 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.91/1.39 % (48899)Will run a generic schedule for satisfiability detection.
% 5.91/1.39 % (48908)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=506341956:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.91/1.39 % (48905)% WARNING: option uhcvi not known.
% 5.91/1.39 % (48904)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3818441801_2999 on theBenchmark for (2999ds/0Mi)
% 5.91/1.39 % (48905)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3898453929:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.91/1.39 % (48906)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1447921420:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.91/1.39 % (48907)dis+10_1_sil=32000:sp=arity:random_seed=3772540899:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.91/1.39 % (48910)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3020533611:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.91/1.39 % (48909)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2080225250:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.91/1.39 % TRYING [1]
% 5.91/1.39 % TRYING [2]
% 5.91/1.39 % TRYING [3]
% 5.91/1.39 % TRYING [4]
% 5.91/1.39 % TRYING [5]
% 5.91/1.39 % (48908)Instruction limit reached!
% 5.91/1.39 % (48908)------------------------------
% 5.91/1.39 % (48908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48908)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48908)Termination reason: Instruction limit
% 5.91/1.39 % (48908)Termination phase: Saturation
% 5.91/1.39 % (48908)Time elapsed: 0.041 s
% 5.91/1.39 % (48908)Peak memory usage: 12 MB
% 5.91/1.39 % (48908)Instructions burned: 119 (million)
% 5.91/1.39 % (48918)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2453735037:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.91/1.39 % TRYING [1]
% 5.91/1.39 % TRYING [2]
% 5.91/1.39 % TRYING [3]
% 5.91/1.39 % TRYING [6]
% 5.91/1.39 % TRYING [4]
% 5.91/1.39 % TRYING [5]
% 5.91/1.39 % (48907)Instruction limit reached!
% 5.91/1.39 % (48907)------------------------------
% 5.91/1.39 % (48907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48907)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48907)Termination reason: Instruction limit
% 5.91/1.39 % (48907)Termination phase: Saturation
% 5.91/1.39 % (48907)Time elapsed: 0.073 s
% 5.91/1.39 % (48907)Peak memory usage: 12 MB
% 5.91/1.39 % (48907)Instructions burned: 109 (million)
% 5.91/1.39 % (48909)Instruction limit reached!
% 5.91/1.39 % (48909)------------------------------
% 5.91/1.39 % (48909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48909)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48909)Termination reason: Instruction limit
% 5.91/1.39 % (48909)Termination phase: Saturation
% 5.91/1.39 % (48909)Time elapsed: 0.079 s
% 5.91/1.39 % (48909)Peak memory usage: 12 MB
% 5.91/1.39 % (48909)Instructions burned: 132 (million)
% 5.91/1.39 % TRYING [6]
% 5.91/1.39 % TRYING [7]
% 5.91/1.39 % (48920)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3973605985:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.91/1.39 % (48921)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=2150560532:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.91/1.39 % (48910)Instruction limit reached!
% 5.91/1.39 % (48910)------------------------------
% 5.91/1.39 % (48910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48910)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48910)Termination reason: Instruction limit
% 5.91/1.39 % (48910)Termination phase: Saturation
% 5.91/1.39 % (48910)Time elapsed: 0.109 s
% 5.91/1.39 % (48910)Peak memory usage: 13 MB
% 5.91/1.39 % (48910)Instructions burned: 160 (million)
% 5.91/1.39 % TRYING [7]
% 5.91/1.39 % (48924)ott-21_1_sil=16000:fs=off:random_seed=3871441303:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.91/1.39 % TRYING [8]
% 5.91/1.39 % (48918)Instruction limit reached!
% 5.91/1.39 % (48918)------------------------------
% 5.91/1.39 % (48918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48918)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48918)Termination reason: Instruction limit
% 5.91/1.39 % (48918)Termination phase: Finite model building constraint generation
% 5.91/1.39 % (48918)Time elapsed: 0.133 s
% 5.91/1.39 % (48918)Peak memory usage: 25 MB
% 5.91/1.39 % (48918)Instructions burned: 714 (million)
% 5.91/1.39 % (48920)Instruction limit reached!
% 5.91/1.39 % (48920)------------------------------
% 5.91/1.39 % (48920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48920)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48920)Termination reason: Instruction limit
% 5.91/1.39 % (48920)Termination phase: Saturation
% 5.91/1.39 % (48920)Time elapsed: 0.092 s
% 5.91/1.39 % (48920)Peak memory usage: 13 MB
% 5.91/1.39 % (48920)Instructions burned: 131 (million)
% 5.91/1.39 % (48926)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1280737456:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.91/1.39 % (48927)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3084492236:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.91/1.39 % TRYING [1]
% 5.91/1.39 % TRYING [2]
% 5.91/1.39 % TRYING [3]
% 5.91/1.39 % (48924)Instruction limit reached!
% 5.91/1.39 % (48924)------------------------------
% 5.91/1.39 % (48924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48924)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48924)Termination reason: Instruction limit
% 5.91/1.39 % (48924)Termination phase: Saturation
% 5.91/1.39 % (48924)Time elapsed: 0.095 s
% 5.91/1.39 % (48924)Peak memory usage: 12 MB
% 5.91/1.39 % (48924)Instructions burned: 180 (million)
% 5.91/1.39 % TRYING [4]
% 5.91/1.39 % (48930)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1330711888:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 5.91/1.39 % TRYING [9]
% 5.91/1.39 % TRYING [5]
% 5.91/1.39 % TRYING [6]
% 5.91/1.39 % (48926)Instruction limit reached!
% 5.91/1.39 % (48926)------------------------------
% 5.91/1.39 % (48926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48926)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48926)Termination reason: Instruction limit
% 5.91/1.39 % (48926)Termination phase: Saturation
% 5.91/1.39 % (48926)Time elapsed: 0.178 s
% 5.91/1.39 % (48926)Peak memory usage: 14 MB
% 5.91/1.39 % (48926)Instructions burned: 478 (million)
% 5.91/1.39 % (48932)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3827317383:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.91/1.39 % TRYING [14]
% 5.91/1.39 % TRYING [7]
% 5.91/1.39 % TRYING [10]
% 5.91/1.39 % (48921)Instruction limit reached!
% 5.91/1.39 % (48921)------------------------------
% 5.91/1.39 % (48921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48921)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48921)Termination reason: Instruction limit
% 5.91/1.39 % (48921)Termination phase: Saturation
% 5.91/1.39 % (48921)Time elapsed: 0.425 s
% 5.91/1.39 % (48921)Peak memory usage: 17 MB
% 5.91/1.39 % (48921)Instructions burned: 685 (million)
% 5.91/1.39 % (48927)Instruction limit reached!
% 5.91/1.39 % (48927)------------------------------
% 5.91/1.39 % (48927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48927)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48927)Termination reason: Instruction limit
% 5.91/1.39 % (48927)Termination phase: Finite model building constraint generation
% 5.91/1.39 % (48927)Time elapsed: 0.330 s
% 5.91/1.39 % (48927)Peak memory usage: 19 MB
% 5.91/1.39 % (48927)Instructions burned: 865 (million)
% 5.91/1.39 % (48934)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=2473444130: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)
% 5.91/1.39 % (48935)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1997712767:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.91/1.39 % (48932)Instruction limit reached!
% 5.91/1.39 % (48932)------------------------------
% 5.91/1.39 % (48932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.39 % (48932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.39 % (48932)CaDiCaL version: 2.1.3
% 5.91/1.39 % (48932)Termination reason: Instruction limit
% 5.91/1.39 % (48932)Termination phase: Finite model building constraint generation
% 5.91/1.39 % (48932)Time elapsed: 0.187 s
% 5.91/1.39 % (48932)Peak memory usage: 59 MB
% 5.91/1.39 % (48932)Instructions burned: 894 (million)
% 5.91/1.39 % (48938)fmb+10_1_sil=64000:random_seed=1863131930:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.91/1.39 % TRYING [1]
% 5.91/1.39 % TRYING [2]
% 5.91/1.39 % TRYING [3]
% 5.91/1.39 % TRYING [4]
% 5.91/1.39 % TRYING [5]
% 5.91/1.39 % TRYING [6]
% 5.91/1.39 % TRYING [7]
% 5.91/1.39 % TRYING [8]
% 5.91/1.39 % TRYING [9]
% 5.91/1.39 % (48930) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-48899-48930"...
% 5.91/1.39 % (48930)...printing done.
% 5.91/1.39 % (48930)Refutation found. Thanks to Tanya!
% 5.91/1.39 % SZS status Unsatisfiable for theBenchmark
% 5.91/1.39 % SZS output start Proof for theBenchmark
% See solution above
% 5.91/1.40 % (48930)------------------------------
% 5.91/1.40 % (48930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.91/1.40 % (48930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.91/1.40 % (48930)CaDiCaL version: 2.1.3
% 5.91/1.40 % (48930)Termination reason: Refutation
% 5.91/1.40 % (48930)Time elapsed: 0.677 s
% 5.91/1.40 % (48930)Peak memory usage: 20 MB
% 5.91/1.40 % (48930)Instructions burned: 1091 (million)
% 5.91/1.40 % (48899)Success in time 0.965 s
% 5.91/1.40 % Vampire exiting
%------------------------------------------------------------------------------