%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD046-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:11 AM UTC 2026
% Result : Unsatisfiable 36.61s 6.53s
% Output : Refutation 43.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 19
% Syntax : Number of formulae : 90 ( 76 unt; 0 def)
% Number of atoms : 119 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 63 ( 34 ~; 29 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 46 ( 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X4,X5,X2)
| ~ sum(X0,X3,X4)
| ~ sum(X3,X5,X1)
| sum(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_addition_1) ).
fof(f3,axiom,
! [X0] :
( sum(additive_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_identity_addition) ).
fof(f4,axiom,
! [X0] :
( sum(additive_inverse(X0),X0,additive_identity)
| ~ defined(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_inverse_addition) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ sum(X1,X0,X2)
| sum(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_addition) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X4,X5,X2)
| ~ product(X0,X3,X4)
| ~ product(X3,X5,X1)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_multiplication_1) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X4,X1,X5)
| ~ product(X3,X4,X0)
| product(X0,X1,X2)
| ~ product(X3,X5,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_multiplication_2) ).
fof(f8,axiom,
! [X0] :
( product(multiplicative_identity,X0,X0)
| ~ defined(X0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',existence_of_inverse_multiplication) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ product(X1,X0,X2)
| product(X0,X1,X2) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',distributivity_1) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X4,X1,X6)
| ~ sum(X3,X4,X0)
| ~ product(X3,X1,X5)
| product(X0,X1,X2)
| ~ sum(X5,X6,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity_2) ).
fof(f14,axiom,
defined(additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_definedness_of_additive_identity) ).
fof(f15,axiom,
! [X0] :
( defined(additive_inverse(X0))
| ~ defined(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_definedness_of_additive_inverse) ).
fof(f17,axiom,
defined(multiplicative_identity),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',totality_of_multiplication) ).
fof(f27,axiom,
defined(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_is_defined) ).
fof(f28,negated_conjecture,
~ sum(additive_identity,a,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_sum_2) ).
fof(f29,negated_conjecture,
~ sum(additive_identity,multiplicative_inverse(additive_inverse(a)),additive_inverse(multiplicative_inverse(a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_sum_3) ).
fof(f30,plain,
~ sum(multiplicative_inverse(additive_inverse(a)),additive_identity,additive_inverse(multiplicative_inverse(a))),
inference(unit_resulting_resolution,[],[f5,f29]) ).
fof(f31,plain,
~ sum(a,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f5,f28]) ).
fof(f32,plain,
sum(additive_inverse(a),a,additive_identity),
inference(unit_resulting_resolution,[],[f4,f27]) ).
fof(f33,plain,
sum(a,additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f5,f32]) ).
fof(f34,plain,
sum(additive_identity,a,a),
inference(unit_resulting_resolution,[],[f3,f27]) ).
fof(f35,plain,
product(multiplicative_inverse(a),a,multiplicative_identity),
inference(unit_resulting_resolution,[],[f9,f27,f28]) ).
fof(f37,plain,
defined(additive_inverse(a)),
inference(unit_resulting_resolution,[],[f15,f27]) ).
fof(f38,plain,
defined(additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f15,f37]) ).
fof(f39,plain,
sum(additive_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f3,f37]) ).
fof(f40,plain,
sum(additive_inverse(additive_inverse(a)),additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f4,f37]) ).
fof(f45,plain,
defined(multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f18,f27,f28]) ).
fof(f46,plain,
defined(additive_inverse(multiplicative_inverse(a))),
inference(unit_resulting_resolution,[],[f15,f45]) ).
fof(f48,plain,
sum(additive_inverse(multiplicative_inverse(a)),multiplicative_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f4,f45]) ).
fof(f52,plain,
sum(a,additive_identity,a),
inference(unit_resulting_resolution,[],[f1,f32,f33,f34]) ).
fof(f59,plain,
~ sum(additive_identity,additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f1,f31,f33,f52]) ).
fof(f129,plain,
sum(additive_identity,additive_inverse(multiplicative_inverse(a)),additive_inverse(multiplicative_inverse(a))),
inference(unit_resulting_resolution,[],[f3,f46]) ).
fof(f199,plain,
sum(additive_identity,additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f3,f38]) ).
fof(f218,plain,
sum(additive_inverse(a),additive_inverse(additive_inverse(a)),additive_identity),
inference(unit_resulting_resolution,[],[f5,f40]) ).
fof(f275,plain,
sum(multiplicative_inverse(a),additive_inverse(multiplicative_inverse(a)),additive_identity),
inference(unit_resulting_resolution,[],[f5,f48]) ).
fof(f289,plain,
product(multiplicative_identity,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f8,f14]) ).
fof(f294,plain,
product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f8,f45]) ).
fof(f295,plain,
product(multiplicative_identity,a,a),
inference(unit_resulting_resolution,[],[f8,f27]) ).
fof(f333,plain,
product(additive_identity,multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f10,f289]) ).
fof(f336,plain,
product(a,multiplicative_inverse(a),multiplicative_identity),
inference(unit_resulting_resolution,[],[f10,f35]) ).
fof(f337,plain,
product(a,multiplicative_identity,a),
inference(unit_resulting_resolution,[],[f10,f295]) ).
fof(f513,plain,
defined(additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f15,f17]) ).
fof(f514,plain,
sum(additive_identity,multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f3,f17]) ).
fof(f515,plain,
sum(additive_inverse(multiplicative_identity),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f4,f17]) ).
fof(f522,plain,
sum(multiplicative_identity,additive_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f5,f514]) ).
fof(f544,plain,
sum(additive_identity,additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f3,f513]) ).
fof(f977,plain,
sum(multiplicative_identity,additive_inverse(multiplicative_identity),additive_identity),
inference(unit_resulting_resolution,[],[f5,f515]) ).
fof(f1266,plain,
sum(a,additive_identity,additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f1,f33,f218,f199]) ).
fof(f1335,plain,
product(additive_inverse(additive_inverse(a)),multiplicative_identity,a),
inference(unit_resulting_resolution,[],[f12,f52,f333,f337,f1266]) ).
fof(f1549,plain,
product(additive_inverse(additive_inverse(a)),multiplicative_inverse(a),multiplicative_identity),
inference(unit_resulting_resolution,[],[f6,f1335,f294,f336]) ).
fof(f1618,plain,
~ sum(multiplicative_inverse(additive_inverse(a)),multiplicative_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f1,f30,f275,f129]) ).
fof(f2777,plain,
defined(multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f18,f37,f59]) ).
fof(f2778,plain,
product(multiplicative_inverse(additive_inverse(a)),additive_inverse(a),multiplicative_identity),
inference(unit_resulting_resolution,[],[f9,f37,f59]) ).
fof(f2869,plain,
sum(additive_identity,multiplicative_inverse(additive_inverse(a)),multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f3,f2777]) ).
fof(f2871,plain,
product(multiplicative_identity,multiplicative_inverse(additive_inverse(a)),multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f8,f2777]) ).
fof(f2909,plain,
sum(multiplicative_inverse(additive_inverse(a)),additive_identity,multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f5,f2869]) ).
fof(f2913,plain,
product(additive_inverse(a),multiplicative_inverse(additive_inverse(a)),multiplicative_identity),
inference(unit_resulting_resolution,[],[f10,f2778]) ).
fof(f2956,plain,
product(multiplicative_inverse(additive_inverse(a)),multiplicative_identity,multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f6,f2778,f2913,f2871]) ).
fof(f3461,plain,
product(additive_inverse(a),additive_identity,multiply(additive_inverse(a),additive_identity)),
inference(unit_resulting_resolution,[],[f20,f14,f37]) ).
fof(f3481,plain,
product(multiplicative_inverse(a),additive_identity,multiply(multiplicative_inverse(a),additive_identity)),
inference(unit_resulting_resolution,[],[f20,f14,f45]) ).
fof(f3486,plain,
product(multiplicative_inverse(a),additive_inverse(a),multiply(multiplicative_inverse(a),additive_inverse(a))),
inference(unit_resulting_resolution,[],[f20,f37,f45]) ).
fof(f3509,plain,
product(a,multiplicative_inverse(additive_inverse(a)),multiply(a,multiplicative_inverse(additive_inverse(a)))),
inference(unit_resulting_resolution,[],[f20,f2777,f27]) ).
fof(f3589,plain,
product(additive_inverse(a),multiplicative_inverse(a),multiply(multiplicative_inverse(a),additive_inverse(a))),
inference(unit_resulting_resolution,[],[f10,f3486]) ).
fof(f4855,plain,
product(additive_identity,additive_inverse(a),multiply(additive_inverse(a),additive_identity)),
inference(unit_resulting_resolution,[],[f10,f3461]) ).
fof(f4908,plain,
sum(multiply(additive_inverse(a),additive_identity),multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f11,f2778,f2869,f2778,f4855]) ).
fof(f4929,plain,
sum(multiply(additive_inverse(a),additive_identity),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f977,f977,f4908]) ).
fof(f5133,plain,
sum(additive_identity,multiply(additive_inverse(a),additive_identity),additive_identity),
inference(unit_resulting_resolution,[],[f5,f4929]) ).
fof(f6852,plain,
product(additive_identity,multiplicative_inverse(a),multiply(multiplicative_inverse(a),additive_identity)),
inference(unit_resulting_resolution,[],[f10,f3481]) ).
fof(f6875,plain,
sum(multiply(multiplicative_inverse(a),additive_inverse(a)),multiplicative_identity,multiply(multiplicative_inverse(a),additive_identity)),
inference(unit_resulting_resolution,[],[f11,f1549,f218,f3589,f6852]) ).
fof(f6896,plain,
sum(multiply(multiplicative_inverse(a),additive_identity),multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f11,f1549,f199,f1549,f6852]) ).
fof(f6955,plain,
sum(multiply(multiplicative_inverse(a),additive_identity),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f977,f977,f6896]) ).
fof(f8032,plain,
sum(multiply(multiplicative_inverse(a),additive_inverse(a)),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f522,f6955,f6875]) ).
fof(f8109,plain,
product(additive_identity,multiplicative_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f12,f218,f1549,f3589,f8032]) ).
fof(f8146,plain,
product(additive_identity,a,additive_identity),
inference(unit_resulting_resolution,[],[f7,f333,f35,f8109]) ).
fof(f8161,plain,
product(multiplicative_inverse(a),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f10,f8109]) ).
fof(f8386,plain,
product(a,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f6,f289,f336,f8161]) ).
fof(f8971,plain,
product(additive_identity,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f5133,f3461,f33,f8386]) ).
fof(f9245,plain,
product(additive_inverse(a),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f5133,f3461,f39,f8971]) ).
fof(f9335,plain,
product(additive_identity,additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f10,f9245]) ).
fof(f9554,plain,
product(additive_identity,multiplicative_inverse(additive_inverse(a)),additive_identity),
inference(unit_resulting_resolution,[],[f7,f333,f2913,f9335]) ).
fof(f23668,plain,
product(multiplicative_inverse(additive_inverse(a)),a,multiply(a,multiplicative_inverse(additive_inverse(a)))),
inference(unit_resulting_resolution,[],[f10,f3509]) ).
fof(f23671,plain,
sum(multiply(a,multiplicative_inverse(additive_inverse(a))),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f11,f33,f2913,f9554,f3509]) ).
fof(f31241,plain,
sum(multiply(a,multiplicative_inverse(additive_inverse(a))),additive_identity,additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f1,f23671,f977,f544]) ).
fof(f32877,plain,
product(multiplicative_inverse(additive_inverse(a)),a,additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f12,f8146,f2909,f23668,f31241]) ).
fof(f32898,plain,
product(additive_inverse(multiplicative_identity),multiplicative_inverse(a),multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f7,f336,f2956,f32877]) ).
fof(f42982,plain,
~ product(additive_inverse(multiplicative_identity),multiplicative_inverse(a),multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f11,f515,f8109,f294,f1618]) ).
fof(f43054,plain,
$false,
inference(forward_subsumption_resolution,[],[f42982,f32898]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD046-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n003.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 00:38:43 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running first-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.19/2.54 % (2185531)Input is clausal, will run a generic CNF schedule.
% 14.19/2.54 % (2185542)dis-21_1_sil=8000:lcm=predicate:random_seed=2141989605: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)
% 14.19/2.54 % (2185539)lrs+10_1_sil=8000:sp=occurrence:random_seed=2865952444:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 14.19/2.54 % (2185541)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1115337609:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 14.19/2.54 % (2185537)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3620645778:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 14.19/2.54 % (2185536)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=1764879857:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 14.19/2.54 % (2185538)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2870106604:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 14.19/2.54 % (2185542)Instruction limit reached!
% 14.19/2.54 % (2185542)------------------------------
% 14.19/2.54 % (2185542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.54 % (2185542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.54 % (2185542)CaDiCaL version: 2.1.3
% 14.19/2.54 % (2185542)Termination reason: Instruction limit
% 14.19/2.54 % (2185542)Termination phase: Saturation
% 14.19/2.54 % (2185542)Time elapsed: 0.042 s
% 14.19/2.54 % (2185542)Peak memory usage: 90 MB
% 14.19/2.54 % (2185542)Instructions burned: 118 (million)
% 14.19/2.54 % (2185540)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1211733390:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 14.19/2.54 % (2185539)Instruction limit reached!
% 14.19/2.54 % (2185539)------------------------------
% 14.19/2.54 % (2185539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.54 % (2185539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.54 % (2185539)CaDiCaL version: 2.1.3
% 14.19/2.54 % (2185539)Termination reason: Instruction limit
% 14.19/2.54 % (2185539)Termination phase: Saturation
% 14.19/2.54 % (2185539)Time elapsed: 0.069 s
% 14.19/2.54 % (2185539)Peak memory usage: 88 MB
% 14.19/2.54 % (2185539)Instructions burned: 107 (million)
% 14.19/2.54 % (2185540)Instruction limit reached!
% 14.19/2.54 % (2185540)------------------------------
% 14.19/2.54 % (2185540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.54 % (2185540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.54 % (2185540)CaDiCaL version: 2.1.3
% 14.19/2.54 % (2185540)Termination reason: Instruction limit
% 14.19/2.54 % (2185540)Termination phase: Saturation
% 14.19/2.54 % (2185540)Time elapsed: 0.062 s
% 14.19/2.54 % (2185540)Peak memory usage: 88 MB
% 14.19/2.54 % (2185540)Instructions burned: 114 (million)
% 14.19/2.54 % (2185541)Instruction limit reached!
% 14.19/2.54 % (2185541)------------------------------
% 14.19/2.54 % (2185541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.54 % (2185541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.54 % (2185541)CaDiCaL version: 2.1.3
% 14.19/2.54 % (2185541)Termination reason: Instruction limit
% 14.19/2.54 % (2185541)Termination phase: Saturation
% 14.19/2.54 % (2185541)Time elapsed: 0.103 s
% 14.19/2.54 % (2185541)Peak memory usage: 88 MB
% 14.19/2.54 % (2185541)Instructions burned: 180 (million)
% 14.19/2.54 % (2185583)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=653433157:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 14.19/2.54 % (2185583)Instruction limit reached!
% 14.19/2.54 % (2185583)------------------------------
% 14.19/2.54 % (2185583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.54 % (2185583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.54 % (2185583)CaDiCaL version: 2.1.3
% 14.19/2.54 % (2185583)Termination reason: Instruction limit
% 14.19/2.54 % (2185583)Termination phase: Saturation
% 14.19/2.54 % (2185583)Time elapsed: 0.030 s
% 14.19/2.54 % (2185583)Peak memory usage: 87 MB
% 14.19/2.54 % (2185583)Instructions burned: 147 (million)
% 14.19/2.54 % (2185611)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1405816502: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)
% 26.65/4.21 % (2185618)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3926475524:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 26.65/4.21 % (2185623)lrs+10_64_to=lpo:sil=8000:random_seed=1227165617:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 26.65/4.21 % (2185638)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1550675099:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 26.65/4.21 % (2185611)Instruction limit reached!
% 26.65/4.21 % (2185611)------------------------------
% 26.65/4.21 % (2185611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.21 % (2185611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.21 % (2185611)CaDiCaL version: 2.1.3
% 26.65/4.21 % (2185611)Termination reason: Instruction limit
% 26.65/4.21 % (2185611)Termination phase: Saturation
% 26.65/4.21 % (2185611)Time elapsed: 0.100 s
% 26.65/4.21 % (2185611)Peak memory usage: 91 MB
% 26.65/4.21 % (2185611)Instructions burned: 190 (million)
% 26.65/4.21 % (2185623)Instruction limit reached!
% 26.65/4.21 % (2185623)------------------------------
% 26.65/4.21 % (2185623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.21 % (2185623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.21 % (2185623)CaDiCaL version: 2.1.3
% 26.65/4.21 % (2185623)Termination reason: Instruction limit
% 26.65/4.21 % (2185623)Termination phase: Saturation
% 26.65/4.21 % (2185623)Time elapsed: 0.082 s
% 26.65/4.21 % (2185623)Peak memory usage: 90 MB
% 26.65/4.21 % (2185623)Instructions burned: 126 (million)
% 26.65/4.21 % (2185638)Instruction limit reached!
% 26.65/4.21 % (2185638)------------------------------
% 26.65/4.21 % (2185638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.21 % (2185638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.21 % (2185638)CaDiCaL version: 2.1.3
% 26.65/4.21 % (2185638)Termination reason: Instruction limit
% 26.65/4.21 % (2185638)Termination phase: Saturation
% 26.65/4.21 % (2185638)Time elapsed: 0.070 s
% 26.65/4.21 % (2185638)Peak memory usage: 89 MB
% 26.65/4.21 % (2185638)Instructions burned: 196 (million)
% 26.65/4.21 % (2185618)Instruction limit reached!
% 26.65/4.21 % (2185618)------------------------------
% 26.65/4.21 % (2185618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.21 % (2185618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.21 % (2185618)CaDiCaL version: 2.1.3
% 26.65/4.21 % (2185618)Termination reason: Instruction limit
% 26.65/4.21 % (2185618)Termination phase: Saturation
% 26.65/4.21 % (2185618)Time elapsed: 0.131 s
% 26.65/4.21 % (2185618)Peak memory usage: 89 MB
% 26.65/4.21 % (2185618)Instructions burned: 219 (million)
% 26.65/4.21 % (2185682)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4048730683:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 26.65/4.21 % (2185685)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2942264957:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 26.65/4.21 % (2185673)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4156738516:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 26.65/4.21 % (2185683)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=616212184:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 26.65/4.21 % (2185683)Instruction limit reached!
% 26.65/4.21 % (2185683)------------------------------
% 26.65/4.21 % (2185683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.65/4.21 % (2185683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.65/4.21 % (2185683)CaDiCaL version: 2.1.3
% 26.65/4.21 % (2185683)Termination reason: Instruction limit
% 26.65/4.21 % (2185683)Termination phase: Saturation
% 26.65/4.21 % (2185683)Time elapsed: 0.096 s
% 26.65/4.21 % (2185683)Peak memory usage: 89 MB
% 26.65/4.21 % (2185683)Instructions burned: 106 (million)
% 26.65/4.21 % (2185685)Instruction limit reached!
% 26.65/4.21 % (2185685)------------------------------
% 26.65/4.21 % (2185685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185685)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185685)Termination reason: Instruction limit
% 36.61/6.53 % (2185685)Termination phase: Saturation
% 36.61/6.53 % (2185685)Time elapsed: 0.115 s
% 36.61/6.53 % (2185685)Peak memory usage: 89 MB
% 36.61/6.53 % (2185685)Instructions burned: 107 (million)
% 36.61/6.53 % (2185673)Instruction limit reached!
% 36.61/6.53 % (2185673)------------------------------
% 36.61/6.53 % (2185673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185673)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185673)Termination reason: Instruction limit
% 36.61/6.53 % (2185673)Termination phase: Saturation
% 36.61/6.53 % (2185673)Time elapsed: 0.170 s
% 36.61/6.53 % (2185673)Peak memory usage: 90 MB
% 36.61/6.53 % (2185673)Instructions burned: 157 (million)
% 36.61/6.53 % (2185722)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=808640620:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 36.61/6.53 % (2185723)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4115550940:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 36.61/6.53 % (2185724)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1215711312:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 36.61/6.53 % (2185724)Instruction limit reached!
% 36.61/6.53 % (2185724)------------------------------
% 36.61/6.53 % (2185724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185724)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185724)Termination reason: Instruction limit
% 36.61/6.53 % (2185724)Termination phase: Saturation
% 36.61/6.53 % (2185724)Time elapsed: 0.137 s
% 36.61/6.53 % (2185724)Peak memory usage: 89 MB
% 36.61/6.53 % (2185724)Instructions burned: 134 (million)
% 36.61/6.53 % (2185722)Instruction limit reached!
% 36.61/6.53 % (2185722)------------------------------
% 36.61/6.53 % (2185722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185722)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185722)Termination reason: Instruction limit
% 36.61/6.53 % (2185722)Termination phase: Saturation
% 36.61/6.53 % (2185722)Time elapsed: 0.246 s
% 36.61/6.53 % (2185722)Peak memory usage: 88 MB
% 36.61/6.53 % (2185722)Instructions burned: 243 (million)
% 36.61/6.53 % (2185736)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1558800463:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 36.61/6.53 % (2185737)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3322324341:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 36.61/6.53 % (2185736)Instruction limit reached!
% 36.61/6.53 % (2185736)------------------------------
% 36.61/6.53 % (2185736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185736)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185736)Termination reason: Instruction limit
% 36.61/6.53 % (2185736)Termination phase: Saturation
% 36.61/6.53 % (2185736)Time elapsed: 0.276 s
% 36.61/6.53 % (2185736)Peak memory usage: 108 MB
% 36.61/6.53 % (2185736)Instructions burned: 499 (million)
% 36.61/6.53 % (2185737)Instruction limit reached!
% 36.61/6.53 % (2185737)------------------------------
% 36.61/6.53 % (2185737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185737)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185737)Termination reason: Instruction limit
% 36.61/6.53 % (2185737)Termination phase: Saturation
% 36.61/6.53 % (2185737)Time elapsed: 0.172 s
% 36.61/6.53 % (2185737)Peak memory usage: 91 MB
% 36.61/6.53 % (2185737)Instructions burned: 193 (million)
% 36.61/6.53 % (2185743)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=798186674:cond=on:i=156:bs=on:gtg=exists_all:er=known_2981 on theBenchmark for (2981ds/156Mi)
% 36.61/6.53 % (2185742)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=694614505:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi)
% 36.61/6.53 % (2185743)Instruction limit reached!
% 36.61/6.53 % (2185743)------------------------------
% 36.61/6.53 % (2185743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185743)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185743)Termination reason: Instruction limit
% 36.61/6.53 % (2185743)Termination phase: Saturation
% 36.61/6.53 % (2185743)Time elapsed: 0.116 s
% 36.61/6.53 % (2185743)Peak memory usage: 88 MB
% 36.61/6.53 % (2185743)Instructions burned: 157 (million)
% 36.61/6.53 % (2185742)Instruction limit reached!
% 36.61/6.53 % (2185742)------------------------------
% 36.61/6.53 % (2185742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185742)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185742)Termination reason: Instruction limit
% 36.61/6.53 % (2185742)Termination phase: Saturation
% 36.61/6.53 % (2185742)Time elapsed: 0.245 s
% 36.61/6.53 % (2185742)Peak memory usage: 90 MB
% 36.61/6.53 % (2185742)Instructions burned: 264 (million)
% 36.61/6.53 % (2185750)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=3229646076:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi)
% 36.61/6.53 % (2185682)Instruction limit reached!
% 36.61/6.53 % (2185682)------------------------------
% 36.61/6.53 % (2185682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185682)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185682)Termination reason: Instruction limit
% 36.61/6.53 % (2185682)Termination phase: Saturation
% 36.61/6.53 % (2185682)Time elapsed: 1.885 s
% 36.61/6.53 % (2185682)Peak memory usage: 147 MB
% 36.61/6.53 % (2185682)Instructions burned: 3394 (million)
% 36.61/6.53 % (2185753)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1883033243:i=537:av=off:ss=included_2976 on theBenchmark for (2976ds/537Mi)
% 36.61/6.53 % (2185756)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=796571232:i=180:bd=preordered:av=off_2974 on theBenchmark for (2974ds/180Mi)
% 36.61/6.53 % (2185756)Instruction limit reached!
% 36.61/6.53 % (2185756)------------------------------
% 36.61/6.53 % (2185756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185756)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185756)Termination reason: Instruction limit
% 36.61/6.53 % (2185756)Termination phase: Saturation
% 36.61/6.53 % (2185756)Time elapsed: 0.087 s
% 36.61/6.53 % (2185756)Peak memory usage: 93 MB
% 36.61/6.53 % (2185756)Instructions burned: 181 (million)
% 36.61/6.53 % (2185760)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=107648615:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/10307Mi)
% 36.61/6.53 % (2185753)Instruction limit reached!
% 36.61/6.53 % (2185753)------------------------------
% 36.61/6.53 % (2185753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185753)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185753)Termination reason: Instruction limit
% 36.61/6.53 % (2185753)Termination phase: Saturation
% 36.61/6.53 % (2185753)Time elapsed: 0.506 s
% 36.61/6.53 % (2185753)Peak memory usage: 90 MB
% 36.61/6.53 % (2185753)Instructions burned: 538 (million)
% 36.61/6.53 % (2185764)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=2757917596:i=412:gtgl=4:gtg=exists_all_2968 on theBenchmark for (2968ds/412Mi)
% 36.61/6.53 % (2185764)Instruction limit reached!
% 36.61/6.53 % (2185764)------------------------------
% 36.61/6.53 % (2185764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185764)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185764)Termination reason: Instruction limit
% 36.61/6.53 % (2185764)Termination phase: Saturation
% 36.61/6.53 % (2185764)Time elapsed: 0.332 s
% 36.61/6.53 % (2185764)Peak memory usage: 90 MB
% 36.61/6.53 % (2185764)Instructions burned: 412 (million)
% 36.61/6.53 % (2185766)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=3485932553:s2pl=no:i=8478:s2at=4:nm=6_2962 on theBenchmark for (2962ds/8478Mi)
% 36.61/6.53 % (2185537)First to succeed.
% 36.61/6.53 % (2185537)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2185531"
% 36.61/6.53 % (2185750)Instruction limit reached!
% 36.61/6.53 % (2185750)------------------------------
% 36.61/6.53 % (2185750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.61/6.53 % (2185750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.61/6.53 % (2185750)CaDiCaL version: 2.1.3
% 36.61/6.53 % (2185750)Termination reason: Instruction limit
% 36.61/6.53 % (2185750)Termination phase: Saturation
% 36.61/6.53 % (2185750)Time elapsed: 3.247 s
% 36.61/6.53 % (2185750)Peak memory usage: 144 MB
% 36.61/6.53 % (2185750)Instructions burned: 3256 (million)
% 36.61/6.53 % (2185770)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=1284951541:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2942 on theBenchmark for (2942ds/303Mi)
% 36.61/6.53 % (2185537)Refutation found. Thanks to Tanya!
% 36.61/6.53 % SZS status Unsatisfiable for theBenchmark
% 36.61/6.53 % SZS output start Proof for theBenchmark
% See solution above
% 43.37/6.73 % (2185537)------------------------------
% 43.37/6.73 % (2185537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.37/6.73 % (2185537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.37/6.73 % (2185537)CaDiCaL version: 2.1.3
% 43.37/6.73 % (2185537)Termination reason: Refutation
% 43.37/6.73 % (2185537)Time elapsed: 5.465 s
% 43.37/6.73 % (2185537)Peak memory usage: 163 MB
% 43.37/6.73 % (2185537)Instructions burned: 6003 (million)
% 43.37/6.73 % (2185537)------------------------------
% 43.37/6.73 % (2185537)------------------------------
% 43.37/6.73 % (2185531)Success in time 6.071 s
% 43.37/6.73 % Vampire exiting
%------------------------------------------------------------------------------