%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD089-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 09:49:26 AM UTC 2026
% Result : Unsatisfiable 30.39s 4.75s
% Output : Refutation 30.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 23
% Syntax : Number of formulae : 71 ( 53 unt; 1 def)
% Number of atoms : 109 ( 2 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 76 ( 38 ~; 38 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 50 ( 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4,X5] :
( sum(X0,X1,X2)
| ~ sum(X0,X3,X4)
| ~ sum(X3,X5,X1)
| ~ sum(X4,X5,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_addition_1) ).
fof(f3,axiom,
! [X0] :
( sum(additive_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_identity_addition) ).
fof(f4,axiom,
! [X0] :
( sum(additive_inverse(X0),X0,additive_identity)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_inverse_addition) ).
fof(f5,axiom,
! [X2,X0,X1] :
( sum(X0,X1,X2)
| ~ sum(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_addition) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4,X5] :
( product(X0,X1,X2)
| ~ product(X3,X4,X0)
| ~ product(X4,X1,X5)
| ~ product(X3,X5,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_multiplication_2) ).
fof(f8,axiom,
! [X0] :
( product(multiplicative_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_identity_multiplication) ).
fof(f9,axiom,
! [X0] :
( product(multiplicative_inverse(X0),X0,multiplicative_identity)
| sum(additive_identity,X0,additive_identity)
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_inverse_multiplication) ).
fof(f10,axiom,
! [X2,X0,X1] :
( product(X0,X1,X2)
| ~ product(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_multiplication) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X5,X6,X2)
| ~ sum(X3,X4,X5)
| sum(X0,X1,X2)
| ~ product(X3,X6,X0)
| ~ product(X4,X6,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity_1) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( product(X0,X1,X2)
| ~ sum(X3,X4,X0)
| ~ product(X3,X1,X5)
| ~ product(X4,X1,X6)
| ~ sum(X5,X6,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity_2) ).
fof(f14,axiom,
defined(additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_additive_identity) ).
fof(f15,axiom,
! [X0] :
( defined(additive_inverse(X0))
| ~ defined(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_additive_inverse) ).
fof(f17,axiom,
defined(multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplicative_identity) ).
fof(f18,axiom,
! [X0] :
( sum(additive_identity,X0,additive_identity)
| ~ defined(X0)
| defined(multiplicative_inverse(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplicative_inverse) ).
fof(f20,axiom,
! [X0,X1] :
( product(X0,X1,multiply(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality_of_multiplication) ).
fof(f23,axiom,
! [X0,X1] :
( less_or_equal(X1,X0)
| less_or_equal(X0,X1)
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality_of_order_relation) ).
fof(f24,axiom,
! [X2,X3,X0,X1,X4] :
( ~ sum(X3,X4,X1)
| ~ less_or_equal(X2,X3)
| ~ sum(X2,X4,X0)
| less_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_order_relation_and_addition) ).
fof(f25,axiom,
! [X2,X0,X1] :
( ~ product(X1,X2,X0)
| ~ less_or_equal(additive_identity,X1)
| ~ less_or_equal(additive_identity,X2)
| less_or_equal(additive_identity,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_order_relation_and_multiplication) ).
fof(f27,axiom,
defined(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_is_defined) ).
fof(f28,negated_conjecture,
~ sum(additive_identity,a,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_sum_2) ).
fof(f29,negated_conjecture,
less_or_equal(multiplicative_inverse(a),additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_or_equal_3) ).
fof(f30,negated_conjecture,
~ less_or_equal(a,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_less_or_equal_4) ).
fof(f31,definition,
sF0 = multiplicative_inverse(a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f32,plain,
multiplicative_inverse(a) = sF0,
inference(reorient_equations,[],[f31]) ).
fof(f33,plain,
less_or_equal(sF0,additive_identity),
inference(definition_folding,[],[f29,f32]) ).
fof(f34,plain,
( product(sF0,a,multiplicative_identity)
| sum(additive_identity,a,additive_identity)
| ~ defined(a) ),
inference(superposition,[],[f9,f32]) ).
fof(f35,plain,
( product(sF0,a,multiplicative_identity)
| ~ defined(a) ),
inference(forward_subsumption_resolution,[],[f34,f28]) ).
fof(f36,plain,
product(sF0,a,multiplicative_identity),
inference(forward_subsumption_resolution,[],[f35,f27]) ).
fof(f38,plain,
sum(additive_identity,a,a),
inference(unit_resulting_resolution,[],[f3,f27]) ).
fof(f39,plain,
defined(multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f18,f28,f27]) ).
fof(f40,plain,
sum(additive_inverse(a),a,additive_identity),
inference(unit_resulting_resolution,[],[f4,f27]) ).
fof(f42,plain,
defined(sF0),
inference(forward_demodulation,[],[f39,f32]) ).
fof(f50,plain,
~ less_or_equal(additive_identity,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f24,f30,f40,f38]) ).
fof(f53,plain,
sum(additive_inverse(sF0),sF0,additive_identity),
inference(unit_resulting_resolution,[],[f4,f42]) ).
fof(f60,plain,
product(a,sF0,multiplicative_identity),
inference(unit_resulting_resolution,[],[f10,f36]) ).
fof(f76,plain,
defined(additive_inverse(a)),
inference(unit_resulting_resolution,[],[f15,f27]) ).
fof(f77,plain,
defined(additive_inverse(sF0)),
inference(unit_resulting_resolution,[],[f15,f42]) ).
fof(f116,plain,
product(multiplicative_identity,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f8,f14]) ).
fof(f128,plain,
product(sF0,additive_identity,multiply(sF0,additive_identity)),
inference(unit_resulting_resolution,[],[f20,f42,f14]) ).
fof(f130,plain,
less_or_equal(additive_identity,a),
inference(unit_resulting_resolution,[],[f23,f27,f30,f14]) ).
fof(f133,plain,
sum(additive_identity,multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f3,f17]) ).
fof(f134,plain,
sum(additive_inverse(multiplicative_identity),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f4,f17]) ).
fof(f158,plain,
sum(multiplicative_identity,additive_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f5,f133]) ).
fof(f161,plain,
product(additive_identity,multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f10,f116]) ).
fof(f241,plain,
sum(additive_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f3,f76]) ).
fof(f243,plain,
product(multiplicative_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f8,f76]) ).
fof(f264,plain,
product(sF0,additive_inverse(a),multiply(sF0,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f20,f42,f76]) ).
fof(f270,plain,
product(additive_inverse(a),multiplicative_identity,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f10,f243]) ).
fof(f413,plain,
sum(sF0,additive_inverse(sF0),additive_identity),
inference(unit_resulting_resolution,[],[f5,f53]) ).
fof(f608,plain,
sum(multiplicative_identity,additive_inverse(multiplicative_identity),additive_identity),
inference(unit_resulting_resolution,[],[f5,f134]) ).
fof(f673,plain,
product(additive_inverse(a),sF0,multiply(sF0,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f10,f264]) ).
fof(f1099,plain,
product(multiply(sF0,additive_inverse(a)),a,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f7,f36,f270,f673]) ).
fof(f1415,plain,
product(additive_identity,sF0,multiply(sF0,additive_identity)),
inference(unit_resulting_resolution,[],[f10,f128]) ).
fof(f1432,plain,
sum(multiply(sF0,additive_inverse(a)),multiplicative_identity,multiply(sF0,additive_identity)),
inference(unit_resulting_resolution,[],[f11,f60,f673,f40,f1415]) ).
fof(f1437,plain,
sum(multiply(sF0,additive_identity),multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f11,f60,f60,f38,f1415]) ).
fof(f1451,plain,
sum(multiply(sF0,additive_identity),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f608,f608,f1437]) ).
fof(f1822,plain,
sum(multiply(sF0,additive_inverse(a)),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f158,f1432,f1451]) ).
fof(f1919,plain,
sum(multiplicative_identity,multiply(sF0,additive_inverse(a)),additive_identity),
inference(unit_resulting_resolution,[],[f5,f1822]) ).
fof(f1920,plain,
product(additive_identity,sF0,additive_identity),
inference(unit_resulting_resolution,[],[f12,f60,f40,f673,f1822]) ).
fof(f1936,plain,
product(additive_identity,a,additive_identity),
inference(unit_resulting_resolution,[],[f7,f161,f36,f1920]) ).
fof(f1984,plain,
sum(additive_identity,multiply(sF0,additive_inverse(a)),multiply(sF0,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f11,f673,f673,f241,f1920]) ).
fof(f3185,plain,
sum(additive_identity,additive_inverse(sF0),additive_inverse(sF0)),
inference(unit_resulting_resolution,[],[f3,f77]) ).
fof(f3235,plain,
product(a,additive_inverse(sF0),multiply(a,additive_inverse(sF0))),
inference(unit_resulting_resolution,[],[f20,f27,f77]) ).
fof(f3273,plain,
less_or_equal(additive_identity,additive_inverse(sF0)),
inference(unit_resulting_resolution,[],[f24,f33,f413,f3185]) ).
fof(f3357,plain,
product(additive_inverse(sF0),a,multiply(a,additive_inverse(sF0))),
inference(unit_resulting_resolution,[],[f10,f3235]) ).
fof(f3358,plain,
less_or_equal(additive_identity,multiply(a,additive_inverse(sF0))),
inference(unit_resulting_resolution,[],[f25,f130,f3273,f3235]) ).
fof(f3376,plain,
sum(multiply(a,additive_inverse(sF0)),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f11,f36,f1936,f53,f3357]) ).
fof(f3585,plain,
less_or_equal(multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f24,f133,f3376,f3358]) ).
fof(f19889,plain,
less_or_equal(additive_identity,multiply(sF0,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f24,f3585,f1919,f1984]) ).
fof(f26116,plain,
~ less_or_equal(additive_identity,multiply(sF0,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f25,f130,f50,f1099]) ).
fof(f26117,plain,
$false,
inference(forward_subsumption_resolution,[],[f26116,f19889]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD089-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n006.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.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 01:00:10 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.71/1.69 % (374234)Input is clausal, will run a generic CNF schedule.
% 7.71/1.69 % (374245)dis-21_1_sil=8000:lcm=predicate:random_seed=3839742542:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.71/1.69 % (374245)Instruction limit reached!
% 7.71/1.69 % (374245)------------------------------
% 7.71/1.69 % (374245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.71/1.69 % (374245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/1.69 % (374245)CaDiCaL version: 2.1.3
% 7.71/1.69 % (374245)Termination reason: Instruction limit
% 7.71/1.69 % (374245)Termination phase: Saturation
% 7.71/1.69 % (374245)Time elapsed: 0.040 s
% 7.71/1.69 % (374245)Peak memory usage: 89 MB
% 7.71/1.69 % (374245)Instructions burned: 119 (million)
% 7.71/1.69 % (374243)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2584539999:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.71/1.69 % (374239)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=341800990:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.71/1.69 % (374241)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2935299458:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.71/1.69 % (374240)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=281899257:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.71/1.69 % (374242)lrs+10_1_sil=8000:sp=occurrence:random_seed=2414439468:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.71/1.69 % (374244)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=521955086:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.71/1.69 % (374242)Instruction limit reached!
% 7.71/1.69 % (374242)------------------------------
% 7.71/1.69 % (374242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.71/1.69 % (374242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/1.69 % (374242)CaDiCaL version: 2.1.3
% 7.71/1.69 % (374242)Termination reason: Instruction limit
% 7.71/1.69 % (374242)Termination phase: Saturation
% 7.71/1.69 % (374242)Time elapsed: 0.055 s
% 7.71/1.69 % (374242)Peak memory usage: 87 MB
% 7.71/1.69 % (374242)Instructions burned: 108 (million)
% 7.71/1.69 % (374243)Instruction limit reached!
% 7.71/1.69 % (374243)------------------------------
% 7.71/1.69 % (374243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.71/1.69 % (374243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/1.69 % (374243)CaDiCaL version: 2.1.3
% 7.71/1.69 % (374243)Termination reason: Instruction limit
% 7.71/1.69 % (374243)Termination phase: Saturation
% 7.71/1.69 % (374243)Time elapsed: 0.068 s
% 7.71/1.69 % (374243)Peak memory usage: 88 MB
% 7.71/1.69 % (374243)Instructions burned: 115 (million)
% 7.71/1.69 % (374247)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1740904879:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.71/1.69 % (374244)Instruction limit reached!
% 7.71/1.69 % (374244)------------------------------
% 7.71/1.69 % (374244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.71/1.69 % (374244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/1.69 % (374244)CaDiCaL version: 2.1.3
% 7.71/1.69 % (374244)Termination reason: Instruction limit
% 7.71/1.69 % (374244)Termination phase: Saturation
% 7.71/1.69 % (374244)Time elapsed: 0.117 s
% 7.71/1.69 % (374244)Peak memory usage: 89 MB
% 7.71/1.69 % (374244)Instructions burned: 180 (million)
% 7.71/1.69 % (374247)Instruction limit reached!
% 7.71/1.69 % (374247)------------------------------
% 7.71/1.69 % (374247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.71/1.69 % (374247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/1.69 % (374247)CaDiCaL version: 2.1.3
% 7.71/1.69 % (374247)Termination reason: Instruction limit
% 7.71/1.69 % (374247)Termination phase: Saturation
% 7.71/1.69 % (374247)Time elapsed: 0.031 s
% 7.71/1.69 % (374247)Peak memory usage: 88 MB
% 7.71/1.69 % (374247)Instructions burned: 147 (million)
% 7.71/1.69 % (374254)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1614325138:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 19.36/3.20 % (374255)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3372852657:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 19.36/3.20 % (374258)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4081572683:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 19.36/3.20 % (374257)lrs+10_64_to=lpo:sil=8000:random_seed=3685983881:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 19.36/3.20 % (374258)Instruction limit reached!
% 19.36/3.20 % (374258)------------------------------
% 19.36/3.20 % (374258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.36/3.20 % (374258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.36/3.20 % (374258)CaDiCaL version: 2.1.3
% 19.36/3.20 % (374258)Termination reason: Instruction limit
% 19.36/3.20 % (374258)Termination phase: Saturation
% 19.36/3.20 % (374258)Time elapsed: 0.037 s
% 19.36/3.20 % (374258)Peak memory usage: 87 MB
% 19.36/3.20 % (374258)Instructions burned: 197 (million)
% 19.36/3.20 % (374254)Instruction limit reached!
% 19.36/3.20 % (374254)------------------------------
% 19.36/3.20 % (374254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.36/3.20 % (374254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.36/3.20 % (374254)CaDiCaL version: 2.1.3
% 19.36/3.20 % (374254)Termination reason: Instruction limit
% 19.36/3.20 % (374254)Termination phase: Saturation
% 19.36/3.20 % (374254)Time elapsed: 0.098 s
% 19.36/3.20 % (374254)Peak memory usage: 93 MB
% 19.36/3.20 % (374254)Instructions burned: 190 (million)
% 19.36/3.20 % (374257)Instruction limit reached!
% 19.36/3.20 % (374257)------------------------------
% 19.36/3.20 % (374257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.36/3.20 % (374257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.36/3.20 % (374257)CaDiCaL version: 2.1.3
% 19.36/3.20 % (374257)Termination reason: Instruction limit
% 19.36/3.20 % (374257)Termination phase: Saturation
% 19.36/3.20 % (374257)Time elapsed: 0.073 s
% 19.36/3.20 % (374257)Peak memory usage: 90 MB
% 19.36/3.20 % (374257)Instructions burned: 127 (million)
% 19.36/3.20 % (374255)Instruction limit reached!
% 19.36/3.20 % (374255)------------------------------
% 19.36/3.20 % (374255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.36/3.20 % (374255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.36/3.20 % (374255)CaDiCaL version: 2.1.3
% 19.36/3.20 % (374255)Termination reason: Instruction limit
% 19.36/3.20 % (374255)Termination phase: Saturation
% 19.36/3.20 % (374255)Time elapsed: 0.121 s
% 19.36/3.20 % (374255)Peak memory usage: 88 MB
% 19.36/3.20 % (374255)Instructions burned: 220 (million)
% 19.36/3.20 % (374263)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=923037649:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 19.36/3.20 % (374264)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3817019005:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 19.36/3.20 % (374263)Instruction limit reached!
% 19.36/3.20 % (374263)------------------------------
% 19.36/3.20 % (374263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.36/3.20 % (374263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.36/3.20 % (374263)CaDiCaL version: 2.1.3
% 19.36/3.20 % (374263)Termination reason: Instruction limit
% 19.36/3.20 % (374263)Termination phase: Saturation
% 19.36/3.20 % (374263)Time elapsed: 0.056 s
% 19.36/3.20 % (374263)Peak memory usage: 90 MB
% 19.36/3.20 % (374263)Instructions burned: 158 (million)
% 19.36/3.20 % (374265)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1608451586:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 19.36/3.20 % (374266)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2043029248:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 19.36/3.20 % (374265)Instruction limit reached!
% 19.36/3.20 % (374265)------------------------------
% 19.36/3.20 % (374265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.36/3.20 % (374265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374265)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374265)Termination reason: Instruction limit
% 30.39/4.75 % (374265)Termination phase: Saturation
% 30.39/4.75 % (374265)Time elapsed: 0.054 s
% 30.39/4.75 % (374265)Peak memory usage: 89 MB
% 30.39/4.75 % (374265)Instructions burned: 106 (million)
% 30.39/4.75 % (374266)Instruction limit reached!
% 30.39/4.75 % (374266)------------------------------
% 30.39/4.75 % (374266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374266)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374266)Termination reason: Instruction limit
% 30.39/4.75 % (374266)Termination phase: Saturation
% 30.39/4.75 % (374266)Time elapsed: 0.071 s
% 30.39/4.75 % (374266)Peak memory usage: 88 MB
% 30.39/4.75 % (374266)Instructions burned: 108 (million)
% 30.39/4.75 % (374269)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1967364099:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 30.39/4.75 % (374269)Instruction limit reached!
% 30.39/4.75 % (374269)------------------------------
% 30.39/4.75 % (374269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374269)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374269)Termination reason: Instruction limit
% 30.39/4.75 % (374269)Termination phase: Saturation
% 30.39/4.75 % (374269)Time elapsed: 0.082 s
% 30.39/4.75 % (374269)Peak memory usage: 89 MB
% 30.39/4.75 % (374269)Instructions burned: 245 (million)
% 30.39/4.75 % (374272)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3502992736:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 30.39/4.75 % (374273)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=968789731:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 30.39/4.75 % (374273)Instruction limit reached!
% 30.39/4.75 % (374273)------------------------------
% 30.39/4.75 % (374273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374273)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374273)Termination reason: Instruction limit
% 30.39/4.75 % (374273)Termination phase: Saturation
% 30.39/4.75 % (374273)Time elapsed: 0.050 s
% 30.39/4.75 % (374273)Peak memory usage: 87 MB
% 30.39/4.75 % (374273)Instructions burned: 136 (million)
% 30.39/4.75 % (374275)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=569150105:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 30.39/4.75 % (374275)Instruction limit reached!
% 30.39/4.75 % (374275)------------------------------
% 30.39/4.75 % (374275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374275)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374275)Termination reason: Instruction limit
% 30.39/4.75 % (374275)Termination phase: Saturation
% 30.39/4.75 % (374275)Time elapsed: 0.146 s
% 30.39/4.75 % (374275)Peak memory usage: 108 MB
% 30.39/4.75 % (374275)Instructions burned: 500 (million)
% 30.39/4.75 % (374278)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3875710471:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 30.39/4.75 % (374278)Instruction limit reached!
% 30.39/4.75 % (374278)------------------------------
% 30.39/4.75 % (374278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374278)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374278)Termination reason: Instruction limit
% 30.39/4.75 % (374278)Termination phase: Saturation
% 30.39/4.75 % (374278)Time elapsed: 0.104 s
% 30.39/4.75 % (374278)Peak memory usage: 91 MB
% 30.39/4.75 % (374278)Instructions burned: 193 (million)
% 30.39/4.75 % (374280)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3012003172:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 30.39/4.75 % (374280)Instruction limit reached!
% 30.39/4.75 % (374280)------------------------------
% 30.39/4.75 % (374280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374280)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374280)Termination reason: Instruction limit
% 30.39/4.75 % (374280)Termination phase: Saturation
% 30.39/4.75 % (374280)Time elapsed: 0.050 s
% 30.39/4.75 % (374280)Peak memory usage: 87 MB
% 30.39/4.75 % (374280)Instructions burned: 266 (million)
% 30.39/4.75 % (374283)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3926139903:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 30.39/4.75 % (374284)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1709432506:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 30.39/4.75 % (374283)Instruction limit reached!
% 30.39/4.75 % (374283)------------------------------
% 30.39/4.75 % (374283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374283)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374283)Termination reason: Instruction limit
% 30.39/4.75 % (374283)Termination phase: Saturation
% 30.39/4.75 % (374283)Time elapsed: 0.067 s
% 30.39/4.75 % (374283)Peak memory usage: 87 MB
% 30.39/4.75 % (374283)Instructions burned: 158 (million)
% 30.39/4.75 % (374287)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2990479585:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 30.39/4.75 % (374287)Instruction limit reached!
% 30.39/4.75 % (374287)------------------------------
% 30.39/4.75 % (374287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374287)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374287)Termination reason: Instruction limit
% 30.39/4.75 % (374287)Termination phase: Saturation
% 30.39/4.75 % (374287)Time elapsed: 0.188 s
% 30.39/4.75 % (374287)Peak memory usage: 87 MB
% 30.39/4.75 % (374287)Instructions burned: 538 (million)
% 30.39/4.75 % (374289)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4187557359:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 30.39/4.75 % (374289)Instruction limit reached!
% 30.39/4.75 % (374289)------------------------------
% 30.39/4.75 % (374289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374289)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374289)Termination reason: Instruction limit
% 30.39/4.75 % (374289)Termination phase: Saturation
% 30.39/4.75 % (374289)Time elapsed: 0.092 s
% 30.39/4.75 % (374289)Peak memory usage: 93 MB
% 30.39/4.75 % (374289)Instructions burned: 181 (million)
% 30.39/4.75 % (374291)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3638677630:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi)
% 30.39/4.75 % (374284)Instruction limit reached!
% 30.39/4.75 % (374284)------------------------------
% 30.39/4.75 % (374284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374284)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374284)Termination reason: Instruction limit
% 30.39/4.75 % (374284)Termination phase: Saturation
% 30.39/4.75 % (374284)Time elapsed: 1.071 s
% 30.39/4.75 % (374284)Peak memory usage: 147 MB
% 30.39/4.75 % (374284)Instructions burned: 3259 (million)
% 30.39/4.75 % (374293)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3743797285:i=412:gtgl=4:gtg=exists_all_2975 on theBenchmark for (2975ds/412Mi)
% 30.39/4.75 % (374293)Instruction limit reached!
% 30.39/4.75 % (374293)------------------------------
% 30.39/4.75 % (374293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374293)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374293)Termination reason: Instruction limit
% 30.39/4.75 % (374293)Termination phase: Saturation
% 30.39/4.75 % (374293)Time elapsed: 0.110 s
% 30.39/4.75 % (374293)Peak memory usage: 90 MB
% 30.39/4.75 % (374293)Instructions burned: 414 (million)
% 30.39/4.75 % (374264)Instruction limit reached!
% 30.39/4.75 % (374264)------------------------------
% 30.39/4.75 % (374264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374264)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374264)Termination reason: Instruction limit
% 30.39/4.75 % (374264)Termination phase: Saturation
% 30.39/4.75 % (374264)Time elapsed: 2.157 s
% 30.39/4.75 % (374264)Peak memory usage: 149 MB
% 30.39/4.75 % (374264)Instructions burned: 3397 (million)
% 30.39/4.75 % (374295)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=817509276:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 30.39/4.75 % (374296)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3234824829:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 30.39/4.75 % (374296)Instruction limit reached!
% 30.39/4.75 % (374296)------------------------------
% 30.39/4.75 % (374296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374296)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374296)Termination reason: Instruction limit
% 30.39/4.75 % (374296)Termination phase: Saturation
% 30.39/4.75 % (374296)Time elapsed: 0.175 s
% 30.39/4.75 % (374296)Peak memory usage: 89 MB
% 30.39/4.75 % (374296)Instructions burned: 305 (million)
% 30.39/4.75 % (374299)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2422863796:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 30.39/4.75 % (374299)Instruction limit reached!
% 30.39/4.75 % (374299)------------------------------
% 30.39/4.75 % (374299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374299)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374299)Termination reason: Instruction limit
% 30.39/4.75 % (374299)Termination phase: Saturation
% 30.39/4.75 % (374299)Time elapsed: 0.389 s
% 30.39/4.75 % (374299)Peak memory usage: 92 MB
% 30.39/4.75 % (374299)Instructions burned: 720 (million)
% 30.39/4.75 % (374301)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3317845363:i=598:bs=on:bd=preordered:av=off:ss=axioms_2963 on theBenchmark for (2963ds/598Mi)
% 30.39/4.75 % (374295)First to succeed.
% 30.39/4.75 % (374295)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-374234"
% 30.39/4.75 % (374301)Instruction limit reached!
% 30.39/4.75 % (374301)------------------------------
% 30.39/4.75 % (374301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374301)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374301)Termination reason: Instruction limit
% 30.39/4.75 % (374301)Termination phase: Saturation
% 30.39/4.75 % (374301)Time elapsed: 0.340 s
% 30.39/4.75 % (374301)Peak memory usage: 89 MB
% 30.39/4.75 % (374301)Instructions burned: 600 (million)
% 30.39/4.75 % (374272)Instruction limit reached!
% 30.39/4.75 % (374272)------------------------------
% 30.39/4.75 % (374272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.39/4.75 % (374272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.39/4.75 % (374272)CaDiCaL version: 2.1.3
% 30.39/4.75 % (374272)Termination reason: Instruction limit
% 30.39/4.75 % (374272)Termination phase: Saturation
% 30.39/4.75 % (374272)Time elapsed: 3.392 s
% 30.39/4.75 % (374272)Peak memory usage: 154 MB
% 30.39/4.75 % (374272)Instructions burned: 5208 (million)
% 30.39/4.75 % (374295)Refutation found. Thanks to Tanya!
% 30.39/4.75 % SZS status Unsatisfiable for theBenchmark
% 30.39/4.75 % SZS output start Proof for theBenchmark
% See solution above
% 30.94/4.94 % (374295)------------------------------
% 30.94/4.94 % (374295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.94/4.94 % (374295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.94/4.94 % (374295)CaDiCaL version: 2.1.3
% 30.94/4.94 % (374295)Termination reason: Refutation
% 30.94/4.94 % (374295)Time elapsed: 1.331 s
% 30.94/4.94 % (374295)Peak memory usage: 154 MB
% 30.94/4.94 % (374295)Instructions burned: 4220 (million)
% 30.94/4.94 % (374295)------------------------------
% 30.94/4.94 % (374295)------------------------------
% 30.94/4.94 % (374234)Success in time 4.316 s
% 30.94/4.94 % Vampire exiting
%------------------------------------------------------------------------------