%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL503+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 11:58:49 AM UTC 2026
% Result : Theorem 61.35s 18.18s
% Output : Refutation 61.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 12
% Syntax : Number of formulae : 85 ( 58 unt; 0 def)
% Number of atoms : 123 ( 5 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 90 ( 52 ~; 23 |; 2 &)
% ( 5 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 7 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 158 ( 156 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',modus_ponens) ).
fof(f4,axiom,
( implies_1
<=> ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',implies_1) ).
fof(f16,axiom,
( kn1
<=> ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',kn1) ).
fof(f17,axiom,
( kn2
<=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',kn2) ).
fof(f18,axiom,
( kn3
<=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',kn3) ).
fof(f29,axiom,
( op_implies_and
=> ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+1.ax',op_implies_and) ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+5.ax',rosser_op_implies_and) ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+5.ax',rosser_modus_ponens) ).
fof(f36,axiom,
kn1,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+5.ax',rosser_kn1) ).
fof(f37,axiom,
kn2,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+5.ax',rosser_kn2) ).
fof(f38,axiom,
kn3,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+5.ax',rosser_kn3) ).
fof(f43,conjecture,
implies_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hilbert_implies_1) ).
fof(f44,negated_conjecture,
~ implies_1,
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f45,plain,
~ implies_1,
inference(flattening,[],[f44]) ).
fof(f46,plain,
( kn3
=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
inference(unused_predicate_definition_removal,[],[f18]) ).
fof(f47,plain,
( kn2
=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
inference(unused_predicate_definition_removal,[],[f17]) ).
fof(f48,plain,
( kn1
=> ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
inference(unused_predicate_definition_removal,[],[f16]) ).
fof(f49,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0)))
=> implies_1 ),
inference(unused_predicate_definition_removal,[],[f4]) ).
fof(f51,plain,
( modus_ponens
=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f54,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) )
| ~ modus_ponens ),
inference(ennf_transformation,[],[f51]) ).
fof(f55,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) )
| ~ modus_ponens ),
inference(flattening,[],[f54]) ).
fof(f57,plain,
( implies_1
| ? [X0,X1] : ~ is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(ennf_transformation,[],[f49]) ).
fof(f58,plain,
( ! [X0] : is_a_theorem(implies(X0,and(X0,X0)))
| ~ kn1 ),
inference(ennf_transformation,[],[f48]) ).
fof(f59,plain,
( ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(ennf_transformation,[],[f47]) ).
fof(f60,plain,
( ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
| ~ kn3 ),
inference(ennf_transformation,[],[f46]) ).
fof(f62,plain,
( ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(ennf_transformation,[],[f29]) ).
fof(f64,plain,
( implies_1
| ~ is_a_theorem(implies(sK0,implies(sK1,sK0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f57]) ).
fof(f65,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1))
| ~ modus_ponens ),
inference(cnf_transformation,[],[f55]) ).
fof(f67,plain,
( implies_1
| ~ is_a_theorem(implies(sK0,implies(sK1,sK0))) ),
inference(cnf_transformation,[],[f64]) ).
fof(f68,plain,
! [X0] :
( is_a_theorem(implies(X0,and(X0,X0)))
| ~ kn1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f69,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f70,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
| ~ kn3 ),
inference(cnf_transformation,[],[f60]) ).
fof(f72,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[],[f62]) ).
fof(f75,plain,
op_implies_and,
inference(cnf_transformation,[],[f33]) ).
fof(f77,plain,
modus_ponens,
inference(cnf_transformation,[],[f35]) ).
fof(f78,plain,
kn1,
inference(cnf_transformation,[],[f36]) ).
fof(f79,plain,
kn2,
inference(cnf_transformation,[],[f37]) ).
fof(f80,plain,
kn3,
inference(cnf_transformation,[],[f38]) ).
fof(f85,plain,
~ implies_1,
inference(cnf_transformation,[],[f45]) ).
fof(f86,plain,
~ is_a_theorem(implies(sK0,implies(sK1,sK0))),
inference(forward_subsumption_resolution,[],[f67,f85]) ).
fof(f87,plain,
! [X0] : is_a_theorem(implies(X0,and(X0,X0))),
inference(forward_subsumption_resolution,[],[f68,f78]) ).
fof(f88,plain,
! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)),
inference(forward_subsumption_resolution,[],[f69,f79]) ).
fof(f90,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
inference(forward_subsumption_resolution,[],[f65,f77]) ).
fof(f95,plain,
! [X0] : ~ is_a_theorem(and(implies(sK0,implies(sK1,sK0)),X0)),
inference(unit_resulting_resolution,[],[f90,f86,f88]) ).
fof(f101,plain,
! [X0,X1] : ~ is_a_theorem(and(and(implies(sK0,implies(sK1,sK0)),X0),X1)),
inference(unit_resulting_resolution,[],[f90,f88,f95]) ).
fof(f103,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(implies(implies(and(X0,X1),X0),and(and(implies(sK0,implies(sK1,sK0)),X2),X3))),
inference(unit_resulting_resolution,[],[f90,f88,f101]) ).
fof(f252,plain,
! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))),
inference(forward_subsumption_resolution,[],[f72,f75]) ).
fof(f477,plain,
! [X2,X0,X1] : implies(X2,and(X0,not(X1))) = not(and(X2,implies(X0,X1))),
inference(superposition,[],[f252,f252]) ).
fof(f1634,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))),
inference(forward_subsumption_resolution,[],[f70,f80]) ).
fof(f1844,plain,
! [X0,X1] : is_a_theorem(implies(not(and(and(X0,X0),X1)),not(and(X1,X0)))),
inference(unit_resulting_resolution,[],[f90,f87,f1634]) ).
fof(f1845,plain,
! [X2,X0,X1] : is_a_theorem(implies(not(and(X0,X1)),not(and(X1,and(X0,X2))))),
inference(unit_resulting_resolution,[],[f90,f88,f1634]) ).
fof(f2343,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X2,X0),implies(implies(X0,X1),not(and(not(X1),X2))))),
inference(superposition,[],[f1634,f252]) ).
fof(f2344,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(X1),X2),implies(not(and(X2,X0)),implies(X0,X1)))),
inference(superposition,[],[f1634,f252]) ).
fof(f7285,plain,
! [X2,X0,X1] : is_a_theorem(implies(not(and(not(and(X0,X1)),X2)),not(and(X2,not(and(and(X1,X1),X0)))))),
inference(unit_resulting_resolution,[],[f90,f1634,f1844]) ).
fof(f7288,plain,
! [X0,X1] : is_a_theorem(implies(implies(and(X0,X0),X1),not(and(not(X1),X0)))),
inference(superposition,[],[f1844,f252]) ).
fof(f7290,plain,
! [X2,X0,X1] : is_a_theorem(implies(not(and(not(and(X0,X1)),X2)),implies(X2,and(and(X1,X1),X0)))),
inference(forward_demodulation,[],[f7285,f252]) ).
fof(f11748,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(and(X0,X1)),X2),not(and(not(X2),not(and(and(X1,X1),X0)))))),
inference(unit_resulting_resolution,[],[f90,f1844,f2343]) ).
fof(f11749,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(not(and(X0,and(X1,X2))),X3),not(and(not(X3),not(and(X1,X0)))))),
inference(unit_resulting_resolution,[],[f90,f1845,f2343]) ).
fof(f12637,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(X1),X2),implies(implies(X2,X0),implies(not(X0),X1)))),
inference(superposition,[],[f2343,f252]) ).
fof(f12640,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(and(X0,X1)),X2),implies(not(X2),and(and(X1,X1),X0)))),
inference(forward_demodulation,[],[f11748,f252]) ).
fof(f12641,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(not(and(X0,and(X1,X2))),X3),implies(not(X3),and(X1,X0)))),
inference(forward_demodulation,[],[f11749,f252]) ).
fof(f13802,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X0),X1))
| is_a_theorem(implies(not(and(X1,X2)),implies(X2,X0))) ),
inference(resolution,[],[f2344,f90]) ).
fof(f58593,plain,
! [X2,X0,X1] : ~ is_a_theorem(not(and(not(and(X0,implies(sK0,implies(sK1,sK0)))),implies(and(X1,X2),X1)))),
inference(unit_resulting_resolution,[],[f90,f103,f7290]) ).
fof(f70008,plain,
! [X2,X0,X1] : ~ is_a_theorem(implies(not(and(X0,implies(sK0,implies(sK1,sK0)))),and(and(X1,X2),not(X1)))),
inference(superposition,[],[f58593,f477]) ).
fof(f70113,plain,
! [X0,X1] : ~ is_a_theorem(not(and(not(and(not(X0),X0)),not(and(X1,implies(sK0,implies(sK1,sK0))))))),
inference(unit_resulting_resolution,[],[f90,f7290,f70008]) ).
fof(f70121,plain,
! [X0,X1] : ~ is_a_theorem(implies(not(and(not(X0),X0)),and(X1,implies(sK0,implies(sK1,sK0))))),
inference(forward_demodulation,[],[f70113,f252]) ).
fof(f70144,plain,
! [X0,X1] : ~ is_a_theorem(not(and(not(and(implies(sK0,implies(sK1,sK0)),X0)),not(and(not(X1),X1))))),
inference(unit_resulting_resolution,[],[f90,f7290,f70121]) ).
fof(f70152,plain,
! [X0,X1] : ~ is_a_theorem(implies(not(and(implies(sK0,implies(sK1,sK0)),X0)),and(not(X1),X1))),
inference(forward_demodulation,[],[f70144,f252]) ).
fof(f70180,plain,
! [X2,X0,X1] : ~ is_a_theorem(implies(implies(X0,and(X0,X0)),implies(not(and(implies(sK0,implies(sK1,sK0)),X1)),and(not(X2),X2)))),
inference(unit_resulting_resolution,[],[f90,f87,f70152]) ).
fof(f193655,plain,
! [X0] : ~ is_a_theorem(implies(not(and(not(X0),X0)),implies(sK0,implies(sK1,sK0)))),
inference(unit_resulting_resolution,[],[f90,f12637,f70180]) ).
fof(f193667,plain,
~ is_a_theorem(implies(not(implies(sK1,sK0)),not(sK0))),
inference(unit_resulting_resolution,[],[f13802,f193655]) ).
fof(f193744,plain,
! [X0,X1] : ~ is_a_theorem(implies(implies(and(X0,X1),X0),implies(not(implies(sK1,sK0)),not(sK0)))),
inference(unit_resulting_resolution,[],[f90,f88,f193667]) ).
fof(f194201,plain,
! [X0] : ~ is_a_theorem(implies(not(not(sK0)),and(implies(sK1,sK0),X0))),
inference(unit_resulting_resolution,[],[f90,f12637,f193744]) ).
fof(f194235,plain,
! [X2,X0,X1] : ~ is_a_theorem(implies(implies(and(X0,X1),X0),implies(not(not(sK0)),and(implies(sK1,sK0),X2)))),
inference(unit_resulting_resolution,[],[f90,f88,f194201]) ).
fof(f195619,plain,
! [X0,X1] : ~ is_a_theorem(implies(not(and(implies(sK1,sK0),X0)),and(not(sK0),X1))),
inference(unit_resulting_resolution,[],[f90,f12637,f194235]) ).
fof(f195701,plain,
! [X2,X0,X1] : ~ is_a_theorem(implies(not(and(X0,and(not(sK0),X1))),and(implies(sK1,sK0),X2))),
inference(unit_resulting_resolution,[],[f90,f12641,f195619]) ).
fof(f195898,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(implies(not(and(X0,and(implies(sK1,sK0),X1))),and(X2,and(not(sK0),X3)))),
inference(unit_resulting_resolution,[],[f90,f12641,f195701]) ).
fof(f196600,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(implies(not(and(and(not(sK0),X0),X1)),and(X2,and(implies(sK1,sK0),X3)))),
inference(unit_resulting_resolution,[],[f90,f12640,f195898]) ).
fof(f196644,plain,
! [X2,X3,X0,X1] : ~ is_a_theorem(implies(not(and(and(implies(sK1,sK0),X0),X1)),and(and(not(sK0),X2),X3))),
inference(unit_resulting_resolution,[],[f90,f12640,f196600]) ).
fof(f196732,plain,
! [X2,X0,X1] : ~ is_a_theorem(implies(not(and(X0,not(sK0))),and(and(implies(sK1,sK0),X1),X2))),
inference(unit_resulting_resolution,[],[f90,f12640,f196644]) ).
fof(f196744,plain,
! [X2,X0,X1] : ~ is_a_theorem(implies(implies(X0,sK0),and(and(implies(sK1,sK0),X1),X2))),
inference(forward_demodulation,[],[f196732,f252]) ).
fof(f196787,plain,
! [X0,X1] : ~ is_a_theorem(not(and(not(and(X0,implies(sK1,sK0))),implies(X1,sK0)))),
inference(unit_resulting_resolution,[],[f90,f7290,f196744]) ).
fof(f196829,plain,
! [X0,X1] : ~ is_a_theorem(implies(and(implies(X0,sK0),implies(X0,sK0)),and(X1,implies(sK1,sK0)))),
inference(unit_resulting_resolution,[],[f90,f7288,f196787]) ).
fof(f197443,plain,
! [X0,X1] : ~ is_a_theorem(not(and(not(and(implies(sK1,sK0),X0)),and(implies(X1,sK0),implies(X1,sK0))))),
inference(unit_resulting_resolution,[],[f90,f7290,f196829]) ).
fof(f198737,plain,
$false,
inference(unit_resulting_resolution,[],[f90,f88,f7288,f197443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL503+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 % Computer : n026.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Sun Sep 27 15:56:30 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.44 Running first-order model finding
% 0.13/0.44 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
% 27.98/4.48 % (3027123)Will run a generic schedule for satisfiability detection.
% 27.98/4.48 % (3027134)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1505587902:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.98/4.48 % (3027129)% WARNING: option uhcvi not known.
% 27.98/4.48 % (3027128)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3131030584_2999 on theBenchmark for (2999ds/0Mi)
% 27.98/4.48 % (3027133)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1353181564:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.98/4.48 % (3027129)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3652921012:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.98/4.48 % (3027130)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3589313908:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.98/4.48 % (3027131)dis+10_1_sil=32000:sp=arity:random_seed=3819070752:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.98/4.48 % (3027132)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1637545565:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.98/4.48 % TRYING [1]
% 27.98/4.48 % TRYING [2]
% 27.98/4.48 % TRYING [3]
% 27.98/4.48 % TRYING [4]
% 27.98/4.48 % (3027134)Instruction limit reached!
% 27.98/4.48 % (3027134)------------------------------
% 27.98/4.48 % (3027134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.48 % (3027134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.48 % (3027134)CaDiCaL version: 2.1.3
% 27.98/4.48 % (3027134)Termination reason: Instruction limit
% 27.98/4.48 % (3027134)Termination phase: Saturation
% 27.98/4.48 % (3027134)Time elapsed: 0.062 s
% 27.98/4.48 % (3027134)Peak memory usage: 14 MB
% 27.98/4.48 % (3027134)Instructions burned: 160 (million)
% 27.98/4.48 % (3027142)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3148608585:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 27.98/4.48 % (3027131)Instruction limit reached!
% 27.98/4.48 % (3027131)------------------------------
% 27.98/4.48 % (3027131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.48 % (3027131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.48 % (3027131)CaDiCaL version: 2.1.3
% 27.98/4.48 % (3027131)Termination reason: Instruction limit
% 27.98/4.48 % (3027131)Termination phase: Saturation
% 27.98/4.48 % (3027131)Time elapsed: 0.068 s
% 27.98/4.48 % (3027131)Peak memory usage: 13 MB
% 27.98/4.48 % (3027131)Instructions burned: 104 (million)
% 27.98/4.48 % TRYING [1]
% 27.98/4.48 % TRYING [2]
% 27.98/4.48 % TRYING [3]
% 27.98/4.48 % TRYING [4]
% 27.98/4.48 % (3027132)Instruction limit reached!
% 27.98/4.48 % (3027132)------------------------------
% 27.98/4.48 % (3027132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.48 % (3027132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.48 % (3027132)CaDiCaL version: 2.1.3
% 27.98/4.48 % (3027132)Termination reason: Instruction limit
% 27.98/4.48 % (3027132)Termination phase: Saturation
% 27.98/4.48 % (3027132)Time elapsed: 0.077 s
% 27.98/4.48 % (3027132)Peak memory usage: 13 MB
% 27.98/4.48 % (3027132)Instructions burned: 116 (million)
% 27.98/4.48 % (3027133)Instruction limit reached!
% 27.98/4.48 % (3027133)------------------------------
% 27.98/4.48 % (3027133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.48 % (3027133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.98/4.48 % (3027133)CaDiCaL version: 2.1.3
% 27.98/4.48 % (3027133)Termination reason: Instruction limit
% 27.98/4.48 % (3027133)Termination phase: Saturation
% 27.98/4.48 % (3027133)Time elapsed: 0.085 s
% 27.98/4.48 % (3027133)Peak memory usage: 13 MB
% 27.98/4.48 % (3027133)Instructions burned: 131 (million)
% 27.98/4.48 % (3027144)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=792348553:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.98/4.48 % (3027145)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=603538561:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.98/4.48 % (3027146)ott-21_1_sil=16000:fs=off:random_seed=2094694839:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 27.98/4.48 % (3027144)Instruction limit reached!
% 27.98/4.48 % (3027144)------------------------------
% 27.98/4.48 % (3027144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.98/4.48 % (3027144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.38/7.90 % (3027144)CaDiCaL version: 2.1.3
% 52.38/7.90 % (3027144)Termination reason: Instruction limit
% 52.38/7.90 % (3027144)Termination phase: Saturation
% 52.38/7.90 % (3027144)Time elapsed: 0.090 s
% 52.38/7.90 % (3027144)Peak memory usage: 14 MB
% 52.38/7.90 % (3027144)Instructions burned: 131 (million)
% 52.38/7.90 % (3027146)Instruction limit reached!
% 52.38/7.90 % (3027146)------------------------------
% 52.38/7.90 % (3027146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.38/7.90 % (3027146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.38/7.90 % (3027146)CaDiCaL version: 2.1.3
% 52.38/7.90 % (3027146)Termination reason: Instruction limit
% 52.38/7.90 % (3027146)Termination phase: Saturation
% 52.38/7.90 % (3027146)Time elapsed: 0.086 s
% 52.38/7.90 % (3027146)Peak memory usage: 12 MB
% 52.38/7.90 % (3027146)Instructions burned: 182 (million)
% 52.38/7.90 % (3027150)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=948797792:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 52.38/7.90 % TRYING [5]
% 52.38/7.90 % TRYING [5]
% 52.38/7.90 % (3027151)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=664558997:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 52.38/7.90 % TRYING [1]
% 52.38/7.90 % TRYING [2]
% 52.38/7.90 % TRYING [3]
% 52.38/7.90 % TRYING [4]
% 52.38/7.90 % (3027142)Instruction limit reached!
% 52.38/7.90 % (3027142)------------------------------
% 52.38/7.90 % (3027142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.38/7.90 % (3027142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.38/7.90 % (3027142)CaDiCaL version: 2.1.3
% 52.38/7.90 % (3027142)Termination reason: Instruction limit
% 52.38/7.90 % (3027142)Termination phase: Finite model building SAT solving
% 52.38/7.90 % (3027142)Time elapsed: 0.227 s
% 52.38/7.90 % (3027142)Peak memory usage: 16 MB
% 52.38/7.90 % (3027142)Instructions burned: 714 (million)
% 52.38/7.90 % (3027154)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=163271523:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 52.38/7.90 % (3027150)Instruction limit reached!
% 52.38/7.90 % (3027150)------------------------------
% 52.38/7.90 % (3027150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.38/7.90 % (3027150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.38/7.90 % (3027150)CaDiCaL version: 2.1.3
% 52.38/7.90 % (3027150)Termination reason: Instruction limit
% 52.38/7.90 % (3027150)Termination phase: Saturation
% 52.38/7.90 % (3027150)Time elapsed: 0.318 s
% 52.38/7.90 % (3027150)Peak memory usage: 14 MB
% 52.38/7.90 % (3027150)Instructions burned: 478 (million)
% 52.38/7.90 % (3027156)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2347180227:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 52.38/7.90 % (3027145)Instruction limit reached!
% 52.38/7.90 % (3027145)------------------------------
% 52.38/7.90 % (3027145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.38/7.90 % (3027145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.38/7.90 % (3027145)CaDiCaL version: 2.1.3
% 52.38/7.90 % (3027145)Termination reason: Instruction limit
% 52.38/7.90 % (3027145)Termination phase: Saturation
% 52.38/7.90 % (3027145)Time elapsed: 0.452 s
% 52.38/7.90 % (3027145)Peak memory usage: 18 MB
% 52.38/7.90 % (3027145)Instructions burned: 685 (million)
% 52.38/7.90 % (3027158)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=1955082345:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 52.38/7.90 % TRYING [14]
% 52.38/7.90 % TRYING [5]
% 52.38/7.90 % (3027151)Instruction limit reached!
% 52.38/7.90 % (3027151)------------------------------
% 52.38/7.90 % (3027151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.38/7.90 % (3027151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.38/7.90 % (3027151)CaDiCaL version: 2.1.3
% 52.38/7.90 % (3027151)Termination reason: Instruction limit
% 52.38/7.90 % (3027151)Termination phase: Finite model building constraint generation
% 52.38/7.90 % (3027151)Time elapsed: 0.401 s
% 52.38/7.90 % (3027151)Peak memory usage: 18 MB
% 52.38/7.90 % (3027151)Instructions burned: 867 (million)
% 52.38/7.90 % (3027160)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3600687617:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 52.38/7.90 % (3027154)Instruction limit reached!
% 52.38/7.90 % (3027154)------------------------------
% 118.73/17.27 % (3027154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.73/17.27 % (3027154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/17.27 % (3027154)CaDiCaL version: 2.1.3
% 118.73/17.27 % (3027154)Termination reason: Instruction limit
% 118.73/17.27 % (3027154)Termination phase: Saturation
% 118.73/17.27 % (3027154)Time elapsed: 0.383 s
% 118.73/17.27 % (3027154)Peak memory usage: 26 MB
% 118.73/17.27 % (3027154)Instructions burned: 1179 (million)
% 118.73/17.27 % (3027162)fmb+10_1_sil=64000:random_seed=2632424447:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 118.73/17.27 % TRYING [1]
% 118.73/17.27 % TRYING [2]
% 118.73/17.27 % TRYING [3]
% 118.73/17.27 % TRYING [4]
% 118.73/17.27 % TRYING [5]
% 118.73/17.27 % (3027156)Instruction limit reached!
% 118.73/17.27 % (3027156)------------------------------
% 118.73/17.27 % (3027156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.73/17.27 % (3027156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/17.27 % (3027156)CaDiCaL version: 2.1.3
% 118.73/17.27 % (3027156)Termination reason: Instruction limit
% 118.73/17.27 % (3027156)Termination phase: Finite model building constraint generation
% 118.73/17.28 % (3027156)Time elapsed: 0.311 s
% 118.73/17.28 % (3027156)Peak memory usage: 66 MB
% 118.73/17.28 % (3027156)Instructions burned: 892 (million)
% 118.73/17.28 % (3027164)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2409692378:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 118.73/17.28 % TRYING [20]
% 118.73/17.28 % (3027158)Instruction limit reached!
% 118.73/17.28 % (3027158)------------------------------
% 118.73/17.28 % (3027158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.73/17.28 % (3027158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/17.28 % (3027158)CaDiCaL version: 2.1.3
% 118.73/17.28 % (3027158)Termination reason: Instruction limit
% 118.73/17.28 % (3027158)Termination phase: Saturation
% 118.73/17.28 % (3027158)Time elapsed: 0.463 s
% 118.73/17.28 % (3027158)Peak memory usage: 20 MB
% 118.73/17.28 % (3027158)Instructions burned: 693 (million)
% 118.73/17.28 % (3027166)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2443426172:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 118.73/17.28 % TRYING [8]
% 118.73/17.28 % (3027160)Instruction limit reached!
% 118.73/17.28 % (3027160)------------------------------
% 118.73/17.28 % (3027160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.73/17.28 % (3027160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/17.28 % (3027160)CaDiCaL version: 2.1.3
% 118.73/17.28 % (3027160)Termination reason: Instruction limit
% 118.73/17.28 % (3027160)Termination phase: Saturation
% 118.73/17.28 % (3027160)Time elapsed: 0.536 s
% 118.73/17.28 % (3027160)Peak memory usage: 21 MB
% 118.73/17.28 % (3027160)Instructions burned: 879 (million)
% 118.73/17.28 % (3027168)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1390135495:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 118.73/17.28 % (3027166)Instruction limit reached!
% 118.73/17.28 % (3027166)------------------------------
% 118.73/17.28 % (3027166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.73/17.28 % (3027166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/17.28 % (3027166)CaDiCaL version: 2.1.3
% 118.73/17.28 % (3027166)Termination reason: Instruction limit
% 118.73/17.28 % (3027166)Termination phase: Finite model building SAT solving
% 118.73/17.28 % (3027166)Time elapsed: 0.475 s
% 118.73/17.28 % (3027166)Peak memory usage: 52 MB
% 118.73/17.28 % (3027166)Instructions burned: 922 (million)
% 118.73/17.28 % (3027170)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3109569214:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 118.73/17.28 % TRYING [6]
% 118.73/17.28 % (3027170)Instruction limit reached!
% 118.73/17.28 % (3027170)------------------------------
% 118.73/17.28 % (3027170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.73/17.28 % (3027170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.73/17.28 % (3027170)CaDiCaL version: 2.1.3
% 118.73/17.28 % (3027170)Termination reason: Instruction limit
% 118.73/17.28 % (3027170)Termination phase: Saturation
% 118.73/17.28 % (3027170)Time elapsed: 0.692 s
% 118.73/17.28 % (3027170)Peak memory usage: 27 MB
% 118.73/17.28 % (3027170)Instructions burned: 1473 (million)
% 118.73/17.28 % (3027172)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1723797974:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 118.73/17.28 % TRYING [77]
% 118.73/17.28 % TRYING [6]
% 118.73/17.28 % (3027168)Instruction limit reached!
% 61.35/18.18 % (3027168)------------------------------
% 61.35/18.18 % (3027168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027168)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027168)Termination reason: Instruction limit
% 61.35/18.18 % (3027168)Termination phase: Saturation
% 61.35/18.18 % (3027168)Time elapsed: 2.806 s
% 61.35/18.18 % (3027168)Peak memory usage: 54 MB
% 61.35/18.18 % (3027168)Instructions burned: 5132 (million)
% 61.35/18.18 % (3027174)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=40338688:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 61.35/18.18 % TRYING [16]
% 61.35/18.18 % (3027164)Instruction limit reached!
% 61.35/18.18 % (3027164)------------------------------
% 61.35/18.18 % (3027164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027164)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027164)Termination reason: Instruction limit
% 61.35/18.18 % (3027164)Termination phase: Finite model building constraint generation
% 61.35/18.18 % (3027164)Time elapsed: 3.355 s
% 61.35/18.18 % (3027164)Peak memory usage: 599 MB
% 61.35/18.18 % (3027164)Instructions burned: 9516 (million)
% 61.35/18.18 % (3027176)ott-2_1_sil=16000:newcnf=on:random_seed=234414661:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 61.35/18.18 % (3027172)Instruction limit reached!
% 61.35/18.18 % (3027172)------------------------------
% 61.35/18.18 % (3027172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027172)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027172)Termination reason: Instruction limit
% 61.35/18.18 % (3027172)Termination phase: Finite model building constraint generation
% 61.35/18.18 % (3027172)Time elapsed: 2.309 s
% 61.35/18.18 % (3027172)Peak memory usage: 415 MB
% 61.35/18.18 % (3027172)Instructions burned: 6325 (million)
% 61.35/18.18 % (3027178)ott+10_1_sil=32000:tgt=ground:random_seed=2672747754:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 61.35/18.18 % (3027174)Instruction limit reached!
% 61.35/18.18 % (3027174)------------------------------
% 61.35/18.18 % (3027174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027174)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027174)Termination reason: Instruction limit
% 61.35/18.18 % (3027174)Termination phase: Finite model building constraint generation
% 61.35/18.18 % (3027174)Time elapsed: 0.735 s
% 61.35/18.18 % (3027174)Peak memory usage: 132 MB
% 61.35/18.18 % (3027174)Instructions burned: 2176 (million)
% 61.35/18.18 % (3027180)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=486405022:i=54282_2951 on theBenchmark for (2951ds/54282Mi)
% 61.35/18.18 % TRYING [1]
% 61.35/18.18 % TRYING [2]
% 61.35/18.18 % TRYING [3]
% 61.35/18.18 % TRYING [4]
% 61.35/18.18 % (3027176)Instruction limit reached!
% 61.35/18.18 % (3027176)------------------------------
% 61.35/18.18 % (3027176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027176)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027176)Termination reason: Instruction limit
% 61.35/18.18 % (3027176)Termination phase: Saturation
% 61.35/18.18 % (3027176)Time elapsed: 0.553 s
% 61.35/18.18 % (3027176)Peak memory usage: 18 MB
% 61.35/18.18 % (3027176)Instructions burned: 870 (million)
% 61.35/18.18 % (3027182)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1617133985:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 61.35/18.18 % TRYING [5]
% 61.35/18.18 % (3027182)Instruction limit reached!
% 61.35/18.18 % (3027182)------------------------------
% 61.35/18.18 % (3027182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027182)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027182)Termination reason: Instruction limit
% 61.35/18.18 % (3027182)Termination phase: Saturation
% 61.35/18.18 % (3027182)Time elapsed: 2.069 s
% 61.35/18.18 % (3027182)Peak memory usage: 45 MB
% 61.35/18.18 % (3027182)Instructions burned: 3512 (million)
% 61.35/18.18 % (3027184)dis+21_1_sil=32000:sas=cadical:random_seed=2600694729:i=3773:amm=off_2929 on theBenchmark for (2929ds/3773Mi)
% 61.35/18.18 % TRYING [6]
% 61.35/18.18 % (3027178)Instruction limit reached!
% 61.35/18.18 % (3027178)------------------------------
% 61.35/18.18 % (3027178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027178)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027178)Termination reason: Instruction limit
% 61.35/18.18 % (3027178)Termination phase: Saturation
% 61.35/18.18 % (3027178)Time elapsed: 3.234 s
% 61.35/18.18 % (3027178)Peak memory usage: 55 MB
% 61.35/18.18 % (3027178)Instructions burned: 5115 (million)
% 61.35/18.18 % (3027186)ott+11_1_sil=16000:gs=on:random_seed=3302137912:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2920 on theBenchmark for (2920ds/2251Mi)
% 61.35/18.18 % (3027162)Instruction limit reached!
% 61.35/18.18 % (3027162)------------------------------
% 61.35/18.18 % (3027162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027162)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027162)Termination reason: Instruction limit
% 61.35/18.18 % (3027162)Termination phase: Finite model building SAT solving
% 61.35/18.18 % (3027162)Time elapsed: 7.422 s
% 61.35/18.18 % (3027162)Peak memory usage: 27 MB
% 61.35/18.18 % (3027162)Instructions burned: 22063 (million)
% 61.35/18.18 % (3027188)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2528318831:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi)
% 61.35/18.18 % TRYING [7]
% 61.35/18.18 % (3027184)Instruction limit reached!
% 61.35/18.18 % (3027184)------------------------------
% 61.35/18.18 % (3027184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027184)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027184)Termination reason: Instruction limit
% 61.35/18.18 % (3027184)Termination phase: Saturation
% 61.35/18.18 % (3027184)Time elapsed: 2.284 s
% 61.35/18.18 % (3027184)Peak memory usage: 48 MB
% 61.35/18.18 % (3027184)Instructions burned: 3775 (million)
% 61.35/18.18 % (3027190)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1335859561:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2906 on theBenchmark for (2906ds/4591Mi)
% 61.35/18.18 % (3027186)Instruction limit reached!
% 61.35/18.18 % (3027186)------------------------------
% 61.35/18.18 % (3027186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027186)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027186)Termination reason: Instruction limit
% 61.35/18.18 % (3027186)Termination phase: Saturation
% 61.35/18.18 % (3027186)Time elapsed: 1.433 s
% 61.35/18.18 % (3027186)Peak memory usage: 39 MB
% 61.35/18.18 % (3027186)Instructions burned: 2251 (million)
% 61.35/18.18 % (3027192)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2325608095:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 61.35/18.18 % (3027190)Instruction limit reached!
% 61.35/18.18 % (3027190)------------------------------
% 61.35/18.18 % (3027190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027190)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027190)Termination reason: Instruction limit
% 61.35/18.18 % (3027190)Termination phase: Saturation
% 61.35/18.18 % (3027190)Time elapsed: 2.315 s
% 61.35/18.18 % (3027190)Peak memory usage: 40 MB
% 61.35/18.18 % (3027190)Instructions burned: 4591 (million)
% 61.35/18.18 % (3027194)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=556842400:i=5211_2883 on theBenchmark for (2883ds/5211Mi)
% 61.35/18.18 % (3027194)Instruction limit reached!
% 61.35/18.18 % (3027194)------------------------------
% 61.35/18.18 % (3027194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027194)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027194)Termination reason: Instruction limit
% 61.35/18.18 % (3027194)Termination phase: Saturation
% 61.35/18.18 % (3027194)Time elapsed: 3.095 s
% 61.35/18.18 % (3027194)Peak memory usage: 58 MB
% 61.35/18.18 % (3027194)Instructions burned: 5212 (million)
% 61.35/18.18 % (3027196)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2269546270:i=5497:nm=2_2852 on theBenchmark for (2852ds/5497Mi)
% 61.35/18.18 % TRYING [17]
% 61.35/18.18 % (3027196)Instruction limit reached!
% 61.35/18.18 % (3027196)------------------------------
% 61.35/18.18 % (3027196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027196)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027196)Termination reason: Instruction limit
% 61.35/18.18 % (3027196)Termination phase: Finite model building constraint generation
% 61.35/18.18 % (3027196)Time elapsed: 2.022 s
% 61.35/18.18 % (3027196)Peak memory usage: 372 MB
% 61.35/18.18 % (3027196)Instructions burned: 5499 (million)
% 61.35/18.18 % (3027199)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1510981185:fmbsr=2:i=46332_2831 on theBenchmark for (2831ds/46332Mi)
% 61.35/18.18 % TRYING [15]
% 61.35/18.18 % (3027192) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3027123-3027192"...
% 61.35/18.18 % (3027192)...printing done.
% 61.35/18.18 % (3027192)Refutation found. Thanks to Tanya!
% 61.35/18.18 % SZS status Theorem for theBenchmark
% 61.35/18.18 % SZS output start Proof for theBenchmark
% See solution above
% 61.35/18.18 % (3027192)------------------------------
% 61.35/18.18 % (3027192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.35/18.18 % (3027192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.35/18.18 % (3027192)CaDiCaL version: 2.1.3
% 61.35/18.18 % (3027192)Termination reason: Refutation
% 61.35/18.18 % (3027192)Time elapsed: 8.206 s
% 61.35/18.18 % (3027192)Peak memory usage: 107 MB
% 61.35/18.18 % (3027192)Instructions burned: 16052 (million)
% 61.35/18.18 % (3027123)Success in time 17.727 s
% 61.35/18.18 % Vampire exiting
%------------------------------------------------------------------------------