%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW474+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:40:11 PM UTC 2026
% Result : Theorem 6.41s 1.27s
% Output : Refutation 6.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 66 ( 30 unt; 5 def)
% Number of atoms : 132 ( 17 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 127 ( 61 ~; 54 |; 0 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 12 con; 0-2 aty)
% Number of variables : 52 ( 0 sgn 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f55,axiom,
! [X0] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),bot_bo1055319631e_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_empty) ).
fof(f59,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
=> ( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_cut) ).
fof(f108,axiom,
! [X0] :
( hBOOL(hoare_298929751gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP_com_bool(wt,X0))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_MGF) ).
fof(f232,axiom,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_Collect__def) ).
fof(f268,axiom,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,hAPP_H1645666623e_bool(fequal1531560888_state,X0)) = hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_singleton__conv2) ).
fof(f270,axiom,
! [X0,X1] :
( hBOOL(wT_bodies)
=> ( hAPP_p799580910on_com(body,X0) = some_com(X1)
=> hBOOL(hAPP_com_bool(wt,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_WT__bodiesD) ).
fof(f458,axiom,
! [X0] : set_Ho1831989999_state(some_H1133819688_state(X0)) = hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_403_Option_Oset_Osimps_I2_J) ).
fof(f861,axiom,
hBOOL(hoare_298929751gleton),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f862,axiom,
hBOOL(wT_bodies),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(f866,axiom,
hAPP_p799580910on_com(body,pn) = some_com(y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5) ).
fof(f868,conjecture,
hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_7) ).
fof(f869,negated_conjecture,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(negated_conjecture,[status(cth)],[f868]) ).
fof(f876,plain,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(flattening,[],[f869]) ).
fof(f900,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2)) ),
inference(ennf_transformation,[],[f59]) ).
fof(f901,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2)) ),
inference(flattening,[],[f900]) ).
fof(f958,plain,
! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_298929751gleton) ),
inference(ennf_transformation,[],[f108]) ).
fof(f959,plain,
! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_298929751gleton) ),
inference(flattening,[],[f958]) ).
fof(f1082,plain,
! [X0,X1] :
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| ~ hBOOL(wT_bodies) ),
inference(ennf_transformation,[],[f270]) ).
fof(f1083,plain,
! [X0,X1] :
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| ~ hBOOL(wT_bodies) ),
inference(flattening,[],[f1082]) ).
fof(f1633,plain,
! [X0] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),bot_bo1055319631e_bool)),
inference(cnf_transformation,[],[f55]) ).
fof(f1637,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2)) ),
inference(cnf_transformation,[],[f901]) ).
fof(f1693,plain,
! [X0] :
( ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ),
inference(cnf_transformation,[],[f959]) ).
fof(f1888,plain,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,X0) = X0,
inference(cnf_transformation,[],[f232]) ).
fof(f1943,plain,
! [X0] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = hAPP_f921536533e_bool(collec727977250_state,hAPP_H1645666623e_bool(fequal1531560888_state,X0)),
inference(cnf_transformation,[],[f268]) ).
fof(f1947,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| hBOOL(hAPP_com_bool(wt,X1)) ),
inference(cnf_transformation,[],[f1083]) ).
fof(f2318,plain,
! [X0] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = set_Ho1831989999_state(some_H1133819688_state(X0)),
inference(cnf_transformation,[],[f458]) ).
fof(f2880,plain,
hBOOL(hoare_298929751gleton),
inference(cnf_transformation,[],[f861]) ).
fof(f2881,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[],[f862]) ).
fof(f2885,plain,
hAPP_p799580910on_com(body,pn) = some_com(y),
inference(cnf_transformation,[],[f866]) ).
fof(f2887,plain,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(cnf_transformation,[],[f876]) ).
fof(f3049,definition,
( spl167_6
<=> hBOOL(hoare_298929751gleton) ),
introduced(definition,[new_symbols(definition,[spl167_6])],[avatar_definition]) ).
fof(f3120,definition,
( spl167_21
<=> ! [X0,X1] :
( hAPP_p799580910on_com(body,X0) != some_com(X1)
| hBOOL(hAPP_com_bool(wt,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl167_21])],[avatar_definition]) ).
fof(f3121,plain,
( ! [X0,X1] :
( hAPP_p799580910on_com(body,X0) != some_com(X1)
| hBOOL(hAPP_com_bool(wt,X1)) )
| ~ spl167_21 ),
inference(avatar_component_clause,[],[f3120]) ).
fof(f3123,definition,
( spl167_22
<=> hBOOL(wT_bodies) ),
introduced(definition,[new_symbols(definition,[spl167_22])],[avatar_definition]) ).
fof(f3126,plain,
( spl167_21
| ~ spl167_22 ),
inference(avatar_split_clause,[],[f1947,f3123,f3120]) ).
fof(f3152,definition,
( spl167_28
<=> ! [X0] :
( ~ hBOOL(hAPP_com_bool(wt,X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ) ),
introduced(definition,[new_symbols(definition,[spl167_28])],[avatar_definition]) ).
fof(f3153,plain,
( ! [X0] :
( ~ hBOOL(hAPP_com_bool(wt,X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) )
| ~ spl167_28 ),
inference(avatar_component_clause,[],[f3152]) ).
fof(f3154,plain,
( spl167_28
| ~ spl167_22
| ~ spl167_6 ),
inference(avatar_split_clause,[],[f1693,f3049,f3123,f3152]) ).
fof(f3163,plain,
spl167_6,
inference(avatar_split_clause,[],[f2880,f3049]) ).
fof(f3164,plain,
spl167_22,
inference(avatar_split_clause,[],[f2881,f3123]) ).
fof(f3635,plain,
( ! [X0] :
( some_com(X0) != some_com(y)
| hBOOL(hAPP_com_bool(wt,X0)) )
| ~ spl167_21 ),
inference(superposition,[],[f3121,f2885]) ).
fof(f3653,plain,
( hBOOL(hAPP_com_bool(wt,y))
| ~ spl167_21 ),
inference(equality_resolution,[],[f3635]) ).
fof(f3695,plain,
! [X0] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = hAPP_H1645666623e_bool(fequal1531560888_state,X0),
inference(forward_demodulation,[],[f1943,f1888]) ).
fof(f3698,plain,
! [X0] : hAPP_H1645666623e_bool(fequal1531560888_state,X0) = set_Ho1831989999_state(some_H1133819688_state(X0)),
inference(superposition,[],[f3695,f2318]) ).
fof(f3699,plain,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)))),
inference(superposition,[],[f2887,f3695]) ).
fof(f8049,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X0)) ),
inference(resolution,[],[f1637,f1633]) ).
fof(f8617,plain,
( ! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),set_Ho1831989999_state(some_H1133819688_state(hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP_com_bool(wt,X0)) )
| ~ spl167_28 ),
inference(forward_demodulation,[],[f3153,f2318]) ).
fof(f8618,plain,
( ! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0))))
| ~ hBOOL(hAPP_com_bool(wt,X0)) )
| ~ spl167_28 ),
inference(forward_demodulation,[],[f8617,f3698]) ).
fof(f16369,definition,
( spl167_125
<=> ! [X0,X1] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X1))))
| ~ hBOOL(hAPP_com_bool(wt,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl167_125])],[avatar_definition]) ).
fof(f16370,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP_com_bool(wt,X1))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X1)))) )
| ~ spl167_125 ),
inference(avatar_component_clause,[],[f16369]) ).
fof(f17028,plain,
( ! [X0] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y))))
| ~ spl167_21
| ~ spl167_125 ),
inference(resolution,[],[f16370,f3653]) ).
fof(f17047,plain,
( $false
| ~ spl167_21
| ~ spl167_125 ),
inference(backward_subsumption_resolution,[],[f3699,f17028]) ).
fof(f17056,plain,
( ~ spl167_21
| ~ spl167_125 ),
inference(avatar_contradiction_clause,[],[f17047]) ).
fof(f27497,plain,
( ! [X0,X1] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X1))))
| ~ hBOOL(hAPP_com_bool(wt,X1)) )
| ~ spl167_28 ),
inference(resolution,[],[f8049,f8618]) ).
fof(f27537,plain,
( spl167_125
| ~ spl167_28 ),
inference(avatar_split_clause,[],[f27497,f3152,f16369]) ).
cnf(s24,plain,
( spl167_21
| ~ spl167_22 ),
inference(sat_conversion,[],[f3126]) ).
cnf(s34,plain,
( ~ spl167_6
| ~ spl167_22
| spl167_28 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s40,plain,
spl167_6,
inference(sat_conversion,[],[f3163]) ).
cnf(s41,plain,
spl167_22,
inference(sat_conversion,[],[f3164]) ).
cnf(s731,plain,
( ~ spl167_21
| ~ spl167_125 ),
inference(sat_conversion,[],[f17056]) ).
cnf(s791,plain,
( ~ spl167_28
| spl167_125 ),
inference(sat_conversion,[],[f27537]) ).
cnf(s824,plain,
spl167_28,
inference(rat,[],[s34,s41,s40]) ).
cnf(s825,plain,
spl167_125,
inference(rat,[],[s791,s824]) ).
cnf(s827,plain,
~ spl167_21,
inference(rat,[],[s731,s825]) ).
cnf(s834,plain,
$false,
inference(rat,[],[s24,s41,s827]) ).
fof(f27538,plain,
$false,
inference(avatar_sat_refutation,[],[s834]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW474+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n003.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 14:10:12 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 6.41/1.27 % (1604349)Will run a generic schedule for satisfiability detection.
% 6.41/1.27 % (1604357)dis+10_1_sil=32000:sp=arity:random_seed=4177037118:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.41/1.27 % (1604355)% WARNING: option uhcvi not known.
% 6.41/1.27 % (1604355)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=518096586:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.41/1.27 % (1604356)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2308081703:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.41/1.27 % (1604354)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2812768780_2999 on theBenchmark for (2999ds/0Mi)
% 6.41/1.27 % (1604358)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3118328672:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.41/1.27 % (1604359)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=617017477:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.41/1.27 % (1604360)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1653325632:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.41/1.27 % (1604357)Instruction limit reached!
% 6.41/1.27 % (1604357)------------------------------
% 6.41/1.27 % (1604357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604357)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604357)Termination reason: Instruction limit
% 6.41/1.27 % (1604357)Termination phase: Saturation
% 6.41/1.27 % (1604357)Time elapsed: 0.027 s
% 6.41/1.27 % (1604357)Peak memory usage: 14 MB
% 6.41/1.27 % (1604357)Instructions burned: 103 (million)
% 6.41/1.27 % (1604368)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1018194032:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.41/1.27 % (1604358)Instruction limit reached!
% 6.41/1.27 % (1604358)------------------------------
% 6.41/1.27 % (1604358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604358)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604358)Termination reason: Instruction limit
% 6.41/1.27 % (1604358)Termination phase: Saturation
% 6.41/1.27 % (1604358)Time elapsed: 0.055 s
% 6.41/1.27 % (1604358)Peak memory usage: 14 MB
% 6.41/1.27 % (1604358)Instructions burned: 118 (million)
% 6.41/1.27 % (1604370)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2503167825:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.41/1.27 % (1604360)Instruction limit reached!
% 6.41/1.27 % (1604360)------------------------------
% 6.41/1.27 % (1604360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604360)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604360)Termination reason: Instruction limit
% 6.41/1.27 % (1604360)Termination phase: Saturation
% 6.41/1.27 % (1604360)Time elapsed: 0.088 s
% 6.41/1.27 % (1604360)Peak memory usage: 15 MB
% 6.41/1.27 % (1604360)Instructions burned: 159 (million)
% 6.41/1.27 % (1604372)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=3544803649:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.41/1.27 % (1604359)Instruction limit reached!
% 6.41/1.27 % (1604359)------------------------------
% 6.41/1.27 % (1604359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604359)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604359)Termination reason: Instruction limit
% 6.41/1.27 % (1604359)Termination phase: Saturation
% 6.41/1.27 % (1604359)Time elapsed: 0.114 s
% 6.41/1.27 % (1604359)Peak memory usage: 15 MB
% 6.41/1.27 % (1604359)Instructions burned: 131 (million)
% 6.41/1.27 % (1604374)ott-21_1_sil=16000:fs=off:random_seed=2678837842:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.41/1.27 % (1604370)Instruction limit reached!
% 6.41/1.27 % (1604370)------------------------------
% 6.41/1.27 % (1604370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604370)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604370)Termination reason: Instruction limit
% 6.41/1.27 % (1604370)Termination phase: Saturation
% 6.41/1.27 % (1604370)Time elapsed: 0.065 s
% 6.41/1.27 % (1604370)Peak memory usage: 14 MB
% 6.41/1.27 % (1604370)Instructions burned: 132 (million)
% 6.41/1.27 % (1604381)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2343001477:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.41/1.27 % (1604368)Instruction limit reached!
% 6.41/1.27 % (1604368)------------------------------
% 6.41/1.27 % (1604368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604368)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604368)Termination reason: Instruction limit
% 6.41/1.27 % (1604368)Termination phase: Finite model building preprocessing
% 6.41/1.27 % (1604368)Time elapsed: 0.179 s
% 6.41/1.27 % (1604368)Peak memory usage: 23 MB
% 6.41/1.27 % (1604368)Instructions burned: 716 (million)
% 6.41/1.27 % (1604400)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2150277143:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.41/1.27 % (1604374)Instruction limit reached!
% 6.41/1.27 % (1604374)------------------------------
% 6.41/1.27 % (1604374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604374)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604374)Termination reason: Instruction limit
% 6.41/1.27 % (1604374)Termination phase: Saturation
% 6.41/1.27 % (1604374)Time elapsed: 0.093 s
% 6.41/1.27 % (1604374)Peak memory usage: 14 MB
% 6.41/1.27 % (1604374)Instructions burned: 181 (million)
% 6.41/1.27 % (1604408)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3908917840:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 6.41/1.27 % TRYING [1]
% 6.41/1.27 % (1604381)Instruction limit reached!
% 6.41/1.27 % (1604381)------------------------------
% 6.41/1.27 % (1604381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604381)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604381)Termination reason: Instruction limit
% 6.41/1.27 % (1604381)Termination phase: Saturation
% 6.41/1.27 % (1604381)Time elapsed: 0.281 s
% 6.41/1.27 % (1604381)Peak memory usage: 16 MB
% 6.41/1.27 % (1604381)Instructions burned: 477 (million)
% 6.41/1.27 % TRYING [2]
% 6.41/1.27 % (1604467)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4086013583:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.41/1.27 % (1604400)Instruction limit reached!
% 6.41/1.27 % (1604400)------------------------------
% 6.41/1.27 % (1604400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604400)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604400)Termination reason: Instruction limit
% 6.41/1.27 % (1604400)Termination phase: Finite model building preprocessing
% 6.41/1.27 % (1604400)Time elapsed: 0.243 s
% 6.41/1.27 % (1604400)Peak memory usage: 27 MB
% 6.41/1.27 % (1604400)Instructions burned: 866 (million)
% 6.41/1.27 % (1604480)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=932840661: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)
% 6.41/1.27 % (1604372)Instruction limit reached!
% 6.41/1.27 % (1604372)------------------------------
% 6.41/1.27 % (1604372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604372)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604372)Termination reason: Instruction limit
% 6.41/1.27 % (1604372)Termination phase: Saturation
% 6.41/1.27 % (1604372)Time elapsed: 0.396 s
% 6.41/1.27 % (1604372)Peak memory usage: 19 MB
% 6.41/1.27 % (1604372)Instructions burned: 685 (million)
% 6.41/1.27 % (1604489)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1846505602:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.41/1.27 % TRYING [3]
% 6.41/1.27 % (1604480)Instruction limit reached!
% 6.41/1.27 % (1604480)------------------------------
% 6.41/1.27 % (1604480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604480)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604480)Termination reason: Instruction limit
% 6.41/1.27 % (1604480)Termination phase: Saturation
% 6.41/1.27 % (1604480)Time elapsed: 0.218 s
% 6.41/1.27 % (1604480)Peak memory usage: 20 MB
% 6.41/1.27 % (1604480)Instructions burned: 692 (million)
% 6.41/1.27 % (1604518)fmb+10_1_sil=64000:random_seed=1232247052:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 6.41/1.27 % (1604467)Instruction limit reached!
% 6.41/1.27 % (1604467)------------------------------
% 6.41/1.27 % (1604467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604467)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604467)Termination reason: Instruction limit
% 6.41/1.27 % (1604467)Termination phase: Finite model building preprocessing
% 6.41/1.27 % (1604467)Time elapsed: 0.422 s
% 6.41/1.27 % (1604467)Peak memory usage: 27 MB
% 6.41/1.27 % (1604467)Instructions burned: 890 (million)
% 6.41/1.27 % (1604520)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2369936159:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.41/1.27 % TRYING [1]
% 6.41/1.27 % TRYING [2]
% 6.41/1.27 % (1604355) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1604349-1604355"...
% 6.41/1.27 % (1604355)...printing done.
% 6.41/1.27 % (1604355)Refutation found. Thanks to Tanya!
% 6.41/1.27 % SZS status Theorem for theBenchmark
% 6.41/1.27 % SZS output start Proof for theBenchmark
% See solution above
% 6.41/1.27 % (1604355)------------------------------
% 6.41/1.27 % (1604355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.41/1.27 % (1604355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.27 % (1604355)CaDiCaL version: 2.1.3
% 6.41/1.27 % (1604355)Termination reason: Refutation
% 6.41/1.27 % (1604355)Time elapsed: 0.944 s
% 6.41/1.27 % (1604355)Peak memory usage: 27 MB
% 6.41/1.27 % (1604355)Instructions burned: 1509 (million)
% 6.41/1.27 % (1604349)Success in time 1.04 s
% 6.41/1.27 % Vampire exiting
%------------------------------------------------------------------------------