%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV031-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:20:18 AM UTC 2026
% Result : Unsatisfiable 4.22s 1.54s
% Output : Refutation 5.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 32
% Syntax : Number of formulae : 184 ( 20 unt; 11 def)
% Number of atoms : 656 ( 58 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 843 ( 371 ~; 461 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 12 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 39 ( 0 sgn 39 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : plus(X0,n1) != n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f2,axiom,
! [X0] : gt(plus(X0,n1),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f5,axiom,
! [X2,X0,X1] :
( minus(X0,X1) = X2
| plus(X2,X1) != X0
| def_10(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ def_10(X0,X1)
| ~ gt(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f7,axiom,
! [X0,X1] :
( ~ def_10(X0,X1)
| X1 != X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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/sandbox/benchmark/theBenchmark.p',axiom_8) ).
fof(f11,axiom,
! [X0,X1] :
( gt(X0,X1)
| ~ gt(plus(X0,n1),X1)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
fof(f12,plain,
! [X0,X1] :
( ~ gt(plus(X0,n1),X1)
| gt(X0,X1)
| X0 = X1 ),
inference(reorient_equations,[],[f11]) ).
fof(f16,axiom,
! [X2,X0,X1] :
( gt(X0,X2)
| ~ gt(X0,X1)
| ~ gt(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
fof(f18,axiom,
! [X0] :
( X0 = n0
| gt(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f19,plain,
! [X0] :
( gt(X0,n0)
| n0 = X0 ),
inference(reorient_equations,[],[f18]) ).
fof(f22,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_17) ).
fof(f24,axiom,
! [X0] : plus(n0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
fof(f25,axiom,
n1 = plus(n0,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(f35,axiom,
! [X0] :
( ~ p_Reset(X0)
| wr_level(plus(X0,n1)) = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_27) ).
fof(f36,plain,
! [X0] :
( n0 = wr_level(plus(X0,n1))
| ~ p_Reset(X0) ),
inference(reorient_equations,[],[f35]) ).
fof(f52,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1)
| ~ p_Wr(X0)
| p_Rd(X0)
| ~ gt(fifo_length,int_level(X0))
| ~ gt(minus(fifo_length,n1),wr_level(X0))
| p_Reset(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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/sandbox/benchmark/theBenchmark.p',axiom_41) ).
fof(f54,plain,
! [X0] :
( gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Wr(X0)
| p_Rd(X0)
| ~ gt(fifo_length,int_level(X0))
| p_Reset(X0)
| n0 = wr_level(plus(X0,n1)) ),
inference(reorient_equations,[],[f53]) ).
fof(f56,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = wr_level(X0)
| ~ p_Wr(X0)
| p_Rd(X0)
| gt(fifo_length,int_level(X0))
| p_Reset(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_43) ).
fof(f85,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1)
| ~ p_Wr(X0)
| ~ p_Rd(X0)
| ~ gt(minus(fifo_length,n1),wr_level(X0))
| p_Reset(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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/sandbox/benchmark/theBenchmark.p',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] :
( wr_level(plus(X0,n1)) = wr_level(X0)
| p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_69) ).
fof(f113,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f114,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f116,plain,
! [X2,X1] :
( minus(plus(X2,X1),X1) = X2
| def_10(X1,plus(X2,X1)) ),
inference(equality_resolution,[],[f5]) ).
fof(f118,plain,
! [X1] : ~ def_10(X1,X1),
inference(equality_resolution,[],[f8]) ).
fof(f121,plain,
! [X0] :
( ~ gt(plus(wr_level(x_139),n1),X0)
| ~ gt(X0,fifo_length) ),
inference(resolution,[],[f113,f16]) ).
fof(f127,definition,
( spl0_2
<=> fifo_length = plus(wr_level(x_139),n1) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f128,plain,
( fifo_length != plus(wr_level(x_139),n1)
| spl0_2 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f129,plain,
( fifo_length = plus(wr_level(x_139),n1)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f134,plain,
( ! [X0] :
( gt(fifo_length,plus(X0,n1))
| ~ gt(wr_level(x_139),X0) )
| ~ spl0_2 ),
inference(superposition,[],[f9,f129]) ).
fof(f190,plain,
( minus(fifo_length,n1) = wr_level(x_139)
| def_10(n1,fifo_length)
| ~ spl0_2 ),
inference(superposition,[],[f116,f129]) ).
fof(f192,definition,
( spl0_3
<=> def_10(n1,fifo_length) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f194,plain,
( def_10(n1,fifo_length)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f196,definition,
( spl0_4
<=> minus(fifo_length,n1) = wr_level(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f198,plain,
( minus(fifo_length,n1) = wr_level(x_139)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,plain,
( spl0_3
| spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f190,f127,f196,f192]) ).
fof(f361,plain,
( gt(wr_level(plus(x_139,n1)),fifo_length)
| fifo_length = wr_level(plus(x_139,n1)) ),
inference(resolution,[],[f114,f12]) ).
fof(f364,plain,
( gt(plus(wr_level(x_139),n1),fifo_length)
| p_Wr(x_139)
| p_Reset(x_139) ),
inference(superposition,[],[f114,f88]) ).
fof(f367,plain,
( gt(plus(wr_level(x_139),n1),fifo_length)
| ~ p_Wr(x_139)
| p_Rd(x_139)
| gt(fifo_length,int_level(x_139))
| p_Reset(x_139) ),
inference(superposition,[],[f114,f56]) ).
fof(f368,plain,
( ~ p_Wr(x_139)
| p_Rd(x_139)
| gt(fifo_length,int_level(x_139))
| p_Reset(x_139) ),
inference(forward_subsumption_resolution,[],[f367,f113]) ).
fof(f371,plain,
( p_Wr(x_139)
| p_Reset(x_139) ),
inference(forward_subsumption_resolution,[],[f364,f113]) ).
fof(f374,definition,
( spl0_33
<=> fifo_length = wr_level(plus(x_139,n1)) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f376,plain,
( fifo_length = wr_level(plus(x_139,n1))
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f378,definition,
( spl0_34
<=> gt(wr_level(plus(x_139,n1)),fifo_length) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f380,plain,
( gt(wr_level(plus(x_139,n1)),fifo_length)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,plain,
( spl0_33
| spl0_34 ),
inference(avatar_split_clause,[],[f361,f378,f374]) ).
fof(f384,definition,
( spl0_35
<=> p_Reset(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f385,plain,
( ~ p_Reset(x_139)
| spl0_35 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f386,plain,
( p_Reset(x_139)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f388,definition,
( spl0_36
<=> gt(fifo_length,int_level(x_139)) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f390,plain,
( gt(fifo_length,int_level(x_139))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f392,definition,
( spl0_37
<=> p_Rd(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f393,plain,
( ~ p_Rd(x_139)
| spl0_37 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( p_Rd(x_139)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f396,definition,
( spl0_38
<=> p_Wr(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f397,plain,
( p_Wr(x_139)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f399,plain,
( spl0_35
| spl0_36
| spl0_37
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f368,f396,f392,f388,f384]) ).
fof(f402,plain,
( spl0_35
| spl0_38 ),
inference(avatar_split_clause,[],[f371,f396,f384]) ).
fof(f408,plain,
( gt(n0,fifo_length)
| ~ p_Reset(x_139)
| ~ spl0_34 ),
inference(superposition,[],[f380,f36]) ).
fof(f410,plain,
( gt(plus(wr_level(x_139),n1),fifo_length)
| ~ p_Wr(x_139)
| p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34 ),
inference(superposition,[],[f380,f52]) ).
fof(f411,plain,
( gt(plus(wr_level(x_139),n1),fifo_length)
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34 ),
inference(superposition,[],[f380,f85]) ).
fof(f413,plain,
( gt(n0,fifo_length)
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f408,f386]) ).
fof(f444,plain,
~ gt(n0,fifo_length),
inference(resolution,[],[f121,f2]) ).
fof(f445,plain,
( ~ gt(n0,fifo_length)
| n0 = plus(wr_level(x_139),n1) ),
inference(resolution,[],[f121,f19]) ).
fof(f449,plain,
( n0 = plus(wr_level(x_139),n1)
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f445,f413]) ).
fof(f457,plain,
( $false
| ~ spl0_34
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f449,f1]) ).
fof(f458,plain,
( ~ spl0_34
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f457]) ).
fof(f520,plain,
( gt(minus(fifo_length,n1),minus(fifo_length,n1))
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl0_4 ),
inference(superposition,[],[f87,f198]) ).
fof(f521,plain,
( gt(minus(fifo_length,n1),minus(fifo_length,n1))
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f520,f36]) ).
fof(f523,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f521,f22]) ).
fof(f524,plain,
( ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl0_4
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f523,f397]) ).
fof(f525,plain,
( n0 = wr_level(plus(x_139,n1))
| ~ spl0_4
| ~ spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f524,f394]) ).
fof(f549,plain,
( gt(n0,fifo_length)
| ~ spl0_4
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38 ),
inference(superposition,[],[f380,f525]) ).
fof(f561,plain,
( $false
| ~ spl0_4
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f549,f444]) ).
fof(f562,plain,
( ~ spl0_4
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f561]) ).
fof(f596,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f411,f113]) ).
fof(f598,plain,
( ~ p_Rd(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f596,f397]) ).
fof(f600,plain,
( ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f598,f394]) ).
fof(f602,definition,
( spl0_52
<=> gt(minus(fifo_length,n1),wr_level(x_139)) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f603,plain,
( gt(minus(fifo_length,n1),wr_level(x_139))
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f604,plain,
( ~ gt(minus(fifo_length,n1),wr_level(x_139))
| spl0_52 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f610,plain,
( ~ gt(minus(fifo_length,n1),wr_level(x_139))
| ~ spl0_34
| spl0_35
| ~ spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f600,f385]) ).
fof(f611,plain,
( ~ spl0_52
| ~ spl0_34
| spl0_35
| ~ spl0_37
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f610,f396,f392,f384,f378,f602]) ).
fof(f612,plain,
( ~ p_Wr(x_139)
| p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| p_Reset(x_139)
| n0 = wr_level(plus(x_139,n1))
| spl0_52 ),
inference(resolution,[],[f604,f54]) ).
fof(f613,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| p_Reset(x_139)
| n0 = wr_level(plus(x_139,n1))
| spl0_52 ),
inference(resolution,[],[f604,f87]) ).
fof(f617,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f613,f36]) ).
fof(f618,plain,
( ~ p_Rd(x_139)
| n0 = wr_level(plus(x_139,n1))
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f617,f397]) ).
fof(f619,plain,
( n0 = wr_level(plus(x_139,n1))
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f618,f394]) ).
fof(f620,plain,
( ~ gt(fifo_length,n1)
| ~ spl0_3 ),
inference(resolution,[],[f194,f6]) ).
fof(f638,plain,
( gt(n0,fifo_length)
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(superposition,[],[f380,f619]) ).
fof(f649,plain,
( $false
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f638,f444]) ).
fof(f650,plain,
( ~ spl0_34
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(avatar_contradiction_clause,[],[f649]) ).
fof(f653,plain,
( ~ p_Wr(x_139)
| p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| n0 = wr_level(plus(x_139,n1))
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f612,f36]) ).
fof(f654,plain,
( p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| n0 = wr_level(plus(x_139,n1))
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f653,f397]) ).
fof(f655,plain,
( ~ gt(fifo_length,int_level(x_139))
| n0 = wr_level(plus(x_139,n1))
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f654,f393]) ).
fof(f656,plain,
( n0 = wr_level(plus(x_139,n1))
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f655,f390]) ).
fof(f664,plain,
( gt(n0,fifo_length)
| ~ spl0_34
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(superposition,[],[f380,f656]) ).
fof(f675,plain,
( $false
| ~ spl0_34
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f664,f444]) ).
fof(f676,plain,
( ~ spl0_34
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(avatar_contradiction_clause,[],[f675]) ).
fof(f679,plain,
( ~ p_Wr(x_139)
| p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f410,f113]) ).
fof(f681,plain,
( p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f679,f397]) ).
fof(f683,plain,
( ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34
| spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f681,f393]) ).
fof(f685,plain,
( ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_34
| ~ spl0_36
| spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f683,f390]) ).
fof(f687,plain,
( p_Reset(x_139)
| ~ spl0_34
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f685,f603]) ).
fof(f689,plain,
( $false
| ~ spl0_34
| spl0_35
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f687,f385]) ).
fof(f690,plain,
( ~ spl0_34
| spl0_35
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f689]) ).
fof(f697,plain,
( fifo_length = plus(wr_level(x_139),n1)
| ~ p_Wr(x_139)
| p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_33 ),
inference(superposition,[],[f376,f52]) ).
fof(f698,plain,
( fifo_length = plus(wr_level(x_139),n1)
| ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| ~ spl0_33 ),
inference(superposition,[],[f376,f85]) ).
fof(f701,plain,
( n0 = fifo_length
| ~ p_Reset(x_139)
| ~ spl0_33 ),
inference(superposition,[],[f36,f376]) ).
fof(f743,plain,
( gt(fifo_length,n1)
| ~ gt(wr_level(x_139),n0)
| ~ spl0_2 ),
inference(superposition,[],[f134,f24]) ).
fof(f746,plain,
( ~ gt(wr_level(x_139),n0)
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f743,f620]) ).
fof(f748,plain,
( n0 = wr_level(x_139)
| ~ spl0_2
| ~ spl0_3 ),
inference(resolution,[],[f746,f19]) ).
fof(f757,definition,
( spl0_57
<=> n0 = wr_level(x_139) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f759,plain,
( n0 = wr_level(x_139)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f761,plain,
( spl0_57
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f748,f192,f127,f757]) ).
fof(f773,plain,
( plus(n0,n1) = fifo_length
| ~ spl0_2
| ~ spl0_57 ),
inference(superposition,[],[f129,f759]) ).
fof(f789,plain,
( n1 = fifo_length
| ~ spl0_2
| ~ spl0_57 ),
inference(forward_demodulation,[],[f773,f25]) ).
fof(f869,plain,
( def_10(n1,n1)
| ~ spl0_2
| ~ spl0_3
| ~ spl0_57 ),
inference(superposition,[],[f194,f789]) ).
fof(f886,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f869,f118]) ).
fof(f887,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f886]) ).
fof(f941,plain,
( gt(minus(fifo_length,n1),minus(fifo_length,n1))
| ~ spl0_4
| ~ spl0_52 ),
inference(superposition,[],[f603,f198]) ).
fof(f945,plain,
( $false
| ~ spl0_4
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f941,f22]) ).
fof(f946,plain,
( ~ spl0_4
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f945]) ).
fof(f955,plain,
( ~ p_Wr(x_139)
| p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f697,f128]) ).
fof(f967,plain,
( p_Rd(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f955,f397]) ).
fof(f970,plain,
( ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33
| spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f967,f393]) ).
fof(f973,plain,
( ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f970,f390]) ).
fof(f976,plain,
( p_Reset(x_139)
| spl0_2
| ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f973,f603]) ).
fof(f979,plain,
( $false
| spl0_2
| ~ spl0_33
| spl0_35
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f976,f385]) ).
fof(f980,plain,
( spl0_2
| ~ spl0_33
| spl0_35
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f979]) ).
fof(f981,plain,
( n0 = fifo_length
| ~ spl0_33
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f701,f386]) ).
fof(f987,plain,
( ~ gt(plus(wr_level(x_139),n1),n0)
| ~ spl0_33
| ~ spl0_35 ),
inference(superposition,[],[f113,f981]) ).
fof(f1004,plain,
( $false
| ~ spl0_33
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f987,f2]) ).
fof(f1005,plain,
( ~ spl0_33
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1004]) ).
fof(f1026,plain,
( n0 = fifo_length
| ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(superposition,[],[f376,f656]) ).
fof(f1039,plain,
( ~ gt(plus(wr_level(x_139),n1),n0)
| ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(superposition,[],[f113,f1026]) ).
fof(f1060,plain,
( $false
| ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f1039,f2]) ).
fof(f1061,plain,
( ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(avatar_contradiction_clause,[],[f1060]) ).
fof(f1074,plain,
( n0 = fifo_length
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(superposition,[],[f376,f619]) ).
fof(f1112,plain,
( ~ gt(plus(wr_level(x_139),n1),n0)
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(superposition,[],[f113,f1074]) ).
fof(f1134,plain,
( $false
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(forward_subsumption_resolution,[],[f1112,f2]) ).
fof(f1135,plain,
( ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(avatar_contradiction_clause,[],[f1134]) ).
fof(f1144,plain,
( ~ p_Wr(x_139)
| ~ p_Rd(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f698,f128]) ).
fof(f1161,plain,
( ~ p_Rd(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1144,f397]) ).
fof(f1164,plain,
( ~ gt(minus(fifo_length,n1),wr_level(x_139))
| p_Reset(x_139)
| spl0_2
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1161,f394]) ).
fof(f1167,plain,
( p_Reset(x_139)
| spl0_2
| ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f1164,f603]) ).
fof(f1170,plain,
( $false
| spl0_2
| ~ spl0_33
| spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f1167,f385]) ).
fof(f1171,plain,
( spl0_2
| ~ spl0_33
| spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f1170]) ).
cnf(s2,plain,
( ~ spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f199]) ).
cnf(s51,plain,
( spl0_33
| spl0_34 ),
inference(sat_conversion,[],[f382]) ).
cnf(s52,plain,
( spl0_35
| spl0_36
| spl0_37
| ~ spl0_38 ),
inference(sat_conversion,[],[f399]) ).
cnf(s53,plain,
( spl0_35
| spl0_38 ),
inference(sat_conversion,[],[f402]) ).
cnf(s58,plain,
( ~ spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f458]) ).
cnf(s63,plain,
( ~ spl0_4
| ~ spl0_34
| ~ spl0_37
| ~ spl0_38 ),
inference(sat_conversion,[],[f562]) ).
cnf(s67,plain,
( ~ spl0_34
| spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(sat_conversion,[],[f611]) ).
cnf(s68,plain,
( ~ spl0_34
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(sat_conversion,[],[f650]) ).
cnf(s71,plain,
( ~ spl0_34
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(sat_conversion,[],[f676]) ).
cnf(s74,plain,
( ~ spl0_34
| spl0_35
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(sat_conversion,[],[f690]) ).
cnf(s80,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_57 ),
inference(sat_conversion,[],[f761]) ).
cnf(s83,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_57 ),
inference(sat_conversion,[],[f887]) ).
cnf(s85,plain,
( ~ spl0_4
| ~ spl0_52 ),
inference(sat_conversion,[],[f946]) ).
cnf(s88,plain,
( spl0_2
| ~ spl0_33
| spl0_35
| ~ spl0_36
| spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(sat_conversion,[],[f980]) ).
cnf(s90,plain,
( ~ spl0_33
| ~ spl0_35 ),
inference(sat_conversion,[],[f1005]) ).
cnf(s93,plain,
( ~ spl0_33
| ~ spl0_36
| spl0_37
| ~ spl0_38
| spl0_52 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s97,plain,
( ~ spl0_33
| ~ spl0_37
| ~ spl0_38
| spl0_52 ),
inference(sat_conversion,[],[f1135]) ).
cnf(s101,plain,
( spl0_2
| ~ spl0_33
| spl0_35
| ~ spl0_37
| ~ spl0_38
| ~ spl0_52 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s103,plain,
( ~ spl0_34
| ~ spl0_4 ),
inference(rat,[],[s52,s71,s63,s53,s58,s85]) ).
cnf(s104,plain,
~ spl0_4,
inference(rat,[],[s93,s52,s97,s53,s90,s51,s103,s85]) ).
cnf(s105,plain,
( ~ spl0_3
| ~ spl0_2 ),
inference(rat,[],[s80,s83]) ).
cnf(s106,plain,
~ spl0_2,
inference(rat,[],[s105,s2,s104]) ).
cnf(s108,plain,
( ~ spl0_37
| ~ spl0_34 ),
inference(rat,[],[s67,s68,s53,s58]) ).
cnf(s109,plain,
~ spl0_34,
inference(rat,[],[s74,s71,s52,s108,s53,s58]) ).
cnf(s110,plain,
spl0_33,
inference(rat,[],[s51,s109]) ).
cnf(s111,plain,
~ spl0_35,
inference(rat,[],[s90,s110]) ).
cnf(s112,plain,
spl0_38,
inference(rat,[],[s53,s111]) ).
cnf(s113,plain,
~ spl0_37,
inference(rat,[],[s101,s97,s106,s110,s112,s111]) ).
cnf(s114,plain,
spl0_36,
inference(rat,[],[s52,s112,s111,s113]) ).
cnf(s115,plain,
spl0_52,
inference(rat,[],[s93,s113,s112,s110,s114]) ).
cnf(s116,plain,
$false,
inference(rat,[],[s88,s113,s112,s111,s110,s106,s115,s114]) ).
fof(f1172,plain,
$false,
inference(avatar_sat_refutation,[],[s116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV031-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 11:00:04 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.22/1.54 % (3205022)Input is clausal, will run a generic CNF schedule.
% 4.22/1.54 % (3205027)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=951969398:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.22/1.54 % (3205028)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2375723543:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.22/1.54 % (3205029)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=312223229:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.22/1.54 % (3205031)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4205641611:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.22/1.54 % (3205030)lrs+10_1_sil=8000:sp=occurrence:random_seed=4189967491:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.22/1.54 % (3205032)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3470082486:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.22/1.54 % (3205033)dis-21_1_sil=8000:lcm=predicate:random_seed=3951709066:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 4.22/1.54 % (3205033)Instruction limit reached!
% 4.22/1.54 % (3205033)------------------------------
% 4.22/1.54 % (3205033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205033)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205033)Termination reason: Instruction limit
% 4.22/1.54 % (3205033)Termination phase: Saturation
% 4.22/1.54 % (3205033)Time elapsed: 0.068 s
% 4.22/1.54 % (3205033)Peak memory usage: 88 MB
% 4.22/1.54 % (3205033)Instructions burned: 117 (million)
% 4.22/1.54 % (3205030)Instruction limit reached!
% 4.22/1.54 % (3205030)------------------------------
% 4.22/1.54 % (3205030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205030)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205030)Termination reason: Instruction limit
% 4.22/1.54 % (3205030)Termination phase: Saturation
% 4.22/1.54 % (3205030)Time elapsed: 0.070 s
% 4.22/1.54 % (3205030)Peak memory usage: 88 MB
% 4.22/1.54 % (3205030)Instructions burned: 108 (million)
% 4.22/1.54 % (3205031)Instruction limit reached!
% 4.22/1.54 % (3205031)------------------------------
% 4.22/1.54 % (3205031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205031)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205031)Termination reason: Instruction limit
% 4.22/1.54 % (3205031)Termination phase: Saturation
% 4.22/1.54 % (3205031)Time elapsed: 0.079 s
% 4.22/1.54 % (3205031)Peak memory usage: 89 MB
% 4.22/1.54 % (3205031)Instructions burned: 116 (million)
% 4.22/1.54 % (3205032)Instruction limit reached!
% 4.22/1.54 % (3205032)------------------------------
% 4.22/1.54 % (3205032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205032)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205032)Termination reason: Instruction limit
% 4.22/1.54 % (3205032)Termination phase: Saturation
% 4.22/1.54 % (3205032)Time elapsed: 0.124 s
% 4.22/1.54 % (3205032)Peak memory usage: 89 MB
% 4.22/1.54 % (3205032)Instructions burned: 181 (million)
% 4.22/1.54 % (3205041)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1636928442:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.22/1.54 % (3205042)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2312724105:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.22/1.54 % (3205043)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=959957310:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.22/1.54 % (3205043)First to succeed.
% 4.22/1.54 % (3205043)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3205022"
% 4.22/1.54 % (3205044)lrs+10_64_to=lpo:sil=8000:random_seed=2205439289:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.22/1.54 % (3205041)Instruction limit reached!
% 4.22/1.54 % (3205041)------------------------------
% 4.22/1.54 % (3205041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205041)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205041)Termination reason: Instruction limit
% 4.22/1.54 % (3205041)Termination phase: Saturation
% 4.22/1.54 % (3205041)Time elapsed: 0.094 s
% 4.22/1.54 % (3205041)Peak memory usage: 89 MB
% 4.22/1.54 % (3205041)Instructions burned: 144 (million)
% 4.22/1.54 % (3205042)Instruction limit reached!
% 4.22/1.54 % (3205042)------------------------------
% 4.22/1.54 % (3205042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205042)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205042)Termination reason: Instruction limit
% 4.22/1.54 % (3205042)Termination phase: Saturation
% 4.22/1.54 % (3205042)Time elapsed: 0.101 s
% 4.22/1.54 % (3205042)Peak memory usage: 89 MB
% 4.22/1.54 % (3205042)Instructions burned: 189 (million)
% 4.22/1.54 % (3205044)Instruction limit reached!
% 4.22/1.54 % (3205044)------------------------------
% 4.22/1.54 % (3205044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.22/1.54 % (3205044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.22/1.54 % (3205044)CaDiCaL version: 2.1.3
% 4.22/1.54 % (3205044)Termination reason: Instruction limit
% 4.22/1.54 % (3205044)Termination phase: Saturation
% 4.22/1.54 % (3205044)Time elapsed: 0.067 s
% 4.22/1.54 % (3205044)Peak memory usage: 88 MB
% 4.22/1.54 % (3205044)Instructions burned: 126 (million)
% 4.22/1.54 % (3205027)Also succeeded, but the first one will report.
% 4.22/1.54 % (3205050)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1198279925:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 4.22/1.54 % (3205049)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3077650329:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 4.22/1.54 % (3205043)Refutation found. Thanks to Tanya!
% 4.22/1.54 % SZS status Unsatisfiable for theBenchmark
% 4.22/1.54 % SZS output start Proof for theBenchmark
% See solution above
% 5.50/1.74 % (3205043)------------------------------
% 5.50/1.74 % (3205043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.50/1.74 % (3205043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.50/1.74 % (3205043)CaDiCaL version: 2.1.3
% 5.50/1.74 % (3205043)Termination reason: Refutation
% 5.50/1.74 % (3205043)Time elapsed: 0.023 s
% 5.50/1.74 % (3205043)Peak memory usage: 89 MB
% 5.50/1.74 % (3205043)Instructions burned: 34 (million)
% 5.50/1.74 % (3205043)------------------------------
% 5.50/1.74 % (3205043)------------------------------
% 5.50/1.74 % (3205022)Success in time 0.694 s
% 5.50/1.74 % Vampire exiting
%------------------------------------------------------------------------------