%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW365+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 : n011.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:53 PM UTC 2026
% Result : Theorem 127.36s 34.84s
% Output : Refutation 127.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 9
% Syntax : Number of formulae : 34 ( 22 unt; 0 def)
% Number of atoms : 52 ( 19 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 39 ( 21 ~; 12 |; 1 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 47 ( 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f37,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
=> hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__absorb) ).
fof(f2178,axiom,
! [X0,X1,X2] :
( class_Lattices_Osemilattice__sup(X2)
=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X2),X1),X0))
<=> hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X2),X1),X0) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__iff__sup) ).
fof(f2200,axiom,
! [X0,X1,X2] : hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)))),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__is__Un) ).
fof(f3275,axiom,
! [X0,X1] : hAPP(c_Set_OCollect(X1),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Collect__def) ).
fof(f3288,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(f4989,axiom,
! [X0,X1] :
( class_Lattices_Olattice(X1)
=> class_Lattices_Osemilattice__sup(tc_fun(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_fun__Lattices_Osemilattice__sup) ).
fof(f5134,axiom,
class_Lattices_Olattice(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Lattices_Olattice) ).
fof(f5230,axiom,
hBOOL(hAPP(hAPP(c_member(t_a),hAPP(v_mgt__call,v_pn)),v_G)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_6) ).
fof(f5231,conjecture,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_7) ).
fof(f5232,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G)),
inference(negated_conjecture,[status(cth)],[f5231]) ).
fof(f5258,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G)),
inference(flattening,[],[f5232]) ).
fof(f5469,plain,
! [X0,X1,X2] :
( hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = X0
| ~ hBOOL(hAPP(hAPP(c_member(X2),X1),X0)) ),
inference(ennf_transformation,[],[f37]) ).
fof(f7367,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X2),X1),X0))
<=> hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X2),X1),X0) = X0 )
| ~ class_Lattices_Osemilattice__sup(X2) ),
inference(ennf_transformation,[],[f2178]) ).
fof(f9578,plain,
! [X0,X1] :
( class_Lattices_Osemilattice__sup(tc_fun(X0,X1))
| ~ class_Lattices_Olattice(X1) ),
inference(ennf_transformation,[],[f4989]) ).
fof(f10321,plain,
! [X0,X1,X2] :
( ( ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X2),X1),X0))
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X2),X1),X0) != X0 )
& ( hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X2),X1),X0) = X0
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X2),X1),X0)) ) )
| ~ class_Lattices_Osemilattice__sup(X2) ),
inference(nnf_transformation,[],[f7367]) ).
fof(f11388,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = X0 ),
inference(cnf_transformation,[],[f5469]) ).
fof(f14258,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X2),X1),X0))
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X2),X1),X0) != X0
| ~ class_Lattices_Osemilattice__sup(X2) ),
inference(cnf_transformation,[],[f10321]) ).
fof(f14288,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)))),X0),
inference(cnf_transformation,[],[f2200]) ).
fof(f15720,plain,
! [X0,X1] : hAPP(c_Set_OCollect(X1),X0) = X0,
inference(cnf_transformation,[],[f3275]) ).
fof(f15737,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,[],[f3288]) ).
fof(f18212,plain,
! [X0,X1] :
( class_Lattices_Osemilattice__sup(tc_fun(X0,X1))
| ~ class_Lattices_Olattice(X1) ),
inference(cnf_transformation,[],[f9578]) ).
fof(f18357,plain,
class_Lattices_Olattice(tc_HOL_Obool),
inference(cnf_transformation,[],[f5134]) ).
fof(f18453,plain,
hBOOL(hAPP(hAPP(c_member(t_a),hAPP(v_mgt__call,v_pn)),v_G)),
inference(cnf_transformation,[],[f5230]) ).
fof(f18454,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G)),
inference(cnf_transformation,[],[f5258]) ).
fof(f20437,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2,tc_HOL_Obool)),hAPP(c_Set_OCollect(X2),hAPP(c_fequal,X1))),X0),
inference(forward_demodulation,[],[f14288,f15737]) ).
fof(f20975,plain,
! [X2,X0,X1] : hAPP(hAPP(c_Set_Oinsert(X2),X1),X0) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2,tc_HOL_Obool)),hAPP(c_fequal,X1)),X0),
inference(forward_demodulation,[],[f20437,f15720]) ).
fof(f61459,plain,
v_G = hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G),
inference(resolution,[],[f11388,f18453]) ).
fof(f94843,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(c_Set_OCollect(t_a),hAPP(c_fequal,hAPP(v_mgt__call,v_pn)))),v_G)),
inference(superposition,[],[f18454,f15737]) ).
fof(f94931,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(c_fequal,hAPP(v_mgt__call,v_pn))),v_G)),
inference(forward_demodulation,[],[f94843,f15720]) ).
fof(f113919,plain,
( v_G != hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(t_a,tc_HOL_Obool)),hAPP(c_fequal,hAPP(v_mgt__call,v_pn))),v_G)
| ~ class_Lattices_Osemilattice__sup(tc_fun(t_a,tc_HOL_Obool)) ),
inference(resolution,[],[f14258,f94931]) ).
fof(f114032,plain,
( v_G != hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G)
| ~ class_Lattices_Osemilattice__sup(tc_fun(t_a,tc_HOL_Obool)) ),
inference(forward_demodulation,[],[f113919,f20975]) ).
fof(f114069,plain,
~ class_Lattices_Osemilattice__sup(tc_fun(t_a,tc_HOL_Obool)),
inference(forward_subsumption_resolution,[],[f114032,f61459]) ).
fof(f114118,plain,
~ class_Lattices_Olattice(tc_HOL_Obool),
inference(resolution,[],[f114069,f18212]) ).
fof(f114119,plain,
$false,
inference(forward_subsumption_resolution,[],[f114118,f18357]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW365+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.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % 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:42:16 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.23 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
% 28.71/4.61 % (3387782)Will run a generic schedule for satisfiability detection.
% 28.71/4.61 % (3387787)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1218652357_2996 on theBenchmark for (2996ds/0Mi)
% 28.71/4.61 % (3387788)% WARNING: option uhcvi not known.
% 28.71/4.61 % (3387788)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4253293030:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi)
% 28.71/4.61 % (3387789)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=427166314:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi)
% 28.71/4.61 % (3387790)dis+10_1_sil=32000:sp=arity:random_seed=1074457629:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi)
% 28.71/4.61 % (3387791)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=832673506:i=116_2996 on theBenchmark for (2996ds/116Mi)
% 28.71/4.61 % (3387793)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4029613774:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi)
% 28.71/4.61 % (3387792)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1706826347:i=131_2996 on theBenchmark for (2996ds/131Mi)
% 28.71/4.61 % (3387790)Instruction limit reached!
% 28.71/4.61 % (3387790)------------------------------
% 28.71/4.61 % (3387790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.61 % (3387790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.61 % (3387790)CaDiCaL version: 2.1.3
% 28.71/4.61 % (3387790)Termination reason: Instruction limit
% 28.71/4.61 % (3387790)Termination phase: Preprocessing 3
% 28.71/4.61 % (3387790)Time elapsed: 0.065 s
% 28.71/4.61 % (3387790)Peak memory usage: 20 MB
% 28.71/4.61 % (3387790)Instructions burned: 103 (million)
% 28.71/4.61 % (3387791)Instruction limit reached!
% 28.71/4.61 % (3387791)------------------------------
% 28.71/4.61 % (3387791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.61 % (3387791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.61 % (3387791)CaDiCaL version: 2.1.3
% 28.71/4.61 % (3387791)Termination reason: Instruction limit
% 28.71/4.61 % (3387791)Termination phase: NewCNF
% 28.71/4.61 % (3387791)Time elapsed: 0.076 s
% 28.71/4.61 % (3387791)Peak memory usage: 21 MB
% 28.71/4.61 % (3387791)Instructions burned: 116 (million)
% 28.71/4.61 % (3387792)Instruction limit reached!
% 28.71/4.61 % (3387792)------------------------------
% 28.71/4.61 % (3387792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.61 % (3387792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.61 % (3387792)CaDiCaL version: 2.1.3
% 28.71/4.61 % (3387792)Termination reason: Instruction limit
% 28.71/4.61 % (3387792)Termination phase: Preprocessing 3
% 28.71/4.61 % (3387792)Time elapsed: 0.080 s
% 28.71/4.61 % (3387792)Peak memory usage: 20 MB
% 28.71/4.61 % (3387792)Instructions burned: 131 (million)
% 28.71/4.61 % (3387801)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3429110304:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 28.71/4.61 % (3387793)Instruction limit reached!
% 28.71/4.61 % (3387793)------------------------------
% 28.71/4.61 % (3387793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.61 % (3387793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.61 % (3387793)CaDiCaL version: 2.1.3
% 28.71/4.61 % (3387793)Termination reason: Instruction limit
% 28.71/4.61 % (3387793)Termination phase: Clausification
% 28.71/4.61 % (3387793)Time elapsed: 0.095 s
% 28.71/4.61 % (3387793)Peak memory usage: 21 MB
% 28.71/4.61 % (3387793)Instructions burned: 160 (million)
% 28.71/4.61 % (3387802)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4131919346:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 28.71/4.61 % (3387803)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=4160238797:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 28.71/4.61 % (3387806)ott-21_1_sil=16000:fs=off:random_seed=829810743:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 28.71/4.61 % (3387802)Instruction limit reached!
% 28.71/4.61 % (3387802)------------------------------
% 28.71/4.61 % (3387802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.71/4.61 % (3387802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.32/9.21 % (3387802)CaDiCaL version: 2.1.3
% 61.32/9.21 % (3387802)Termination reason: Instruction limit
% 61.32/9.21 % (3387802)Termination phase: Preprocessing 3
% 61.32/9.21 % (3387802)Time elapsed: 0.079 s
% 61.32/9.21 % (3387802)Peak memory usage: 20 MB
% 61.32/9.21 % (3387802)Instructions burned: 133 (million)
% 61.32/9.21 % (3387809)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3883694872:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 61.32/9.21 % (3387806)Instruction limit reached!
% 61.32/9.21 % (3387806)------------------------------
% 61.32/9.21 % (3387806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.32/9.21 % (3387806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.32/9.21 % (3387806)CaDiCaL version: 2.1.3
% 61.32/9.21 % (3387806)Termination reason: Instruction limit
% 61.32/9.21 % (3387806)Termination phase: Property scanning
% 61.32/9.21 % (3387806)Time elapsed: 0.103 s
% 61.32/9.21 % (3387806)Peak memory usage: 22 MB
% 61.32/9.21 % (3387806)Instructions burned: 180 (million)
% 61.32/9.21 % (3387811)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1957861989:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 61.32/9.21 % (3387801)Instruction limit reached!
% 61.32/9.21 % (3387801)------------------------------
% 61.32/9.21 % (3387801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.32/9.21 % (3387801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.32/9.21 % (3387801)CaDiCaL version: 2.1.3
% 61.32/9.21 % (3387801)Termination reason: Instruction limit
% 61.32/9.21 % (3387801)Termination phase: Finite model building preprocessing
% 61.32/9.21 % (3387801)Time elapsed: 0.332 s
% 61.32/9.21 % (3387801)Peak memory usage: 25 MB
% 61.32/9.21 % (3387801)Instructions burned: 715 (million)
% 61.32/9.21 % (3387809)Instruction limit reached!
% 61.32/9.21 % (3387809)------------------------------
% 61.32/9.21 % (3387809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.32/9.21 % (3387809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.32/9.21 % (3387809)CaDiCaL version: 2.1.3
% 61.32/9.21 % (3387809)Termination reason: Instruction limit
% 61.32/9.21 % (3387809)Termination phase: Property scanning
% 61.32/9.21 % (3387809)Time elapsed: 0.224 s
% 61.32/9.21 % (3387809)Peak memory usage: 23 MB
% 61.32/9.21 % (3387809)Instructions burned: 477 (million)
% 61.32/9.21 % (3387803)Instruction limit reached!
% 61.32/9.21 % (3387803)------------------------------
% 61.32/9.21 % (3387803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.32/9.21 % (3387803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.32/9.21 % (3387803)CaDiCaL version: 2.1.3
% 61.32/9.21 % (3387803)Termination reason: Instruction limit
% 61.32/9.21 % (3387803)Termination phase: Saturation
% 61.32/9.21 % (3387803)Time elapsed: 0.325 s
% 61.32/9.21 % (3387803)Peak memory usage: 25 MB
% 61.32/9.21 % (3387803)Instructions burned: 691 (million)
% 61.32/9.21 % (3387813)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=575311356:i=1179_2991 on theBenchmark for (2991ds/1179Mi)
% 61.32/9.21 % (3387814)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2306195586:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 61.32/9.21 % (3387815)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=3558723701: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)
% 61.32/9.21 % (3387811)Instruction limit reached!
% 61.32/9.21 % (3387811)------------------------------
% 61.32/9.21 % (3387811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.32/9.21 % (3387811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.32/9.21 % (3387811)CaDiCaL version: 2.1.3
% 61.32/9.21 % (3387811)Termination reason: Instruction limit
% 61.32/9.21 % (3387811)Termination phase: Finite model building preprocessing
% 61.32/9.21 % (3387811)Time elapsed: 0.401 s
% 61.32/9.21 % (3387811)Peak memory usage: 30 MB
% 61.32/9.21 % (3387811)Instructions burned: 865 (million)
% 61.32/9.21 % (3387819)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1685444726:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 61.32/9.21 % (3387815)Instruction limit reached!
% 61.32/9.21 % (3387815)------------------------------
% 61.32/9.21 % (3387815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.32/9.21 % (3387815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387815)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387815)Termination reason: Instruction limit
% 124.01/18.06 % (3387815)Termination phase: Saturation
% 124.01/18.06 % (3387815)Time elapsed: 0.340 s
% 124.01/18.06 % (3387815)Peak memory usage: 27 MB
% 124.01/18.06 % (3387815)Instructions burned: 692 (million)
% 124.01/18.06 % (3387821)fmb+10_1_sil=64000:random_seed=1703587294:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 124.01/18.06 % (3387814)Instruction limit reached!
% 124.01/18.06 % (3387814)------------------------------
% 124.01/18.06 % (3387814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 124.01/18.06 % (3387814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387814)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387814)Termination reason: Instruction limit
% 124.01/18.06 % (3387814)Termination phase: Finite model building preprocessing
% 124.01/18.06 % (3387814)Time elapsed: 0.420 s
% 124.01/18.06 % (3387814)Peak memory usage: 31 MB
% 124.01/18.06 % (3387814)Instructions burned: 889 (million)
% 124.01/18.06 % (3387823)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=74109174:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 124.01/18.06 % (3387813)Instruction limit reached!
% 124.01/18.06 % (3387813)------------------------------
% 124.01/18.06 % (3387813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 124.01/18.06 % (3387813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387813)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387813)Termination reason: Instruction limit
% 124.01/18.06 % (3387813)Termination phase: Saturation
% 124.01/18.06 % (3387813)Time elapsed: 0.634 s
% 124.01/18.06 % (3387813)Peak memory usage: 30 MB
% 124.01/18.06 % (3387813)Instructions burned: 1179 (million)
% 124.01/18.06 % (3387819)Instruction limit reached!
% 124.01/18.06 % (3387819)------------------------------
% 124.01/18.06 % (3387819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 124.01/18.06 % (3387819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387819)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387819)Termination reason: Instruction limit
% 124.01/18.06 % (3387819)Termination phase: Saturation
% 124.01/18.06 % (3387819)Time elapsed: 0.415 s
% 124.01/18.06 % (3387819)Peak memory usage: 30 MB
% 124.01/18.06 % (3387819)Instructions burned: 880 (million)
% 124.01/18.06 % (3387825)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2119699632:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 124.01/18.06 % (3387826)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4030505930:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 124.01/18.06 % (3387825)Instruction limit reached!
% 124.01/18.06 % (3387825)------------------------------
% 124.01/18.06 % (3387825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 124.01/18.06 % (3387825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387825)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387825)Termination reason: Instruction limit
% 124.01/18.06 % (3387825)Termination phase: Finite model building preprocessing
% 124.01/18.06 % (3387825)Time elapsed: 0.434 s
% 124.01/18.06 % (3387825)Peak memory usage: 31 MB
% 124.01/18.06 % (3387825)Instructions burned: 922 (million)
% 124.01/18.06 % (3387829)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2945660686:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 124.01/18.06 % (3387829)Instruction limit reached!
% 124.01/18.06 % (3387829)------------------------------
% 124.01/18.06 % (3387829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 124.01/18.06 % (3387829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387829)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387829)Termination reason: Instruction limit
% 124.01/18.06 % (3387829)Termination phase: Saturation
% 124.01/18.06 % (3387829)Time elapsed: 0.631 s
% 124.01/18.06 % (3387829)Peak memory usage: 28 MB
% 124.01/18.06 % (3387829)Instructions burned: 1472 (million)
% 124.01/18.06 % (3387831)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3145454499:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 124.01/18.06 % (3387826)Instruction limit reached!
% 124.01/18.06 % (3387826)------------------------------
% 124.01/18.06 % (3387826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 124.01/18.06 % (3387826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.01/18.06 % (3387826)CaDiCaL version: 2.1.3
% 124.01/18.06 % (3387826)Termination reason: Instruction limit
% 127.36/34.83 % (3387826)Termination phase: Saturation
% 127.36/34.83 % (3387826)Time elapsed: 2.869 s
% 127.36/34.83 % (3387826)Peak memory usage: 60 MB
% 127.36/34.83 % (3387826)Instructions burned: 5132 (million)
% 127.36/34.83 % (3387833)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1186912932:fmbsr=2.30978:i=2174_2956 on theBenchmark for (2956ds/2174Mi)
% 127.36/34.83 % (3387833)Instruction limit reached!
% 127.36/34.83 % (3387833)------------------------------
% 127.36/34.83 % (3387833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387833)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387833)Termination reason: Instruction limit
% 127.36/34.83 % (3387833)Termination phase: Finite model building preprocessing
% 127.36/34.83 % (3387833)Time elapsed: 0.999 s
% 127.36/34.83 % (3387833)Peak memory usage: 48 MB
% 127.36/34.83 % (3387833)Instructions burned: 2176 (million)
% 127.36/34.83 % (3387835)ott-2_1_sil=16000:newcnf=on:random_seed=1769795886:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2946 on theBenchmark for (2946ds/869Mi)
% 127.36/34.83 % (3387831)Instruction limit reached!
% 127.36/34.83 % (3387831)------------------------------
% 127.36/34.83 % (3387831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387831)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387831)Termination reason: Instruction limit
% 127.36/34.83 % (3387831)Termination phase: Finite model building preprocessing
% 127.36/34.83 % (3387831)Time elapsed: 3.185 s
% 127.36/34.83 % (3387831)Peak memory usage: 67 MB
% 127.36/34.83 % (3387831)Instructions burned: 6326 (million)
% 127.36/34.83 % (3387837)ott+10_1_sil=32000:tgt=ground:random_seed=114995759:i=5114:av=off_2941 on theBenchmark for (2941ds/5114Mi)
% 127.36/34.83 % (3387835)Instruction limit reached!
% 127.36/34.83 % (3387835)------------------------------
% 127.36/34.83 % (3387835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387835)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387835)Termination reason: Instruction limit
% 127.36/34.83 % (3387835)Termination phase: Saturation
% 127.36/34.83 % (3387835)Time elapsed: 0.436 s
% 127.36/34.83 % (3387835)Peak memory usage: 28 MB
% 127.36/34.83 % (3387835)Instructions burned: 869 (million)
% 127.36/34.83 % (3387839)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3443787572:i=54282_2941 on theBenchmark for (2941ds/54282Mi)
% 127.36/34.83 % (3387823)Instruction limit reached!
% 127.36/34.83 % (3387823)------------------------------
% 127.36/34.83 % (3387823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387823)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387823)Termination reason: Instruction limit
% 127.36/34.83 % (3387823)Termination phase: Finite model building preprocessing
% 127.36/34.83 % (3387823)Time elapsed: 4.901 s
% 127.36/34.83 % (3387823)Peak memory usage: 88 MB
% 127.36/34.83 % (3387823)Instructions burned: 9517 (million)
% 127.36/34.83 % (3387841)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3624828312:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi)
% 127.36/34.83 % TRYING [1]
% 127.36/34.83 % TRYING [2]
% 127.36/34.83 % (3387841)Instruction limit reached!
% 127.36/34.83 % (3387841)------------------------------
% 127.36/34.83 % (3387841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387841)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387841)Termination reason: Instruction limit
% 127.36/34.83 % (3387841)Termination phase: Saturation
% 127.36/34.83 % (3387841)Time elapsed: 2.0000 s
% 127.36/34.83 % (3387841)Peak memory usage: 51 MB
% 127.36/34.83 % (3387841)Instructions burned: 3512 (million)
% 127.36/34.83 % (3387843)dis+21_1_sil=32000:sas=cadical:random_seed=3879949029:i=3773:amm=off_2917 on theBenchmark for (2917ds/3773Mi)
% 127.36/34.83 % (3387837)Instruction limit reached!
% 127.36/34.83 % (3387837)------------------------------
% 127.36/34.83 % (3387837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387837)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387837)Termination reason: Instruction limit
% 127.36/34.83 % (3387837)Termination phase: Saturation
% 127.36/34.83 % (3387837)Time elapsed: 3.147 s
% 127.36/34.83 % (3387837)Peak memory usage: 64 MB
% 127.36/34.83 % (3387837)Instructions burned: 5115 (million)
% 127.36/34.83 % (3387845)ott+11_1_sil=16000:gs=on:random_seed=1531546739:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2910 on theBenchmark for (2910ds/2251Mi)
% 127.36/34.83 % TRYING [3]
% 127.36/34.83 % (3387845)Instruction limit reached!
% 127.36/34.83 % (3387845)------------------------------
% 127.36/34.83 % (3387845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387845)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387845)Termination reason: Instruction limit
% 127.36/34.83 % (3387845)Termination phase: Saturation
% 127.36/34.83 % (3387845)Time elapsed: 1.194 s
% 127.36/34.83 % (3387845)Peak memory usage: 34 MB
% 127.36/34.83 % (3387845)Instructions burned: 2252 (million)
% 127.36/34.83 % (3387847)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=782832085:fmbsr=1.6:i=67534_2898 on theBenchmark for (2898ds/67534Mi)
% 127.36/34.83 % (3387843)Instruction limit reached!
% 127.36/34.83 % (3387843)------------------------------
% 127.36/34.83 % (3387843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387843)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387843)Termination reason: Instruction limit
% 127.36/34.83 % (3387843)Termination phase: Saturation
% 127.36/34.83 % (3387843)Time elapsed: 2.150 s
% 127.36/34.83 % (3387843)Peak memory usage: 55 MB
% 127.36/34.83 % (3387843)Instructions burned: 3773 (million)
% 127.36/34.83 % (3387849)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1747575361:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2896 on theBenchmark for (2896ds/4591Mi)
% 127.36/34.83 % (3387849)Instruction limit reached!
% 127.36/34.83 % (3387849)------------------------------
% 127.36/34.83 % (3387849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387849)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387849)Termination reason: Instruction limit
% 127.36/34.83 % (3387849)Termination phase: Saturation
% 127.36/34.83 % (3387849)Time elapsed: 1.722 s
% 127.36/34.83 % (3387849)Peak memory usage: 31 MB
% 127.36/34.83 % (3387849)Instructions burned: 4593 (million)
% 127.36/34.83 % (3387851)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4058404025:i=29340_2878 on theBenchmark for (2878ds/29340Mi)
% 127.36/34.83 % (3387821)Instruction limit reached!
% 127.36/34.83 % (3387821)------------------------------
% 127.36/34.83 % (3387821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387821)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387821)Termination reason: Instruction limit
% 127.36/34.83 % (3387821)Termination phase: Finite model building preprocessing
% 127.36/34.83 % (3387821)Time elapsed: 11.568 s
% 127.36/34.83 % (3387821)Peak memory usage: 216 MB
% 127.36/34.83 % (3387821)Instructions burned: 22063 (million)
% 127.36/34.83 % (3387853)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2833804602:i=5211_2871 on theBenchmark for (2871ds/5211Mi)
% 127.36/34.83 % (3387853)Instruction limit reached!
% 127.36/34.83 % (3387853)------------------------------
% 127.36/34.83 % (3387853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387853)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387853)Termination reason: Instruction limit
% 127.36/34.83 % (3387853)Termination phase: Saturation
% 127.36/34.83 % (3387853)Time elapsed: 2.156 s
% 127.36/34.83 % (3387853)Peak memory usage: 47 MB
% 127.36/34.83 % (3387853)Instructions burned: 5212 (million)
% 127.36/34.83 % (3387855)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3849239285:i=5497:nm=2_2850 on theBenchmark for (2850ds/5497Mi)
% 127.36/34.83 % (3387855)Instruction limit reached!
% 127.36/34.83 % (3387855)------------------------------
% 127.36/34.83 % (3387855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.83 % (3387855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.83 % (3387855)CaDiCaL version: 2.1.3
% 127.36/34.83 % (3387855)Termination reason: Instruction limit
% 127.36/34.83 % (3387855)Termination phase: Finite model building preprocessing
% 127.36/34.84 % (3387855)Time elapsed: 2.811 s
% 127.36/34.84 % (3387855)Peak memory usage: 64 MB
% 127.36/34.84 % (3387855)Instructions burned: 5497 (million)
% 127.36/34.84 % (3387857)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2879009280:fmbsr=2:i=46332_2821 on theBenchmark for (2821ds/46332Mi)
% 127.36/34.84 % TRYING [1]
% 127.36/34.84 % TRYING [2]
% 127.36/34.84 % TRYING [3]
% 127.36/34.84 % (3387847)Cannot represent all propositional literals internally
% 127.36/34.84 % (3387847)Refutation not found, incomplete strategy
% 127.36/34.84 % (3387847)------------------------------
% 127.36/34.84 % (3387847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.84 % (3387847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.84 % (3387847)CaDiCaL version: 2.1.3
% 127.36/34.84 % (3387847)Termination reason: Refutation not found, incomplete strategy
% 127.36/34.84 % (3387847)Time elapsed: 12.463 s
% 127.36/34.84 % (3387847)Peak memory usage: 192 MB
% 127.36/34.84 % (3387847)Instructions burned: 23959 (million)
% 127.36/34.84 % (3387847)------------------------------
% 127.36/34.84 % (3387847)------------------------------
% 127.36/34.84 % (3387860)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=605599393:i=14071_2772 on theBenchmark for (2772ds/14071Mi)
% 127.36/34.84 % TRYING [4]
% 127.36/34.84 % (3387851)Instruction limit reached!
% 127.36/34.84 % (3387851)------------------------------
% 127.36/34.84 % (3387851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.84 % (3387851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.84 % (3387851)CaDiCaL version: 2.1.3
% 127.36/34.84 % (3387851)Termination reason: Instruction limit
% 127.36/34.84 % (3387851)Termination phase: Saturation
% 127.36/34.84 % (3387851)Time elapsed: 15.317 s
% 127.36/34.84 % (3387851)Peak memory usage: 188 MB
% 127.36/34.84 % (3387851)Instructions burned: 29341 (million)
% 127.36/34.84 % (3387862)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2529892327:i=22565:add=on:rawr=on_2724 on theBenchmark for (2724ds/22565Mi)
% 127.36/34.84 % (3387860)Instruction limit reached!
% 127.36/34.84 % (3387860)------------------------------
% 127.36/34.84 % (3387860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.84 % (3387860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.84 % (3387860)CaDiCaL version: 2.1.3
% 127.36/34.84 % (3387860)Termination reason: Instruction limit
% 127.36/34.84 % (3387860)Termination phase: Finite model building preprocessing
% 127.36/34.84 % (3387860)Time elapsed: 7.358 s
% 127.36/34.84 % (3387860)Peak memory usage: 109 MB
% 127.36/34.84 % (3387860)Instructions burned: 14072 (million)
% 127.36/34.84 % (3387864)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1335699141:i=8173:av=off_2698 on theBenchmark for (2698ds/8173Mi)
% 127.36/34.84 % (3387857)Cannot represent all propositional literals internally
% 127.36/34.84 % (3387857)Refutation not found, incomplete strategy
% 127.36/34.84 % (3387857)------------------------------
% 127.36/34.84 % (3387857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.84 % (3387857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.84 % (3387857)CaDiCaL version: 2.1.3
% 127.36/34.84 % (3387857)Termination reason: Refutation not found, incomplete strategy
% 127.36/34.84 % (3387857)Time elapsed: 12.427 s
% 127.36/34.84 % (3387857)Peak memory usage: 192 MB
% 127.36/34.84 % (3387857)Instructions burned: 23958 (million)
% 127.36/34.84 % (3387857)------------------------------
% 127.36/34.84 % (3387857)------------------------------
% 127.36/34.84 % (3387866)dis+10_16:1_sil=16000:random_seed=653604974:i=9155:fsr=off_2696 on theBenchmark for (2696ds/9155Mi)
% 127.36/34.84 % (3387839)Instruction limit reached!
% 127.36/34.84 % (3387839)------------------------------
% 127.36/34.84 % (3387839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.84 % (3387839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.84 % (3387839)CaDiCaL version: 2.1.3
% 127.36/34.84 % (3387839)Termination reason: Instruction limit
% 127.36/34.84 % (3387839)Termination phase: Finite model building constraint generation
% 127.36/34.84 % (3387839)Time elapsed: 25.467 s
% 127.36/34.84 % (3387839)Peak memory usage: 2589 MB
% 127.36/34.84 % (3387839)Instructions burned: 54283 (million)
% 127.36/34.84 % (3387868)ott-3_8_sil=64000:random_seed=1412688451:i=20139:bs=on_2683 on theBenchmark for (2683ds/20139Mi)
% 127.36/34.84 % (3387864) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3387782-3387864"...
% 127.36/34.84 % (3387864)...printing done.
% 127.36/34.84 % (3387864)Refutation found. Thanks to Tanya!
% 127.36/34.84 % SZS status Theorem for theBenchmark
% 127.36/34.84 % SZS output start Proof for theBenchmark
% See solution above
% 127.36/34.84 % (3387864)------------------------------
% 127.36/34.84 % (3387864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.36/34.84 % (3387864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.36/34.84 % (3387864)CaDiCaL version: 2.1.3
% 127.36/34.84 % (3387864)Termination reason: Refutation
% 127.36/34.84 % (3387864)Time elapsed: 4.137 s
% 127.36/34.84 % (3387864)Peak memory usage: 83 MB
% 127.36/34.84 % (3387864)Instructions burned: 6667 (million)
% 127.36/34.84 % (3387782)Success in time 34.584 s
% 127.36/34.84 % Vampire exiting
%------------------------------------------------------------------------------