%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW328+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 01:39:50 PM UTC 2026
% Result : Theorem 2.25s 0.75s
% Output : Refutation 2.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 14
% Syntax : Number of formulae : 107 ( 17 unt; 9 def)
% Number of atoms : 314 ( 24 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 363 ( 156 ~; 162 |; 20 &)
% ( 9 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 12 con; 0-2 aty)
% Number of variables : 88 ( 0 sgn 82 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5205,axiom,
! [X0] :
( ! [X1] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,X0,X1) )
=> ! [X2,X3] :
( ( v_P(X2,X3)
& hBOOL(hAPP(v_b,X3)) )
=> ! [X4] :
( c_Natural_Oevaln(v_c,X3,X0,X4)
=> v_P(X2,X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f5206,axiom,
hBOOL(hAPP(v_ba,v_s0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f5207,axiom,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_2) ).
fof(f5210,axiom,
( c_Com_Ocom_OWhile(v_ba,v_ca) = c_Com_Ocom_OWhile(v_b,v_c)
=> ( ! [X0] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0) )
=> ! [X1] :
( v_P(X1,v_s1)
=> ( v_P(X1,v_s2)
& ~ hBOOL(hAPP(v_b,v_s2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_5) ).
fof(f5211,conjecture,
( ( v_ba = v_b
& v_ca = v_c )
=> ( ! [X0] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0) )
=> ! [X1] :
( v_P(X1,v_s0)
=> ( v_P(X1,v_s2)
& ~ hBOOL(hAPP(v_b,v_s2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_6) ).
fof(f5212,negated_conjecture,
~ ( ( v_ba = v_b
& v_ca = v_c )
=> ( ! [X0] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0) )
=> ! [X1] :
( v_P(X1,v_s0)
=> ( v_P(X1,v_s2)
& ~ hBOOL(hAPP(v_b,v_s2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f5211]) ).
fof(f9467,plain,
! [X0] :
( ! [X2,X3] :
( ! [X4] :
( v_P(X2,X4)
| ~ c_Natural_Oevaln(v_c,X3,X0,X4) )
| ~ v_P(X2,X3)
| ~ hBOOL(hAPP(v_b,X3)) )
| ? [X1] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X0,X1)
& hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_G)) ) ),
inference(ennf_transformation,[],[f5205]) ).
fof(f9468,plain,
! [X0] :
( ! [X2,X3] :
( ! [X4] :
( v_P(X2,X4)
| ~ c_Natural_Oevaln(v_c,X3,X0,X4) )
| ~ v_P(X2,X3)
| ~ hBOOL(hAPP(v_b,X3)) )
| ? [X1] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X0,X1)
& hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_G)) ) ),
inference(flattening,[],[f9467]) ).
fof(f9471,plain,
( ! [X1] :
( ( v_P(X1,v_s2)
& ~ hBOOL(hAPP(v_b,v_s2)) )
| ~ v_P(X1,v_s1) )
| ? [X0] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0)
& hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G)) )
| c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_ba,v_ca) ),
inference(ennf_transformation,[],[f5210]) ).
fof(f9472,plain,
( ! [X1] :
( ( v_P(X1,v_s2)
& ~ hBOOL(hAPP(v_b,v_s2)) )
| ~ v_P(X1,v_s1) )
| ? [X0] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0)
& hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G)) )
| c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_ba,v_ca) ),
inference(flattening,[],[f9471]) ).
fof(f9473,plain,
( ? [X1] :
( ( ~ v_P(X1,v_s2)
| hBOOL(hAPP(v_b,v_s2)) )
& v_P(X1,v_s0) )
& ! [X0] :
( c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G)) )
& v_ba = v_b
& v_ca = v_c ),
inference(ennf_transformation,[],[f5212]) ).
fof(f9474,plain,
( ? [X1] :
( ( ~ v_P(X1,v_s2)
| hBOOL(hAPP(v_b,v_s2)) )
& v_P(X1,v_s0) )
& ! [X0] :
( c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G)) )
& v_ba = v_b
& v_ca = v_c ),
inference(flattening,[],[f9473]) ).
fof(f16429,plain,
! [X2,X3,X0,X4] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK486(X0)),v_G))
| ~ hBOOL(hAPP(v_b,X3))
| ~ v_P(X2,X3)
| ~ c_Natural_Oevaln(v_c,X3,X0,X4)
| v_P(X2,X4) ),
inference(cnf_transformation,[],[f9468]) ).
fof(f16430,plain,
! [X2,X3,X0,X4] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X0,sK486(X0))
| ~ hBOOL(hAPP(v_b,X3))
| ~ v_P(X2,X3)
| ~ c_Natural_Oevaln(v_c,X3,X0,X4)
| v_P(X2,X4) ),
inference(cnf_transformation,[],[f9468]) ).
fof(f16431,plain,
hBOOL(hAPP(v_ba,v_s0)),
inference(cnf_transformation,[],[f5206]) ).
fof(f16432,plain,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
inference(cnf_transformation,[],[f5207]) ).
fof(f16438,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_ba,v_ca)
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| ~ hBOOL(hAPP(v_b,v_s2)) ),
inference(cnf_transformation,[],[f9472]) ).
fof(f16439,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_ba,v_ca)
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(cnf_transformation,[],[f9472]) ).
fof(f16440,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| ~ hBOOL(hAPP(v_b,v_s2)) ),
inference(cnf_transformation,[],[f9472]) ).
fof(f16441,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(cnf_transformation,[],[f9472]) ).
fof(f16442,plain,
( hBOOL(hAPP(v_b,v_s2))
| ~ v_P(sK489,v_s2) ),
inference(cnf_transformation,[],[f9474]) ).
fof(f16443,plain,
v_P(sK489,v_s0),
inference(cnf_transformation,[],[f9474]) ).
fof(f16444,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
| c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0) ),
inference(cnf_transformation,[],[f9474]) ).
fof(f16445,plain,
v_c = v_ca,
inference(cnf_transformation,[],[f9474]) ).
fof(f16446,plain,
v_b = v_ba,
inference(cnf_transformation,[],[f9474]) ).
fof(f17251,plain,
! [X2,X3,X0,X4] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X0,sK486(X0))
| ~ hBOOL(hAPP(v_ba,X3))
| ~ v_P(X2,X3)
| ~ c_Natural_Oevaln(v_ca,X3,X0,X4)
| v_P(X2,X4) ),
inference(definition_unfolding,[],[f16430,f16446,f16445]) ).
fof(f17252,plain,
! [X2,X3,X0,X4] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK486(X0)),v_G))
| ~ hBOOL(hAPP(v_ba,X3))
| ~ v_P(X2,X3)
| ~ c_Natural_Oevaln(v_ca,X3,X0,X4)
| v_P(X2,X4) ),
inference(definition_unfolding,[],[f16429,f16446,f16445]) ).
fof(f17257,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(definition_unfolding,[],[f16441,f16446,f16445]) ).
fof(f17258,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| ~ hBOOL(hAPP(v_ba,v_s2)) ),
inference(definition_unfolding,[],[f16440,f16446,f16445,f16446]) ).
fof(f17259,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(definition_unfolding,[],[f16439,f16446,f16445]) ).
fof(f17260,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| ~ hBOOL(hAPP(v_ba,v_s2)) ),
inference(definition_unfolding,[],[f16438,f16446,f16445,f16446]) ).
fof(f17261,plain,
( hBOOL(hAPP(v_ba,v_s2))
| ~ v_P(sK489,v_s2) ),
inference(definition_unfolding,[],[f16442,f16446]) ).
fof(f22317,plain,
! [X2,X3,X0,X4] :
( ~ c_Natural_Oevaln(v_ca,X3,X0,X4)
| hBOOL(hAPP(v_ba,X3))
| ~ v_P(X2,X3)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,X0,sK486(X0))
| v_P(X2,X4) ),
inference(consistent_polarity_flipping,[],[f17251]) ).
fof(f22318,plain,
! [X2,X3,X0,X4] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK486(X0)),v_G))
| hBOOL(hAPP(v_ba,X3))
| ~ v_P(X2,X3)
| ~ c_Natural_Oevaln(v_ca,X3,X0,X4)
| v_P(X2,X4) ),
inference(consistent_polarity_flipping,[],[f17252]) ).
fof(f22319,plain,
~ hBOOL(hAPP(v_ba,v_s0)),
inference(consistent_polarity_flipping,[],[f16431]) ).
fof(f22323,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| hBOOL(hAPP(v_ba,v_s2)) ),
inference(consistent_polarity_flipping,[],[f17258]) ).
fof(f22324,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(consistent_polarity_flipping,[],[f17259]) ).
fof(f22325,plain,
! [X1] :
( c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_ba,v_ca)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| hBOOL(hAPP(v_ba,v_s2)) ),
inference(consistent_polarity_flipping,[],[f17260]) ).
fof(f22326,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
| c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0) ),
inference(consistent_polarity_flipping,[],[f16444]) ).
fof(f22327,plain,
( ~ hBOOL(hAPP(v_ba,v_s2))
| ~ v_P(sK489,v_s2) ),
inference(consistent_polarity_flipping,[],[f17261]) ).
fof(f22328,plain,
! [X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| hBOOL(hAPP(v_ba,v_s2)) ),
inference(trivial_inequality_removal,[],[f22325]) ).
fof(f22329,plain,
! [X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(trivial_inequality_removal,[],[f22324]) ).
fof(f22330,plain,
! [X1] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| hBOOL(hAPP(v_ba,v_s2)) ),
inference(trivial_inequality_removal,[],[f22323]) ).
fof(f22331,plain,
! [X1] :
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ),
inference(trivial_inequality_removal,[],[f17257]) ).
fof(f22346,definition,
( spl490_1
<=> v_P(sK489,v_s2) ),
introduced(definition,[new_symbols(definition,[spl490_1])],[avatar_definition]) ).
fof(f22348,plain,
( ~ v_P(sK489,v_s2)
| spl490_1 ),
inference(avatar_component_clause,[],[f22346]) ).
fof(f22350,definition,
( spl490_2
<=> hBOOL(hAPP(v_ba,v_s2)) ),
introduced(definition,[new_symbols(definition,[spl490_2])],[avatar_definition]) ).
fof(f22353,plain,
( ~ spl490_1
| ~ spl490_2 ),
inference(avatar_split_clause,[],[f22327,f22350,f22346]) ).
fof(f22355,definition,
( spl490_3
<=> ! [X1] : ~ v_P(X1,v_s1) ),
introduced(definition,[new_symbols(definition,[spl490_3])],[avatar_definition]) ).
fof(f22356,plain,
( ! [X1] : ~ v_P(X1,v_s1)
| ~ spl490_3 ),
inference(avatar_component_clause,[],[f22355]) ).
fof(f22358,definition,
( spl490_4
<=> hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G)) ),
introduced(definition,[new_symbols(definition,[spl490_4])],[avatar_definition]) ).
fof(f22360,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK488),v_G))
| spl490_4 ),
inference(avatar_component_clause,[],[f22358]) ).
fof(f22361,plain,
( spl490_2
| spl490_3
| ~ spl490_4 ),
inference(avatar_split_clause,[],[f22328,f22358,f22355,f22350]) ).
fof(f22363,definition,
( spl490_5
<=> ! [X1] :
( ~ v_P(X1,v_s1)
| v_P(X1,v_s2) ) ),
introduced(definition,[new_symbols(definition,[spl490_5])],[avatar_definition]) ).
fof(f22364,plain,
( ! [X1] :
( ~ v_P(X1,v_s1)
| v_P(X1,v_s2) )
| ~ spl490_5 ),
inference(avatar_component_clause,[],[f22363]) ).
fof(f22365,plain,
( spl490_5
| ~ spl490_4 ),
inference(avatar_split_clause,[],[f22329,f22358,f22363]) ).
fof(f22367,definition,
( spl490_6
<=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488) ),
introduced(definition,[new_symbols(definition,[spl490_6])],[avatar_definition]) ).
fof(f22369,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| spl490_6 ),
inference(avatar_component_clause,[],[f22367]) ).
fof(f22370,plain,
( spl490_2
| spl490_3
| ~ spl490_6 ),
inference(avatar_split_clause,[],[f22330,f22367,f22355,f22350]) ).
fof(f22371,plain,
( spl490_5
| ~ spl490_6 ),
inference(avatar_split_clause,[],[f22331,f22367,f22363]) ).
fof(f22377,definition,
( spl490_8
<=> ! [X1] : ~ v_P(X1,v_s0) ),
introduced(definition,[new_symbols(definition,[spl490_8])],[avatar_definition]) ).
fof(f22378,plain,
( ! [X1] : ~ v_P(X1,v_s0)
| ~ spl490_8 ),
inference(avatar_component_clause,[],[f22377]) ).
fof(f22389,definition,
( spl490_11
<=> ! [X1] :
( ~ v_P(X1,v_s0)
| v_P(X1,v_s1) ) ),
introduced(definition,[new_symbols(definition,[spl490_11])],[avatar_definition]) ).
fof(f22390,plain,
( ! [X1] :
( ~ v_P(X1,v_s0)
| v_P(X1,v_s1) )
| ~ spl490_11 ),
inference(avatar_component_clause,[],[f22389]) ).
fof(f22458,plain,
( c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK488)
| spl490_4 ),
inference(resolution,[],[f22326,f22360]) ).
fof(f22459,plain,
( $false
| spl490_4
| spl490_6 ),
inference(forward_subsumption_resolution,[],[f22458,f22369]) ).
fof(f22460,plain,
( spl490_4
| spl490_6 ),
inference(avatar_contradiction_clause,[],[f22459]) ).
fof(f22461,plain,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(v_ca,X0,X2,X3)
| ~ v_P(X1,X0)
| hBOOL(hAPP(v_ba,X0))
| v_P(X1,X3)
| c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(X2)) ),
inference(resolution,[],[f22318,f22326]) ).
fof(f22463,plain,
! [X0] :
( ~ v_P(X0,v_s0)
| hBOOL(hAPP(v_ba,v_s0))
| v_P(X0,v_s1)
| c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na)) ),
inference(resolution,[],[f16432,f22461]) ).
fof(f22464,plain,
! [X0] :
( hBOOL(hAPP(v_ba,v_s0))
| ~ v_P(X0,v_s0)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na))
| v_P(X0,v_s1) ),
inference(resolution,[],[f16432,f22317]) ).
fof(f22465,plain,
! [X0] :
( ~ v_P(X0,v_s0)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na))
| v_P(X0,v_s1) ),
inference(forward_subsumption_resolution,[],[f22464,f22319]) ).
fof(f22466,plain,
! [X0] :
( ~ v_P(X0,v_s0)
| v_P(X0,v_s1)
| c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na)) ),
inference(forward_subsumption_resolution,[],[f22463,f22319]) ).
fof(f22467,plain,
( ! [X0] :
( ~ v_P(X0,v_s0)
| ~ c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na)) )
| ~ spl490_3 ),
inference(forward_subsumption_resolution,[],[f22465,f22356]) ).
fof(f22468,plain,
( ! [X0] :
( ~ v_P(X0,v_s0)
| c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na)) )
| ~ spl490_3 ),
inference(forward_subsumption_resolution,[],[f22466,f22356]) ).
fof(f22470,definition,
( spl490_27
<=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK486(v_na)) ),
introduced(definition,[new_symbols(definition,[spl490_27])],[avatar_definition]) ).
fof(f22473,plain,
( ~ spl490_27
| spl490_8
| ~ spl490_3 ),
inference(avatar_split_clause,[],[f22467,f22355,f22377,f22470]) ).
fof(f22474,plain,
( spl490_27
| spl490_8
| ~ spl490_3 ),
inference(avatar_split_clause,[],[f22468,f22355,f22377,f22470]) ).
fof(f22475,plain,
( $false
| ~ spl490_8 ),
inference(backward_subsumption_resolution,[],[f16443,f22378]) ).
fof(f22476,plain,
~ spl490_8,
inference(avatar_contradiction_clause,[],[f22475]) ).
fof(f22477,plain,
( ~ spl490_27
| spl490_11 ),
inference(avatar_split_clause,[],[f22465,f22389,f22470]) ).
fof(f22478,plain,
( spl490_27
| spl490_11 ),
inference(avatar_split_clause,[],[f22466,f22389,f22470]) ).
fof(f22479,plain,
( v_P(sK489,v_s1)
| ~ spl490_11 ),
inference(resolution,[],[f22390,f16443]) ).
fof(f22480,plain,
( v_P(sK489,v_s2)
| ~ spl490_5
| ~ spl490_11 ),
inference(resolution,[],[f22479,f22364]) ).
fof(f22481,plain,
( $false
| spl490_1
| ~ spl490_5
| ~ spl490_11 ),
inference(forward_subsumption_resolution,[],[f22480,f22348]) ).
fof(f22482,plain,
( spl490_1
| ~ spl490_5
| ~ spl490_11 ),
inference(avatar_contradiction_clause,[],[f22481]) ).
cnf(s1,plain,
( ~ spl490_1
| ~ spl490_2 ),
inference(sat_conversion,[],[f22353]) ).
cnf(s2,plain,
( spl490_2
| spl490_3
| ~ spl490_4 ),
inference(sat_conversion,[],[f22361]) ).
cnf(s3,plain,
( ~ spl490_4
| spl490_5 ),
inference(sat_conversion,[],[f22365]) ).
cnf(s4,plain,
( spl490_2
| spl490_3
| ~ spl490_6 ),
inference(sat_conversion,[],[f22370]) ).
cnf(s5,plain,
( spl490_5
| ~ spl490_6 ),
inference(sat_conversion,[],[f22371]) ).
cnf(s20,plain,
( spl490_4
| spl490_6 ),
inference(sat_conversion,[],[f22460]) ).
cnf(s21,plain,
( ~ spl490_3
| spl490_8
| ~ spl490_27 ),
inference(sat_conversion,[],[f22473]) ).
cnf(s22,plain,
( ~ spl490_3
| spl490_8
| spl490_27 ),
inference(sat_conversion,[],[f22474]) ).
cnf(s23,plain,
~ spl490_8,
inference(sat_conversion,[],[f22476]) ).
cnf(s24,plain,
( spl490_11
| ~ spl490_27 ),
inference(sat_conversion,[],[f22477]) ).
cnf(s25,plain,
( spl490_11
| spl490_27 ),
inference(sat_conversion,[],[f22478]) ).
cnf(s26,plain,
( spl490_1
| ~ spl490_5
| ~ spl490_11 ),
inference(sat_conversion,[],[f22482]) ).
cnf(s27,plain,
( ~ spl490_3
| spl490_27 ),
inference(rat,[],[s22,s23]) ).
cnf(s28,plain,
( ~ spl490_3
| ~ spl490_27 ),
inference(rat,[],[s21,s23]) ).
cnf(s32,plain,
( spl490_3
| spl490_2 ),
inference(rat,[],[s20,s2,s4]) ).
cnf(s33,plain,
~ spl490_3,
inference(rat,[],[s28,s27]) ).
cnf(s34,plain,
spl490_2,
inference(rat,[],[s32,s33]) ).
cnf(s35,plain,
spl490_11,
inference(rat,[],[s24,s25]) ).
cnf(s36,plain,
spl490_5,
inference(rat,[],[s20,s3,s5]) ).
cnf(s37,plain,
~ spl490_1,
inference(rat,[],[s1,s34]) ).
cnf(s38,plain,
$false,
inference(rat,[],[s26,s37,s35,s36]) ).
fof(f22483,plain,
$false,
inference(avatar_sat_refutation,[],[s38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW328+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n005.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 13:35:46 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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
% 2.25/0.75 % (785158)Will run a generic schedule for satisfiability detection.
% 2.25/0.75 % (785169)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=581466837:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 2.25/0.75 % (785164)% WARNING: option uhcvi not known.
% 2.25/0.75 % (785168)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2702108591:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 2.25/0.75 % (785165)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2970405962:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 2.25/0.75 % (785164)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2585081022:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 2.25/0.75 % (785166)dis+10_1_sil=32000:sp=arity:random_seed=922655178:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 2.25/0.75 % (785167)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2787171840:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 2.25/0.75 % (785163)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2843044416_2998 on theBenchmark for (2998ds/0Mi)
% 2.25/0.75 % (785169)Instruction limit reached!
% 2.25/0.75 % (785169)------------------------------
% 2.25/0.75 % (785169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785169)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785169)Termination reason: Instruction limit
% 2.25/0.75 % (785169)Termination phase: Property scanning
% 2.25/0.75 % (785169)Time elapsed: 0.053 s
% 2.25/0.75 % (785169)Peak memory usage: 22 MB
% 2.25/0.75 % (785169)Instructions burned: 159 (million)
% 2.25/0.75 % (785177)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=362848475:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 2.25/0.75 % (785166)Instruction limit reached!
% 2.25/0.75 % (785166)------------------------------
% 2.25/0.75 % (785166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785166)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785166)Termination reason: Instruction limit
% 2.25/0.75 % (785166)Termination phase: Preprocessing 3
% 2.25/0.75 % (785166)Time elapsed: 0.064 s
% 2.25/0.75 % (785166)Peak memory usage: 20 MB
% 2.25/0.75 % (785166)Instructions burned: 104 (million)
% 2.25/0.75 % (785167)Instruction limit reached!
% 2.25/0.75 % (785167)------------------------------
% 2.25/0.75 % (785167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785167)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785167)Termination reason: Instruction limit
% 2.25/0.75 % (785167)Termination phase: NewCNF
% 2.25/0.75 % (785167)Time elapsed: 0.074 s
% 2.25/0.75 % (785167)Peak memory usage: 21 MB
% 2.25/0.75 % (785167)Instructions burned: 117 (million)
% 2.25/0.75 % (785168)Instruction limit reached!
% 2.25/0.75 % (785168)------------------------------
% 2.25/0.75 % (785168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785168)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785168)Termination reason: Instruction limit
% 2.25/0.75 % (785168)Termination phase: Preprocessing 3
% 2.25/0.75 % (785168)Time elapsed: 0.079 s
% 2.25/0.75 % (785168)Peak memory usage: 20 MB
% 2.25/0.75 % (785168)Instructions burned: 131 (million)
% 2.25/0.75 % (785179)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3245165749:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 2.25/0.75 % (785180)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=3404978469:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 2.25/0.75 % (785181)ott-21_1_sil=16000:fs=off:random_seed=2963389193:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 2.25/0.75 % (785179)Instruction limit reached!
% 2.25/0.75 % (785179)------------------------------
% 2.25/0.75 % (785179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785179)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785179)Termination reason: Instruction limit
% 2.25/0.75 % (785179)Termination phase: Preprocessing 3
% 2.25/0.75 % (785179)Time elapsed: 0.078 s
% 2.25/0.75 % (785179)Peak memory usage: 20 MB
% 2.25/0.75 % (785179)Instructions burned: 132 (million)
% 2.25/0.75 % (785185)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=190434281:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 2.25/0.75 % (785181)Instruction limit reached!
% 2.25/0.75 % (785181)------------------------------
% 2.25/0.75 % (785181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785181)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785181)Termination reason: Instruction limit
% 2.25/0.75 % (785181)Termination phase: Property scanning
% 2.25/0.75 % (785181)Time elapsed: 0.103 s
% 2.25/0.75 % (785181)Peak memory usage: 21 MB
% 2.25/0.75 % (785181)Instructions burned: 181 (million)
% 2.25/0.75 % (785187)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=734857724:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 2.25/0.75 % (785177)Instruction limit reached!
% 2.25/0.75 % (785177)------------------------------
% 2.25/0.75 % (785177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.75 % (785177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.75 % (785177)CaDiCaL version: 2.1.3
% 2.25/0.75 % (785177)Termination reason: Instruction limit
% 2.25/0.75 % (785177)Termination phase: Finite model building preprocessing
% 2.25/0.75 % (785177)Time elapsed: 0.179 s
% 2.25/0.75 % (785177)Peak memory usage: 25 MB
% 2.25/0.75 % (785177)Instructions burned: 716 (million)
% 2.25/0.75 % (785189)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=474304515:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 2.25/0.75 % (785164) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-785158-785164"...
% 2.25/0.75 % (785164)...printing done.
% 2.25/0.75 % (785164)Refutation found. Thanks to Tanya!
% 2.25/0.75 % SZS status Theorem for theBenchmark
% 2.25/0.75 % SZS output start Proof for theBenchmark
% See solution above
% 2.25/0.76 % (785164)------------------------------
% 2.25/0.76 % (785164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.25/0.76 % (785164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.76 % (785164)CaDiCaL version: 2.1.3
% 2.25/0.76 % (785164)Termination reason: Refutation
% 2.25/0.76 % (785164)Time elapsed: 0.335 s
% 2.25/0.76 % (785164)Peak memory usage: 26 MB
% 2.25/0.76 % (785164)Instructions burned: 709 (million)
% 2.25/0.76 % (785158)Success in time 0.529 s
% 2.25/0.76 % Vampire exiting
%------------------------------------------------------------------------------