%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD093-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 : n013.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:27 AM UTC 2026
% Result : Unsatisfiable 128.96s 21.86s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 26
% Syntax : Number of formulae : 114 ( 94 unt; 0 def)
% Number of atoms : 159 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 94 ( 49 ~; 45 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 67 ( 67 !; 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(f2,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X4,X1,X5)
| ~ sum(X3,X4,X0)
| sum(X0,X1,X2)
| ~ sum(X3,X5,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_addition_2) ).
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(f19,axiom,
! [X0,X1] :
( sum(X0,X1,add(X0,X1))
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',totality_of_addition) ).
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(f22,axiom,
! [X2,X0,X1] :
( ~ less_or_equal(X2,X1)
| ~ less_or_equal(X0,X2)
| less_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_order_relation) ).
fof(f23,axiom,
! [X0,X1] :
( less_or_equal(X1,X0)
| less_or_equal(X0,X1)
| ~ defined(X0)
| ~ defined(X1) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',compatibility_of_order_relation_and_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,
less_or_equal(multiplicative_identity,multiplicative_inverse(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal_3) ).
fof(f30,negated_conjecture,
~ less_or_equal(a,multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_less_or_equal_4) ).
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(additive_identity,a,a),
inference(unit_resulting_resolution,[],[f3,f27]) ).
fof(f34,plain,
product(multiplicative_identity,a,a),
inference(unit_resulting_resolution,[],[f8,f27]) ).
fof(f35,plain,
product(multiplicative_inverse(a),a,multiplicative_identity),
inference(unit_resulting_resolution,[],[f9,f28,f27]) ).
fof(f36,plain,
product(a,multiplicative_inverse(a),multiplicative_identity),
inference(unit_resulting_resolution,[],[f10,f35]) ).
fof(f37,plain,
product(a,multiplicative_identity,a),
inference(unit_resulting_resolution,[],[f10,f34]) ).
fof(f40,plain,
sum(a,additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f5,f32]) ).
fof(f44,plain,
sum(a,additive_identity,a),
inference(unit_resulting_resolution,[],[f5,f33]) ).
fof(f62,plain,
~ sum(additive_identity,additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f1,f31,f40,f44]) ).
fof(f73,plain,
sum(additive_identity,multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f3,f17]) ).
fof(f74,plain,
sum(additive_inverse(multiplicative_identity),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f4,f17]) ).
fof(f76,plain,
less_or_equal(multiplicative_identity,a),
inference(unit_resulting_resolution,[],[f23,f27,f30,f17]) ).
fof(f128,plain,
sum(multiplicative_identity,additive_inverse(multiplicative_identity),additive_identity),
inference(unit_resulting_resolution,[],[f5,f74]) ).
fof(f133,plain,
sum(multiplicative_identity,additive_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f5,f73]) ).
fof(f135,plain,
defined(multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f18,f27,f28]) ).
fof(f136,plain,
sum(additive_identity,multiplicative_inverse(a),multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f3,f135]) ).
fof(f138,plain,
product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f8,f135]) ).
fof(f172,plain,
product(multiplicative_inverse(a),multiplicative_identity,multiplicative_inverse(a)),
inference(unit_resulting_resolution,[],[f10,f138]) ).
fof(f183,plain,
defined(additive_inverse(a)),
inference(unit_resulting_resolution,[],[f15,f27]) ).
fof(f184,plain,
defined(additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f15,f17]) ).
fof(f186,plain,
sum(additive_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f3,f183]) ).
fof(f187,plain,
sum(additive_inverse(additive_inverse(a)),additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f4,f183]) ).
fof(f188,plain,
product(multiplicative_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f8,f183]) ).
fof(f189,plain,
defined(additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f15,f183]) ).
fof(f195,plain,
sum(multiplicative_identity,additive_inverse(a),add(multiplicative_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f19,f17,f183]) ).
fof(f204,plain,
product(multiplicative_inverse(a),additive_inverse(a),multiply(multiplicative_inverse(a),additive_inverse(a))),
inference(unit_resulting_resolution,[],[f20,f135,f183]) ).
fof(f211,plain,
sum(additive_inverse(a),additive_identity,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f1,f32,f40,f186]) ).
fof(f218,plain,
product(additive_inverse(a),multiplicative_identity,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f10,f188]) ).
fof(f291,plain,
product(additive_identity,multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f40,f37,f40,f218]) ).
fof(f297,plain,
product(multiplicative_identity,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f10,f291]) ).
fof(f354,plain,
product(additive_identity,additive_inverse(a),multiply(additive_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f20,f183,f14]) ).
fof(f362,plain,
product(a,additive_identity,multiply(a,additive_identity)),
inference(unit_resulting_resolution,[],[f20,f27,f14]) ).
fof(f641,plain,
product(additive_identity,a,multiply(a,additive_identity)),
inference(unit_resulting_resolution,[],[f10,f362]) ).
fof(f665,plain,
sum(multiply(a,additive_identity),multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f11,f35,f35,f136,f641]) ).
fof(f679,plain,
sum(multiply(a,additive_identity),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f128,f128,f665]) ).
fof(f839,plain,
sum(additive_inverse(a),additive_inverse(additive_inverse(a)),additive_identity),
inference(unit_resulting_resolution,[],[f5,f187]) ).
fof(f1199,plain,
product(additive_inverse(a),multiplicative_inverse(a),multiply(multiplicative_inverse(a),additive_inverse(a))),
inference(unit_resulting_resolution,[],[f10,f204]) ).
fof(f1557,plain,
sum(additive_identity,additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f3,f184]) ).
fof(f1595,plain,
sum(multiplicative_inverse(a),additive_inverse(multiplicative_identity),add(multiplicative_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f19,f135,f184]) ).
fof(f1596,plain,
sum(a,additive_inverse(multiplicative_identity),add(a,additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f19,f27,f184]) ).
fof(f1604,plain,
product(additive_inverse(a),additive_inverse(multiplicative_identity),multiply(additive_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f20,f183,f184]) ).
fof(f1608,plain,
product(a,additive_inverse(multiplicative_identity),multiply(a,additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f20,f27,f184]) ).
fof(f1612,plain,
product(additive_inverse(multiplicative_identity),a,multiply(a,additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f10,f1608]) ).
fof(f1637,plain,
sum(multiply(a,additive_inverse(multiplicative_identity)),a,multiply(a,additive_identity)),
inference(unit_resulting_resolution,[],[f11,f34,f641,f74,f1612]) ).
fof(f1646,plain,
sum(multiply(a,additive_inverse(multiplicative_identity)),a,additive_identity),
inference(unit_resulting_resolution,[],[f1,f44,f679,f1637]) ).
fof(f1716,plain,
product(additive_identity,a,additive_identity),
inference(unit_resulting_resolution,[],[f12,f34,f74,f1612,f1646]) ).
fof(f1738,plain,
product(additive_identity,multiplicative_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f7,f291,f36,f1716]) ).
fof(f1747,plain,
product(a,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f10,f1716]) ).
fof(f2129,plain,
sum(multiply(multiplicative_inverse(a),additive_inverse(a)),multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f11,f36,f32,f1199,f1738]) ).
fof(f2187,plain,
sum(multiply(multiplicative_inverse(a),additive_inverse(a)),additive_identity,additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f1,f1557,f128,f2129]) ).
fof(f3374,plain,
sum(additive_inverse(multiplicative_identity),a,add(a,additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f5,f1596]) ).
fof(f3376,plain,
less_or_equal(additive_identity,add(a,additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f24,f76,f128,f1596]) ).
fof(f4007,plain,
product(additive_inverse(multiplicative_identity),additive_inverse(a),multiply(additive_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f10,f1604]) ).
fof(f5204,plain,
product(additive_inverse(a),additive_identity,multiply(additive_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f10,f354]) ).
fof(f24940,plain,
sum(add(multiplicative_identity,additive_inverse(a)),a,multiplicative_identity),
inference(unit_resulting_resolution,[],[f2,f133,f32,f195]) ).
fof(f26896,plain,
~ less_or_equal(additive_identity,add(multiplicative_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f24,f30,f33,f24940]) ).
fof(f27475,plain,
product(additive_inverse(a),multiplicative_inverse(a),additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f12,f211,f1738,f1199,f2187]) ).
fof(f27506,plain,
product(additive_inverse(multiplicative_identity),a,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f7,f218,f35,f27475]) ).
fof(f27522,plain,
product(multiplicative_inverse(a),additive_inverse(a),additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f10,f27475]) ).
fof(f27569,plain,
product(a,additive_inverse(multiplicative_identity),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f6,f188,f36,f27522]) ).
fof(f31709,plain,
sum(additive_identity,additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f3,f189]) ).
fof(f31802,plain,
sum(a,additive_identity,additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f1,f40,f839,f31709]) ).
fof(f32161,plain,
product(multiplicative_identity,a,additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f12,f133,f1716,f34,f31802]) ).
fof(f32256,plain,
product(additive_inverse(additive_inverse(a)),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f7,f297,f1747,f32161]) ).
fof(f66096,plain,
defined(multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f18,f183,f62]) ).
fof(f66097,plain,
product(multiplicative_inverse(additive_inverse(a)),additive_inverse(a),multiplicative_identity),
inference(unit_resulting_resolution,[],[f9,f183,f62]) ).
fof(f184165,plain,
sum(additive_identity,multiplicative_inverse(additive_inverse(a)),multiplicative_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f3,f66096]) ).
fof(f184332,plain,
sum(multiply(additive_identity,additive_inverse(a)),multiplicative_identity,multiplicative_identity),
inference(unit_resulting_resolution,[],[f11,f354,f66097,f66097,f184165]) ).
fof(f184361,plain,
sum(multiply(additive_identity,additive_inverse(a)),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f128,f128,f184332]) ).
fof(f186134,plain,
product(additive_identity,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f32256,f839,f5204,f184361]) ).
fof(f190236,plain,
product(additive_inverse(a),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f184361,f5204,f211,f186134]) ).
fof(f193486,plain,
product(additive_identity,additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f10,f190236]) ).
fof(f195402,plain,
sum(additive_inverse(a),multiply(additive_inverse(a),additive_inverse(multiplicative_identity)),additive_identity),
inference(unit_resulting_resolution,[],[f11,f4007,f128,f188,f193486]) ).
fof(f195515,plain,
sum(additive_identity,multiply(additive_inverse(a),additive_inverse(multiplicative_identity)),multiply(additive_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f11,f4007,f1557,f4007,f193486]) ).
fof(f238264,plain,
sum(a,additive_identity,multiply(additive_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f1,f40,f195515,f195402]) ).
fof(f239323,plain,
product(multiplicative_identity,a,multiply(additive_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f12,f133,f1716,f34,f238264]) ).
fof(f239519,plain,
product(multiplicative_inverse(a),multiply(additive_inverse(a),additive_inverse(multiplicative_identity)),multiplicative_identity),
inference(unit_resulting_resolution,[],[f6,f172,f35,f239323]) ).
fof(f303940,plain,
product(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity),multiplicative_identity),
inference(unit_resulting_resolution,[],[f7,f27522,f1604,f239519]) ).
fof(f307268,plain,
product(add(a,additive_inverse(multiplicative_identity)),additive_inverse(multiplicative_identity),add(multiplicative_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f12,f195,f27569,f3374,f303940]) ).
fof(f603667,plain,
product(add(multiplicative_inverse(a),additive_inverse(multiplicative_identity)),a,add(multiplicative_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f12,f195,f27506,f35,f1595]) ).
fof(f603672,plain,
less_or_equal(additive_identity,add(multiplicative_inverse(a),additive_inverse(multiplicative_identity))),
inference(unit_resulting_resolution,[],[f24,f29,f128,f1595]) ).
fof(f771039,plain,
~ less_or_equal(additive_identity,a),
inference(unit_resulting_resolution,[],[f25,f26896,f603672,f603667]) ).
fof(f771104,plain,
less_or_equal(a,additive_identity),
inference(unit_resulting_resolution,[],[f23,f27,f14,f771039]) ).
fof(f771844,plain,
less_or_equal(multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f22,f76,f771104]) ).
fof(f772384,plain,
less_or_equal(additive_identity,additive_inverse(multiplicative_identity)),
inference(unit_resulting_resolution,[],[f24,f128,f1557,f771844]) ).
fof(f773394,plain,
~ product(add(a,additive_inverse(multiplicative_identity)),additive_inverse(multiplicative_identity),add(multiplicative_identity,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f25,f26896,f3376,f772384]) ).
fof(f773595,plain,
$false,
inference(forward_subsumption_resolution,[],[f773394,f307268]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD093-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n013.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 01:01:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 7.53/1.91 % (1762722)Input is clausal, will run a generic CNF schedule.
% 7.53/1.91 % (1762730)lrs+10_1_sil=8000:sp=occurrence:random_seed=2614711128:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.53/1.91 % (1762729)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3231341430:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.53/1.91 % (1762728)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1534339727:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.53/1.91 % (1762727)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=1228710108:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.53/1.91 % (1762730)Instruction limit reached!
% 7.53/1.91 % (1762730)------------------------------
% 7.53/1.91 % (1762730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/1.91 % (1762730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.91 % (1762730)CaDiCaL version: 2.1.3
% 7.53/1.91 % (1762730)Termination reason: Instruction limit
% 7.53/1.91 % (1762730)Termination phase: Saturation
% 7.53/1.91 % (1762730)Time elapsed: 0.035 s
% 7.53/1.91 % (1762730)Peak memory usage: 88 MB
% 7.53/1.91 % (1762730)Instructions burned: 109 (million)
% 7.53/1.91 % (1762732)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3021059822:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.53/1.91 % (1762731)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3201119709:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.53/1.91 % (1762733)dis-21_1_sil=8000:lcm=predicate:random_seed=3425512240: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.53/1.91 % (1762731)Instruction limit reached!
% 7.53/1.91 % (1762731)------------------------------
% 7.53/1.91 % (1762731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/1.91 % (1762731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.91 % (1762731)CaDiCaL version: 2.1.3
% 7.53/1.91 % (1762731)Termination reason: Instruction limit
% 7.53/1.91 % (1762731)Termination phase: Saturation
% 7.53/1.91 % (1762731)Time elapsed: 0.068 s
% 7.53/1.91 % (1762731)Peak memory usage: 88 MB
% 7.53/1.91 % (1762731)Instructions burned: 114 (million)
% 7.53/1.91 % (1762733)Instruction limit reached!
% 7.53/1.91 % (1762733)------------------------------
% 7.53/1.91 % (1762733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/1.91 % (1762733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.91 % (1762733)CaDiCaL version: 2.1.3
% 7.53/1.91 % (1762733)Termination reason: Instruction limit
% 7.53/1.91 % (1762733)Termination phase: Saturation
% 7.53/1.91 % (1762733)Time elapsed: 0.072 s
% 7.53/1.91 % (1762733)Peak memory usage: 89 MB
% 7.53/1.91 % (1762733)Instructions burned: 118 (million)
% 7.53/1.91 % (1762738)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=3055867096:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.53/1.91 % (1762738)Instruction limit reached!
% 7.53/1.91 % (1762738)------------------------------
% 7.53/1.91 % (1762738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/1.91 % (1762738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.91 % (1762738)CaDiCaL version: 2.1.3
% 7.53/1.91 % (1762738)Termination reason: Instruction limit
% 7.53/1.91 % (1762738)Termination phase: Saturation
% 7.53/1.91 % (1762738)Time elapsed: 0.029 s
% 7.53/1.91 % (1762738)Peak memory usage: 87 MB
% 7.53/1.91 % (1762738)Instructions burned: 146 (million)
% 7.53/1.91 % (1762732)Instruction limit reached!
% 7.53/1.91 % (1762732)------------------------------
% 7.53/1.91 % (1762732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/1.91 % (1762732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.91 % (1762732)CaDiCaL version: 2.1.3
% 7.53/1.91 % (1762732)Termination reason: Instruction limit
% 7.53/1.91 % (1762732)Termination phase: Saturation
% 7.53/1.91 % (1762732)Time elapsed: 0.116 s
% 7.53/1.91 % (1762732)Peak memory usage: 89 MB
% 7.53/1.91 % (1762732)Instructions burned: 181 (million)
% 21.61/3.76 % (1762743)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2781207285:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 21.61/3.76 % (1762745)lrs+10_64_to=lpo:sil=8000:random_seed=1909048440:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 21.61/3.76 % (1762742)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1678601024: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)
% 21.61/3.76 % (1762745)Instruction limit reached!
% 21.61/3.76 % (1762745)------------------------------
% 21.61/3.76 % (1762745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.61/3.76 % (1762745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.61/3.76 % (1762745)CaDiCaL version: 2.1.3
% 21.61/3.76 % (1762745)Termination reason: Instruction limit
% 21.61/3.76 % (1762745)Termination phase: Saturation
% 21.61/3.76 % (1762745)Time elapsed: 0.033 s
% 21.61/3.76 % (1762745)Peak memory usage: 87 MB
% 21.61/3.76 % (1762745)Instructions burned: 128 (million)
% 21.61/3.76 % (1762746)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3448411943:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 21.61/3.76 % (1762742)Instruction limit reached!
% 21.61/3.76 % (1762742)------------------------------
% 21.61/3.76 % (1762742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.61/3.76 % (1762742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.61/3.76 % (1762742)CaDiCaL version: 2.1.3
% 21.61/3.76 % (1762742)Termination reason: Instruction limit
% 21.61/3.76 % (1762742)Termination phase: Saturation
% 21.61/3.76 % (1762742)Time elapsed: 0.098 s
% 21.61/3.76 % (1762742)Peak memory usage: 93 MB
% 21.61/3.76 % (1762742)Instructions burned: 191 (million)
% 21.61/3.76 % (1762746)Instruction limit reached!
% 21.61/3.76 % (1762746)------------------------------
% 21.61/3.76 % (1762746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.61/3.76 % (1762746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.61/3.76 % (1762746)CaDiCaL version: 2.1.3
% 21.61/3.76 % (1762746)Termination reason: Instruction limit
% 21.61/3.76 % (1762746)Termination phase: Saturation
% 21.61/3.76 % (1762746)Time elapsed: 0.069 s
% 21.61/3.76 % (1762746)Peak memory usage: 87 MB
% 21.61/3.76 % (1762746)Instructions burned: 195 (million)
% 21.61/3.76 % (1762750)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2062379810:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 21.61/3.76 % (1762743)Instruction limit reached!
% 21.61/3.76 % (1762743)------------------------------
% 21.61/3.76 % (1762743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.61/3.76 % (1762743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.61/3.76 % (1762743)CaDiCaL version: 2.1.3
% 21.61/3.76 % (1762743)Termination reason: Instruction limit
% 21.61/3.76 % (1762743)Termination phase: Saturation
% 21.61/3.76 % (1762743)Time elapsed: 0.122 s
% 21.61/3.76 % (1762743)Peak memory usage: 88 MB
% 21.61/3.76 % (1762743)Instructions burned: 219 (million)
% 21.61/3.76 % (1762750)Instruction limit reached!
% 21.61/3.76 % (1762750)------------------------------
% 21.61/3.76 % (1762750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.61/3.76 % (1762750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.61/3.76 % (1762750)CaDiCaL version: 2.1.3
% 21.61/3.76 % (1762750)Termination reason: Instruction limit
% 21.61/3.76 % (1762750)Termination phase: Saturation
% 21.61/3.76 % (1762750)Time elapsed: 0.056 s
% 21.61/3.76 % (1762750)Peak memory usage: 90 MB
% 21.61/3.76 % (1762750)Instructions burned: 157 (million)
% 21.61/3.76 % (1762754)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=2773248690:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 21.61/3.76 % (1762752)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1334060638:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 21.61/3.76 % (1762755)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2530236899:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 21.61/3.76 % (1762756)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1386043704:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 43.19/6.79 % (1762754)Instruction limit reached!
% 43.19/6.79 % (1762754)------------------------------
% 43.19/6.79 % (1762754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.19/6.79 % (1762754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.19/6.79 % (1762754)CaDiCaL version: 2.1.3
% 43.19/6.79 % (1762754)Termination reason: Instruction limit
% 43.19/6.79 % (1762754)Termination phase: Saturation
% 43.19/6.79 % (1762754)Time elapsed: 0.055 s
% 43.19/6.79 % (1762754)Peak memory usage: 89 MB
% 43.19/6.79 % (1762754)Instructions burned: 107 (million)
% 43.19/6.79 % (1762755)Instruction limit reached!
% 43.19/6.79 % (1762755)------------------------------
% 43.19/6.79 % (1762755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.19/6.79 % (1762755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.19/6.79 % (1762755)CaDiCaL version: 2.1.3
% 43.19/6.79 % (1762755)Termination reason: Instruction limit
% 43.19/6.79 % (1762755)Termination phase: Saturation
% 43.19/6.79 % (1762755)Time elapsed: 0.073 s
% 43.19/6.79 % (1762755)Peak memory usage: 88 MB
% 43.19/6.79 % (1762755)Instructions burned: 108 (million)
% 43.19/6.79 % (1762756)Instruction limit reached!
% 43.19/6.79 % (1762756)------------------------------
% 43.19/6.79 % (1762756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.19/6.79 % (1762756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.19/6.79 % (1762756)CaDiCaL version: 2.1.3
% 43.19/6.79 % (1762756)Termination reason: Instruction limit
% 43.19/6.79 % (1762756)Termination phase: Saturation
% 43.19/6.79 % (1762756)Time elapsed: 0.089 s
% 43.19/6.79 % (1762756)Peak memory usage: 89 MB
% 43.19/6.79 % (1762756)Instructions burned: 244 (million)
% 43.19/6.79 % (1762761)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=850201838:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 43.19/6.79 % (1762762)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3005472812:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 43.19/6.79 % (1762763)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=958684867:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 43.19/6.79 % (1762762)Instruction limit reached!
% 43.19/6.79 % (1762762)------------------------------
% 43.19/6.79 % (1762762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.19/6.79 % (1762762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.19/6.79 % (1762762)CaDiCaL version: 2.1.3
% 43.19/6.79 % (1762762)Termination reason: Instruction limit
% 43.19/6.79 % (1762762)Termination phase: Saturation
% 43.19/6.79 % (1762762)Time elapsed: 0.050 s
% 43.19/6.79 % (1762762)Peak memory usage: 87 MB
% 43.19/6.79 % (1762762)Instructions burned: 136 (million)
% 43.19/6.79 % (1762767)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=247287217:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 43.19/6.79 % (1762767)Instruction limit reached!
% 43.19/6.79 % (1762767)------------------------------
% 43.19/6.79 % (1762767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.19/6.79 % (1762767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.19/6.79 % (1762767)CaDiCaL version: 2.1.3
% 43.19/6.79 % (1762767)Termination reason: Instruction limit
% 43.19/6.79 % (1762767)Termination phase: Saturation
% 43.19/6.79 % (1762767)Time elapsed: 0.102 s
% 43.19/6.79 % (1762767)Peak memory usage: 91 MB
% 43.19/6.79 % (1762767)Instructions burned: 193 (million)
% 43.19/6.79 % (1762763)Instruction limit reached!
% 43.19/6.79 % (1762763)------------------------------
% 43.19/6.79 % (1762763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.19/6.79 % (1762763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.19/6.79 % (1762763)CaDiCaL version: 2.1.3
% 43.19/6.79 % (1762763)Termination reason: Instruction limit
% 43.19/6.79 % (1762763)Termination phase: Saturation
% 43.19/6.79 % (1762763)Time elapsed: 0.263 s
% 43.19/6.79 % (1762763)Peak memory usage: 107 MB
% 43.19/6.79 % (1762763)Instructions burned: 500 (million)
% 43.19/6.79 % (1762769)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4046510050:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 43.19/6.79 % (1762770)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=702616619:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 55.46/8.52 % (1762769)Instruction limit reached!
% 55.46/8.52 % (1762769)------------------------------
% 55.46/8.52 % (1762769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.46/8.52 % (1762769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.46/8.52 % (1762769)CaDiCaL version: 2.1.3
% 55.46/8.52 % (1762769)Termination reason: Instruction limit
% 55.46/8.52 % (1762769)Termination phase: Saturation
% 55.46/8.52 % (1762769)Time elapsed: 0.090 s
% 55.46/8.52 % (1762769)Peak memory usage: 87 MB
% 55.46/8.52 % (1762769)Instructions burned: 266 (million)
% 55.46/8.52 % (1762770)Instruction limit reached!
% 55.46/8.52 % (1762770)------------------------------
% 55.46/8.52 % (1762770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.46/8.52 % (1762770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.46/8.52 % (1762770)CaDiCaL version: 2.1.3
% 55.46/8.52 % (1762770)Termination reason: Instruction limit
% 55.46/8.52 % (1762770)Termination phase: Saturation
% 55.46/8.52 % (1762770)Time elapsed: 0.064 s
% 55.46/8.52 % (1762770)Peak memory usage: 87 MB
% 55.46/8.52 % (1762770)Instructions burned: 156 (million)
% 55.46/8.52 % (1762773)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=2129637842:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 55.46/8.52 % (1762774)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=313362165:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 55.46/8.52 % (1762774)Instruction limit reached!
% 55.46/8.52 % (1762774)------------------------------
% 55.46/8.52 % (1762774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.46/8.52 % (1762774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.46/8.52 % (1762774)CaDiCaL version: 2.1.3
% 55.46/8.52 % (1762774)Termination reason: Instruction limit
% 55.46/8.52 % (1762774)Termination phase: Saturation
% 55.46/8.52 % (1762774)Time elapsed: 0.188 s
% 55.46/8.52 % (1762774)Peak memory usage: 87 MB
% 55.46/8.52 % (1762774)Instructions burned: 539 (million)
% 55.46/8.52 % (1762777)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2684915696:i=180:bd=preordered:av=off_2983 on theBenchmark for (2983ds/180Mi)
% 55.46/8.52 % (1762777)Instruction limit reached!
% 55.46/8.52 % (1762777)------------------------------
% 55.46/8.52 % (1762777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.46/8.52 % (1762777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.46/8.52 % (1762777)CaDiCaL version: 2.1.3
% 55.46/8.52 % (1762777)Termination reason: Instruction limit
% 55.46/8.52 % (1762777)Termination phase: Saturation
% 55.46/8.52 % (1762777)Time elapsed: 0.092 s
% 55.46/8.52 % (1762777)Peak memory usage: 93 MB
% 55.46/8.52 % (1762777)Instructions burned: 181 (million)
% 55.46/8.52 % (1762779)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=1130215595:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi)
% 55.46/8.52 % (1762752)Instruction limit reached!
% 55.46/8.52 % (1762752)------------------------------
% 55.46/8.52 % (1762752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.46/8.52 % (1762752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.46/8.52 % (1762752)CaDiCaL version: 2.1.3
% 55.46/8.52 % (1762752)Termination reason: Instruction limit
% 55.46/8.52 % (1762752)Termination phase: Saturation
% 55.46/8.52 % (1762752)Time elapsed: 2.150 s
% 55.46/8.52 % (1762752)Peak memory usage: 147 MB
% 55.46/8.52 % (1762752)Instructions burned: 3394 (million)
% 55.46/8.52 % (1762781)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=3816844442:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 55.46/8.52 % (1762781)Instruction limit reached!
% 55.46/8.52 % (1762781)------------------------------
% 55.46/8.52 % (1762781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.46/8.52 % (1762781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.46/8.52 % (1762781)CaDiCaL version: 2.1.3
% 55.46/8.52 % (1762781)Termination reason: Instruction limit
% 55.46/8.52 % (1762781)Termination phase: Saturation
% 81.77/12.16 % (1762781)Time elapsed: 0.212 s
% 81.77/12.16 % (1762781)Peak memory usage: 90 MB
% 81.77/12.16 % (1762781)Instructions burned: 413 (million)
% 81.77/12.16 % (1762783)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=1027319729:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi)
% 81.77/12.16 % (1762773)Instruction limit reached!
% 81.77/12.16 % (1762773)------------------------------
% 81.77/12.16 % (1762773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.77/12.16 % (1762773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.77/12.16 % (1762773)CaDiCaL version: 2.1.3
% 81.77/12.16 % (1762773)Termination reason: Instruction limit
% 81.77/12.16 % (1762773)Termination phase: Saturation
% 81.77/12.16 % (1762773)Time elapsed: 1.895 s
% 81.77/12.16 % (1762773)Peak memory usage: 143 MB
% 81.77/12.16 % (1762773)Instructions burned: 3257 (million)
% 81.77/12.16 % (1762785)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=1561661194:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2966 on theBenchmark for (2966ds/303Mi)
% 81.77/12.16 % (1762785)Instruction limit reached!
% 81.77/12.16 % (1762785)------------------------------
% 81.77/12.16 % (1762785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.77/12.16 % (1762785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.77/12.16 % (1762785)CaDiCaL version: 2.1.3
% 81.77/12.16 % (1762785)Termination reason: Instruction limit
% 81.77/12.16 % (1762785)Termination phase: Saturation
% 81.77/12.16 % (1762785)Time elapsed: 0.180 s
% 81.77/12.16 % (1762785)Peak memory usage: 90 MB
% 81.77/12.16 % (1762785)Instructions burned: 304 (million)
% 81.77/12.16 % (1762787)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4268353900:st=4:i=720:sd=3:fsr=off:ss=axioms_2963 on theBenchmark for (2963ds/720Mi)
% 81.77/12.16 % (1762761)Instruction limit reached!
% 81.77/12.16 % (1762761)------------------------------
% 81.77/12.16 % (1762761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.77/12.16 % (1762761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.77/12.16 % (1762761)CaDiCaL version: 2.1.3
% 81.77/12.16 % (1762761)Termination reason: Instruction limit
% 81.77/12.16 % (1762761)Termination phase: Saturation
% 81.77/12.16 % (1762761)Time elapsed: 3.328 s
% 81.77/12.16 % (1762761)Peak memory usage: 156 MB
% 81.77/12.16 % (1762761)Instructions burned: 5209 (million)
% 81.77/12.16 % (1762787)Instruction limit reached!
% 81.77/12.16 % (1762787)------------------------------
% 81.77/12.16 % (1762787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.77/12.16 % (1762787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.77/12.16 % (1762787)CaDiCaL version: 2.1.3
% 81.77/12.16 % (1762787)Termination reason: Instruction limit
% 81.77/12.16 % (1762787)Termination phase: Saturation
% 81.77/12.16 % (1762787)Time elapsed: 0.386 s
% 81.77/12.16 % (1762787)Peak memory usage: 93 MB
% 81.77/12.16 % (1762787)Instructions burned: 720 (million)
% 81.77/12.16 % (1762789)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=505169054:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 81.77/12.16 % (1762790)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3006385798:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi)
% 81.77/12.16 % (1762789)Instruction limit reached!
% 81.77/12.16 % (1762789)------------------------------
% 81.77/12.16 % (1762789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.77/12.16 % (1762789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.77/12.16 % (1762789)CaDiCaL version: 2.1.3
% 81.77/12.16 % (1762789)Termination reason: Instruction limit
% 81.77/12.16 % (1762789)Termination phase: Saturation
% 81.77/12.16 % (1762789)Time elapsed: 0.336 s
% 81.77/12.16 % (1762789)Peak memory usage: 89 MB
% 81.77/12.16 % (1762789)Instructions burned: 599 (million)
% 81.77/12.16 % (1762793)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1545379021:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2954 on theBenchmark for (2954ds/1997Mi)
% 81.77/12.16 % (1762793)Instruction limit reached!
% 81.77/12.16 % (1762793)------------------------------
% 119.10/17.42 % (1762793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.10/17.42 % (1762793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.10/17.42 % (1762793)CaDiCaL version: 2.1.3
% 119.10/17.42 % (1762793)Termination reason: Instruction limit
% 119.10/17.42 % (1762793)Termination phase: Saturation
% 119.10/17.42 % (1762793)Time elapsed: 1.442 s
% 119.10/17.42 % (1762793)Peak memory usage: 136 MB
% 119.10/17.42 % (1762793)Instructions burned: 1997 (million)
% 119.10/17.42 % (1762795)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=760177304:i=2088:bd=preordered:av=off_2938 on theBenchmark for (2938ds/2088Mi)
% 119.10/17.42 % (1762790)Instruction limit reached!
% 119.10/17.42 % (1762790)------------------------------
% 119.10/17.42 % (1762790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.10/17.42 % (1762790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.10/17.42 % (1762790)CaDiCaL version: 2.1.3
% 119.10/17.42 % (1762790)Termination reason: Instruction limit
% 119.10/17.42 % (1762790)Termination phase: Saturation
% 119.10/17.42 % (1762790)Time elapsed: 2.081 s
% 119.10/17.42 % (1762790)Peak memory usage: 142 MB
% 119.10/17.42 % (1762790)Instructions burned: 2989 (million)
% 119.10/17.42 % (1762797)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4031742451:i=1098:nicw=on_2936 on theBenchmark for (2936ds/1098Mi)
% 119.10/17.42 % (1762797)Instruction limit reached!
% 119.10/17.42 % (1762797)------------------------------
% 119.10/17.42 % (1762797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.10/17.42 % (1762797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.10/17.42 % (1762797)CaDiCaL version: 2.1.3
% 119.10/17.42 % (1762797)Termination reason: Instruction limit
% 119.10/17.42 % (1762797)Termination phase: Saturation
% 119.10/17.42 % (1762797)Time elapsed: 0.562 s
% 119.10/17.42 % (1762797)Peak memory usage: 120 MB
% 119.10/17.42 % (1762797)Instructions burned: 1099 (million)
% 119.10/17.42 % (1762799)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3717949059:i=433:bd=preordered_2929 on theBenchmark for (2929ds/433Mi)
% 119.10/17.42 % (1762799)Instruction limit reached!
% 119.10/17.42 % (1762799)------------------------------
% 119.10/17.42 % (1762799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.10/17.42 % (1762799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.10/17.42 % (1762799)CaDiCaL version: 2.1.3
% 119.10/17.42 % (1762799)Termination reason: Instruction limit
% 119.10/17.42 % (1762799)Termination phase: Saturation
% 119.10/17.42 % (1762799)Time elapsed: 0.249 s
% 119.10/17.42 % (1762799)Peak memory usage: 92 MB
% 119.10/17.42 % (1762799)Instructions burned: 433 (million)
% 119.10/17.42 % (1762801)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3181473761:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2925 on theBenchmark for (2925ds/2942Mi)
% 119.10/17.42 % (1762795)Instruction limit reached!
% 119.10/17.42 % (1762795)------------------------------
% 119.10/17.42 % (1762795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.10/17.42 % (1762795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.10/17.42 % (1762795)CaDiCaL version: 2.1.3
% 119.10/17.42 % (1762795)Termination reason: Instruction limit
% 119.10/17.42 % (1762795)Termination phase: Saturation
% 119.10/17.42 % (1762795)Time elapsed: 1.412 s
% 119.10/17.42 % (1762795)Peak memory usage: 136 MB
% 119.10/17.42 % (1762795)Instructions burned: 2088 (million)
% 119.10/17.42 % (1762803)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2500790572:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2923 on theBenchmark for (2923ds/6922Mi)
% 119.10/17.42 % (1762783)Instruction limit reached!
% 119.10/17.42 % (1762783)------------------------------
% 119.10/17.42 % (1762783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.10/17.42 % (1762783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.10/17.42 % (1762783)CaDiCaL version: 2.1.3
% 119.10/17.42 % (1762783)Termination reason: Instruction limit
% 119.10/17.42 % (1762783)Termination phase: Saturation
% 119.10/17.42 % (1762783)Time elapsed: 4.620 s
% 119.10/17.42 % (1762783)Peak memory usage: 181 MB
% 119.10/17.42 % (1762783)Instructions burned: 8480 (million)
% 129.89/20.55 % (1762805)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=440894624:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2921 on theBenchmark for (2921ds/596Mi)
% 129.89/20.55 % (1762805)Instruction limit reached!
% 129.89/20.55 % (1762805)------------------------------
% 129.89/20.55 % (1762805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.89/20.55 % (1762805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.89/20.55 % (1762805)CaDiCaL version: 2.1.3
% 129.89/20.55 % (1762805)Termination reason: Instruction limit
% 129.89/20.55 % (1762805)Termination phase: Saturation
% 129.89/20.55 % (1762805)Time elapsed: 0.295 s
% 129.89/20.55 % (1762805)Peak memory usage: 103 MB
% 129.89/20.55 % (1762805)Instructions burned: 596 (million)
% 129.89/20.55 % (1762807)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=425187968:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2916 on theBenchmark for (2916ds/4123Mi)
% 129.89/20.55 % (1762779)Instruction limit reached!
% 129.89/20.55 % (1762779)------------------------------
% 129.89/20.55 % (1762779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.89/20.55 % (1762779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.89/20.55 % (1762779)CaDiCaL version: 2.1.3
% 129.89/20.55 % (1762779)Termination reason: Instruction limit
% 129.89/20.55 % (1762779)Termination phase: Saturation
% 129.89/20.55 % (1762779)Time elapsed: 6.729 s
% 129.89/20.55 % (1762779)Peak memory usage: 187 MB
% 129.89/20.55 % (1762779)Instructions burned: 10308 (million)
% 129.89/20.55 % (1762809)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3007401703:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2912 on theBenchmark for (2912ds/16411Mi)
% 129.89/20.55 % (1762801)Instruction limit reached!
% 129.89/20.55 % (1762801)------------------------------
% 129.89/20.55 % (1762801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.89/20.55 % (1762801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.89/20.55 % (1762801)CaDiCaL version: 2.1.3
% 129.89/20.55 % (1762801)Termination reason: Instruction limit
% 129.89/20.55 % (1762801)Termination phase: Saturation
% 129.89/20.55 % (1762801)Time elapsed: 2.002 s
% 129.89/20.55 % (1762801)Peak memory usage: 141 MB
% 129.89/20.55 % (1762801)Instructions burned: 2942 (million)
% 129.89/20.55 % (1762811)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2578952672:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2904 on theBenchmark for (2904ds/1670Mi)
% 129.89/20.55 % (1762811)Instruction limit reached!
% 129.89/20.55 % (1762811)------------------------------
% 129.89/20.55 % (1762811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.89/20.55 % (1762811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.89/20.55 % (1762811)CaDiCaL version: 2.1.3
% 129.89/20.55 % (1762811)Termination reason: Instruction limit
% 129.89/20.55 % (1762811)Termination phase: Saturation
% 129.89/20.55 % (1762811)Time elapsed: 1.051 s
% 129.89/20.55 % (1762811)Peak memory usage: 134 MB
% 129.89/20.55 % (1762811)Instructions burned: 1670 (million)
% 129.89/20.55 % (1762813)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=34843306:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2892 on theBenchmark for (2892ds/1722Mi)
% 129.89/20.55 % (1762807)Instruction limit reached!
% 129.89/20.55 % (1762807)------------------------------
% 129.89/20.55 % (1762807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.89/20.55 % (1762807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.89/20.55 % (1762807)CaDiCaL version: 2.1.3
% 129.89/20.55 % (1762807)Termination reason: Instruction limit
% 129.89/20.55 % (1762807)Termination phase: Saturation
% 129.89/20.55 % (1762807)Time elapsed: 2.493 s
% 129.89/20.55 % (1762807)Peak memory usage: 155 MB
% 129.89/20.55 % (1762807)Instructions burned: 4123 (million)
% 129.89/20.55 % (1762815)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2097988583:cts=off:cond=on:i=9530:bs=on:fsd=on_2890 on theBenchmark for (2890ds/9530Mi)
% 129.89/20.55 % (1762803)Instruction limit reached!
% 128.96/21.86 % (1762803)------------------------------
% 128.96/21.86 % (1762803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762803)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762803)Termination reason: Instruction limit
% 128.96/21.86 % (1762803)Termination phase: Saturation
% 128.96/21.86 % (1762803)Time elapsed: 3.684 s
% 128.96/21.86 % (1762803)Peak memory usage: 206 MB
% 128.96/21.86 % (1762803)Instructions burned: 6923 (million)
% 128.96/21.86 % (1762817)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1506033851:st=2:i=4495:sd=10:ss=included_2884 on theBenchmark for (2884ds/4495Mi)
% 128.96/21.86 % (1762813)Instruction limit reached!
% 128.96/21.86 % (1762813)------------------------------
% 128.96/21.86 % (1762813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762813)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762813)Termination reason: Instruction limit
% 128.96/21.86 % (1762813)Termination phase: Saturation
% 128.96/21.86 % (1762813)Time elapsed: 1.197 s
% 128.96/21.86 % (1762813)Peak memory usage: 134 MB
% 128.96/21.86 % (1762813)Instructions burned: 1722 (million)
% 128.96/21.86 % (1762819)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1712621478:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2878 on theBenchmark for (2878ds/4920Mi)
% 128.96/21.86 % (1762817)Instruction limit reached!
% 128.96/21.86 % (1762817)------------------------------
% 128.96/21.86 % (1762817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762817)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762817)Termination reason: Instruction limit
% 128.96/21.86 % (1762817)Termination phase: Saturation
% 128.96/21.86 % (1762817)Time elapsed: 2.968 s
% 128.96/21.86 % (1762817)Peak memory usage: 148 MB
% 128.96/21.86 % (1762817)Instructions burned: 4496 (million)
% 128.96/21.86 % (1762821)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1166912352:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2853 on theBenchmark for (2853ds/2083Mi)
% 128.96/21.86 % (1762819)Instruction limit reached!
% 128.96/21.86 % (1762819)------------------------------
% 128.96/21.86 % (1762819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762819)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762819)Termination reason: Instruction limit
% 128.96/21.86 % (1762819)Termination phase: Saturation
% 128.96/21.86 % (1762819)Time elapsed: 3.117 s
% 128.96/21.86 % (1762819)Peak memory usage: 146 MB
% 128.96/21.86 % (1762819)Instructions burned: 4921 (million)
% 128.96/21.86 % (1762823)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2667518326:i=4629:av=off:gsp=on_2846 on theBenchmark for (2846ds/4629Mi)
% 128.96/21.86 % (1762821)Instruction limit reached!
% 128.96/21.86 % (1762821)------------------------------
% 128.96/21.86 % (1762821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762821)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762821)Termination reason: Instruction limit
% 128.96/21.86 % (1762821)Termination phase: Saturation
% 128.96/21.86 % (1762821)Time elapsed: 1.353 s
% 128.96/21.86 % (1762821)Peak memory usage: 136 MB
% 128.96/21.86 % (1762821)Instructions burned: 2084 (million)
% 128.96/21.86 % (1762825)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3083325662:i=1258:av=off_2838 on theBenchmark for (2838ds/1258Mi)
% 128.96/21.86 % (1762815)Instruction limit reached!
% 128.96/21.86 % (1762815)------------------------------
% 128.96/21.86 % (1762815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762815)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762815)Termination reason: Instruction limit
% 128.96/21.86 % (1762815)Termination phase: Saturation
% 128.96/21.86 % (1762815)Time elapsed: 5.697 s
% 128.96/21.86 % (1762815)Peak memory usage: 149 MB
% 128.96/21.86 % (1762815)Instructions burned: 9530 (million)
% 128.96/21.86 % (1762827)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3248235215:i=7343:av=off:ss=included_2832 on theBenchmark for (2832ds/7343Mi)
% 128.96/21.86 % (1762825)Instruction limit reached!
% 128.96/21.86 % (1762825)------------------------------
% 128.96/21.86 % (1762825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762825)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762825)Termination reason: Instruction limit
% 128.96/21.86 % (1762825)Termination phase: Saturation
% 128.96/21.86 % (1762825)Time elapsed: 0.724 s
% 128.96/21.86 % (1762825)Peak memory usage: 93 MB
% 128.96/21.86 % (1762825)Instructions burned: 1259 (million)
% 128.96/21.86 % (1762829)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2227517999:i=1325:sd=2:ss=axioms:sgt=16_2830 on theBenchmark for (2830ds/1325Mi)
% 128.96/21.86 % (1762829)Instruction limit reached!
% 128.96/21.86 % (1762829)------------------------------
% 128.96/21.86 % (1762829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762829)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762829)Termination reason: Instruction limit
% 128.96/21.86 % (1762829)Termination phase: Saturation
% 128.96/21.86 % (1762829)Time elapsed: 0.749 s
% 128.96/21.86 % (1762829)Peak memory usage: 91 MB
% 128.96/21.86 % (1762829)Instructions burned: 1325 (million)
% 128.96/21.86 % (1762831)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=810079195:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2821 on theBenchmark for (2821ds/2646Mi)
% 128.96/21.86 % (1762823)Instruction limit reached!
% 128.96/21.86 % (1762823)------------------------------
% 128.96/21.86 % (1762823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762823)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762823)Termination reason: Instruction limit
% 128.96/21.86 % (1762823)Termination phase: Saturation
% 128.96/21.86 % (1762823)Time elapsed: 2.484 s
% 128.96/21.86 % (1762823)Peak memory usage: 141 MB
% 128.96/21.86 % (1762823)Instructions burned: 4631 (million)
% 128.96/21.86 % (1762833)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2418204740:i=1489:sd=2:ep=R:ss=axioms_2820 on theBenchmark for (2820ds/1489Mi)
% 128.96/21.86 % (1762833)Instruction limit reached!
% 128.96/21.86 % (1762833)------------------------------
% 128.96/21.86 % (1762833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762833)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762833)Termination reason: Instruction limit
% 128.96/21.86 % (1762833)Termination phase: Saturation
% 128.96/21.86 % (1762833)Time elapsed: 0.955 s
% 128.96/21.86 % (1762833)Peak memory usage: 133 MB
% 128.96/21.86 % (1762833)Instructions burned: 1489 (million)
% 128.96/21.86 % (1762835)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=1345132735:i=1503_2809 on theBenchmark for (2809ds/1503Mi)
% 128.96/21.86 % (1762809)Instruction limit reached!
% 128.96/21.86 % (1762809)------------------------------
% 128.96/21.86 % (1762809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762809)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762809)Termination reason: Instruction limit
% 128.96/21.86 % (1762809)Termination phase: Saturation
% 128.96/21.86 % (1762809)Time elapsed: 10.943 s
% 128.96/21.86 % (1762809)Peak memory usage: 274 MB
% 128.96/21.86 % (1762809)Instructions burned: 16412 (million)
% 128.96/21.86 % (1762831)Instruction limit reached!
% 128.96/21.86 % (1762831)------------------------------
% 128.96/21.86 % (1762831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762831)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762831)Termination reason: Instruction limit
% 128.96/21.86 % (1762831)Termination phase: Saturation
% 128.96/21.86 % (1762831)Time elapsed: 1.917 s
% 128.96/21.86 % (1762831)Peak memory usage: 140 MB
% 128.96/21.86 % (1762831)Instructions burned: 2646 (million)
% 128.96/21.86 % (1762837)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3432852408:i=13942:kws=frequency_2801 on theBenchmark for (2801ds/13942Mi)
% 128.96/21.86 % (1762838)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2536514807:i=3604:fsr=off:er=filter_2801 on theBenchmark for (2801ds/3604Mi)
% 128.96/21.86 % (1762835)Instruction limit reached!
% 128.96/21.86 % (1762835)------------------------------
% 128.96/21.86 % (1762835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.96/21.86 % (1762835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.96/21.86 % (1762835)CaDiCaL version: 2.1.3
% 128.96/21.86 % (1762835)Termination reason: Instruction limit
% 128.96/21.86 % (1762835)Termination phase: Saturation
% 128.96/21.86 % (1762835)Time elapsed: 0.956 s
% 128.96/21.86 % (1762835)Peak memory usage: 132 MB
% 128.96/21.86 % (1762835)Instructions burned: 1505 (million)
% 128.96/21.86 % (1762841)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2859233510:i=1876:sd=1:ss=included:sgt=32_2798 on theBenchmark for (2798ds/1876Mi)
% 128.96/21.86 % (1762728)First to succeed.
% 128.96/21.86 % (1762728)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1762722"
% 128.96/21.86 % (1762728)Refutation found. Thanks to Tanya!
% 128.96/21.86 % SZS status Unsatisfiable for theBenchmark
% 128.96/21.86 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/22.03 % (1762728)------------------------------
% 0.20/22.03 % (1762728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/22.03 % (1762728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/22.03 % (1762728)CaDiCaL version: 2.1.3
% 0.20/22.03 % (1762728)Termination reason: Refutation
% 0.20/22.03 % (1762728)Time elapsed: 20.816 s
% 0.20/22.03 % (1762728)Peak memory usage: 654 MB
% 0.20/22.03 % (1762728)Instructions burned: 70298 (million)
% 0.20/22.03 % (1762728)------------------------------
% 0.20/22.03 % (1762728)------------------------------
% 0.20/22.03 % (1762722)Success in time 21.196 s
% 0.20/22.03 % Vampire exiting
%------------------------------------------------------------------------------