%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW323+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:49 PM UTC 2026
% Result : Theorem 252.43s 42.51s
% Output : Refutation 252.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 6
% Syntax : Number of formulae : 28 ( 14 unt; 3 def)
% Number of atoms : 49 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 41 ( 20 ~; 16 |; 1 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 5 ( 4 usr; 4 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 13 con; 0-3 aty)
% Number of variables : 5 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5228,axiom,
! [X0] :
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,X0)),hAPP(v_c0,X0)),hAPP(v_Q_H,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
=> c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,X0)),hAPP(v_c0,X0)),hAPP(v_Q,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f5232,axiom,
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q_H,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
& c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(c_Set_Oimage(t_a,tc_Hoare__Mirabelle_Otriple(t_b),hAPP(hAPP(c_COMBS(t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(c_COMBS(t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),tc_Hoare__Mirabelle_Otriple(t_b))),hAPP(hAPP(c_COMBB(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_HOL_Obool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),c_Hoare__Mirabelle_Otriple_Otriple(t_b)),v_P_H)),v_c0)),v_Q_H)),v_F)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_4) ).
fof(f5233,conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5) ).
fof(f5234,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))),
inference(negated_conjecture,[status(cth)],[f5233]) ).
fof(f5260,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))),
inference(flattening,[],[f5234]) ).
fof(f9547,plain,
! [X0] :
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,X0)),hAPP(v_c0,X0)),hAPP(v_Q,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,X0)),hAPP(v_c0,X0)),hAPP(v_Q_H,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) ),
inference(ennf_transformation,[],[f5228]) ).
fof(f18354,plain,
! [X0] :
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,X0)),hAPP(v_c0,X0)),hAPP(v_Q,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,X0)),hAPP(v_c0,X0)),hAPP(v_Q_H,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) ),
inference(cnf_transformation,[],[f9547]) ).
fof(f18359,plain,
c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q_H,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))),
inference(cnf_transformation,[],[f5232]) ).
fof(f18360,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))),
inference(cnf_transformation,[],[f5260]) ).
fof(f20071,definition,
( spl576_1
<=> c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[spl576_1])],[avatar_definition]) ).
fof(f20073,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| spl576_1 ),
inference(avatar_component_clause,[],[f20071]) ).
fof(f20074,plain,
~ spl576_1,
inference(avatar_split_clause,[],[f18360,f20071]) ).
fof(f20081,definition,
( spl576_3
<=> c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q_H,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[spl576_3])],[avatar_definition]) ).
fof(f20083,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q_H,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| ~ spl576_3 ),
inference(avatar_component_clause,[],[f20081]) ).
fof(f20084,plain,
spl576_3,
inference(avatar_split_clause,[],[f18359,f20081]) ).
fof(f20107,definition,
( spl576_9
<=> ! [X0] :
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,X0)),hAPP(v_c0,X0)),hAPP(v_Q,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,X0)),hAPP(v_c0,X0)),hAPP(v_Q_H,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) ) ),
introduced(definition,[new_symbols(definition,[spl576_9])],[avatar_definition]) ).
fof(f20108,plain,
( ! [X0] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P_H,X0)),hAPP(v_c0,X0)),hAPP(v_Q_H,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,X0)),hAPP(v_c0,X0)),hAPP(v_Q,X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool)))) )
| ~ spl576_9 ),
inference(avatar_component_clause,[],[f20107]) ).
fof(f20109,plain,
spl576_9,
inference(avatar_split_clause,[],[f18354,f20107]) ).
fof(f255477,plain,
( c_Hoare__Mirabelle_Ohoare__derivs(t_b,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_b)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_b),hAPP(v_P,v_x)),hAPP(v_c0,v_x)),hAPP(v_Q,v_x))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_HOL_Obool))))
| ~ spl576_3
| ~ spl576_9 ),
inference(resolution,[],[f20108,f20083]) ).
fof(f255478,plain,
( $false
| spl576_1
| ~ spl576_3
| ~ spl576_9 ),
inference(forward_subsumption_resolution,[],[f255477,f20073]) ).
fof(f255479,plain,
( spl576_1
| ~ spl576_3
| ~ spl576_9 ),
inference(avatar_contradiction_clause,[],[f255478]) ).
cnf(s1,plain,
~ spl576_1,
inference(sat_conversion,[],[f20074]) ).
cnf(s3,plain,
spl576_3,
inference(sat_conversion,[],[f20084]) ).
cnf(s7,plain,
spl576_9,
inference(sat_conversion,[],[f20109]) ).
cnf(s56125,plain,
( spl576_1
| ~ spl576_3
| ~ spl576_9 ),
inference(sat_conversion,[],[f255479]) ).
cnf(s58224,plain,
spl576_1,
inference(rat,[],[s56125,s7,s3]) ).
cnf(s58227,plain,
$false,
inference(rat,[],[s1,s58224]) ).
fof(f255480,plain,
$false,
inference(avatar_sat_refutation,[],[s58227]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW323+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n014.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 13:35:46 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/0.23 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
% 22.19/3.57 % (1778587)Will run a generic schedule for satisfiability detection.
% 22.19/3.57 % (1778593)% WARNING: option uhcvi not known.
% 22.19/3.57 % (1778592)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4067603241_2998 on theBenchmark for (2998ds/0Mi)
% 22.19/3.57 % (1778595)dis+10_1_sil=32000:sp=arity:random_seed=3058433498:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 22.19/3.57 % (1778593)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1895981564:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 22.19/3.57 % (1778594)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=22417646:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 22.19/3.57 % (1778596)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3926692528:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 22.19/3.57 % (1778597)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1918977270:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 22.19/3.57 % (1778598)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2258935797:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 22.19/3.57 % (1778598)Instruction limit reached!
% 22.19/3.57 % (1778598)------------------------------
% 22.19/3.57 % (1778598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.57 % (1778598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.57 % (1778598)CaDiCaL version: 2.1.3
% 22.19/3.57 % (1778598)Termination reason: Instruction limit
% 22.19/3.57 % (1778598)Termination phase: Clausification
% 22.19/3.57 % (1778598)Time elapsed: 0.060 s
% 22.19/3.57 % (1778598)Peak memory usage: 21 MB
% 22.19/3.57 % (1778598)Instructions burned: 161 (million)
% 22.19/3.57 % (1778595)Instruction limit reached!
% 22.19/3.57 % (1778595)------------------------------
% 22.19/3.57 % (1778595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.57 % (1778595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.57 % (1778595)CaDiCaL version: 2.1.3
% 22.19/3.57 % (1778595)Termination reason: Instruction limit
% 22.19/3.57 % (1778595)Termination phase: Preprocessing 3
% 22.19/3.57 % (1778595)Time elapsed: 0.063 s
% 22.19/3.57 % (1778595)Peak memory usage: 19 MB
% 22.19/3.57 % (1778595)Instructions burned: 103 (million)
% 22.19/3.57 % (1778606)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3389637245:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 22.19/3.57 % (1778596)Instruction limit reached!
% 22.19/3.57 % (1778596)------------------------------
% 22.19/3.57 % (1778596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.57 % (1778596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.57 % (1778596)CaDiCaL version: 2.1.3
% 22.19/3.57 % (1778596)Termination reason: Instruction limit
% 22.19/3.57 % (1778596)Termination phase: NewCNF
% 22.19/3.57 % (1778596)Time elapsed: 0.074 s
% 22.19/3.57 % (1778596)Peak memory usage: 21 MB
% 22.19/3.57 % (1778596)Instructions burned: 116 (million)
% 22.19/3.57 % (1778597)Instruction limit reached!
% 22.19/3.57 % (1778597)------------------------------
% 22.19/3.57 % (1778597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.57 % (1778597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.57 % (1778597)CaDiCaL version: 2.1.3
% 22.19/3.57 % (1778597)Termination reason: Instruction limit
% 22.19/3.57 % (1778597)Termination phase: Preprocessing 3
% 22.19/3.57 % (1778597)Time elapsed: 0.078 s
% 22.19/3.57 % (1778597)Peak memory usage: 20 MB
% 22.19/3.57 % (1778597)Instructions burned: 131 (million)
% 22.19/3.57 % (1778607)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3532854071:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 22.19/3.57 % (1778609)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=935669037:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 22.19/3.57 % (1778610)ott-21_1_sil=16000:fs=off:random_seed=3298227248:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 22.19/3.57 % (1778607)Instruction limit reached!
% 22.19/3.57 % (1778607)------------------------------
% 22.19/3.57 % (1778607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.57 % (1778607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.82 % (1778607)CaDiCaL version: 2.1.3
% 44.96/6.82 % (1778607)Termination reason: Instruction limit
% 44.96/6.82 % (1778607)Termination phase: Preprocessing 3
% 44.96/6.82 % (1778607)Time elapsed: 0.079 s
% 44.96/6.82 % (1778607)Peak memory usage: 20 MB
% 44.96/6.82 % (1778607)Instructions burned: 132 (million)
% 44.96/6.82 % (1778614)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4273473224:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 44.96/6.82 % (1778610)Instruction limit reached!
% 44.96/6.82 % (1778610)------------------------------
% 44.96/6.82 % (1778610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.82 % (1778610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.82 % (1778610)CaDiCaL version: 2.1.3
% 44.96/6.82 % (1778610)Termination reason: Instruction limit
% 44.96/6.82 % (1778610)Termination phase: Property scanning
% 44.96/6.82 % (1778610)Time elapsed: 0.103 s
% 44.96/6.82 % (1778610)Peak memory usage: 21 MB
% 44.96/6.82 % (1778610)Instructions burned: 181 (million)
% 44.96/6.82 % (1778616)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3798831785:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 44.96/6.82 % (1778606)Instruction limit reached!
% 44.96/6.82 % (1778606)------------------------------
% 44.96/6.82 % (1778606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.82 % (1778606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.82 % (1778606)CaDiCaL version: 2.1.3
% 44.96/6.82 % (1778606)Termination reason: Instruction limit
% 44.96/6.82 % (1778606)Termination phase: Finite model building preprocessing
% 44.96/6.82 % (1778606)Time elapsed: 0.183 s
% 44.96/6.82 % (1778606)Peak memory usage: 25 MB
% 44.96/6.82 % (1778606)Instructions burned: 718 (million)
% 44.96/6.82 % (1778618)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3748547469:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 44.96/6.82 % (1778614)Instruction limit reached!
% 44.96/6.82 % (1778614)------------------------------
% 44.96/6.82 % (1778614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.82 % (1778614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.82 % (1778614)CaDiCaL version: 2.1.3
% 44.96/6.82 % (1778614)Termination reason: Instruction limit
% 44.96/6.82 % (1778614)Termination phase: Property scanning
% 44.96/6.82 % (1778614)Time elapsed: 0.225 s
% 44.96/6.82 % (1778614)Peak memory usage: 22 MB
% 44.96/6.82 % (1778614)Instructions burned: 478 (million)
% 44.96/6.82 % (1778609)Instruction limit reached!
% 44.96/6.82 % (1778609)------------------------------
% 44.96/6.82 % (1778609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.82 % (1778609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.82 % (1778609)CaDiCaL version: 2.1.3
% 44.96/6.82 % (1778609)Termination reason: Instruction limit
% 44.96/6.82 % (1778609)Termination phase: Saturation
% 44.96/6.82 % (1778609)Time elapsed: 0.326 s
% 44.96/6.82 % (1778609)Peak memory usage: 24 MB
% 44.96/6.82 % (1778609)Instructions burned: 686 (million)
% 44.96/6.82 % (1778620)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4275883249:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 44.96/6.82 % (1778621)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=3718120998:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 44.96/6.82 % (1778618)Instruction limit reached!
% 44.96/6.82 % (1778618)------------------------------
% 44.96/6.82 % (1778618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.82 % (1778618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.82 % (1778618)CaDiCaL version: 2.1.3
% 44.96/6.82 % (1778618)Termination reason: Instruction limit
% 44.96/6.82 % (1778618)Termination phase: Saturation
% 44.96/6.82 % (1778618)Time elapsed: 0.344 s
% 44.96/6.82 % (1778618)Peak memory usage: 30 MB
% 44.96/6.82 % (1778618)Instructions burned: 1179 (million)
% 44.96/6.82 % (1778624)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2395641151:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 44.96/6.82 % (1778616)Instruction limit reached!
% 44.96/6.82 % (1778616)------------------------------
% 44.96/6.82 % (1778616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.82 % (1778616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778616)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778616)Termination reason: Instruction limit
% 100.98/14.71 % (1778616)Termination phase: Finite model building preprocessing
% 100.98/14.71 % (1778616)Time elapsed: 0.404 s
% 100.98/14.71 % (1778616)Peak memory usage: 30 MB
% 100.98/14.71 % (1778616)Instructions burned: 866 (million)
% 100.98/14.71 % (1778626)fmb+10_1_sil=64000:random_seed=3214109333:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 100.98/14.71 % (1778621)Instruction limit reached!
% 100.98/14.71 % (1778621)------------------------------
% 100.98/14.71 % (1778621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.98/14.71 % (1778621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778621)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778621)Termination reason: Instruction limit
% 100.98/14.71 % (1778621)Termination phase: Saturation
% 100.98/14.71 % (1778621)Time elapsed: 0.345 s
% 100.98/14.71 % (1778621)Peak memory usage: 27 MB
% 100.98/14.71 % (1778621)Instructions burned: 692 (million)
% 100.98/14.71 % (1778628)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=623025783:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 100.98/14.71 % (1778624)Instruction limit reached!
% 100.98/14.71 % (1778624)------------------------------
% 100.98/14.71 % (1778624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.98/14.71 % (1778624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778624)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778624)Termination reason: Instruction limit
% 100.98/14.71 % (1778624)Termination phase: Saturation
% 100.98/14.71 % (1778624)Time elapsed: 0.229 s
% 100.98/14.71 % (1778624)Peak memory usage: 31 MB
% 100.98/14.71 % (1778624)Instructions burned: 881 (million)
% 100.98/14.71 % (1778620)Instruction limit reached!
% 100.98/14.71 % (1778620)------------------------------
% 100.98/14.71 % (1778620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.98/14.71 % (1778620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778620)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778620)Termination reason: Instruction limit
% 100.98/14.71 % (1778620)Termination phase: Finite model building preprocessing
% 100.98/14.71 % (1778620)Time elapsed: 0.416 s
% 100.98/14.71 % (1778620)Peak memory usage: 31 MB
% 100.98/14.71 % (1778620)Instructions burned: 889 (million)
% 100.98/14.71 % (1778630)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3556236785:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 100.98/14.71 % (1778631)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1227029213:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 100.98/14.71 % (1778630)Instruction limit reached!
% 100.98/14.71 % (1778630)------------------------------
% 100.98/14.71 % (1778630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.98/14.71 % (1778630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778630)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778630)Termination reason: Instruction limit
% 100.98/14.71 % (1778630)Termination phase: Finite model building preprocessing
% 100.98/14.71 % (1778630)Time elapsed: 0.234 s
% 100.98/14.71 % (1778630)Peak memory usage: 31 MB
% 100.98/14.71 % (1778630)Instructions burned: 920 (million)
% 100.98/14.71 % (1778634)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1518094056:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 100.98/14.71 % (1778634)Instruction limit reached!
% 100.98/14.71 % (1778634)------------------------------
% 100.98/14.71 % (1778634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.98/14.71 % (1778634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778634)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778634)Termination reason: Instruction limit
% 100.98/14.71 % (1778634)Termination phase: Saturation
% 100.98/14.71 % (1778634)Time elapsed: 0.336 s
% 100.98/14.71 % (1778634)Peak memory usage: 28 MB
% 100.98/14.71 % (1778634)Instructions burned: 1474 (million)
% 100.98/14.71 % (1778636)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3618628809:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 100.98/14.71 % (1778636)Instruction limit reached!
% 100.98/14.71 % (1778636)------------------------------
% 100.98/14.71 % (1778636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.98/14.71 % (1778636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/14.71 % (1778636)CaDiCaL version: 2.1.3
% 100.98/14.71 % (1778636)Termination reason: Instruction limit
% 198.09/28.32 % (1778636)Termination phase: Finite model building preprocessing
% 198.09/28.32 % (1778636)Time elapsed: 1.689 s
% 198.09/28.32 % (1778636)Peak memory usage: 66 MB
% 198.09/28.32 % (1778636)Instructions burned: 6326 (million)
% 198.09/28.32 % (1778638)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=946269592:fmbsr=2.30978:i=2174_2966 on theBenchmark for (2966ds/2174Mi)
% 198.09/28.32 % (1778631)Instruction limit reached!
% 198.09/28.32 % (1778631)------------------------------
% 198.09/28.32 % (1778631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.09/28.32 % (1778631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.09/28.32 % (1778631)CaDiCaL version: 2.1.3
% 198.09/28.32 % (1778631)Termination reason: Instruction limit
% 198.09/28.32 % (1778631)Termination phase: Saturation
% 198.09/28.32 % (1778631)Time elapsed: 2.512 s
% 198.09/28.32 % (1778631)Peak memory usage: 51 MB
% 198.09/28.32 % (1778631)Instructions burned: 5132 (million)
% 198.09/28.32 % (1778640)ott-2_1_sil=16000:newcnf=on:random_seed=2604316362:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi)
% 198.09/28.32 % (1778638)Instruction limit reached!
% 198.09/28.32 % (1778638)------------------------------
% 198.09/28.32 % (1778638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.09/28.32 % (1778638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.09/28.32 % (1778638)CaDiCaL version: 2.1.3
% 198.09/28.32 % (1778638)Termination reason: Instruction limit
% 198.09/28.32 % (1778638)Termination phase: Finite model building preprocessing
% 198.09/28.32 % (1778638)Time elapsed: 0.540 s
% 198.09/28.32 % (1778638)Peak memory usage: 47 MB
% 198.09/28.32 % (1778638)Instructions burned: 2176 (million)
% 198.09/28.32 % (1778642)ott+10_1_sil=32000:tgt=ground:random_seed=3193025600:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi)
% 198.09/28.32 % (1778640)Instruction limit reached!
% 198.09/28.32 % (1778640)------------------------------
% 198.09/28.32 % (1778640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.09/28.32 % (1778640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.09/28.32 % (1778640)CaDiCaL version: 2.1.3
% 198.09/28.32 % (1778640)Termination reason: Instruction limit
% 198.09/28.32 % (1778640)Termination phase: Saturation
% 198.09/28.32 % (1778640)Time elapsed: 0.439 s
% 198.09/28.32 % (1778640)Peak memory usage: 28 MB
% 198.09/28.32 % (1778640)Instructions burned: 869 (million)
% 198.09/28.32 % (1778644)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2477313249:i=54282_2959 on theBenchmark for (2959ds/54282Mi)
% 198.09/28.32 % (1778642)Instruction limit reached!
% 198.09/28.32 % (1778642)------------------------------
% 198.09/28.32 % (1778642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.09/28.32 % (1778642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.09/28.32 % (1778642)CaDiCaL version: 2.1.3
% 198.09/28.32 % (1778642)Termination reason: Instruction limit
% 198.09/28.32 % (1778642)Termination phase: Saturation
% 198.09/28.32 % (1778642)Time elapsed: 1.657 s
% 198.09/28.32 % (1778642)Peak memory usage: 66 MB
% 198.09/28.32 % (1778642)Instructions burned: 5114 (million)
% 198.09/28.32 % (1778646)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1081378249:i=3512:aac=none_2944 on theBenchmark for (2944ds/3512Mi)
% 198.09/28.32 % (1778628)Instruction limit reached!
% 198.09/28.32 % (1778628)------------------------------
% 198.09/28.32 % (1778628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.09/28.32 % (1778628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.09/28.32 % (1778628)CaDiCaL version: 2.1.3
% 198.09/28.32 % (1778628)Termination reason: Instruction limit
% 198.09/28.32 % (1778628)Termination phase: Finite model building preprocessing
% 198.09/28.32 % (1778628)Time elapsed: 4.912 s
% 198.09/28.32 % (1778628)Peak memory usage: 78 MB
% 198.09/28.32 % (1778628)Instructions burned: 9515 (million)
% 198.09/28.32 % (1778648)dis+21_1_sil=32000:sas=cadical:random_seed=1799916851:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 198.09/28.32 % (1778646)Instruction limit reached!
% 198.09/28.32 % (1778646)------------------------------
% 198.09/28.32 % (1778646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 198.09/28.32 % (1778646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 198.09/28.32 % (1778646)CaDiCaL version: 2.1.3
% 198.09/28.32 % (1778646)Termination reason: Instruction limit
% 198.09/28.32 % (1778646)Termination phase: Saturation
% 198.09/28.32 % (1778646)Time elapsed: 1.0000 s
% 257.12/36.81 % (1778646)Peak memory usage: 48 MB
% 257.12/36.81 % (1778646)Instructions burned: 3514 (million)
% 257.12/36.81 % (1778650)ott+11_1_sil=16000:gs=on:random_seed=2768369888:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 257.12/36.81 % (1778650)Instruction limit reached!
% 257.12/36.81 % (1778650)------------------------------
% 257.12/36.81 % (1778650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.12/36.81 % (1778650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.12/36.81 % (1778650)CaDiCaL version: 2.1.3
% 257.12/36.81 % (1778650)Termination reason: Instruction limit
% 257.12/36.81 % (1778650)Termination phase: Saturation
% 257.12/36.81 % (1778650)Time elapsed: 0.632 s
% 257.12/36.81 % (1778650)Peak memory usage: 34 MB
% 257.12/36.81 % (1778650)Instructions burned: 2252 (million)
% 257.12/36.81 % (1778652)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3284017071:fmbsr=1.6:i=67534_2927 on theBenchmark for (2927ds/67534Mi)
% 257.12/36.81 % (1778648)Instruction limit reached!
% 257.12/36.81 % (1778648)------------------------------
% 257.12/36.81 % (1778648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.12/36.81 % (1778648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.12/36.81 % (1778648)CaDiCaL version: 2.1.3
% 257.12/36.81 % (1778648)Termination reason: Instruction limit
% 257.12/36.81 % (1778648)Termination phase: Saturation
% 257.12/36.81 % (1778648)Time elapsed: 2.118 s
% 257.12/36.81 % (1778648)Peak memory usage: 56 MB
% 257.12/36.81 % (1778648)Instructions burned: 3773 (million)
% 257.12/36.81 % (1778654)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3408308286:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2919 on theBenchmark for (2919ds/4591Mi)
% 257.12/36.81 % (1778654)Instruction limit reached!
% 257.12/36.81 % (1778654)------------------------------
% 257.12/36.81 % (1778654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.12/36.81 % (1778654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.12/36.81 % (1778654)CaDiCaL version: 2.1.3
% 257.12/36.81 % (1778654)Termination reason: Instruction limit
% 257.12/36.81 % (1778654)Termination phase: Saturation
% 257.12/36.81 % (1778654)Time elapsed: 1.708 s
% 257.12/36.81 % (1778654)Peak memory usage: 31 MB
% 257.12/36.81 % (1778654)Instructions burned: 4591 (million)
% 257.12/36.81 % (1778656)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=984420908:i=29340_2902 on theBenchmark for (2902ds/29340Mi)
% 257.12/36.81 % (1778626)Instruction limit reached!
% 257.12/36.81 % (1778626)------------------------------
% 257.12/36.81 % (1778626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.12/36.81 % (1778626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.12/36.81 % (1778626)CaDiCaL version: 2.1.3
% 257.12/36.81 % (1778626)Termination reason: Instruction limit
% 257.12/36.81 % (1778626)Termination phase: Finite model building preprocessing
% 257.12/36.81 % (1778626)Time elapsed: 11.450 s
% 257.12/36.81 % (1778626)Peak memory usage: 216 MB
% 257.12/36.81 % (1778626)Instructions burned: 22062 (million)
% 257.12/36.81 % (1778658)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2990092794:i=5211_2876 on theBenchmark for (2876ds/5211Mi)
% 257.12/36.81 % TRYING [1]
% 257.12/36.81 % TRYING [2]
% 257.12/36.81 % (1778652)Cannot represent all propositional literals internally
% 257.12/36.81 % (1778652)Refutation not found, incomplete strategy
% 257.12/36.81 % (1778652)------------------------------
% 257.12/36.81 % (1778652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.12/36.81 % (1778652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.12/36.81 % (1778652)CaDiCaL version: 2.1.3
% 257.12/36.81 % (1778652)Termination reason: Refutation not found, incomplete strategy
% 257.12/36.81 % (1778652)Time elapsed: 6.515 s
% 257.12/36.81 % (1778652)Peak memory usage: 191 MB
% 257.12/36.81 % (1778652)Instructions burned: 23851 (million)
% 257.12/36.81 % (1778652)------------------------------
% 257.12/36.81 % (1778652)------------------------------
% 257.12/36.81 % (1778660)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2587218485:i=5497:nm=2_2862 on theBenchmark for (2862ds/5497Mi)
% 257.12/36.81 % (1778658)Instruction limit reached!
% 257.12/36.81 % (1778658)------------------------------
% 257.12/36.81 % (1778658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 257.12/36.81 % (1778658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.12/36.81 % (1778658)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778658)Termination reason: Instruction limit
% 252.43/42.50 % (1778658)Termination phase: Saturation
% 252.43/42.50 % (1778658)Time elapsed: 2.143 s
% 252.43/42.50 % (1778658)Peak memory usage: 46 MB
% 252.43/42.50 % (1778658)Instructions burned: 5213 (million)
% 252.43/42.50 % (1778662)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4117055637:fmbsr=2:i=46332_2855 on theBenchmark for (2855ds/46332Mi)
% 252.43/42.50 % (1778660)Instruction limit reached!
% 252.43/42.50 % (1778660)------------------------------
% 252.43/42.50 % (1778660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778660)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778660)Termination reason: Instruction limit
% 252.43/42.50 % (1778660)Termination phase: Finite model building preprocessing
% 252.43/42.50 % (1778660)Time elapsed: 1.491 s
% 252.43/42.50 % (1778660)Peak memory usage: 64 MB
% 252.43/42.50 % (1778660)Instructions burned: 5497 (million)
% 252.43/42.50 % (1778664)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3382053277:i=14071_2846 on theBenchmark for (2846ds/14071Mi)
% 252.43/42.50 % TRYING [3]
% 252.43/42.50 % TRYING [1]
% 252.43/42.50 % TRYING [2]
% 252.43/42.50 % (1778664)Instruction limit reached!
% 252.43/42.50 % (1778664)------------------------------
% 252.43/42.50 % (1778664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778664)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778664)Termination reason: Instruction limit
% 252.43/42.50 % (1778664)Termination phase: Finite model building preprocessing
% 252.43/42.50 % (1778664)Time elapsed: 3.930 s
% 252.43/42.50 % (1778664)Peak memory usage: 95 MB
% 252.43/42.50 % (1778664)Instructions burned: 14072 (million)
% 252.43/42.50 % (1778666)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2189811992:i=22565:add=on:rawr=on_2807 on theBenchmark for (2807ds/22565Mi)
% 252.43/42.50 % TRYING [3]
% 252.43/42.50 % (1778656)Instruction limit reached!
% 252.43/42.50 % (1778656)------------------------------
% 252.43/42.50 % (1778656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778656)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778656)Termination reason: Instruction limit
% 252.43/42.50 % (1778656)Termination phase: Saturation
% 252.43/42.50 % (1778656)Time elapsed: 13.403 s
% 252.43/42.50 % (1778656)Peak memory usage: 415 MB
% 252.43/42.50 % (1778656)Instructions burned: 29341 (million)
% 252.43/42.50 % (1778668)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1628048005:i=8173:av=off_2767 on theBenchmark for (2767ds/8173Mi)
% 252.43/42.50 % (1778666)Instruction limit reached!
% 252.43/42.50 % (1778666)------------------------------
% 252.43/42.50 % (1778666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778666)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778666)Termination reason: Instruction limit
% 252.43/42.50 % (1778666)Termination phase: Saturation
% 252.43/42.50 % (1778666)Time elapsed: 6.050 s
% 252.43/42.50 % (1778666)Peak memory usage: 238 MB
% 252.43/42.50 % (1778666)Instructions burned: 22567 (million)
% 252.43/42.50 % (1778670)dis+10_16:1_sil=16000:random_seed=485488883:i=9155:fsr=off_2746 on theBenchmark for (2746ds/9155Mi)
% 252.43/42.50 % (1778662)Cannot represent all propositional literals internally
% 252.43/42.50 % (1778662)Refutation not found, incomplete strategy
% 252.43/42.50 % (1778662)------------------------------
% 252.43/42.50 % (1778662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778662)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778662)Termination reason: Refutation not found, incomplete strategy
% 252.43/42.50 % (1778662)Time elapsed: 12.290 s
% 252.43/42.50 % (1778662)Peak memory usage: 191 MB
% 252.43/42.50 % (1778662)Instructions burned: 23850 (million)
% 252.43/42.50 % (1778662)------------------------------
% 252.43/42.50 % (1778662)------------------------------
% 252.43/42.50 % (1778672)ott-3_8_sil=64000:random_seed=3370959454:i=20139:bs=on_2731 on theBenchmark for (2731ds/20139Mi)
% 252.43/42.50 % (1778670)Instruction limit reached!
% 252.43/42.50 % (1778670)------------------------------
% 252.43/42.50 % (1778670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778670)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778670)Termination reason: Instruction limit
% 252.43/42.50 % (1778670)Termination phase: Saturation
% 252.43/42.50 % (1778670)Time elapsed: 2.746 s
% 252.43/42.50 % (1778670)Peak memory usage: 87 MB
% 252.43/42.50 % (1778670)Instructions burned: 9156 (million)
% 252.43/42.50 % (1778674)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1912444912:fmbsr=2:i=32576_2719 on theBenchmark for (2719ds/32576Mi)
% 252.43/42.50 % (1778668)Instruction limit reached!
% 252.43/42.50 % (1778668)------------------------------
% 252.43/42.50 % (1778668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778668)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778668)Termination reason: Instruction limit
% 252.43/42.50 % (1778668)Termination phase: Saturation
% 252.43/42.50 % (1778668)Time elapsed: 5.105 s
% 252.43/42.50 % (1778668)Peak memory usage: 101 MB
% 252.43/42.50 % (1778668)Instructions burned: 8174 (million)
% 252.43/42.50 % (1778676)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=304458410:i=11404_2715 on theBenchmark for (2715ds/11404Mi)
% 252.43/42.50 % (1778644)Instruction limit reached!
% 252.43/42.50 % (1778644)------------------------------
% 252.43/42.50 % (1778644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778644)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778644)Termination reason: Instruction limit
% 252.43/42.50 % (1778644)Termination phase: Finite model building constraint generation
% 252.43/42.50 % (1778644)Time elapsed: 25.279 s
% 252.43/42.50 % (1778644)Peak memory usage: 2604 MB
% 252.43/42.50 % (1778644)Instructions burned: 54283 (million)
% 252.43/42.50 % (1778678)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3222249644:i=14134_2703 on theBenchmark for (2703ds/14134Mi)
% 252.43/42.50 % (1778674)Cannot represent all propositional literals internally
% 252.43/42.50 % (1778674)Refutation not found, incomplete strategy
% 252.43/42.50 % (1778674)------------------------------
% 252.43/42.50 % (1778674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778674)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778674)Termination reason: Refutation not found, incomplete strategy
% 252.43/42.50 % (1778674)Time elapsed: 6.705 s
% 252.43/42.50 % (1778674)Peak memory usage: 224 MB
% 252.43/42.50 % (1778674)Instructions burned: 24109 (million)
% 252.43/42.50 % (1778674)------------------------------
% 252.43/42.50 % (1778674)------------------------------
% 252.43/42.50 % (1778680)dis+33_16_sil=32000:sac=on:random_seed=394725146:i=15851:nm=0_2651 on theBenchmark for (2651ds/15851Mi)
% 252.43/42.50 % (1778678)Instruction limit reached!
% 252.43/42.50 % (1778678)------------------------------
% 252.43/42.50 % (1778678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778678)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778678)Termination reason: Instruction limit
% 252.43/42.50 % (1778678)Termination phase: Saturation
% 252.43/42.50 % (1778678)Time elapsed: 6.088 s
% 252.43/42.50 % (1778678)Peak memory usage: 72 MB
% 252.43/42.50 % (1778678)Instructions burned: 14137 (million)
% 252.43/42.50 % (1778682)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3279577974:avsq=on:i=17627:add=on:amm=off_2642 on theBenchmark for (2642ds/17627Mi)
% 252.43/42.50 % (1778676)Instruction limit reached!
% 252.43/42.50 % (1778676)------------------------------
% 252.43/42.50 % (1778676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.50 % (1778676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.50 % (1778676)CaDiCaL version: 2.1.3
% 252.43/42.50 % (1778676)Termination reason: Instruction limit
% 252.43/42.50 % (1778676)Termination phase: Saturation
% 252.43/42.50 % (1778676)Time elapsed: 7.639 s
% 252.43/42.50 % (1778676)Peak memory usage: 148 MB
% 252.43/42.50 % (1778676)Instructions burned: 11404 (million)
% 252.43/42.50 % (1778684)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2265856178:s2a=on:i=53295_2639 on theBenchmark for (2639ds/53295Mi)
% 252.43/42.50 % (1778672)Instruction limit reached!
% 252.43/42.50 % (1778672)------------------------------
% 252.43/42.50 % (1778672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.51 % (1778672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.51 % (1778672)CaDiCaL version: 2.1.3
% 252.43/42.51 % (1778672)Termination reason: Instruction limit
% 252.43/42.51 % (1778672)Termination phase: Saturation
% 252.43/42.51 % (1778672)Time elapsed: 9.709 s
% 252.43/42.51 % (1778672)Peak memory usage: 86 MB
% 252.43/42.51 % (1778672)Instructions burned: 20139 (million)
% 252.43/42.51 % (1778686)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3898618578:i=26857:ins=20_2634 on theBenchmark for (2634ds/26857Mi)
% 252.43/42.51 % (1778680)Instruction limit reached!
% 252.43/42.51 % (1778680)------------------------------
% 252.43/42.51 % (1778680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.51 % (1778680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.51 % (1778680)CaDiCaL version: 2.1.3
% 252.43/42.51 % (1778680)Termination reason: Instruction limit
% 252.43/42.51 % (1778680)Termination phase: Saturation
% 252.43/42.51 % (1778680)Time elapsed: 4.144 s
% 252.43/42.51 % (1778680)Peak memory usage: 214 MB
% 252.43/42.51 % (1778680)Instructions burned: 15851 (million)
% 252.43/42.51 % (1778688)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2460190184:i=28120:bs=on:fsr=off_2609 on theBenchmark for (2609ds/28120Mi)
% 252.43/42.51 % (1778594)Instruction limit reached!
% 252.43/42.51 % (1778594)------------------------------
% 252.43/42.51 % (1778594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.51 % (1778594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.51 % (1778594)CaDiCaL version: 2.1.3
% 252.43/42.51 % (1778594)Termination reason: Instruction limit
% 252.43/42.51 % (1778594)Termination phase: Saturation
% 252.43/42.51 % (1778594)Time elapsed: 40.596 s
% 252.43/42.51 % (1778594)Peak memory usage: 243 MB
% 252.43/42.51 % (1778594)Instructions burned: 88026 (million)
% 252.43/42.51 % (1778690)fmb+10_1_sil=256000:fmbss=7:random_seed=4082193584:fmbsr=1.6:i=182295_2591 on theBenchmark for (2591ds/182295Mi)
% 252.43/42.51 % (1778684) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1778587-1778684"...
% 252.43/42.51 % (1778684)...printing done.
% 252.43/42.51 % (1778684)Refutation found. Thanks to Tanya!
% 252.43/42.51 % SZS status Theorem for theBenchmark
% 252.43/42.51 % SZS output start Proof for theBenchmark
% See solution above
% 252.43/42.51 % (1778684)------------------------------
% 252.43/42.51 % (1778684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 252.43/42.51 % (1778684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.43/42.51 % (1778684)CaDiCaL version: 2.1.3
% 252.43/42.51 % (1778684)Termination reason: Refutation
% 252.43/42.51 % (1778684)Time elapsed: 5.468 s
% 252.43/42.51 % (1778684)Peak memory usage: 140 MB
% 252.43/42.51 % (1778684)Instructions burned: 8673 (million)
% 252.43/42.51 % (1778587)Success in time 42.265 s
% 252.43/42.51 % Vampire exiting
%------------------------------------------------------------------------------