%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM308+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 12:18:17 PM UTC 2026
% Result : Theorem 49.56s 10.06s
% Output : Refutation 49.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 16
% Syntax : Number of formulae : 47 ( 32 unt; 0 def)
% Number of atoms : 102 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 101 ( 46 ~; 41 |; 10 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 95 ( 93 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn11) ).
fof(f24,axiom,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn23) ).
fof(f35,axiom,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn34) ).
fof(f257,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit1) ).
fof(f258,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit2) ).
fof(f259,axiom,
rdn_non_zero_digit(rdnn(n3)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit3) ).
fof(f279,axiom,
! [X0] :
( rdn_non_zero_digit(rdnn(X0))
=> rdn_non_zero(rdnn(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_digit) ).
fof(f287,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( rdn_translate(X0,rdn_pos(X3))
& rdn_translate(X1,rdn_pos(X4))
& rdn_add_with_carry(rdnn(n0),X3,X4,X5)
& rdn_translate(X2,rdn_pos(X5)) )
=> sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',sum_entry_point_pos_pos) ).
fof(f297,axiom,
! [X0,X1,X2,X3,X4] :
( ( rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
& rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) )
=> rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',add_digit_digit_digit) ).
fof(f300,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ( rdn_digit_add(rdnn(X1),rdnn(X3),rdnn(X7),rdnn(X8))
& rdn_digit_add(rdnn(X7),rdnn(X0),rdnn(X5),rdnn(X9))
& rdn_digit_add(rdnn(X8),rdnn(X9),rdnn(X10),rdnn(n0))
& rdn_add_with_carry(rdnn(X10),X2,X4,X6)
& rdn_non_zero(X2)
& rdn_non_zero(X4)
& rdn_non_zero(X6) )
=> rdn_add_with_carry(rdnn(X0),rdn(rdnn(X1),X2),rdn(rdnn(X3),X4),rdn(rdnn(X5),X6)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',add_rdn_rdn_rdn) ).
fof(f302,axiom,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',rdn_digit_add_n0_n0_n0_n0) ).
fof(f314,axiom,
rdn_digit_add(rdnn(n1),rdnn(n2),rdnn(n3),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',rdn_digit_add_n1_n2_n3_n0) ).
fof(f315,axiom,
rdn_digit_add(rdnn(n1),rdnn(n3),rdnn(n4),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',rdn_digit_add_n1_n3_n4_n0) ).
fof(f332,axiom,
rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',rdn_digit_add_n3_n0_n3_n0) ).
fof(f342,axiom,
rdn_digit_add(rdnn(n4),rdnn(n0),rdnn(n4),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+2.ax',rdn_digit_add_n4_n0_n4_n0) ).
fof(f402,conjecture,
? [X0] : sum(X0,n23,n34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_something_n23_n34) ).
fof(f403,negated_conjecture,
~ ? [X0] : sum(X0,n23,n34),
inference(negated_conjecture,[status(cth)],[f402]) ).
fof(f411,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(ennf_transformation,[],[f279]) ).
fof(f423,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(X0,X1,X2)
| ~ rdn_translate(X0,rdn_pos(X3))
| ~ rdn_translate(X1,rdn_pos(X4))
| ~ rdn_add_with_carry(rdnn(n0),X3,X4,X5)
| ~ rdn_translate(X2,rdn_pos(X5)) ),
inference(ennf_transformation,[],[f287]) ).
fof(f424,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(X0,X1,X2)
| ~ rdn_translate(X0,rdn_pos(X3))
| ~ rdn_translate(X1,rdn_pos(X4))
| ~ rdn_add_with_carry(rdnn(n0),X3,X4,X5)
| ~ rdn_translate(X2,rdn_pos(X5)) ),
inference(flattening,[],[f423]) ).
fof(f441,plain,
! [X0,X1,X2,X3,X4] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) ),
inference(ennf_transformation,[],[f297]) ).
fof(f442,plain,
! [X0,X1,X2,X3,X4] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) ),
inference(flattening,[],[f441]) ).
fof(f447,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( rdn_add_with_carry(rdnn(X0),rdn(rdnn(X1),X2),rdn(rdnn(X3),X4),rdn(rdnn(X5),X6))
| ~ rdn_digit_add(rdnn(X1),rdnn(X3),rdnn(X7),rdnn(X8))
| ~ rdn_digit_add(rdnn(X7),rdnn(X0),rdnn(X5),rdnn(X9))
| ~ rdn_digit_add(rdnn(X8),rdnn(X9),rdnn(X10),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X10),X2,X4,X6)
| ~ rdn_non_zero(X2)
| ~ rdn_non_zero(X4)
| ~ rdn_non_zero(X6) ),
inference(ennf_transformation,[],[f300]) ).
fof(f448,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( rdn_add_with_carry(rdnn(X0),rdn(rdnn(X1),X2),rdn(rdnn(X3),X4),rdn(rdnn(X5),X6))
| ~ rdn_digit_add(rdnn(X1),rdnn(X3),rdnn(X7),rdnn(X8))
| ~ rdn_digit_add(rdnn(X7),rdnn(X0),rdnn(X5),rdnn(X9))
| ~ rdn_digit_add(rdnn(X8),rdnn(X9),rdnn(X10),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X10),X2,X4,X6)
| ~ rdn_non_zero(X2)
| ~ rdn_non_zero(X4)
| ~ rdn_non_zero(X6) ),
inference(flattening,[],[f447]) ).
fof(f450,plain,
! [X0] : ~ sum(X0,n23,n34),
inference(ennf_transformation,[],[f403]) ).
fof(f465,plain,
rdn_translate(n11,rdn_pos(rdn(rdnn(n1),rdnn(n1)))),
inference(cnf_transformation,[],[f12]) ).
fof(f477,plain,
rdn_translate(n23,rdn_pos(rdn(rdnn(n3),rdnn(n2)))),
inference(cnf_transformation,[],[f24]) ).
fof(f488,plain,
rdn_translate(n34,rdn_pos(rdn(rdnn(n4),rdnn(n3)))),
inference(cnf_transformation,[],[f35]) ).
fof(f710,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[],[f257]) ).
fof(f711,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(cnf_transformation,[],[f258]) ).
fof(f712,plain,
rdn_non_zero_digit(rdnn(n3)),
inference(cnf_transformation,[],[f259]) ).
fof(f732,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(X0))
| rdn_non_zero(rdnn(X0)) ),
inference(cnf_transformation,[],[f411]) ).
fof(f742,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ rdn_add_with_carry(rdnn(n0),X3,X4,X5)
| ~ rdn_translate(X0,rdn_pos(X3))
| ~ rdn_translate(X1,rdn_pos(X4))
| sum(X0,X1,X2)
| ~ rdn_translate(X2,rdn_pos(X5)) ),
inference(cnf_transformation,[],[f424]) ).
fof(f753,plain,
! [X2,X3,X0,X1,X4] :
( ~ rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
| rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3)) ),
inference(cnf_transformation,[],[f442]) ).
fof(f756,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ rdn_digit_add(rdnn(X8),rdnn(X9),rdnn(X10),rdnn(n0))
| ~ rdn_digit_add(rdnn(X1),rdnn(X3),rdnn(X7),rdnn(X8))
| ~ rdn_digit_add(rdnn(X7),rdnn(X0),rdnn(X5),rdnn(X9))
| rdn_add_with_carry(rdnn(X0),rdn(rdnn(X1),X2),rdn(rdnn(X3),X4),rdn(rdnn(X5),X6))
| ~ rdn_add_with_carry(rdnn(X10),X2,X4,X6)
| ~ rdn_non_zero(X2)
| ~ rdn_non_zero(X4)
| ~ rdn_non_zero(X6) ),
inference(cnf_transformation,[],[f448]) ).
fof(f758,plain,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
inference(cnf_transformation,[],[f302]) ).
fof(f770,plain,
rdn_digit_add(rdnn(n1),rdnn(n2),rdnn(n3),rdnn(n0)),
inference(cnf_transformation,[],[f314]) ).
fof(f771,plain,
rdn_digit_add(rdnn(n1),rdnn(n3),rdnn(n4),rdnn(n0)),
inference(cnf_transformation,[],[f315]) ).
fof(f788,plain,
rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0)),
inference(cnf_transformation,[],[f332]) ).
fof(f798,plain,
rdn_digit_add(rdnn(n4),rdnn(n0),rdnn(n4),rdnn(n0)),
inference(cnf_transformation,[],[f342]) ).
fof(f858,plain,
! [X0] : ~ sum(X0,n23,n34),
inference(cnf_transformation,[],[f450]) ).
fof(f860,plain,
rdn_non_zero(rdnn(n1)),
inference(unit_resulting_resolution,[],[f732,f710]) ).
fof(f861,plain,
rdn_non_zero(rdnn(n2)),
inference(unit_resulting_resolution,[],[f732,f711]) ).
fof(f862,plain,
rdn_non_zero(rdnn(n3)),
inference(unit_resulting_resolution,[],[f732,f712]) ).
fof(f22877,plain,
~ rdn_add_with_carry(rdnn(n0),rdn(rdnn(n1),rdnn(n1)),rdn(rdnn(n3),rdnn(n2)),rdn(rdnn(n4),rdnn(n3))),
inference(unit_resulting_resolution,[],[f742,f488,f858,f477,f465]) ).
fof(f24728,plain,
~ rdn_add_with_carry(rdnn(n0),rdnn(n1),rdnn(n2),rdnn(n3)),
inference(unit_resulting_resolution,[],[f756,f862,f861,f860,f758,f771,f798,f22877]) ).
fof(f24797,plain,
$false,
inference(unit_resulting_resolution,[],[f753,f788,f770,f24728]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM308+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n020.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 19:31:04 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 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
% 14.55/2.56 % (3699257)Will run a generic schedule for satisfiability detection.
% 14.55/2.56 % (3699264)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4118551006:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.55/2.56 % (3699263)% WARNING: option uhcvi not known.
% 14.55/2.56 % (3699262)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=325442141_2999 on theBenchmark for (2999ds/0Mi)
% 14.55/2.56 % (3699265)dis+10_1_sil=32000:sp=arity:random_seed=1763963667:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.55/2.56 % (3699263)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=253622072:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.55/2.56 % (3699266)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2787814397:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.55/2.56 % (3699267)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1198834864:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.55/2.56 % (3699268)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2308952648:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.55/2.56 % TRYING [1]
% 14.55/2.56 % TRYING [2]
% 14.55/2.56 % (3699265)Instruction limit reached!
% 14.55/2.56 % (3699265)------------------------------
% 14.55/2.56 % (3699265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.55/2.56 % (3699265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/2.56 % (3699265)CaDiCaL version: 2.1.3
% 14.55/2.56 % (3699265)Termination reason: Instruction limit
% 14.55/2.56 % (3699265)Termination phase: Saturation
% 14.55/2.56 % (3699265)Time elapsed: 0.049 s
% 14.55/2.56 % (3699265)Peak memory usage: 13 MB
% 14.55/2.56 % (3699265)Instructions burned: 108 (million)
% 14.55/2.56 % TRYING [3]
% 14.55/2.56 % (3699266)Instruction limit reached!
% 14.55/2.56 % (3699266)------------------------------
% 14.55/2.56 % (3699266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.55/2.56 % (3699266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/2.56 % (3699266)CaDiCaL version: 2.1.3
% 14.55/2.56 % (3699266)Termination reason: Instruction limit
% 14.55/2.56 % (3699266)Termination phase: Saturation
% 14.55/2.56 % (3699266)Time elapsed: 0.059 s
% 14.55/2.56 % (3699266)Peak memory usage: 13 MB
% 14.55/2.56 % (3699266)Instructions burned: 116 (million)
% 14.55/2.56 % (3699267)Instruction limit reached!
% 14.55/2.56 % (3699267)------------------------------
% 14.55/2.56 % (3699267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.55/2.56 % (3699267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/2.56 % (3699267)CaDiCaL version: 2.1.3
% 14.55/2.56 % (3699267)Termination reason: Instruction limit
% 14.55/2.56 % (3699267)Termination phase: Saturation
% 14.55/2.56 % (3699267)Time elapsed: 0.060 s
% 14.55/2.56 % (3699267)Peak memory usage: 14 MB
% 14.55/2.56 % (3699267)Instructions burned: 132 (million)
% 14.55/2.56 % (3699276)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1834700188:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.55/2.56 % (3699268)Instruction limit reached!
% 14.55/2.56 % (3699268)------------------------------
% 14.55/2.56 % (3699268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.55/2.56 % (3699268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/2.56 % (3699268)CaDiCaL version: 2.1.3
% 14.55/2.56 % (3699268)Termination reason: Instruction limit
% 14.55/2.56 % (3699268)Termination phase: Saturation
% 14.55/2.56 % (3699268)Time elapsed: 0.073 s
% 14.55/2.56 % (3699268)Peak memory usage: 14 MB
% 14.55/2.56 % (3699268)Instructions burned: 160 (million)
% 14.55/2.56 % (3699277)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3474667008:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.55/2.56 % (3699278)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=2162244341:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.55/2.56 % (3699280)ott-21_1_sil=16000:fs=off:random_seed=882235536:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.55/2.56 % TRYING [1]
% 14.55/2.56 % TRYING [2]
% 14.55/2.56 % TRYING [4]
% 14.55/2.56 % TRYING [3]
% 14.55/2.56 % (3699277)Instruction limit reached!
% 14.55/2.56 % (3699277)------------------------------
% 14.55/2.56 % (3699277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.55/2.56 % (3699277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.30 % (3699277)CaDiCaL version: 2.1.3
% 41.51/6.30 % (3699277)Termination reason: Instruction limit
% 41.51/6.30 % (3699277)Termination phase: Saturation
% 41.51/6.30 % (3699277)Time elapsed: 0.065 s
% 41.51/6.30 % (3699277)Peak memory usage: 14 MB
% 41.51/6.30 % (3699277)Instructions burned: 133 (million)
% 41.51/6.30 % (3699284)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1760109708:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 41.51/6.30 % (3699280)Instruction limit reached!
% 41.51/6.30 % (3699280)------------------------------
% 41.51/6.30 % (3699280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.51/6.30 % (3699280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.30 % (3699280)CaDiCaL version: 2.1.3
% 41.51/6.30 % (3699280)Termination reason: Instruction limit
% 41.51/6.30 % (3699280)Termination phase: Saturation
% 41.51/6.30 % (3699280)Time elapsed: 0.080 s
% 41.51/6.30 % (3699280)Peak memory usage: 13 MB
% 41.51/6.30 % (3699280)Instructions burned: 181 (million)
% 41.51/6.30 % (3699286)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1939074768:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.51/6.30 % TRYING [4]
% 41.51/6.30 % TRYING [1]
% 41.51/6.30 % TRYING [2]
% 41.51/6.30 % TRYING [3]
% 41.51/6.30 % (3699276)Instruction limit reached!
% 41.51/6.30 % (3699276)------------------------------
% 41.51/6.30 % (3699276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.51/6.30 % (3699276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.30 % (3699276)CaDiCaL version: 2.1.3
% 41.51/6.30 % (3699276)Termination reason: Instruction limit
% 41.51/6.30 % (3699276)Termination phase: Finite model building constraint generation
% 41.51/6.30 % (3699276)Time elapsed: 0.264 s
% 41.51/6.30 % (3699276)Peak memory usage: 38 MB
% 41.51/6.30 % (3699276)Instructions burned: 715 (million)
% 41.51/6.30 % (3699288)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2528645479:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 41.51/6.30 % (3699284)Instruction limit reached!
% 41.51/6.30 % (3699284)------------------------------
% 41.51/6.30 % (3699284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.51/6.30 % (3699284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.30 % (3699284)CaDiCaL version: 2.1.3
% 41.51/6.30 % (3699284)Termination reason: Instruction limit
% 41.51/6.30 % (3699284)Termination phase: Saturation
% 41.51/6.30 % (3699284)Time elapsed: 0.244 s
% 41.51/6.30 % (3699284)Peak memory usage: 18 MB
% 41.51/6.30 % (3699284)Instructions burned: 477 (million)
% 41.51/6.30 % (3699278)Instruction limit reached!
% 41.51/6.30 % (3699278)------------------------------
% 41.51/6.30 % (3699278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.51/6.30 % (3699278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.30 % (3699278)CaDiCaL version: 2.1.3
% 41.51/6.30 % (3699278)Termination reason: Instruction limit
% 41.51/6.30 % (3699278)Termination phase: Saturation
% 41.51/6.30 % (3699278)Time elapsed: 0.349 s
% 41.51/6.30 % (3699278)Peak memory usage: 23 MB
% 41.51/6.30 % (3699278)Instructions burned: 684 (million)
% 41.51/6.30 % (3699290)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=253055631:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.51/6.30 % (3699291)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=3419534813:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 41.51/6.30 % TRYING [5]
% 41.51/6.30 % TRYING [4]
% 41.51/6.30 % (3699286)Instruction limit reached!
% 41.51/6.30 % (3699286)------------------------------
% 41.51/6.30 % (3699286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.51/6.30 % (3699286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.30 % (3699286)CaDiCaL version: 2.1.3
% 41.51/6.30 % (3699286)Termination reason: Instruction limit
% 41.51/6.30 % (3699286)Termination phase: Finite model building constraint generation
% 41.51/6.30 % (3699286)Time elapsed: 0.325 s
% 41.51/6.30 % (3699286)Peak memory usage: 24 MB
% 41.51/6.30 % (3699286)Instructions burned: 865 (million)
% 41.51/6.30 % (3699294)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1892785849:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 41.51/6.30 % (3699291)Instruction limit reached!
% 41.51/6.30 % (3699291)------------------------------
% 49.56/10.05 % (3699291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699291)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699291)Termination reason: Instruction limit
% 49.56/10.05 % (3699291)Termination phase: Saturation
% 49.56/10.05 % (3699291)Time elapsed: 0.335 s
% 49.56/10.05 % (3699291)Peak memory usage: 25 MB
% 49.56/10.05 % (3699291)Instructions burned: 694 (million)
% 49.56/10.05 % (3699296)fmb+10_1_sil=64000:random_seed=2523140780:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 49.56/10.05 % (3699290)Instruction limit reached!
% 49.56/10.05 % (3699290)------------------------------
% 49.56/10.05 % (3699290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699290)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699290)Termination reason: Instruction limit
% 49.56/10.05 % (3699290)Termination phase: Finite model building constraint generation
% 49.56/10.05 % (3699290)Time elapsed: 0.407 s
% 49.56/10.05 % (3699290)Peak memory usage: 101 MB
% 49.56/10.05 % (3699290)Instructions burned: 891 (million)
% 49.56/10.05 % TRYING [1]
% 49.56/10.05 % TRYING [2]
% 49.56/10.05 % (3699298)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=219332336:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 49.56/10.05 % TRYING [3]
% 49.56/10.05 % TRYING [20]
% 49.56/10.05 % (3699294)Instruction limit reached!
% 49.56/10.05 % (3699294)------------------------------
% 49.56/10.05 % (3699294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699294)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699294)Termination reason: Instruction limit
% 49.56/10.05 % (3699294)Termination phase: Saturation
% 49.56/10.05 % (3699294)Time elapsed: 0.361 s
% 49.56/10.05 % (3699294)Peak memory usage: 20 MB
% 49.56/10.05 % (3699294)Instructions burned: 880 (million)
% 49.56/10.05 % (3699300)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1346665377:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 49.56/10.05 % TRYING [8]
% 49.56/10.05 % (3699288)Instruction limit reached!
% 49.56/10.05 % (3699288)------------------------------
% 49.56/10.05 % (3699288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699288)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699288)Termination reason: Instruction limit
% 49.56/10.05 % (3699288)Termination phase: Saturation
% 49.56/10.05 % (3699288)Time elapsed: 0.604 s
% 49.56/10.05 % (3699288)Peak memory usage: 35 MB
% 49.56/10.05 % (3699288)Instructions burned: 1180 (million)
% 49.56/10.05 % (3699302)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1860524465:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 49.56/10.05 % TRYING [4]
% 49.56/10.05 % (3699300)Instruction limit reached!
% 49.56/10.05 % (3699300)------------------------------
% 49.56/10.05 % (3699300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699300)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699300)Termination reason: Instruction limit
% 49.56/10.05 % (3699300)Termination phase: Finite model building constraint generation
% 49.56/10.05 % (3699300)Time elapsed: 0.315 s
% 49.56/10.05 % (3699300)Peak memory usage: 68 MB
% 49.56/10.05 % (3699300)Instructions burned: 922 (million)
% 49.56/10.05 % (3699304)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4010353719:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 49.56/10.05 % (3699304)Instruction limit reached!
% 49.56/10.05 % (3699304)------------------------------
% 49.56/10.05 % (3699304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699304)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699304)Termination reason: Instruction limit
% 49.56/10.05 % (3699304)Termination phase: Saturation
% 49.56/10.05 % (3699304)Time elapsed: 0.742 s
% 49.56/10.05 % (3699304)Peak memory usage: 27 MB
% 49.56/10.05 % (3699304)Instructions burned: 1473 (million)
% 49.56/10.05 % (3699306)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=132394915:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 49.56/10.05 % (3699306)Cannot represent all propositional literals internally
% 49.56/10.05 % (3699306)Refutation not found, incomplete strategy
% 49.56/10.05 % (3699306)------------------------------
% 49.56/10.05 % (3699306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699306)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699306)Termination reason: Refutation not found, incomplete strategy
% 49.56/10.05 % (3699306)Time elapsed: 0.034 s
% 49.56/10.05 % (3699306)Peak memory usage: 12 MB
% 49.56/10.05 % (3699306)Instructions burned: 72 (million)
% 49.56/10.05 % (3699306)------------------------------
% 49.56/10.05 % (3699306)------------------------------
% 49.56/10.05 % (3699308)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3439753338:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 49.56/10.05 % TRYING [6]
% 49.56/10.05 % TRYING [16]
% 49.56/10.05 % (3699308)Instruction limit reached!
% 49.56/10.05 % (3699308)------------------------------
% 49.56/10.05 % (3699308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699308)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699308)Termination reason: Instruction limit
% 49.56/10.05 % (3699308)Termination phase: Finite model building constraint generation
% 49.56/10.05 % (3699308)Time elapsed: 0.748 s
% 49.56/10.05 % (3699308)Peak memory usage: 127 MB
% 49.56/10.05 % (3699308)Instructions burned: 2174 (million)
% 49.56/10.05 % (3699310)ott-2_1_sil=16000:newcnf=on:random_seed=2865712850:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 49.56/10.05 % (3699310)Instruction limit reached!
% 49.56/10.05 % (3699310)------------------------------
% 49.56/10.05 % (3699310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699310)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699310)Termination reason: Instruction limit
% 49.56/10.05 % (3699310)Termination phase: Saturation
% 49.56/10.05 % (3699310)Time elapsed: 0.380 s
% 49.56/10.05 % (3699310)Peak memory usage: 18 MB
% 49.56/10.05 % (3699310)Instructions burned: 870 (million)
% 49.56/10.05 % (3699312)ott+10_1_sil=32000:tgt=ground:random_seed=4047734390:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 49.56/10.05 % (3699302)Instruction limit reached!
% 49.56/10.05 % (3699302)------------------------------
% 49.56/10.05 % (3699302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699302)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699302)Termination reason: Instruction limit
% 49.56/10.05 % (3699302)Termination phase: Saturation
% 49.56/10.05 % (3699302)Time elapsed: 2.446 s
% 49.56/10.05 % (3699302)Peak memory usage: 49 MB
% 49.56/10.05 % (3699302)Instructions burned: 5133 (million)
% 49.56/10.05 % (3699314)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1678788902:i=54282_2965 on theBenchmark for (2965ds/54282Mi)
% 49.56/10.05 % TRYING [1]
% 49.56/10.05 % TRYING [2]
% 49.56/10.05 % TRYING [3]
% 49.56/10.05 % TRYING [4]
% 49.56/10.05 % TRYING [5]
% 49.56/10.05 % TRYING [5]
% 49.56/10.05 % (3699298)Instruction limit reached!
% 49.56/10.05 % (3699298)------------------------------
% 49.56/10.05 % (3699298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699298)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699298)Termination reason: Instruction limit
% 49.56/10.05 % (3699298)Termination phase: Finite model building constraint generation
% 49.56/10.05 % (3699298)Time elapsed: 3.370 s
% 49.56/10.05 % (3699298)Peak memory usage: 664 MB
% 49.56/10.05 % (3699298)Instructions burned: 9518 (million)
% 49.56/10.05 % (3699316)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1876531389:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 49.56/10.05 % TRYING [6]
% 49.56/10.05 % (3699316)Instruction limit reached!
% 49.56/10.05 % (3699316)------------------------------
% 49.56/10.05 % (3699316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699316)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699316)Termination reason: Instruction limit
% 49.56/10.05 % (3699316)Termination phase: Saturation
% 49.56/10.05 % (3699316)Time elapsed: 1.441 s
% 49.56/10.05 % (3699316)Peak memory usage: 42 MB
% 49.56/10.05 % (3699316)Instructions burned: 3513 (million)
% 49.56/10.05 % (3699318)dis+21_1_sil=32000:sas=cadical:random_seed=1869486215:i=3773:amm=off_2941 on theBenchmark for (2941ds/3773Mi)
% 49.56/10.05 % (3699312)Instruction limit reached!
% 49.56/10.05 % (3699312)------------------------------
% 49.56/10.05 % (3699312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699312)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699312)Termination reason: Instruction limit
% 49.56/10.05 % (3699312)Termination phase: Saturation
% 49.56/10.05 % (3699312)Time elapsed: 2.723 s
% 49.56/10.05 % (3699312)Peak memory usage: 78 MB
% 49.56/10.05 % (3699312)Instructions burned: 5114 (million)
% 49.56/10.05 % (3699320)ott+11_1_sil=16000:gs=on:random_seed=2966545779:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2939 on theBenchmark for (2939ds/2251Mi)
% 49.56/10.05 % (3699320)Instruction limit reached!
% 49.56/10.05 % (3699320)------------------------------
% 49.56/10.05 % (3699320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699320)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699320)Termination reason: Instruction limit
% 49.56/10.05 % (3699320)Termination phase: Saturation
% 49.56/10.05 % (3699320)Time elapsed: 1.231 s
% 49.56/10.05 % (3699320)Peak memory usage: 40 MB
% 49.56/10.05 % (3699320)Instructions burned: 2252 (million)
% 49.56/10.05 % (3699322)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4012965013:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi)
% 49.56/10.05 % (3699318)Instruction limit reached!
% 49.56/10.05 % (3699318)------------------------------
% 49.56/10.05 % (3699318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.05 % (3699318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.05 % (3699318)CaDiCaL version: 2.1.3
% 49.56/10.05 % (3699318)Termination reason: Instruction limit
% 49.56/10.05 % (3699318)Termination phase: Saturation
% 49.56/10.05 % (3699318)Time elapsed: 1.728 s
% 49.56/10.05 % (3699318)Peak memory usage: 61 MB
% 49.56/10.05 % (3699318)Instructions burned: 3773 (million)
% 49.56/10.05 % (3699324)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=239424831:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2923 on theBenchmark for (2923ds/4591Mi)
% 49.56/10.06 % TRYING [7]
% 49.56/10.06 % (3699296)Instruction limit reached!
% 49.56/10.06 % (3699296)------------------------------
% 49.56/10.06 % (3699296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.06 % (3699296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.06 % (3699296)CaDiCaL version: 2.1.3
% 49.56/10.06 % (3699296)Termination reason: Instruction limit
% 49.56/10.06 % (3699296)Termination phase: Finite model building SAT solving
% 49.56/10.06 % (3699296)Time elapsed: 7.822 s
% 49.56/10.06 % (3699296)Peak memory usage: 429 MB
% 49.56/10.06 % (3699296)Instructions burned: 22063 (million)
% 49.56/10.06 % TRYING [7]
% 49.56/10.06 % (3699326)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=467858737:i=29340_2912 on theBenchmark for (2912ds/29340Mi)
% 49.56/10.06 % (3699326) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3699257-3699326"...
% 49.56/10.06 % (3699326)...printing done.
% 49.56/10.06 % (3699326)Refutation found. Thanks to Tanya!
% 49.56/10.06 % SZS status Theorem for theBenchmark
% 49.56/10.06 % SZS output start Proof for theBenchmark
% See solution above
% 49.56/10.06 % (3699326)------------------------------
% 49.56/10.06 % (3699326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.56/10.06 % (3699326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.56/10.06 % (3699326)CaDiCaL version: 2.1.3
% 49.56/10.06 % (3699326)Termination reason: Refutation
% 49.56/10.06 % (3699326)Time elapsed: 0.707 s
% 49.56/10.06 % (3699326)Peak memory usage: 35 MB
% 49.56/10.06 % (3699326)Instructions burned: 1495 (million)
% 49.56/10.06 % (3699257)Success in time 9.617 s
% 49.56/10.06 % Vampire exiting
%------------------------------------------------------------------------------