%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV029-1 : 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 : n020.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 8.07s 1.74s
% Output : Refutation 8.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 39
% Syntax : Number of formulae : 189 ( 24 unt; 14 def)
% Number of atoms : 554 ( 82 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 583 ( 218 ~; 351 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 15 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : plus(X0,n1) != n0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_1) ).
fof(f2,axiom,
! [X0] : gt(plus(X0,n1),n0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_2) ).
fof(f3,axiom,
! [X0] :
( gt(X0,minus(X0,n1))
| ~ gt(X0,n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_3) ).
fof(f9,axiom,
! [X0,X1] :
( gt(plus(X0,n1),plus(X1,n1))
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_9) ).
fof(f11,axiom,
! [X0,X1] :
( gt(X0,X1)
| ~ gt(plus(X0,n1),X1)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_10) ).
fof(f12,plain,
! [X0,X1] :
( ~ gt(plus(X0,n1),X1)
| gt(X0,X1)
| X0 = X1 ),
inference(reorient_equations,[],[f11]) ).
fof(f14,axiom,
! [X0,X1] :
( gt(X0,X1)
| X1 = X0
| gt(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_12) ).
fof(f15,plain,
! [X0,X1] :
( gt(X1,X0)
| X0 = X1
| gt(X0,X1) ),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X2,X0,X1] :
( gt(X0,X2)
| ~ gt(X0,X1)
| ~ gt(X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_14) ).
fof(f18,axiom,
! [X0] :
( X0 = n0
| gt(X0,n0) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_17) ).
fof(f24,axiom,
! [X0] : plus(n0,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_19) ).
fof(f26,axiom,
! [X0] : level(X0) = int_level(X0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_21) ).
fof(f33,axiom,
! [X0] :
( ~ p_Reset(X0)
| int_level(plus(X0,n1)) = n0 ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_26) ).
fof(f34,plain,
! [X0] :
( ~ p_Reset(X0)
| n0 = int_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f33]) ).
fof(f45,axiom,
! [X0] :
( ~ gt(fifo_length,int_level(X0))
| ~ p_Wr(X0)
| p_Rd(X0)
| p_Reset(X0)
| int_level(plus(X0,n1)) = plus(int_level(X0),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_35) ).
fof(f57,axiom,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| gt(fifo_length,int_level(X0))
| int_level(plus(X0,n1)) = int_level(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_44) ).
fof(f58,plain,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| gt(fifo_length,int_level(X0))
| int_level(X0) = int_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f57]) ).
fof(f67,axiom,
! [X0] :
( p_Reset(X0)
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| ~ gt(int_level(X0),n0)
| int_level(plus(X0,n1)) = int_level(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_53) ).
fof(f68,plain,
! [X0] :
( ~ gt(int_level(X0),n0)
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| p_Reset(X0)
| int_level(X0) = int_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f67]) ).
fof(f75,axiom,
! [X0] :
( gt(int_level(X0),n0)
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| p_Reset(X0)
| int_level(plus(X0,n1)) = plus(int_level(X0),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_59) ).
fof(f90,axiom,
! [X0] :
( ~ gt(int_level(X0),n0)
| p_Wr(X0)
| ~ p_Rd(X0)
| p_Reset(X0)
| int_level(plus(X0,n1)) = minus(int_level(X0),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_71) ).
fof(f98,axiom,
! [X0] :
( p_Reset(X0)
| p_Wr(X0)
| ~ p_Rd(X0)
| gt(int_level(X0),n0)
| int_level(plus(X0,n1)) = int_level(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_78) ).
fof(f99,plain,
! [X0] :
( p_Reset(X0)
| p_Wr(X0)
| ~ p_Rd(X0)
| gt(int_level(X0),n0)
| int_level(X0) = int_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f98]) ).
fof(f103,axiom,
! [X0] :
( p_Reset(X0)
| p_Wr(X0)
| p_Rd(X0)
| int_level(plus(X0,n1)) = int_level(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV003-0.ax',axiom_82) ).
fof(f104,plain,
! [X0] :
( p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0)
| int_level(X0) = int_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f103]) ).
fof(f113,negated_conjecture,
~ gt(level(x_139),fifo_length),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f114,negated_conjecture,
gt(level(plus(x_139,n1)),fifo_length),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f115,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
fof(f116,plain,
~ gt(int_level(x_139),fifo_length),
inference(definition_unfolding,[],[f113,f26]) ).
fof(f117,plain,
gt(int_level(plus(x_139,n1)),fifo_length),
inference(definition_unfolding,[],[f114,f26]) ).
fof(f137,plain,
( fifo_length = int_level(x_139)
| gt(fifo_length,int_level(x_139)) ),
inference(resolution,[],[f15,f116]) ).
fof(f139,plain,
! [X0] :
( ~ gt(int_level(x_139),X0)
| ~ gt(X0,fifo_length) ),
inference(resolution,[],[f16,f116]) ).
fof(f141,plain,
( ~ gt(n0,fifo_length)
| n0 = int_level(x_139) ),
inference(resolution,[],[f139,f19]) ).
fof(f142,plain,
( ~ gt(minus(int_level(x_139),n1),fifo_length)
| ~ gt(int_level(x_139),n0) ),
inference(resolution,[],[f139,f3]) ).
fof(f152,definition,
( spl0_3
<=> n0 = int_level(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f153,plain,
( n0 != int_level(x_139)
| spl0_3 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f154,plain,
( n0 = int_level(x_139)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f156,definition,
( spl0_4
<=> gt(n0,fifo_length) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f157,plain,
( gt(n0,fifo_length)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f158,plain,
( ~ gt(n0,fifo_length)
| spl0_4 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f159,plain,
( spl0_3
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f141,f156,f152]) ).
fof(f165,plain,
( ! [X0] :
( ~ gt(n0,X0)
| ~ gt(X0,fifo_length) )
| spl0_4 ),
inference(resolution,[],[f158,f16]) ).
fof(f170,plain,
! [X0] :
( ~ gt(n1,plus(X0,n1))
| gt(n0,X0) ),
inference(superposition,[],[f10,f24]) ).
fof(f174,plain,
( ! [X0,X1] :
( ~ gt(X0,fifo_length)
| ~ gt(n0,X1)
| ~ gt(X1,X0) )
| spl0_4 ),
inference(resolution,[],[f165,f16]) ).
fof(f188,definition,
( spl0_5
<=> gt(fifo_length,int_level(x_139)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f190,plain,
( gt(fifo_length,int_level(x_139))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f192,definition,
( spl0_6
<=> fifo_length = int_level(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f193,plain,
( fifo_length != int_level(x_139)
| spl0_6 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f194,plain,
( fifo_length = int_level(x_139)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f137,f192,f188]) ).
fof(f210,plain,
( ! [X0,X1] :
( ~ gt(plus(X1,n1),fifo_length)
| ~ gt(n0,plus(X0,n1))
| ~ gt(X0,X1) )
| spl0_4 ),
inference(resolution,[],[f174,f9]) ).
fof(f245,definition,
( spl0_7
<=> gt(int_level(x_139),n0) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f246,plain,
( gt(int_level(x_139),n0)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f247,plain,
( ~ gt(int_level(x_139),n0)
| spl0_7 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f249,definition,
( spl0_8
<=> gt(minus(int_level(x_139),n1),fifo_length) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f251,plain,
( ~ gt(minus(int_level(x_139),n1),fifo_length)
| spl0_8 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,plain,
( ~ spl0_7
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f142,f249,f245]) ).
fof(f253,plain,
( n0 = int_level(x_139)
| spl0_7 ),
inference(resolution,[],[f247,f19]) ).
fof(f257,plain,
( spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f253,f245,f152]) ).
fof(f340,plain,
( ~ gt(n0,fifo_length)
| ~ spl0_3 ),
inference(superposition,[],[f116,f154]) ).
fof(f358,definition,
( spl0_12
<=> n0 = fifo_length ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f359,plain,
( n0 = fifo_length
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( n0 != fifo_length
| spl0_12 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f587,plain,
! [X0] :
( gt(fifo_length,int_level(X0))
| p_Rd(X0)
| p_Reset(X0)
| int_level(X0) = int_level(plus(X0,n1)) ),
inference(forward_subsumption_resolution,[],[f58,f104]) ).
fof(f602,plain,
( ! [X0] :
( ~ gt(n1,fifo_length)
| ~ gt(n0,plus(X0,n1))
| ~ gt(X0,n0) )
| spl0_4 ),
inference(superposition,[],[f210,f24]) ).
fof(f611,definition,
( spl0_13
<=> ! [X0] :
( ~ gt(n0,plus(X0,n1))
| ~ gt(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f612,plain,
( ! [X0] :
( ~ gt(n0,plus(X0,n1))
| ~ gt(X0,n0) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f614,definition,
( spl0_14
<=> gt(n1,fifo_length) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f615,plain,
( gt(n1,fifo_length)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f617,plain,
( spl0_13
| ~ spl0_14
| spl0_4 ),
inference(avatar_split_clause,[],[f602,f156,f614,f611]) ).
fof(f676,plain,
! [X0] :
( gt(int_level(X0),n0)
| p_Wr(X0)
| p_Reset(X0)
| int_level(X0) = int_level(plus(X0,n1)) ),
inference(forward_subsumption_resolution,[],[f99,f104]) ).
fof(f677,plain,
( ! [X0] :
( ~ gt(X0,n0)
| plus(X0,n1) = n0
| ~ gt(n0,X0) )
| ~ spl0_13 ),
inference(resolution,[],[f612,f17]) ).
fof(f683,plain,
( ! [X0] :
( ~ gt(X0,n0)
| ~ gt(n0,X0) )
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f677,f1]) ).
fof(f692,plain,
( gt(n0,n0)
| p_Wr(x_139)
| p_Reset(x_139)
| n0 = int_level(plus(x_139,n1))
| ~ spl0_3 ),
inference(superposition,[],[f676,f154]) ).
fof(f694,plain,
( p_Wr(x_139)
| p_Reset(x_139)
| n0 = int_level(plus(x_139,n1))
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f692,f22]) ).
fof(f695,plain,
( p_Wr(x_139)
| n0 = int_level(plus(x_139,n1))
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f694,f34]) ).
fof(f700,plain,
( ! [X0] : ~ gt(n0,plus(X0,n1))
| ~ spl0_13 ),
inference(resolution,[],[f683,f2]) ).
fof(f714,plain,
( ! [X0] :
( plus(X0,n1) = n0
| ~ gt(n0,X0) )
| ~ spl0_13 ),
inference(resolution,[],[f700,f17]) ).
fof(f720,plain,
( ! [X0] : ~ gt(n0,X0)
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f714,f1]) ).
fof(f770,definition,
( spl0_17
<=> n0 = int_level(plus(x_139,n1)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f772,plain,
( n0 = int_level(plus(x_139,n1))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f774,definition,
( spl0_18
<=> p_Wr(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f775,plain,
( ~ p_Wr(x_139)
| spl0_18 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f776,plain,
( p_Wr(x_139)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f777,plain,
( spl0_17
| spl0_18
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f695,f152,f774,f770]) ).
fof(f792,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| int_level(x_139) = int_level(plus(x_139,n1))
| ~ spl0_7 ),
inference(resolution,[],[f246,f68]) ).
fof(f841,plain,
! [X0] :
( ~ p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0)
| int_level(plus(X0,n1)) = minus(int_level(X0),n1)
| n0 = int_level(X0) ),
inference(resolution,[],[f90,f19]) ).
fof(f1055,definition,
( spl0_19
<=> int_level(x_139) = int_level(plus(x_139,n1)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1057,plain,
( int_level(x_139) = int_level(plus(x_139,n1))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1059,definition,
( spl0_20
<=> p_Reset(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f1060,plain,
( ~ p_Reset(x_139)
| spl0_20 ),
inference(avatar_component_clause,[],[f1059]) ).
fof(f1061,plain,
( p_Reset(x_139)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f1059]) ).
fof(f1063,definition,
( spl0_21
<=> p_Rd(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1064,plain,
( p_Rd(x_139)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1065,plain,
( ~ p_Rd(x_139)
| spl0_21 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1066,plain,
( spl0_19
| spl0_20
| ~ spl0_21
| ~ spl0_18
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f792,f245,f774,f1063,f1059,f1055]) ).
fof(f1122,plain,
( n0 = int_level(plus(x_139,n1))
| ~ spl0_20 ),
inference(resolution,[],[f1061,f34]) ).
fof(f1149,plain,
( spl0_17
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1122,f1059,f770]) ).
fof(f1157,plain,
( gt(n0,fifo_length)
| ~ spl0_17 ),
inference(superposition,[],[f117,f772]) ).
fof(f1185,plain,
( $false
| spl0_4
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1157,f158]) ).
fof(f1186,plain,
( spl0_4
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1185]) ).
fof(f1213,plain,
( $false
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f340,f157]) ).
fof(f1214,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f1213]) ).
fof(f1351,plain,
( gt(n0,n0)
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| plus(n0,n1) = int_level(plus(x_139,n1))
| ~ spl0_3 ),
inference(superposition,[],[f75,f154]) ).
fof(f1371,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| plus(n0,n1) = int_level(plus(x_139,n1))
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1351,f22]) ).
fof(f1377,plain,
( ~ p_Rd(x_139)
| p_Reset(x_139)
| plus(n0,n1) = int_level(plus(x_139,n1))
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1371,f776]) ).
fof(f1380,plain,
( p_Reset(x_139)
| plus(n0,n1) = int_level(plus(x_139,n1))
| ~ spl0_3
| ~ spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1377,f1064]) ).
fof(f1381,plain,
( plus(n0,n1) = int_level(plus(x_139,n1))
| ~ spl0_3
| ~ spl0_18
| spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1380,f1060]) ).
fof(f1382,plain,
( n1 = int_level(plus(x_139,n1))
| ~ spl0_3
| ~ spl0_18
| spl0_20
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1381,f24]) ).
fof(f1416,plain,
( gt(n1,fifo_length)
| ~ spl0_3
| ~ spl0_18
| spl0_20
| ~ spl0_21 ),
inference(superposition,[],[f117,f1382]) ).
fof(f1476,plain,
( ! [X0] : ~ gt(n1,plus(X0,n1))
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f170,f720]) ).
fof(f1482,plain,
( ! [X0] :
( ~ gt(n1,X0)
| n0 = X0 )
| ~ spl0_13 ),
inference(superposition,[],[f1476,f21]) ).
fof(f1494,plain,
( n0 = fifo_length
| ~ spl0_13
| ~ spl0_14 ),
inference(resolution,[],[f1482,f615]) ).
fof(f1504,plain,
( $false
| spl0_12
| ~ spl0_13
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1494,f360]) ).
fof(f1505,plain,
( spl0_12
| ~ spl0_13
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1504]) ).
fof(f1513,plain,
( gt(n0,n0)
| ~ spl0_12 ),
inference(superposition,[],[f115,f359]) ).
fof(f1559,plain,
( $false
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1513,f22]) ).
fof(f1560,plain,
~ spl0_12,
inference(avatar_contradiction_clause,[],[f1559]) ).
fof(f1565,plain,
( spl0_14
| ~ spl0_3
| ~ spl0_18
| spl0_20
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f1416,f1063,f1059,f774,f152,f614]) ).
fof(f1574,plain,
( p_Wr(x_139)
| p_Reset(x_139)
| int_level(x_139) = int_level(plus(x_139,n1))
| spl0_21 ),
inference(resolution,[],[f1065,f104]) ).
fof(f2895,plain,
( gt(fifo_length,fifo_length)
| p_Rd(x_139)
| p_Reset(x_139)
| fifo_length = int_level(plus(x_139,n1))
| ~ spl0_6 ),
inference(superposition,[],[f587,f194]) ).
fof(f2908,plain,
( p_Rd(x_139)
| p_Reset(x_139)
| fifo_length = int_level(plus(x_139,n1))
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2895,f22]) ).
fof(f2912,plain,
( p_Reset(x_139)
| fifo_length = int_level(plus(x_139,n1))
| ~ spl0_6
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f2908,f1065]) ).
fof(f2915,plain,
( fifo_length = int_level(plus(x_139,n1))
| ~ spl0_6
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f2912,f1060]) ).
fof(f2972,plain,
( gt(fifo_length,fifo_length)
| ~ spl0_6
| spl0_20
| spl0_21 ),
inference(superposition,[],[f117,f2915]) ).
fof(f3000,plain,
( $false
| ~ spl0_6
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f2972,f22]) ).
fof(f3001,plain,
( ~ spl0_6
| spl0_20
| spl0_21 ),
inference(avatar_contradiction_clause,[],[f3000]) ).
fof(f3002,plain,
( ~ p_Wr(x_139)
| p_Rd(x_139)
| p_Reset(x_139)
| int_level(plus(x_139,n1)) = plus(int_level(x_139),n1)
| ~ spl0_5 ),
inference(resolution,[],[f190,f45]) ).
fof(f3004,plain,
( p_Rd(x_139)
| p_Reset(x_139)
| int_level(plus(x_139,n1)) = plus(int_level(x_139),n1)
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f3002,f776]) ).
fof(f3005,plain,
( p_Reset(x_139)
| int_level(plus(x_139,n1)) = plus(int_level(x_139),n1)
| ~ spl0_5
| ~ spl0_18
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f3004,f1065]) ).
fof(f3006,plain,
( int_level(plus(x_139,n1)) = plus(int_level(x_139),n1)
| ~ spl0_5
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f3005,f1060]) ).
fof(f3501,plain,
( gt(plus(int_level(x_139),n1),fifo_length)
| ~ spl0_5
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(superposition,[],[f117,f3006]) ).
fof(f3544,plain,
( gt(int_level(x_139),fifo_length)
| fifo_length = int_level(x_139)
| ~ spl0_5
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(resolution,[],[f3501,f12]) ).
fof(f3552,plain,
( fifo_length = int_level(x_139)
| ~ spl0_5
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f3544,f116]) ).
fof(f3555,plain,
( $false
| ~ spl0_5
| spl0_6
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f3552,f193]) ).
fof(f3556,plain,
( ~ spl0_5
| spl0_6
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(avatar_contradiction_clause,[],[f3555]) ).
fof(f3558,plain,
( p_Wr(x_139)
| int_level(x_139) = int_level(plus(x_139,n1))
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f1574,f1060]) ).
fof(f4249,plain,
( int_level(x_139) = int_level(plus(x_139,n1))
| spl0_18
| spl0_20
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f3558,f775]) ).
fof(f4250,plain,
( spl0_19
| spl0_18
| spl0_20
| spl0_21 ),
inference(avatar_split_clause,[],[f4249,f1063,f1059,f774,f1055]) ).
fof(f4266,plain,
( gt(int_level(x_139),fifo_length)
| ~ spl0_19 ),
inference(superposition,[],[f117,f1057]) ).
fof(f4300,plain,
( $false
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f4266,f116]) ).
fof(f4301,plain,
~ spl0_19,
inference(avatar_contradiction_clause,[],[f4300]) ).
fof(f4346,plain,
( p_Wr(x_139)
| p_Reset(x_139)
| int_level(plus(x_139,n1)) = minus(int_level(x_139),n1)
| n0 = int_level(x_139)
| ~ spl0_21 ),
inference(resolution,[],[f1064,f841]) ).
fof(f4348,plain,
( p_Reset(x_139)
| int_level(plus(x_139,n1)) = minus(int_level(x_139),n1)
| n0 = int_level(x_139)
| spl0_18
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f4346,f775]) ).
fof(f4349,plain,
( int_level(plus(x_139,n1)) = minus(int_level(x_139),n1)
| n0 = int_level(x_139)
| spl0_18
| spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f4348,f1060]) ).
fof(f4350,plain,
( int_level(plus(x_139,n1)) = minus(int_level(x_139),n1)
| spl0_3
| spl0_18
| spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f4349,f153]) ).
fof(f5758,plain,
( ~ gt(int_level(plus(x_139,n1)),fifo_length)
| spl0_3
| spl0_8
| spl0_18
| spl0_20
| ~ spl0_21 ),
inference(superposition,[],[f251,f4350]) ).
fof(f5762,plain,
( $false
| spl0_3
| spl0_8
| spl0_18
| spl0_20
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f5758,f117]) ).
fof(f5763,plain,
( spl0_3
| spl0_8
| spl0_18
| spl0_20
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f5762]) ).
cnf(s2,plain,
( spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f159]) ).
cnf(s3,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f195]) ).
cnf(s4,plain,
( ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f252]) ).
cnf(s5,plain,
( spl0_3
| spl0_7 ),
inference(sat_conversion,[],[f257]) ).
cnf(s8,plain,
( spl0_4
| spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f617]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f777]) ).
cnf(s11,plain,
( ~ spl0_7
| ~ spl0_18
| spl0_19
| spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f1066]) ).
cnf(s14,plain,
( spl0_17
| ~ spl0_20 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s15,plain,
( spl0_4
| ~ spl0_17 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s19,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s25,plain,
( spl0_12
| ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s29,plain,
~ spl0_12,
inference(sat_conversion,[],[f1560]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_14
| ~ spl0_18
| spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s46,plain,
( ~ spl0_6
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f3001]) ).
cnf(s51,plain,
( ~ spl0_5
| spl0_6
| ~ spl0_18
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s55,plain,
( spl0_18
| spl0_19
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f4250]) ).
cnf(s57,plain,
~ spl0_19,
inference(sat_conversion,[],[f4301]) ).
cnf(s68,plain,
( spl0_3
| spl0_8
| spl0_18
| spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f5763]) ).
cnf(s70,plain,
( spl0_18
| spl0_20
| spl0_21 ),
inference(rat,[],[s55,s57]) ).
cnf(s71,plain,
( ~ spl0_13
| ~ spl0_14 ),
inference(rat,[],[s25,s29]) ).
cnf(s72,plain,
( ~ spl0_7
| ~ spl0_18
| spl0_20
| ~ spl0_21 ),
inference(rat,[],[s11,s57]) ).
cnf(s73,plain,
( ~ spl0_21
| spl0_3 ),
inference(rat,[],[s68,s72,s4,s5,s14,s15,s2]) ).
cnf(s74,plain,
( spl0_6
| spl0_21
| ~ spl0_18
| spl0_20 ),
inference(rat,[],[s3,s51]) ).
cnf(s75,plain,
( spl0_21
| spl0_20 ),
inference(rat,[],[s74,s70,s46]) ).
cnf(s76,plain,
spl0_3,
inference(rat,[],[s75,s73,s14,s15,s2]) ).
cnf(s78,plain,
~ spl0_4,
inference(rat,[],[s19,s76]) ).
cnf(s79,plain,
~ spl0_17,
inference(rat,[],[s15,s78]) ).
cnf(s80,plain,
~ spl0_20,
inference(rat,[],[s14,s79]) ).
cnf(s81,plain,
spl0_18,
inference(rat,[],[s10,s76,s79]) ).
cnf(s83,plain,
spl0_21,
inference(rat,[],[s75,s80]) ).
cnf(s86,plain,
spl0_14,
inference(rat,[],[s30,s81,s80,s76,s83]) ).
cnf(s87,plain,
~ spl0_13,
inference(rat,[],[s71,s86]) ).
cnf(s88,plain,
$false,
inference(rat,[],[s8,s78,s87,s86]) ).
fof(f5766,plain,
$false,
inference(avatar_sat_refutation,[],[s88]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV029-1 : 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.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 10:59:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 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
% 8.07/1.74 % (3203767)Will run a generic schedule for satisfiability detection.
% 8.07/1.74 % (3203775)dis+10_1_sil=32000:sp=arity:random_seed=2977839971:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.07/1.74 % (3203772)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=18602715_2999 on theBenchmark for (2999ds/0Mi)
% 8.07/1.74 % (3203778)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3152311690:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.07/1.74 % (3203774)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=122628592:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.07/1.74 % (3203776)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3394314731:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.07/1.74 % (3203777)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1583084494:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.07/1.74 % (3203773)% WARNING: option uhcvi not known.
% 8.07/1.74 % (3203773)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1551702441:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.07/1.74 % TRYING [1]
% 8.07/1.74 % TRYING [2]
% 8.07/1.74 % TRYING [3]
% 8.07/1.74 % TRYING [4]
% 8.07/1.74 % TRYING [5]
% 8.07/1.74 % TRYING [6]
% 8.07/1.74 % (3203775)Instruction limit reached!
% 8.07/1.74 % (3203775)------------------------------
% 8.07/1.74 % (3203775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203775)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203775)Termination reason: Instruction limit
% 8.07/1.74 % (3203775)Termination phase: Saturation
% 8.07/1.74 % (3203775)Time elapsed: 0.068 s
% 8.07/1.74 % (3203775)Peak memory usage: 12 MB
% 8.07/1.74 % (3203775)Instructions burned: 104 (million)
% 8.07/1.74 % (3203776)Instruction limit reached!
% 8.07/1.74 % (3203776)------------------------------
% 8.07/1.74 % (3203776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203776)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203776)Termination reason: Instruction limit
% 8.07/1.74 % (3203776)Termination phase: Saturation
% 8.07/1.74 % (3203776)Time elapsed: 0.069 s
% 8.07/1.74 % (3203776)Peak memory usage: 11 MB
% 8.07/1.74 % (3203776)Instructions burned: 118 (million)
% 8.07/1.74 % (3203777)Instruction limit reached!
% 8.07/1.74 % (3203777)------------------------------
% 8.07/1.74 % (3203777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203777)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203777)Termination reason: Instruction limit
% 8.07/1.74 % (3203777)Termination phase: Saturation
% 8.07/1.74 % (3203777)Time elapsed: 0.077 s
% 8.07/1.74 % (3203777)Peak memory usage: 12 MB
% 8.07/1.74 % (3203777)Instructions burned: 132 (million)
% 8.07/1.74 % (3203786)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2519417552:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.07/1.74 % (3203787)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1352241474:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.07/1.74 % TRYING [7]
% 8.07/1.74 % (3203788)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=1174261557:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.07/1.74 % TRYING [1]
% 8.07/1.74 % TRYING [2]
% 8.07/1.74 % TRYING [3]
% 8.07/1.74 % TRYING [4]
% 8.07/1.74 % (3203778)Instruction limit reached!
% 8.07/1.74 % (3203778)------------------------------
% 8.07/1.74 % (3203778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203778)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203778)Termination reason: Instruction limit
% 8.07/1.74 % (3203778)Termination phase: Saturation
% 8.07/1.74 % (3203778)Time elapsed: 0.113 s
% 8.07/1.74 % (3203778)Peak memory usage: 13 MB
% 8.07/1.74 % (3203778)Instructions burned: 160 (million)
% 8.07/1.74 % TRYING [5]
% 8.07/1.74 % (3203792)ott-21_1_sil=16000:fs=off:random_seed=856648920:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.07/1.74 % TRYING [8]
% 8.07/1.74 % TRYING [6]
% 8.07/1.74 % (3203787)Instruction limit reached!
% 8.07/1.74 % (3203787)------------------------------
% 8.07/1.74 % (3203787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203787)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203787)Termination reason: Instruction limit
% 8.07/1.74 % (3203787)Termination phase: Saturation
% 8.07/1.74 % (3203787)Time elapsed: 0.088 s
% 8.07/1.74 % (3203787)Peak memory usage: 12 MB
% 8.07/1.74 % (3203787)Instructions burned: 132 (million)
% 8.07/1.74 % (3203794)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1682039832:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 8.07/1.74 % (3203792)Instruction limit reached!
% 8.07/1.74 % (3203792)------------------------------
% 8.07/1.74 % (3203792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203792)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203792)Termination reason: Instruction limit
% 8.07/1.74 % (3203792)Termination phase: Saturation
% 8.07/1.74 % (3203792)Time elapsed: 0.092 s
% 8.07/1.74 % (3203792)Peak memory usage: 12 MB
% 8.07/1.74 % (3203792)Instructions burned: 181 (million)
% 8.07/1.74 % TRYING [7]
% 8.07/1.74 % (3203796)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=752594342:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.07/1.74 % TRYING [9]
% 8.07/1.74 % TRYING [1]
% 8.07/1.74 % TRYING [2]
% 8.07/1.74 % TRYING [3]
% 8.07/1.74 % TRYING [4]
% 8.07/1.74 % TRYING [5]
% 8.07/1.74 % (3203786)Instruction limit reached!
% 8.07/1.74 % (3203786)------------------------------
% 8.07/1.74 % (3203786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203786)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203786)Termination reason: Instruction limit
% 8.07/1.74 % (3203786)Termination phase: Finite model building constraint generation
% 8.07/1.74 % (3203786)Time elapsed: 0.250 s
% 8.07/1.74 % (3203786)Peak memory usage: 24 MB
% 8.07/1.74 % (3203786)Instructions burned: 714 (million)
% 8.07/1.74 % TRYING [6]
% 8.07/1.74 % (3203798)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4058327882:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 8.07/1.74 % TRYING [7]
% 8.07/1.74 % (3203794)Instruction limit reached!
% 8.07/1.74 % (3203794)------------------------------
% 8.07/1.74 % (3203794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203794)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203794)Termination reason: Instruction limit
% 8.07/1.74 % (3203794)Termination phase: Saturation
% 8.07/1.74 % (3203794)Time elapsed: 0.294 s
% 8.07/1.74 % (3203794)Peak memory usage: 13 MB
% 8.07/1.74 % (3203794)Instructions burned: 477 (million)
% 8.07/1.74 % TRYING [10]
% 8.07/1.74 % (3203788)Instruction limit reached!
% 8.07/1.74 % (3203788)------------------------------
% 8.07/1.74 % (3203788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203788)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203788)Termination reason: Instruction limit
% 8.07/1.74 % (3203788)Termination phase: Saturation
% 8.07/1.74 % (3203788)Time elapsed: 0.406 s
% 8.07/1.74 % (3203788)Peak memory usage: 16 MB
% 8.07/1.74 % (3203788)Instructions burned: 685 (million)
% 8.07/1.74 % (3203800)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=742684935:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 8.07/1.74 % (3203801)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=2838167265: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)
% 8.07/1.74 % TRYING [14]
% 8.07/1.74 % TRYING [8]
% 8.07/1.74 % (3203796)Instruction limit reached!
% 8.07/1.74 % (3203796)------------------------------
% 8.07/1.74 % (3203796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203796)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203796)Termination reason: Instruction limit
% 8.07/1.74 % (3203796)Termination phase: Finite model building constraint generation
% 8.07/1.74 % (3203796)Time elapsed: 0.324 s
% 8.07/1.74 % (3203796)Peak memory usage: 19 MB
% 8.07/1.74 % (3203796)Instructions burned: 868 (million)
% 8.07/1.74 % (3203804)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3678072659:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 8.07/1.74 % (3203800)Instruction limit reached!
% 8.07/1.74 % (3203800)------------------------------
% 8.07/1.74 % (3203800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203800)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203800)Termination reason: Instruction limit
% 8.07/1.74 % (3203800)Termination phase: Finite model building constraint generation
% 8.07/1.74 % (3203800)Time elapsed: 0.341 s
% 8.07/1.74 % (3203800)Peak memory usage: 59 MB
% 8.07/1.74 % (3203800)Instructions burned: 891 (million)
% 8.07/1.74 % (3203806)fmb+10_1_sil=64000:random_seed=518990240:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 8.07/1.74 % TRYING [1]
% 8.07/1.74 % TRYING [2]
% 8.07/1.74 % TRYING [3]
% 8.07/1.74 % (3203801)Instruction limit reached!
% 8.07/1.74 % (3203801)------------------------------
% 8.07/1.74 % (3203801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203801)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203801)Termination reason: Instruction limit
% 8.07/1.74 % (3203801)Termination phase: Saturation
% 8.07/1.74 % (3203801)Time elapsed: 0.379 s
% 8.07/1.74 % (3203801)Peak memory usage: 17 MB
% 8.07/1.74 % (3203801)Instructions burned: 693 (million)
% 8.07/1.74 % TRYING [4]
% 8.07/1.74 % TRYING [11]
% 8.07/1.74 % (3203808)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2495908290:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 8.07/1.74 % TRYING [20]
% 8.07/1.74 % TRYING [5]
% 8.07/1.74 % TRYING [6]
% 8.07/1.74 % TRYING [7]
% 8.07/1.74 % (3203798)Instruction limit reached!
% 8.07/1.74 % (3203798)------------------------------
% 8.07/1.74 % (3203798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203798)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203798)Termination reason: Instruction limit
% 8.07/1.74 % (3203798)Termination phase: Saturation
% 8.07/1.74 % (3203798)Time elapsed: 0.715 s
% 8.07/1.74 % (3203798)Peak memory usage: 17 MB
% 8.07/1.74 % (3203798)Instructions burned: 1179 (million)
% 8.07/1.74 % (3203810)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1079299080:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 8.07/1.74 % TRYING [8]
% 8.07/1.74 % (3203804)Instruction limit reached!
% 8.07/1.74 % (3203804)------------------------------
% 8.07/1.74 % (3203804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203804)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203804)Termination reason: Instruction limit
% 8.07/1.74 % (3203804)Termination phase: Saturation
% 8.07/1.74 % (3203804)Time elapsed: 0.522 s
% 8.07/1.74 % (3203804)Peak memory usage: 17 MB
% 8.07/1.74 % (3203804)Instructions burned: 879 (million)
% 8.07/1.74 % (3203812)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=315469974:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 8.07/1.74 % TRYING [8]
% 8.07/1.74 % TRYING [9]
% 8.07/1.74 % (3203812) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3203767-3203812"...
% 8.07/1.74 % (3203812)...printing done.
% 8.07/1.74 % (3203812)Refutation found. Thanks to Tanya!
% 8.07/1.74 % SZS status Unsatisfiable for theBenchmark
% 8.07/1.74 % SZS output start Proof for theBenchmark
% See solution above
% 8.07/1.74 % (3203812)------------------------------
% 8.07/1.74 % (3203812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.07/1.74 % (3203812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.74 % (3203812)CaDiCaL version: 2.1.3
% 8.07/1.74 % (3203812)Termination reason: Refutation
% 8.07/1.74 % (3203812)Time elapsed: 0.157 s
% 8.07/1.74 % (3203812)Peak memory usage: 13 MB
% 8.07/1.74 % (3203812)Instructions burned: 255 (million)
% 8.07/1.74 % (3203767)Success in time 1.339 s
% 8.07/1.74 % Vampire exiting
%------------------------------------------------------------------------------