%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW389+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:55 PM UTC 2026
% Result : Theorem 140.78s 25.69s
% Output : Refutation 140.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 25 ( 20 unt; 0 def)
% Number of atoms : 32 ( 7 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 20 ( 13 ~; 4 |; 1 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-5 aty)
% Number of variables : 47 ( 45 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [X0,X1,X2,X3,X4] :
( ! [X5,X6] :
( hBOOL(hAPP(hAPP(X4,X5),X6))
=> c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X3)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),X3),hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),X6))),X1),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),X3),hAPP(X0,X5)))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_HOL_Obool)))) )
=> c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X3)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),X4),X1),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_HOL_Obool)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_escape) ).
fof(f35,axiom,
! [X0,X1] : hAPP(c_Set_OCollect(X1),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Collect__def) ).
fof(f40,axiom,
! [X0,X1] : hAPP(c_Set_OCollect(X1),hAPP(c_fequal,X0)) = hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_singleton__conv2) ).
fof(f5222,axiom,
! [X0,X1,X2,X3] : hAPP(hAPP(c_COMBK(X3,X2),X1),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__COMBK__1) ).
fof(f5228,axiom,
~ hBOOL(c_fFalse),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fFalse__1) ).
fof(f5241,conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f5242,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(negated_conjecture,[status(cth)],[f5241]) ).
fof(f5261,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(flattening,[],[f5242]) ).
fof(f5453,plain,
! [X0,X1,X2,X3,X4] :
( c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X3)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),X4),X1),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_HOL_Obool))))
| ? [X5,X6] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X3)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),X3),hAPP(hAPP(c_COMBC(tc_Com_Ostate,tc_Com_Ostate,tc_HOL_Obool),c_fequal),X6))),X1),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),X3),hAPP(X0,X5)))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_HOL_Obool))))
& hBOOL(hAPP(hAPP(X4,X5),X6)) ) ),
inference(ennf_transformation,[],[f16]) ).
fof(f9479,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(hAPP(X4,sK1(X0,X1,X2,X3,X4)),sK2(X0,X1,X2,X3,X4)))
| c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X3)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),X4),X1),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_HOL_Obool)))) ),
inference(cnf_transformation,[],[f5453]) ).
fof(f9507,plain,
! [X0,X1] : hAPP(c_Set_OCollect(X1),X0) = X0,
inference(cnf_transformation,[],[f35]) ).
fof(f9514,plain,
! [X0,X1] : hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))) = hAPP(c_Set_OCollect(X1),hAPP(c_fequal,X0)),
inference(cnf_transformation,[],[f40]) ).
fof(f16453,plain,
! [X2,X3,X0,X1] : hAPP(hAPP(c_COMBK(X3,X2),X1),X0) = X1,
inference(cnf_transformation,[],[f5222]) ).
fof(f16459,plain,
~ hBOOL(c_fFalse),
inference(cnf_transformation,[],[f5228]) ).
fof(f16472,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(cnf_transformation,[],[f5261]) ).
fof(f18021,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(X4,sK1(X0,X1,X2,X3,X4)),sK2(X0,X1,X2,X3,X4)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X3)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),X4),X1),X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_HOL_Obool)))) ),
inference(consistent_polarity_flipping,[],[f9479]) ).
fof(f22581,plain,
hBOOL(c_fFalse),
inference(consistent_polarity_flipping,[],[f16459]) ).
fof(f22594,plain,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))),v_c),v_Q)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)))),
inference(consistent_polarity_flipping,[],[f16472]) ).
fof(f48688,plain,
! [X0,X1] : hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))) = hAPP(c_fequal,X0),
inference(forward_demodulation,[],[f9514,f9507]) ).
fof(f48690,plain,
c_Hoare__Mirabelle_Ohoare__derivs(t_a,v_G,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))),v_c),v_Q))),
inference(superposition,[],[f22594,f48688]) ).
fof(f471900,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X2,hAPP(c_fequal,hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(X3),X4),X1),X0)))
| ~ hBOOL(hAPP(hAPP(X4,sK1(X0,X1,X2,X3,X4)),sK2(X0,X1,X2,X3,X4))) ),
inference(forward_demodulation,[],[f18021,f48688]) ).
fof(f471901,plain,
~ hBOOL(hAPP(hAPP(hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse)),sK1(v_Q,v_c,v_G,t_a,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse)))),sK2(v_Q,v_c,v_G,t_a,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))))),
inference(resolution,[],[f471900,f48690]) ).
fof(f472105,plain,
~ hBOOL(hAPP(hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse),sK2(v_Q,v_c,v_G,t_a,hAPP(c_COMBK(tc_fun(tc_Com_Ostate,tc_HOL_Obool),t_a),hAPP(c_COMBK(tc_HOL_Obool,tc_Com_Ostate),c_fFalse))))),
inference(forward_demodulation,[],[f471901,f16453]) ).
fof(f472118,plain,
~ hBOOL(c_fFalse),
inference(forward_demodulation,[],[f472105,f16453]) ).
fof(f472131,plain,
$false,
inference(forward_subsumption_resolution,[],[f472118,f22581]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW389+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n016.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 13:50:48 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 22.40/3.79 % (3633714)Will run a generic schedule for satisfiability detection.
% 22.40/3.79 % (3633723)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3219572641:i=116_2996 on theBenchmark for (2996ds/116Mi)
% 22.40/3.79 % (3633720)% WARNING: option uhcvi not known.
% 22.40/3.79 % (3633719)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1039376488_2996 on theBenchmark for (2996ds/0Mi)
% 22.40/3.79 % (3633720)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1146387251:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi)
% 22.40/3.79 % (3633721)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3406692064:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi)
% 22.40/3.79 % (3633722)dis+10_1_sil=32000:sp=arity:random_seed=1195524073:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi)
% 22.40/3.79 % (3633725)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=699667712:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi)
% 22.40/3.79 % (3633724)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3454436735:i=131_2996 on theBenchmark for (2996ds/131Mi)
% 22.40/3.79 % (3633723)Instruction limit reached!
% 22.40/3.79 % (3633723)------------------------------
% 22.40/3.79 % (3633723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.40/3.79 % (3633723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.79 % (3633723)CaDiCaL version: 2.1.3
% 22.40/3.79 % (3633723)Termination reason: Instruction limit
% 22.40/3.79 % (3633723)Termination phase: NewCNF
% 22.40/3.79 % (3633723)Time elapsed: 0.045 s
% 22.40/3.79 % (3633723)Peak memory usage: 21 MB
% 22.40/3.79 % (3633723)Instructions burned: 119 (million)
% 22.40/3.79 % (3633733)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=246323618:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 22.40/3.79 % (3633722)Instruction limit reached!
% 22.40/3.79 % (3633722)------------------------------
% 22.40/3.79 % (3633722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.40/3.79 % (3633722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.79 % (3633722)CaDiCaL version: 2.1.3
% 22.40/3.79 % (3633722)Termination reason: Instruction limit
% 22.40/3.79 % (3633722)Termination phase: Preprocessing 3
% 22.40/3.79 % (3633722)Time elapsed: 0.064 s
% 22.40/3.79 % (3633722)Peak memory usage: 19 MB
% 22.40/3.79 % (3633722)Instructions burned: 103 (million)
% 22.40/3.79 % (3633724)Instruction limit reached!
% 22.40/3.79 % (3633724)------------------------------
% 22.40/3.79 % (3633724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.40/3.79 % (3633724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.79 % (3633724)CaDiCaL version: 2.1.3
% 22.40/3.79 % (3633724)Termination reason: Instruction limit
% 22.40/3.79 % (3633724)Termination phase: Preprocessing 3
% 22.40/3.79 % (3633724)Time elapsed: 0.079 s
% 22.40/3.79 % (3633724)Peak memory usage: 20 MB
% 22.40/3.79 % (3633724)Instructions burned: 132 (million)
% 22.40/3.79 % (3633735)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1880960627:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 22.40/3.79 % (3633725)Instruction limit reached!
% 22.40/3.79 % (3633725)------------------------------
% 22.40/3.79 % (3633725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.40/3.79 % (3633725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.79 % (3633725)CaDiCaL version: 2.1.3
% 22.40/3.79 % (3633725)Termination reason: Instruction limit
% 22.40/3.79 % (3633725)Termination phase: Clausification
% 22.40/3.79 % (3633725)Time elapsed: 0.097 s
% 22.40/3.79 % (3633725)Peak memory usage: 21 MB
% 22.40/3.79 % (3633725)Instructions burned: 159 (million)
% 22.40/3.79 % (3633736)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=150236974:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 22.40/3.79 % (3633738)ott-21_1_sil=16000:fs=off:random_seed=2342668363:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 22.40/3.79 % (3633735)Instruction limit reached!
% 22.40/3.79 % (3633735)------------------------------
% 22.40/3.79 % (3633735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.40/3.79 % (3633735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.04 % (3633735)CaDiCaL version: 2.1.3
% 46.03/7.04 % (3633735)Termination reason: Instruction limit
% 46.03/7.04 % (3633735)Termination phase: Preprocessing 3
% 46.03/7.04 % (3633735)Time elapsed: 0.079 s
% 46.03/7.04 % (3633735)Peak memory usage: 20 MB
% 46.03/7.04 % (3633735)Instructions burned: 131 (million)
% 46.03/7.04 % (3633741)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3370313271:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 46.03/7.04 % (3633738)Instruction limit reached!
% 46.03/7.04 % (3633738)------------------------------
% 46.03/7.04 % (3633738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.03/7.04 % (3633738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.04 % (3633738)CaDiCaL version: 2.1.3
% 46.03/7.04 % (3633738)Termination reason: Instruction limit
% 46.03/7.04 % (3633738)Termination phase: Property scanning
% 46.03/7.04 % (3633738)Time elapsed: 0.104 s
% 46.03/7.04 % (3633738)Peak memory usage: 21 MB
% 46.03/7.04 % (3633738)Instructions burned: 181 (million)
% 46.03/7.04 % (3633733)Instruction limit reached!
% 46.03/7.04 % (3633733)------------------------------
% 46.03/7.04 % (3633733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.03/7.04 % (3633733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.04 % (3633733)CaDiCaL version: 2.1.3
% 46.03/7.04 % (3633733)Termination reason: Instruction limit
% 46.03/7.04 % (3633733)Termination phase: Finite model building preprocessing
% 46.03/7.04 % (3633733)Time elapsed: 0.179 s
% 46.03/7.04 % (3633733)Peak memory usage: 25 MB
% 46.03/7.04 % (3633733)Instructions burned: 714 (million)
% 46.03/7.04 % (3633744)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2051280239:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 46.03/7.04 % (3633743)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=703119831:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 46.03/7.04 % (3633741)Instruction limit reached!
% 46.03/7.04 % (3633741)------------------------------
% 46.03/7.04 % (3633741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.03/7.04 % (3633741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.04 % (3633741)CaDiCaL version: 2.1.3
% 46.03/7.04 % (3633741)Termination reason: Instruction limit
% 46.03/7.04 % (3633741)Termination phase: Property scanning
% 46.03/7.04 % (3633741)Time elapsed: 0.223 s
% 46.03/7.04 % (3633741)Peak memory usage: 22 MB
% 46.03/7.04 % (3633741)Instructions burned: 477 (million)
% 46.03/7.04 % (3633736)Instruction limit reached!
% 46.03/7.04 % (3633736)------------------------------
% 46.03/7.04 % (3633736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.03/7.04 % (3633736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.04 % (3633736)CaDiCaL version: 2.1.3
% 46.03/7.04 % (3633736)Termination reason: Instruction limit
% 46.03/7.04 % (3633736)Termination phase: Saturation
% 46.03/7.04 % (3633736)Time elapsed: 0.322 s
% 46.03/7.04 % (3633736)Peak memory usage: 24 MB
% 46.03/7.04 % (3633736)Instructions burned: 685 (million)
% 46.03/7.04 % (3633747)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=288925257:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 46.03/7.04 % (3633748)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=3068983656: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)
% 46.03/7.04 % (3633744)Instruction limit reached!
% 46.03/7.04 % (3633744)------------------------------
% 46.03/7.04 % (3633744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.03/7.04 % (3633744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.03/7.04 % (3633744)CaDiCaL version: 2.1.3
% 46.03/7.04 % (3633744)Termination reason: Instruction limit
% 46.03/7.04 % (3633744)Termination phase: Saturation
% 46.03/7.04 % (3633744)Time elapsed: 0.340 s
% 46.03/7.04 % (3633744)Peak memory usage: 30 MB
% 46.03/7.04 % (3633744)Instructions burned: 1180 (million)
% 46.03/7.04 % (3633751)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1246814876:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 46.03/7.04 % (3633743)Instruction limit reached!
% 46.03/7.04 % (3633743)------------------------------
% 46.03/7.04 % (3633743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.03/7.04 % (3633743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633743)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633743)Termination reason: Instruction limit
% 101.39/15.00 % (3633743)Termination phase: Finite model building preprocessing
% 101.39/15.00 % (3633743)Time elapsed: 0.405 s
% 101.39/15.00 % (3633743)Peak memory usage: 30 MB
% 101.39/15.00 % (3633743)Instructions burned: 867 (million)
% 101.39/15.00 % (3633753)fmb+10_1_sil=64000:random_seed=1150172607:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 101.39/15.00 % (3633748)Instruction limit reached!
% 101.39/15.00 % (3633748)------------------------------
% 101.39/15.00 % (3633748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.39/15.00 % (3633748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633748)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633748)Termination reason: Instruction limit
% 101.39/15.00 % (3633748)Termination phase: Saturation
% 101.39/15.00 % (3633748)Time elapsed: 0.347 s
% 101.39/15.00 % (3633748)Peak memory usage: 27 MB
% 101.39/15.00 % (3633748)Instructions burned: 693 (million)
% 101.39/15.00 % (3633755)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2403540883:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 101.39/15.00 % (3633751)Instruction limit reached!
% 101.39/15.00 % (3633751)------------------------------
% 101.39/15.00 % (3633751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.39/15.00 % (3633751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633751)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633751)Termination reason: Instruction limit
% 101.39/15.00 % (3633751)Termination phase: Saturation
% 101.39/15.00 % (3633751)Time elapsed: 0.227 s
% 101.39/15.00 % (3633751)Peak memory usage: 30 MB
% 101.39/15.00 % (3633751)Instructions burned: 884 (million)
% 101.39/15.00 % (3633757)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2761059631:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 101.39/15.00 % (3633747)Instruction limit reached!
% 101.39/15.00 % (3633747)------------------------------
% 101.39/15.00 % (3633747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.39/15.00 % (3633747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633747)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633747)Termination reason: Instruction limit
% 101.39/15.00 % (3633747)Termination phase: Finite model building preprocessing
% 101.39/15.00 % (3633747)Time elapsed: 0.424 s
% 101.39/15.00 % (3633747)Peak memory usage: 31 MB
% 101.39/15.00 % (3633747)Instructions burned: 890 (million)
% 101.39/15.00 % (3633759)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1852322674:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 101.39/15.00 % (3633757)Instruction limit reached!
% 101.39/15.00 % (3633757)------------------------------
% 101.39/15.00 % (3633757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.39/15.00 % (3633757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633757)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633757)Termination reason: Instruction limit
% 101.39/15.00 % (3633757)Termination phase: Finite model building preprocessing
% 101.39/15.00 % (3633757)Time elapsed: 0.237 s
% 101.39/15.00 % (3633757)Peak memory usage: 31 MB
% 101.39/15.00 % (3633757)Instructions burned: 923 (million)
% 101.39/15.00 % (3633761)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3122813227:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 101.39/15.00 % (3633761)Instruction limit reached!
% 101.39/15.00 % (3633761)------------------------------
% 101.39/15.00 % (3633761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.39/15.00 % (3633761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633761)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633761)Termination reason: Instruction limit
% 101.39/15.00 % (3633761)Termination phase: Saturation
% 101.39/15.00 % (3633761)Time elapsed: 0.340 s
% 101.39/15.00 % (3633761)Peak memory usage: 28 MB
% 101.39/15.00 % (3633761)Instructions burned: 1476 (million)
% 101.39/15.00 % (3633763)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1612794191:i=6324_2981 on theBenchmark for (2981ds/6324Mi)
% 101.39/15.00 % (3633763)Instruction limit reached!
% 101.39/15.00 % (3633763)------------------------------
% 101.39/15.00 % (3633763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.39/15.00 % (3633763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.39/15.00 % (3633763)CaDiCaL version: 2.1.3
% 101.39/15.00 % (3633763)Termination reason: Instruction limit
% 140.78/25.68 % (3633763)Termination phase: Finite model building preprocessing
% 140.78/25.68 % (3633763)Time elapsed: 1.718 s
% 140.78/25.68 % (3633763)Peak memory usage: 66 MB
% 140.78/25.68 % (3633763)Instructions burned: 6328 (million)
% 140.78/25.68 % (3633765)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=465042080:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 140.78/25.68 % (3633759)Instruction limit reached!
% 140.78/25.68 % (3633759)------------------------------
% 140.78/25.68 % (3633759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633759)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633759)Termination reason: Instruction limit
% 140.78/25.68 % (3633759)Termination phase: Saturation
% 140.78/25.68 % (3633759)Time elapsed: 2.376 s
% 140.78/25.68 % (3633759)Peak memory usage: 44 MB
% 140.78/25.68 % (3633759)Instructions burned: 5134 (million)
% 140.78/25.68 % (3633767)ott-2_1_sil=16000:newcnf=on:random_seed=2071291150:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2963 on theBenchmark for (2963ds/869Mi)
% 140.78/25.68 % (3633765)Instruction limit reached!
% 140.78/25.68 % (3633765)------------------------------
% 140.78/25.68 % (3633765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633765)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633765)Termination reason: Instruction limit
% 140.78/25.68 % (3633765)Termination phase: Finite model building preprocessing
% 140.78/25.68 % (3633765)Time elapsed: 0.544 s
% 140.78/25.68 % (3633765)Peak memory usage: 48 MB
% 140.78/25.68 % (3633765)Instructions burned: 2177 (million)
% 140.78/25.68 % (3633767)Instruction limit reached!
% 140.78/25.68 % (3633767)------------------------------
% 140.78/25.68 % (3633767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633767)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633767)Termination reason: Instruction limit
% 140.78/25.68 % (3633767)Termination phase: Saturation
% 140.78/25.68 % (3633767)Time elapsed: 0.439 s
% 140.78/25.68 % (3633767)Peak memory usage: 28 MB
% 140.78/25.68 % (3633767)Instructions burned: 870 (million)
% 140.78/25.68 % (3633769)ott+10_1_sil=32000:tgt=ground:random_seed=1315113447:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi)
% 140.78/25.68 % (3633770)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4097152244:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 140.78/25.68 % (3633769)Instruction limit reached!
% 140.78/25.68 % (3633769)------------------------------
% 140.78/25.68 % (3633769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633769)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633769)Termination reason: Instruction limit
% 140.78/25.68 % (3633769)Termination phase: Saturation
% 140.78/25.68 % (3633769)Time elapsed: 1.692 s
% 140.78/25.68 % (3633769)Peak memory usage: 68 MB
% 140.78/25.68 % (3633769)Instructions burned: 5115 (million)
% 140.78/25.68 % (3633773)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4112942821:i=3512:aac=none_2941 on theBenchmark for (2941ds/3512Mi)
% 140.78/25.68 % (3633755)Instruction limit reached!
% 140.78/25.68 % (3633755)------------------------------
% 140.78/25.68 % (3633755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633755)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633755)Termination reason: Instruction limit
% 140.78/25.68 % (3633755)Termination phase: Finite model building preprocessing
% 140.78/25.68 % (3633755)Time elapsed: 4.967 s
% 140.78/25.68 % (3633755)Peak memory usage: 78 MB
% 140.78/25.68 % (3633755)Instructions burned: 9515 (million)
% 140.78/25.68 % (3633775)dis+21_1_sil=32000:sas=cadical:random_seed=3098654823:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 140.78/25.68 % (3633773)Instruction limit reached!
% 140.78/25.68 % (3633773)------------------------------
% 140.78/25.68 % (3633773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633773)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633773)Termination reason: Instruction limit
% 140.78/25.68 % (3633773)Termination phase: Saturation
% 140.78/25.68 % (3633773)Time elapsed: 0.967 s
% 140.78/25.68 % (3633773)Peak memory usage: 45 MB
% 140.78/25.68 % (3633773)Instructions burned: 3518 (million)
% 140.78/25.68 % (3633777)ott+11_1_sil=16000:gs=on:random_seed=281002933:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi)
% 140.78/25.68 % (3633777)Instruction limit reached!
% 140.78/25.68 % (3633777)------------------------------
% 140.78/25.68 % (3633777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633777)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633777)Termination reason: Instruction limit
% 140.78/25.68 % (3633777)Termination phase: Saturation
% 140.78/25.68 % (3633777)Time elapsed: 0.640 s
% 140.78/25.68 % (3633777)Peak memory usage: 34 MB
% 140.78/25.68 % (3633777)Instructions burned: 2254 (million)
% 140.78/25.68 % (3633782)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4027745574:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi)
% 140.78/25.68 % (3633775)Instruction limit reached!
% 140.78/25.68 % (3633775)------------------------------
% 140.78/25.68 % (3633775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633775)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633775)Termination reason: Instruction limit
% 140.78/25.68 % (3633775)Termination phase: Saturation
% 140.78/25.68 % (3633775)Time elapsed: 2.193 s
% 140.78/25.68 % (3633775)Peak memory usage: 54 MB
% 140.78/25.68 % (3633775)Instructions burned: 3773 (million)
% 140.78/25.68 % (3633784)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4275681153:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 140.78/25.68 % (3633784)Instruction limit reached!
% 140.78/25.68 % (3633784)------------------------------
% 140.78/25.68 % (3633784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633784)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633784)Termination reason: Instruction limit
% 140.78/25.68 % (3633784)Termination phase: Saturation
% 140.78/25.68 % (3633784)Time elapsed: 1.735 s
% 140.78/25.68 % (3633784)Peak memory usage: 31 MB
% 140.78/25.68 % (3633784)Instructions burned: 4593 (million)
% 140.78/25.68 % (3633786)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3766197299:i=29340_2898 on theBenchmark for (2898ds/29340Mi)
% 140.78/25.68 % (3633753)Instruction limit reached!
% 140.78/25.68 % (3633753)------------------------------
% 140.78/25.68 % (3633753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633753)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633753)Termination reason: Instruction limit
% 140.78/25.68 % (3633753)Termination phase: Finite model building preprocessing
% 140.78/25.68 % (3633753)Time elapsed: 11.554 s
% 140.78/25.68 % (3633753)Peak memory usage: 217 MB
% 140.78/25.68 % (3633753)Instructions burned: 22063 (million)
% 140.78/25.68 % (3633788)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3545085342:i=5211_2873 on theBenchmark for (2873ds/5211Mi)
% 140.78/25.68 % TRYING [1]
% 140.78/25.68 % TRYING [2]
% 140.78/25.68 % (3633782)Cannot represent all propositional literals internally
% 140.78/25.68 % (3633782)Refutation not found, incomplete strategy
% 140.78/25.68 % (3633782)------------------------------
% 140.78/25.68 % (3633782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633782)CaDiCaL version: 2.1.3
% 140.78/25.68 % (3633782)Termination reason: Refutation not found, incomplete strategy
% 140.78/25.68 % (3633782)Time elapsed: 6.687 s
% 140.78/25.68 % (3633782)Peak memory usage: 192 MB
% 140.78/25.68 % (3633782)Instructions burned: 24032 (million)
% 140.78/25.68 % (3633782)------------------------------
% 140.78/25.68 % (3633782)------------------------------
% 140.78/25.68 % (3633790)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=693808756:i=5497:nm=2_2857 on theBenchmark for (2857ds/5497Mi)
% 140.78/25.68 % (3633788)Instruction limit reached!
% 140.78/25.68 % (3633788)------------------------------
% 140.78/25.68 % (3633788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.68 % (3633788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.68 % (3633788)CaDiCaL version: 2.1.3
% 140.78/25.69 % (3633788)Termination reason: Instruction limit
% 140.78/25.69 % (3633788)Termination phase: Saturation
% 140.78/25.69 % (3633788)Time elapsed: 2.093 s
% 140.78/25.69 % (3633788)Peak memory usage: 46 MB
% 140.78/25.69 % (3633788)Instructions burned: 5218 (million)
% 140.78/25.69 % (3633792)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2691538768:fmbsr=2:i=46332_2852 on theBenchmark for (2852ds/46332Mi)
% 140.78/25.69 % (3633790)Instruction limit reached!
% 140.78/25.69 % (3633790)------------------------------
% 140.78/25.69 % (3633790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.69 % (3633790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.69 % (3633790)CaDiCaL version: 2.1.3
% 140.78/25.69 % (3633790)Termination reason: Instruction limit
% 140.78/25.69 % (3633790)Termination phase: Finite model building preprocessing
% 140.78/25.69 % (3633790)Time elapsed: 1.517 s
% 140.78/25.69 % (3633790)Peak memory usage: 63 MB
% 140.78/25.69 % (3633790)Instructions burned: 5498 (million)
% 140.78/25.69 % (3633794)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3382318651:i=14071_2842 on theBenchmark for (2842ds/14071Mi)
% 140.78/25.69 % TRYING [3]
% 140.78/25.69 % TRYING [1]
% 140.78/25.69 % TRYING [2]
% 140.78/25.69 % (3633794)Instruction limit reached!
% 140.78/25.69 % (3633794)------------------------------
% 140.78/25.69 % (3633794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.69 % (3633794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.69 % (3633794)CaDiCaL version: 2.1.3
% 140.78/25.69 % (3633794)Termination reason: Instruction limit
% 140.78/25.69 % (3633794)Termination phase: Finite model building preprocessing
% 140.78/25.69 % (3633794)Time elapsed: 3.992 s
% 140.78/25.69 % (3633794)Peak memory usage: 95 MB
% 140.78/25.69 % (3633794)Instructions burned: 14077 (million)
% 140.78/25.69 % (3633796)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=257982876:i=22565:add=on:rawr=on_2802 on theBenchmark for (2802ds/22565Mi)
% 140.78/25.69 % TRYING [3]
% 140.78/25.69 % (3633786)Instruction limit reached!
% 140.78/25.69 % (3633786)------------------------------
% 140.78/25.69 % (3633786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.69 % (3633786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.69 % (3633786)CaDiCaL version: 2.1.3
% 140.78/25.69 % (3633786)Termination reason: Instruction limit
% 140.78/25.69 % (3633786)Termination phase: Saturation
% 140.78/25.69 % (3633786)Time elapsed: 13.461 s
% 140.78/25.69 % (3633786)Peak memory usage: 419 MB
% 140.78/25.69 % (3633786)Instructions burned: 29340 (million)
% 140.78/25.69 % (3633798)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3485682028:i=8173:av=off_2763 on theBenchmark for (2763ds/8173Mi)
% 140.78/25.69 % (3633720) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3633714-3633720"...
% 140.78/25.69 % (3633720)...printing done.
% 140.78/25.69 % (3633720)Refutation found. Thanks to Tanya!
% 140.78/25.69 % SZS status Theorem for theBenchmark
% 140.78/25.69 % SZS output start Proof for theBenchmark
% See solution above
% 140.78/25.69 % (3633720)------------------------------
% 140.78/25.69 % (3633720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 140.78/25.69 % (3633720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.78/25.69 % (3633720)CaDiCaL version: 2.1.3
% 140.78/25.69 % (3633720)Termination reason: Refutation
% 140.78/25.69 % (3633720)Time elapsed: 24.677 s
% 140.78/25.69 % (3633720)Peak memory usage: 232 MB
% 140.78/25.69 % (3633720)Instructions burned: 42489 (million)
% 140.78/25.69 % (3633714)Success in time 25.435 s
% 140.78/25.69 % Vampire exiting
%------------------------------------------------------------------------------