%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW295+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 : n016.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:46 PM UTC 2026
% Result : Theorem 12.35s 2.33s
% Output : Refutation 12.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of formulae : 86 ( 8 unt; 8 def)
% Number of atoms : 234 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 258 ( 110 ~; 122 |; 0 &)
% ( 12 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 9 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 66 ( 0 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0)
=> c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_evaln_OBody) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0)
<=> c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_evaln_Oequations_I9_J) ).
fof(f5205,conjecture,
( ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
=> v_Q(X0,X2) ) )
<=> ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_Q(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f5206,negated_conjecture,
~ ( ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
=> v_Q(X0,X2) ) )
<=> ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X1,hAPP(c_Nat_OSuc,v_n),X2)
=> v_Q(X0,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f5205]) ).
fof(f5225,plain,
~ ( ! [X0,X1] :
( v_P(X0,X1)
=> ! [X2] :
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
=> v_Q(X0,X2) ) )
<=> ! [X3,X4] :
( v_P(X3,X4)
=> ! [X5] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5)
=> v_Q(X3,X5) ) ) ),
inference(rectify,[],[f5206]) ).
fof(f5411,plain,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f9453,plain,
( ! [X0,X1] :
( ! [X2] :
( v_Q(X0,X2)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2) )
| ~ v_P(X0,X1) )
<~> ! [X3,X4] :
( ! [X5] :
( v_Q(X3,X5)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5) )
| ~ v_P(X3,X4) ) ),
inference(ennf_transformation,[],[f5225]) ).
fof(f9455,plain,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0) ),
inference(cnf_transformation,[],[f5411]) ).
fof(f9457,plain,
! [X2,X3,X0,X1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X3),X2,hAPP(c_Nat_OSuc,X1),X0)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,X3)),X2,X1,X0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f16409,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK484,hAPP(c_Nat_OSuc,v_n),sK486)
| v_P(sK481,sK482) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16410,plain,
( ~ v_Q(sK483,sK486)
| v_P(sK481,sK482) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16411,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v_P(X3,X4)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5)
| v_Q(X3,X5)
| ~ v_P(X0,X1)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
| v_Q(X0,X2) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16412,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK484,hAPP(c_Nat_OSuc,v_n),sK486)
| ~ v_Q(sK481,sK485) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16413,plain,
( ~ v_Q(sK483,sK486)
| ~ v_Q(sK481,sK485) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16414,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK484,hAPP(c_Nat_OSuc,v_n),sK486)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK482,v_n,sK485) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16415,plain,
( ~ v_Q(sK483,sK486)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK482,v_n,sK485) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16416,plain,
( v_P(sK483,sK484)
| c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK482,v_n,sK485) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16417,plain,
( v_P(sK483,sK484)
| ~ v_Q(sK481,sK485) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f16418,plain,
( v_P(sK483,sK484)
| v_P(sK481,sK482) ),
inference(cnf_transformation,[],[f9453]) ).
fof(f18881,definition,
( spl487_1
<=> v_P(sK481,sK482) ),
introduced(definition,[new_symbols(definition,[spl487_1])],[avatar_definition]) ).
fof(f18883,plain,
( v_P(sK481,sK482)
| ~ spl487_1 ),
inference(avatar_component_clause,[],[f18881]) ).
fof(f18885,definition,
( spl487_2
<=> c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK484,hAPP(c_Nat_OSuc,v_n),sK486) ),
introduced(definition,[new_symbols(definition,[spl487_2])],[avatar_definition]) ).
fof(f18887,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK484,hAPP(c_Nat_OSuc,v_n),sK486)
| ~ spl487_2 ),
inference(avatar_component_clause,[],[f18885]) ).
fof(f18888,plain,
( spl487_1
| spl487_2 ),
inference(avatar_split_clause,[],[f16409,f18885,f18881]) ).
fof(f18890,definition,
( spl487_3
<=> v_Q(sK483,sK486) ),
introduced(definition,[new_symbols(definition,[spl487_3])],[avatar_definition]) ).
fof(f18892,plain,
( ~ v_Q(sK483,sK486)
| spl487_3 ),
inference(avatar_component_clause,[],[f18890]) ).
fof(f18893,plain,
( spl487_1
| ~ spl487_3 ),
inference(avatar_split_clause,[],[f16410,f18890,f18881]) ).
fof(f18895,definition,
( spl487_4
<=> ! [X2,X0,X1] :
( ~ v_P(X0,X1)
| v_Q(X0,X2)
| ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2) ) ),
introduced(definition,[new_symbols(definition,[spl487_4])],[avatar_definition]) ).
fof(f18896,plain,
( ! [X2,X0,X1] :
( ~ c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),X1,v_n,X2)
| v_Q(X0,X2)
| ~ v_P(X0,X1) )
| ~ spl487_4 ),
inference(avatar_component_clause,[],[f18895]) ).
fof(f18898,definition,
( spl487_5
<=> ! [X4,X5,X3] :
( ~ v_P(X3,X4)
| v_Q(X3,X5)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5) ) ),
introduced(definition,[new_symbols(definition,[spl487_5])],[avatar_definition]) ).
fof(f18899,plain,
( ! [X3,X4,X5] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X4,hAPP(c_Nat_OSuc,v_n),X5)
| v_Q(X3,X5)
| ~ v_P(X3,X4) )
| ~ spl487_5 ),
inference(avatar_component_clause,[],[f18898]) ).
fof(f18900,plain,
( spl487_4
| spl487_5 ),
inference(avatar_split_clause,[],[f16411,f18898,f18895]) ).
fof(f18902,definition,
( spl487_6
<=> v_Q(sK481,sK485) ),
introduced(definition,[new_symbols(definition,[spl487_6])],[avatar_definition]) ).
fof(f18904,plain,
( ~ v_Q(sK481,sK485)
| spl487_6 ),
inference(avatar_component_clause,[],[f18902]) ).
fof(f18905,plain,
( ~ spl487_6
| spl487_2 ),
inference(avatar_split_clause,[],[f16412,f18885,f18902]) ).
fof(f18906,plain,
( ~ spl487_6
| ~ spl487_3 ),
inference(avatar_split_clause,[],[f16413,f18890,f18902]) ).
fof(f18908,definition,
( spl487_7
<=> c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK482,v_n,sK485) ),
introduced(definition,[new_symbols(definition,[spl487_7])],[avatar_definition]) ).
fof(f18910,plain,
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK482,v_n,sK485)
| ~ spl487_7 ),
inference(avatar_component_clause,[],[f18908]) ).
fof(f18911,plain,
( spl487_7
| spl487_2 ),
inference(avatar_split_clause,[],[f16414,f18885,f18908]) ).
fof(f18912,plain,
( spl487_7
| ~ spl487_3 ),
inference(avatar_split_clause,[],[f16415,f18890,f18908]) ).
fof(f18914,definition,
( spl487_8
<=> v_P(sK483,sK484) ),
introduced(definition,[new_symbols(definition,[spl487_8])],[avatar_definition]) ).
fof(f18916,plain,
( v_P(sK483,sK484)
| ~ spl487_8 ),
inference(avatar_component_clause,[],[f18914]) ).
fof(f18917,plain,
( spl487_7
| spl487_8 ),
inference(avatar_split_clause,[],[f16416,f18914,f18908]) ).
fof(f18918,plain,
( ~ spl487_6
| spl487_8 ),
inference(avatar_split_clause,[],[f16417,f18914,f18902]) ).
fof(f18919,plain,
( spl487_1
| spl487_8 ),
inference(avatar_split_clause,[],[f16418,f18914,f18881]) ).
fof(f33268,plain,
( ! [X0] :
( v_Q(X0,sK485)
| ~ v_P(X0,sK482) )
| ~ spl487_4
| ~ spl487_7 ),
inference(resolution,[],[f18910,f18896]) ).
fof(f33274,plain,
( ~ v_P(sK481,sK482)
| ~ spl487_4
| spl487_6
| ~ spl487_7 ),
inference(resolution,[],[f33268,f18904]) ).
fof(f33275,plain,
( $false
| ~ spl487_1
| ~ spl487_4
| spl487_6
| ~ spl487_7 ),
inference(forward_subsumption_resolution,[],[f33274,f18883]) ).
fof(f33276,plain,
( ~ spl487_1
| ~ spl487_4
| spl487_6
| ~ spl487_7 ),
inference(avatar_contradiction_clause,[],[f33275]) ).
fof(f47023,plain,
( c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),sK482,hAPP(c_Nat_OSuc,v_n),sK485)
| ~ spl487_7 ),
inference(resolution,[],[f9455,f18910]) ).
fof(f48891,plain,
( ! [X0] :
( v_Q(X0,sK486)
| ~ v_P(X0,sK484) )
| ~ spl487_2
| ~ spl487_5 ),
inference(resolution,[],[f18887,f18899]) ).
fof(f48892,plain,
( c_Natural_Oevaln(hAPP(c_Option_Othe(tc_Com_Ocom),hAPP(c_Com_Obody,v_pn)),sK484,v_n,sK486)
| ~ spl487_2 ),
inference(resolution,[],[f18887,f9457]) ).
fof(f49321,plain,
( ~ v_P(sK483,sK484)
| ~ spl487_2
| spl487_3
| ~ spl487_5 ),
inference(resolution,[],[f48891,f18892]) ).
fof(f55273,plain,
( ! [X0] :
( v_Q(X0,sK486)
| ~ v_P(X0,sK484) )
| ~ spl487_2
| ~ spl487_4 ),
inference(resolution,[],[f48892,f18896]) ).
fof(f55540,plain,
( ~ v_P(sK483,sK484)
| ~ spl487_2
| spl487_3
| ~ spl487_4 ),
inference(resolution,[],[f55273,f18892]) ).
fof(f55541,plain,
( $false
| ~ spl487_2
| spl487_3
| ~ spl487_4
| ~ spl487_8 ),
inference(forward_subsumption_resolution,[],[f55540,f18916]) ).
fof(f55542,plain,
( ~ spl487_2
| spl487_3
| ~ spl487_4
| ~ spl487_8 ),
inference(avatar_contradiction_clause,[],[f55541]) ).
fof(f55543,plain,
( ~ spl487_8
| ~ spl487_2
| spl487_3
| ~ spl487_5 ),
inference(avatar_split_clause,[],[f49321,f18898,f18890,f18885,f18914]) ).
fof(f56409,plain,
( ! [X0] :
( v_Q(X0,sK485)
| ~ v_P(X0,sK482) )
| ~ spl487_5
| ~ spl487_7 ),
inference(resolution,[],[f47023,f18899]) ).
fof(f56531,plain,
( ~ v_P(sK481,sK482)
| ~ spl487_5
| spl487_6
| ~ spl487_7 ),
inference(resolution,[],[f56409,f18904]) ).
fof(f56532,plain,
( $false
| ~ spl487_1
| ~ spl487_5
| spl487_6
| ~ spl487_7 ),
inference(forward_subsumption_resolution,[],[f56531,f18883]) ).
fof(f56533,plain,
( ~ spl487_1
| ~ spl487_5
| spl487_6
| ~ spl487_7 ),
inference(avatar_contradiction_clause,[],[f56532]) ).
cnf(s1,plain,
( spl487_1
| spl487_2 ),
inference(sat_conversion,[],[f18888]) ).
cnf(s2,plain,
( spl487_1
| ~ spl487_3 ),
inference(sat_conversion,[],[f18893]) ).
cnf(s3,plain,
( spl487_4
| spl487_5 ),
inference(sat_conversion,[],[f18900]) ).
cnf(s4,plain,
( spl487_2
| ~ spl487_6 ),
inference(sat_conversion,[],[f18905]) ).
cnf(s5,plain,
( ~ spl487_3
| ~ spl487_6 ),
inference(sat_conversion,[],[f18906]) ).
cnf(s6,plain,
( spl487_2
| spl487_7 ),
inference(sat_conversion,[],[f18911]) ).
cnf(s7,plain,
( ~ spl487_3
| spl487_7 ),
inference(sat_conversion,[],[f18912]) ).
cnf(s8,plain,
( spl487_7
| spl487_8 ),
inference(sat_conversion,[],[f18917]) ).
cnf(s9,plain,
( ~ spl487_6
| spl487_8 ),
inference(sat_conversion,[],[f18918]) ).
cnf(s10,plain,
( spl487_1
| spl487_8 ),
inference(sat_conversion,[],[f18919]) ).
cnf(s1444,plain,
( ~ spl487_1
| ~ spl487_4
| spl487_6
| ~ spl487_7 ),
inference(sat_conversion,[],[f33276]) ).
cnf(s3017,plain,
( ~ spl487_2
| spl487_3
| ~ spl487_4
| ~ spl487_8 ),
inference(sat_conversion,[],[f55542]) ).
cnf(s3018,plain,
( ~ spl487_2
| spl487_3
| ~ spl487_5
| ~ spl487_8 ),
inference(sat_conversion,[],[f55543]) ).
cnf(s3071,plain,
( ~ spl487_1
| ~ spl487_5
| spl487_6
| ~ spl487_7 ),
inference(sat_conversion,[],[f56533]) ).
cnf(s3462,plain,
( spl487_3
| ~ spl487_8
| ~ spl487_2 ),
inference(rat,[],[s3,s3017,s3018]) ).
cnf(s3463,plain,
spl487_1,
inference(rat,[],[s3462,s1,s2,s10]) ).
cnf(s3464,plain,
( spl487_6
| ~ spl487_7 ),
inference(rat,[],[s3,s1444,s3071,s3463]) ).
cnf(s3465,plain,
spl487_2,
inference(rat,[],[s3464,s4,s6]) ).
cnf(s3466,plain,
spl487_7,
inference(rat,[],[s3462,s7,s8,s3465]) ).
cnf(s3467,plain,
spl487_6,
inference(rat,[],[s3464,s3466]) ).
cnf(s3468,plain,
spl487_8,
inference(rat,[],[s9,s3467]) ).
cnf(s3469,plain,
~ spl487_3,
inference(rat,[],[s5,s3467]) ).
cnf(s3470,plain,
$false,
inference(rat,[],[s3462,s3465,s3468,s3469]) ).
fof(f56534,plain,
$false,
inference(avatar_sat_refutation,[],[s3470]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n016.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 13:35:34 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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
% 12.35/2.33 % (3625398)Will run a generic schedule for satisfiability detection.
% 12.35/2.33 % (3625407)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3226021696:i=116_2996 on theBenchmark for (2996ds/116Mi)
% 12.35/2.33 % (3625404)% WARNING: option uhcvi not known.
% 12.35/2.33 % (3625403)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=266828891_2996 on theBenchmark for (2996ds/0Mi)
% 12.35/2.33 % (3625405)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3173628303:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi)
% 12.35/2.33 % (3625404)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3304606573:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi)
% 12.35/2.33 % (3625406)dis+10_1_sil=32000:sp=arity:random_seed=2441837552:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi)
% 12.35/2.33 % (3625408)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3493610599:i=131_2996 on theBenchmark for (2996ds/131Mi)
% 12.35/2.33 % (3625409)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2475315525:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi)
% 12.35/2.33 % (3625407)Instruction limit reached!
% 12.35/2.33 % (3625407)------------------------------
% 12.35/2.33 % (3625407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625407)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625407)Termination reason: Instruction limit
% 12.35/2.33 % (3625407)Termination phase: NewCNF
% 12.35/2.33 % (3625407)Time elapsed: 0.045 s
% 12.35/2.33 % (3625407)Peak memory usage: 21 MB
% 12.35/2.33 % (3625407)Instructions burned: 118 (million)
% 12.35/2.33 % (3625417)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1295563564:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 12.35/2.33 % (3625406)Instruction limit reached!
% 12.35/2.33 % (3625406)------------------------------
% 12.35/2.33 % (3625406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625406)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625406)Termination reason: Instruction limit
% 12.35/2.33 % (3625406)Termination phase: Preprocessing 3
% 12.35/2.33 % (3625406)Time elapsed: 0.066 s
% 12.35/2.33 % (3625406)Peak memory usage: 20 MB
% 12.35/2.33 % (3625406)Instructions burned: 103 (million)
% 12.35/2.33 % (3625408)Instruction limit reached!
% 12.35/2.33 % (3625408)------------------------------
% 12.35/2.33 % (3625408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625408)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625408)Termination reason: Instruction limit
% 12.35/2.33 % (3625408)Termination phase: Preprocessing 3
% 12.35/2.33 % (3625408)Time elapsed: 0.080 s
% 12.35/2.33 % (3625408)Peak memory usage: 20 MB
% 12.35/2.33 % (3625408)Instructions burned: 131 (million)
% 12.35/2.33 % (3625419)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3718524327:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 12.35/2.33 % (3625409)Instruction limit reached!
% 12.35/2.33 % (3625409)------------------------------
% 12.35/2.33 % (3625409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625409)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625409)Termination reason: Instruction limit
% 12.35/2.33 % (3625409)Termination phase: Property scanning
% 12.35/2.33 % (3625409)Time elapsed: 0.100 s
% 12.35/2.33 % (3625409)Peak memory usage: 21 MB
% 12.35/2.33 % (3625409)Instructions burned: 161 (million)
% 12.35/2.33 % (3625420)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=3344074081:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 12.35/2.33 % (3625423)ott-21_1_sil=16000:fs=off:random_seed=2296398957:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 12.35/2.33 % (3625419)Instruction limit reached!
% 12.35/2.33 % (3625419)------------------------------
% 12.35/2.33 % (3625419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625419)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625419)Termination reason: Instruction limit
% 12.35/2.33 % (3625419)Termination phase: Preprocessing 3
% 12.35/2.33 % (3625419)Time elapsed: 0.079 s
% 12.35/2.33 % (3625419)Peak memory usage: 20 MB
% 12.35/2.33 % (3625419)Instructions burned: 131 (million)
% 12.35/2.33 % (3625425)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=248856948:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 12.35/2.33 % (3625423)Instruction limit reached!
% 12.35/2.33 % (3625423)------------------------------
% 12.35/2.33 % (3625423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625423)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625423)Termination reason: Instruction limit
% 12.35/2.33 % (3625423)Termination phase: Property scanning
% 12.35/2.33 % (3625423)Time elapsed: 0.104 s
% 12.35/2.33 % (3625423)Peak memory usage: 22 MB
% 12.35/2.33 % (3625423)Instructions burned: 182 (million)
% 12.35/2.33 % (3625417)Instruction limit reached!
% 12.35/2.33 % (3625417)------------------------------
% 12.35/2.33 % (3625417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625417)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625417)Termination reason: Instruction limit
% 12.35/2.33 % (3625417)Termination phase: Finite model building preprocessing
% 12.35/2.33 % (3625417)Time elapsed: 0.178 s
% 12.35/2.33 % (3625417)Peak memory usage: 25 MB
% 12.35/2.33 % (3625417)Instructions burned: 715 (million)
% 12.35/2.33 % (3625428)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1078441607:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 12.35/2.33 % (3625427)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1199356348:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 12.35/2.33 % (3625425)Instruction limit reached!
% 12.35/2.33 % (3625425)------------------------------
% 12.35/2.33 % (3625425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625425)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625425)Termination reason: Instruction limit
% 12.35/2.33 % (3625425)Termination phase: Property scanning
% 12.35/2.33 % (3625425)Time elapsed: 0.222 s
% 12.35/2.33 % (3625425)Peak memory usage: 22 MB
% 12.35/2.33 % (3625425)Instructions burned: 479 (million)
% 12.35/2.33 % (3625420)Instruction limit reached!
% 12.35/2.33 % (3625420)------------------------------
% 12.35/2.33 % (3625420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625420)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625420)Termination reason: Instruction limit
% 12.35/2.33 % (3625420)Termination phase: Saturation
% 12.35/2.33 % (3625420)Time elapsed: 0.319 s
% 12.35/2.33 % (3625420)Peak memory usage: 24 MB
% 12.35/2.33 % (3625420)Instructions burned: 684 (million)
% 12.35/2.33 % (3625431)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3918417018:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 12.35/2.33 % (3625432)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=2714837634:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 12.35/2.33 % (3625428)Instruction limit reached!
% 12.35/2.33 % (3625428)------------------------------
% 12.35/2.33 % (3625428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625428)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625428)Termination reason: Instruction limit
% 12.35/2.33 % (3625428)Termination phase: Saturation
% 12.35/2.33 % (3625428)Time elapsed: 0.338 s
% 12.35/2.33 % (3625428)Peak memory usage: 30 MB
% 12.35/2.33 % (3625428)Instructions burned: 1179 (million)
% 12.35/2.33 % (3625435)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2097585003:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 12.35/2.33 % (3625427)Instruction limit reached!
% 12.35/2.33 % (3625427)------------------------------
% 12.35/2.33 % (3625427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625427)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625427)Termination reason: Instruction limit
% 12.35/2.33 % (3625427)Termination phase: Finite model building preprocessing
% 12.35/2.33 % (3625427)Time elapsed: 0.403 s
% 12.35/2.33 % (3625427)Peak memory usage: 29 MB
% 12.35/2.33 % (3625427)Instructions burned: 866 (million)
% 12.35/2.33 % (3625437)fmb+10_1_sil=64000:random_seed=2207084915:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 12.35/2.33 % (3625432)Instruction limit reached!
% 12.35/2.33 % (3625432)------------------------------
% 12.35/2.33 % (3625432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625432)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625432)Termination reason: Instruction limit
% 12.35/2.33 % (3625432)Termination phase: Saturation
% 12.35/2.33 % (3625432)Time elapsed: 0.342 s
% 12.35/2.33 % (3625432)Peak memory usage: 28 MB
% 12.35/2.33 % (3625432)Instructions burned: 692 (million)
% 12.35/2.33 % (3625439)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=997877127:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 12.35/2.33 % (3625435)Instruction limit reached!
% 12.35/2.33 % (3625435)------------------------------
% 12.35/2.33 % (3625435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625435)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625435)Termination reason: Instruction limit
% 12.35/2.33 % (3625435)Termination phase: Saturation
% 12.35/2.33 % (3625435)Time elapsed: 0.225 s
% 12.35/2.33 % (3625435)Peak memory usage: 30 MB
% 12.35/2.33 % (3625435)Instructions burned: 884 (million)
% 12.35/2.33 % (3625441)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2299171:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 12.35/2.33 % (3625431)Instruction limit reached!
% 12.35/2.33 % (3625431)------------------------------
% 12.35/2.33 % (3625431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625431)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625431)Termination reason: Instruction limit
% 12.35/2.33 % (3625431)Termination phase: Finite model building preprocessing
% 12.35/2.33 % (3625431)Time elapsed: 0.419 s
% 12.35/2.33 % (3625431)Peak memory usage: 31 MB
% 12.35/2.33 % (3625431)Instructions burned: 889 (million)
% 12.35/2.33 % (3625443)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=889532594:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 12.35/2.33 % (3625441)Instruction limit reached!
% 12.35/2.33 % (3625441)------------------------------
% 12.35/2.33 % (3625441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625441)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625441)Termination reason: Instruction limit
% 12.35/2.33 % (3625441)Termination phase: Finite model building preprocessing
% 12.35/2.33 % (3625441)Time elapsed: 0.237 s
% 12.35/2.33 % (3625441)Peak memory usage: 31 MB
% 12.35/2.33 % (3625441)Instructions burned: 923 (million)
% 12.35/2.33 % (3625445)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1632219674:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 12.35/2.33 % (3625445)Instruction limit reached!
% 12.35/2.33 % (3625445)------------------------------
% 12.35/2.33 % (3625445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.33 % (3625445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.33 % (3625445)CaDiCaL version: 2.1.3
% 12.35/2.33 % (3625445)Termination reason: Instruction limit
% 12.35/2.33 % (3625445)Termination phase: Saturation
% 12.35/2.33 % (3625445)Time elapsed: 0.394 s
% 12.35/2.33 % (3625445)Peak memory usage: 29 MB
% 12.35/2.33 % (3625445)Instructions burned: 1474 (million)
% 12.35/2.33 % (3625447)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=444636783:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 12.35/2.33 % (3625404) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3625398-3625404"...
% 12.35/2.33 % (3625404)...printing done.
% 12.35/2.33 % (3625404)Refutation found. Thanks to Tanya!
% 12.35/2.33 % SZS status Theorem for theBenchmark
% 12.35/2.33 % SZS output start Proof for theBenchmark
% See solution above
% 12.35/2.34 % (3625404)------------------------------
% 12.35/2.34 % (3625404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.35/2.34 % (3625404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.35/2.34 % (3625404)CaDiCaL version: 2.1.3
% 12.35/2.34 % (3625404)Termination reason: Refutation
% 12.35/2.34 % (3625404)Time elapsed: 1.692 s
% 12.35/2.34 % (3625404)Peak memory usage: 45 MB
% 12.35/2.34 % (3625404)Instructions burned: 2872 (million)
% 12.35/2.34 % (3625398)Success in time 2.108 s
% 12.35/2.34 % Vampire exiting
%------------------------------------------------------------------------------