%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : FLD073-4 : 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 : n010.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:22 AM UTC 2026
% Result : Unsatisfiable 108.62s 29.83s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 23
% Syntax : Number of formulae : 130 ( 101 unt; 0 def)
% Number of atoms : 196 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 135 ( 69 ~; 66 |; 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; 5 con; 0-2 aty)
% Number of variables : 90 ( 90 !; 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(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(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(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,axiom,
defined(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_is_defined) ).
fof(f29,axiom,
defined(u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_is_defined) ).
fof(f30,negated_conjecture,
less_or_equal(a,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal_4) ).
fof(f31,negated_conjecture,
less_or_equal(b,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal_5) ).
fof(f32,negated_conjecture,
product(a,b,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_6) ).
fof(f33,negated_conjecture,
~ less_or_equal(additive_identity,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_less_or_equal_7) ).
fof(f41,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,a)
| ~ product(X1,b,X2)
| product(X0,X2,u) ),
inference(resolution,[],[f32,f6]) ).
fof(f43,plain,
product(b,a,u),
inference(resolution,[],[f32,f10]) ).
fof(f44,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,a)
| sum(X2,X3,u)
| ~ product(X0,b,X2)
| ~ product(X1,b,X3) ),
inference(resolution,[],[f32,f11]) ).
fof(f45,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,a,X1)
| ~ product(X0,b,X2)
| product(X1,b,X3)
| ~ sum(X2,u,X3) ),
inference(resolution,[],[f32,f12]) ).
fof(f50,plain,
sum(additive_identity,u,u),
inference(unit_resulting_resolution,[],[f3,f29]) ).
fof(f51,plain,
sum(additive_inverse(u),u,additive_identity),
inference(unit_resulting_resolution,[],[f4,f29]) ).
fof(f52,plain,
product(multiplicative_identity,u,u),
inference(unit_resulting_resolution,[],[f8,f29]) ).
fof(f53,plain,
defined(additive_inverse(u)),
inference(unit_resulting_resolution,[],[f15,f29]) ).
fof(f68,plain,
sum(additive_identity,b,b),
inference(unit_resulting_resolution,[],[f3,f28]) ).
fof(f69,plain,
sum(additive_inverse(b),b,additive_identity),
inference(unit_resulting_resolution,[],[f4,f28]) ).
fof(f70,plain,
product(multiplicative_identity,b,b),
inference(unit_resulting_resolution,[],[f8,f28]) ).
fof(f71,plain,
defined(additive_inverse(b)),
inference(unit_resulting_resolution,[],[f15,f28]) ).
fof(f84,plain,
product(additive_identity,b,multiply(additive_identity,b)),
inference(unit_resulting_resolution,[],[f20,f14,f28]) ).
fof(f89,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,b)
| ~ product(X1,a,X2)
| product(X0,X2,u) ),
inference(resolution,[],[f43,f6]) ).
fof(f92,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,b)
| sum(X2,X3,u)
| ~ product(X0,a,X2)
| ~ product(X1,a,X3) ),
inference(resolution,[],[f43,f11]) ).
fof(f93,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,b,X1)
| ~ product(X0,a,X2)
| product(X1,a,X3)
| ~ sum(X2,u,X3) ),
inference(resolution,[],[f43,f12]) ).
fof(f95,plain,
sum(additive_identity,a,a),
inference(unit_resulting_resolution,[],[f3,f27]) ).
fof(f96,plain,
sum(additive_inverse(a),a,additive_identity),
inference(unit_resulting_resolution,[],[f4,f27]) ).
fof(f97,plain,
product(multiplicative_identity,a,a),
inference(unit_resulting_resolution,[],[f8,f27]) ).
fof(f98,plain,
defined(additive_inverse(a)),
inference(unit_resulting_resolution,[],[f15,f27]) ).
fof(f112,plain,
product(a,b,multiply(a,b)),
inference(unit_resulting_resolution,[],[f20,f28,f27]) ).
fof(f114,plain,
product(additive_identity,a,multiply(additive_identity,a)),
inference(unit_resulting_resolution,[],[f20,f14,f27]) ).
fof(f122,plain,
sum(u,additive_inverse(u),additive_identity),
inference(resolution,[],[f51,f5]) ).
fof(f125,plain,
~ less_or_equal(additive_inverse(u),additive_identity),
inference(unit_resulting_resolution,[],[f24,f33,f51,f50]) ).
fof(f130,plain,
sum(u,additive_identity,u),
inference(resolution,[],[f50,f5]) ).
fof(f135,plain,
sum(b,additive_identity,b),
inference(resolution,[],[f68,f5]) ).
fof(f140,plain,
sum(a,additive_identity,a),
inference(resolution,[],[f95,f5]) ).
fof(f145,plain,
sum(b,additive_inverse(b),additive_identity),
inference(resolution,[],[f69,f5]) ).
fof(f150,plain,
sum(a,additive_inverse(a),additive_identity),
inference(resolution,[],[f96,f5]) ).
fof(f155,plain,
product(u,multiplicative_identity,u),
inference(resolution,[],[f52,f10]) ).
fof(f164,plain,
product(b,multiplicative_identity,b),
inference(resolution,[],[f70,f10]) ).
fof(f173,plain,
product(a,multiplicative_identity,a),
inference(resolution,[],[f97,f10]) ).
fof(f324,plain,
sum(additive_identity,additive_inverse(b),additive_inverse(b)),
inference(unit_resulting_resolution,[],[f3,f71]) ).
fof(f325,plain,
sum(additive_inverse(additive_inverse(b)),additive_inverse(b),additive_identity),
inference(unit_resulting_resolution,[],[f4,f71]) ).
fof(f327,plain,
defined(additive_inverse(additive_inverse(b))),
inference(unit_resulting_resolution,[],[f15,f71]) ).
fof(f346,plain,
product(additive_identity,additive_inverse(b),multiply(additive_identity,additive_inverse(b))),
inference(unit_resulting_resolution,[],[f20,f14,f71]) ).
fof(f349,plain,
product(a,additive_inverse(b),multiply(a,additive_inverse(b))),
inference(unit_resulting_resolution,[],[f20,f27,f71]) ).
fof(f352,plain,
sum(additive_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f3,f98]) ).
fof(f353,plain,
sum(additive_inverse(additive_inverse(a)),additive_inverse(a),additive_identity),
inference(unit_resulting_resolution,[],[f4,f98]) ).
fof(f354,plain,
product(multiplicative_identity,additive_inverse(a),additive_inverse(a)),
inference(unit_resulting_resolution,[],[f8,f98]) ).
fof(f355,plain,
defined(additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f15,f98]) ).
fof(f371,plain,
product(additive_inverse(a),additive_inverse(b),multiply(additive_inverse(a),additive_inverse(b))),
inference(unit_resulting_resolution,[],[f20,f71,f98]) ).
fof(f382,plain,
product(b,additive_inverse(a),multiply(b,additive_inverse(a))),
inference(unit_resulting_resolution,[],[f20,f28,f98]) ).
fof(f497,plain,
product(additive_inverse(a),b,multiply(b,additive_inverse(a))),
inference(resolution,[],[f382,f10]) ).
fof(f516,plain,
less_or_equal(additive_identity,additive_inverse(a)),
inference(unit_resulting_resolution,[],[f24,f30,f150,f352]) ).
fof(f567,plain,
less_or_equal(additive_identity,additive_inverse(b)),
inference(unit_resulting_resolution,[],[f24,f31,f145,f324]) ).
fof(f614,plain,
product(additive_inverse(b),a,multiply(a,additive_inverse(b))),
inference(resolution,[],[f349,f10]) ).
fof(f699,plain,
sum(additive_identity,additive_inverse(u),additive_inverse(u)),
inference(unit_resulting_resolution,[],[f3,f53]) ).
fof(f700,plain,
sum(additive_inverse(additive_inverse(u)),additive_inverse(u),additive_identity),
inference(unit_resulting_resolution,[],[f4,f53]) ).
fof(f702,plain,
defined(additive_inverse(additive_inverse(u))),
inference(unit_resulting_resolution,[],[f15,f53]) ).
fof(f763,plain,
sum(additive_inverse(u),additive_identity,additive_inverse(u)),
inference(resolution,[],[f699,f5]) ).
fof(f821,plain,
product(additive_inverse(a),multiplicative_identity,additive_inverse(a)),
inference(resolution,[],[f354,f10]) ).
fof(f881,plain,
product(multiply(a,b),multiplicative_identity,u),
inference(unit_resulting_resolution,[],[f7,f32,f164,f112]) ).
fof(f884,plain,
product(u,multiplicative_identity,multiply(a,b)),
inference(unit_resulting_resolution,[],[f7,f164,f32,f112]) ).
fof(f1025,plain,
! [X0,X1] :
( ~ product(additive_identity,b,X0)
| sum(X0,X1,u)
| ~ product(a,b,X1) ),
inference(resolution,[],[f44,f95]) ).
fof(f1048,plain,
sum(additive_inverse(b),additive_inverse(additive_inverse(b)),additive_identity),
inference(resolution,[],[f325,f5]) ).
fof(f1056,plain,
sum(additive_inverse(a),additive_inverse(additive_inverse(a)),additive_identity),
inference(resolution,[],[f353,f5]) ).
fof(f1099,plain,
sum(additive_inverse(u),additive_inverse(additive_inverse(u)),additive_identity),
inference(resolution,[],[f700,f5]) ).
fof(f1196,plain,
! [X0,X1] :
( ~ product(additive_identity,a,X1)
| ~ product(b,a,X0)
| sum(X0,X1,u) ),
inference(resolution,[],[f92,f135]) ).
fof(f1198,plain,
! [X0] :
( ~ product(b,a,X0)
| sum(X0,multiply(additive_identity,a),u)
| ~ defined(additive_identity)
| ~ defined(a) ),
inference(resolution,[],[f1196,f20]) ).
fof(f1199,plain,
! [X0] :
( ~ product(b,a,X0)
| sum(X0,multiply(additive_identity,a),u)
| ~ defined(a) ),
inference(forward_subsumption_resolution,[],[f1198,f14]) ).
fof(f1200,plain,
! [X0] :
( ~ product(b,a,X0)
| sum(X0,multiply(additive_identity,a),u) ),
inference(forward_subsumption_resolution,[],[f1199,f27]) ).
fof(f1457,plain,
! [X0] :
( sum(multiply(additive_identity,b),X0,u)
| ~ product(a,b,X0)
| ~ defined(additive_identity)
| ~ defined(b) ),
inference(resolution,[],[f1025,f20]) ).
fof(f1458,plain,
! [X0] :
( sum(multiply(additive_identity,b),X0,u)
| ~ product(a,b,X0)
| ~ defined(b) ),
inference(forward_subsumption_resolution,[],[f1457,f14]) ).
fof(f1459,plain,
! [X0] :
( ~ product(a,b,X0)
| sum(multiply(additive_identity,b),X0,u) ),
inference(forward_subsumption_resolution,[],[f1458,f28]) ).
fof(f1578,plain,
product(additive_identity,multiplicative_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f96,f173,f96,f821]) ).
fof(f1669,plain,
product(multiplicative_identity,additive_identity,additive_identity),
inference(resolution,[],[f1578,f10]) ).
fof(f1925,plain,
less_or_equal(additive_identity,multiply(additive_inverse(a),additive_inverse(b))),
inference(unit_resulting_resolution,[],[f25,f516,f567,f371]) ).
fof(f1961,plain,
~ sum(multiply(additive_inverse(a),additive_inverse(b)),additive_inverse(u),additive_identity),
inference(unit_resulting_resolution,[],[f24,f125,f699,f1925]) ).
fof(f2865,plain,
product(additive_inverse(b),additive_identity,multiply(additive_identity,additive_inverse(b))),
inference(resolution,[],[f346,f10]) ).
fof(f3685,plain,
sum(multiply(additive_identity,b),u,u),
inference(resolution,[],[f1459,f32]) ).
fof(f3693,plain,
sum(multiply(additive_identity,b),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f122,f122,f3685]) ).
fof(f3943,plain,
sum(additive_identity,additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f3,f355]) ).
fof(f3983,plain,
sum(additive_identity,additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b))),
inference(unit_resulting_resolution,[],[f3,f327]) ).
fof(f4051,plain,
sum(b,additive_identity,additive_inverse(additive_inverse(b))),
inference(unit_resulting_resolution,[],[f1,f145,f1048,f3983]) ).
fof(f4165,plain,
product(additive_inverse(additive_inverse(b)),multiplicative_identity,b),
inference(unit_resulting_resolution,[],[f12,f135,f1578,f164,f4051]) ).
fof(f4179,plain,
product(additive_inverse(additive_inverse(b)),a,u),
inference(unit_resulting_resolution,[],[f89,f97,f4165]) ).
fof(f4378,plain,
sum(a,additive_identity,additive_inverse(additive_inverse(a))),
inference(unit_resulting_resolution,[],[f1,f150,f1056,f3943]) ).
fof(f4489,plain,
product(additive_inverse(additive_inverse(a)),multiplicative_identity,a),
inference(unit_resulting_resolution,[],[f12,f140,f1578,f173,f4378]) ).
fof(f4503,plain,
product(additive_inverse(additive_inverse(a)),b,u),
inference(unit_resulting_resolution,[],[f41,f70,f4489]) ).
fof(f5170,plain,
sum(u,multiply(additive_identity,a),u),
inference(resolution,[],[f1200,f43]) ).
fof(f5205,plain,
sum(multiply(additive_identity,a),u,u),
inference(resolution,[],[f5170,f5]) ).
fof(f5216,plain,
sum(multiply(additive_identity,a),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f1,f122,f122,f5205]) ).
fof(f5405,plain,
sum(multiply(b,additive_inverse(a)),u,multiply(additive_identity,b)),
inference(unit_resulting_resolution,[],[f11,f497,f4503,f1056,f84]) ).
fof(f5538,plain,
sum(multiply(a,additive_inverse(b)),u,multiply(additive_identity,a)),
inference(unit_resulting_resolution,[],[f11,f614,f4179,f1048,f114]) ).
fof(f5619,plain,
sum(multiply(a,additive_inverse(b)),u,additive_identity),
inference(unit_resulting_resolution,[],[f1,f130,f5216,f5538]) ).
fof(f5765,plain,
sum(multiply(a,b),additive_identity,u),
inference(unit_resulting_resolution,[],[f11,f1578,f155,f130,f884]) ).
fof(f6303,plain,
sum(multiply(b,additive_inverse(a)),u,additive_identity),
inference(unit_resulting_resolution,[],[f1,f130,f3693,f5405]) ).
fof(f10140,plain,
sum(additive_identity,additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u))),
inference(unit_resulting_resolution,[],[f3,f702]) ).
fof(f11128,plain,
sum(u,additive_identity,additive_inverse(additive_inverse(u))),
inference(unit_resulting_resolution,[],[f1,f122,f1099,f10140]) ).
fof(f11291,plain,
product(u,multiplicative_identity,additive_inverse(additive_inverse(u))),
inference(unit_resulting_resolution,[],[f12,f1578,f5765,f881,f11128]) ).
fof(f11588,plain,
product(b,a,additive_inverse(additive_inverse(u))),
inference(unit_resulting_resolution,[],[f6,f43,f173,f11291]) ).
fof(f12661,plain,
product(additive_identity,a,additive_identity),
inference(unit_resulting_resolution,[],[f93,f69,f614,f5619]) ).
fof(f12915,plain,
sum(additive_inverse(additive_inverse(u)),multiply(a,additive_inverse(b)),additive_identity),
inference(unit_resulting_resolution,[],[f11,f11588,f614,f145,f12661]) ).
fof(f13507,plain,
sum(additive_identity,multiply(a,additive_inverse(b)),additive_inverse(u)),
inference(unit_resulting_resolution,[],[f2,f763,f1099,f12915]) ).
fof(f13652,plain,
product(additive_inverse(b),a,additive_inverse(u)),
inference(unit_resulting_resolution,[],[f12,f324,f12661,f614,f13507]) ).
fof(f13929,plain,
product(a,additive_inverse(b),additive_inverse(u)),
inference(resolution,[],[f13652,f10]) ).
fof(f14020,plain,
sum(additive_inverse(u),multiply(additive_identity,additive_inverse(b)),additive_inverse(u)),
inference(unit_resulting_resolution,[],[f11,f346,f140,f13929,f13929]) ).
fof(f21932,plain,
product(additive_identity,b,additive_identity),
inference(unit_resulting_resolution,[],[f45,f96,f497,f6303]) ).
fof(f22764,plain,
product(b,additive_identity,additive_identity),
inference(resolution,[],[f21932,f10]) ).
fof(f23185,plain,
product(additive_inverse(additive_inverse(b)),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f6,f1669,f4165,f22764]) ).
fof(f35263,plain,
sum(additive_identity,multiply(additive_identity,additive_inverse(b)),additive_identity),
inference(unit_resulting_resolution,[],[f2,f700,f700,f14020]) ).
fof(f35611,plain,
product(additive_identity,additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f325,f23185,f2865,f35263]) ).
fof(f36530,plain,
product(additive_inverse(b),additive_identity,additive_identity),
inference(unit_resulting_resolution,[],[f12,f35263,f2865,f324,f35611]) ).
fof(f37010,plain,
product(additive_identity,additive_inverse(b),additive_identity),
inference(resolution,[],[f36530,f10]) ).
fof(f37687,plain,
sum(multiply(additive_inverse(a),additive_inverse(b)),additive_inverse(u),additive_identity),
inference(unit_resulting_resolution,[],[f11,f13929,f96,f371,f37010]) ).
fof(f37950,plain,
$false,
inference(forward_subsumption_resolution,[],[f37687,f1961]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD073-4 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n010.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 00:53:03 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/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
% 6.50/1.76 % (2522243)Input is clausal, will run a generic CNF schedule.
% 6.50/1.76 % (2522252)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2773125722:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.50/1.76 % (2522253)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1153246059:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.50/1.76 % (2522251)lrs+10_1_sil=8000:sp=occurrence:random_seed=1630789551:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.50/1.76 % (2522254)dis-21_1_sil=8000:lcm=predicate:random_seed=1569568697: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)
% 6.50/1.76 % (2522248)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=1450353208:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.50/1.76 % (2522249)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3075009035:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.50/1.76 % (2522250)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1542934317:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.50/1.76 % (2522252)Instruction limit reached!
% 6.50/1.76 % (2522252)------------------------------
% 6.50/1.76 % (2522252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.50/1.76 % (2522252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.76 % (2522252)CaDiCaL version: 2.1.3
% 6.50/1.76 % (2522252)Termination reason: Instruction limit
% 6.50/1.76 % (2522252)Termination phase: Saturation
% 6.50/1.76 % (2522252)Time elapsed: 0.034 s
% 6.50/1.76 % (2522252)Peak memory usage: 88 MB
% 6.50/1.76 % (2522252)Instructions burned: 118 (million)
% 6.50/1.76 % (2522251)Instruction limit reached!
% 6.50/1.76 % (2522251)------------------------------
% 6.50/1.76 % (2522251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.50/1.76 % (2522251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.76 % (2522251)CaDiCaL version: 2.1.3
% 6.50/1.76 % (2522251)Termination reason: Instruction limit
% 6.50/1.76 % (2522251)Termination phase: Saturation
% 6.50/1.76 % (2522251)Time elapsed: 0.051 s
% 6.50/1.76 % (2522251)Peak memory usage: 87 MB
% 6.50/1.76 % (2522251)Instructions burned: 108 (million)
% 6.50/1.76 % (2522254)Instruction limit reached!
% 6.50/1.76 % (2522254)------------------------------
% 6.50/1.76 % (2522254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.50/1.76 % (2522254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.76 % (2522254)CaDiCaL version: 2.1.3
% 6.50/1.76 % (2522254)Termination reason: Instruction limit
% 6.50/1.76 % (2522254)Termination phase: Saturation
% 6.50/1.76 % (2522254)Time elapsed: 0.059 s
% 6.50/1.76 % (2522254)Peak memory usage: 88 MB
% 6.50/1.76 % (2522254)Instructions burned: 119 (million)
% 6.50/1.76 % (2522262)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=211013573:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.50/1.76 % (2522253)Instruction limit reached!
% 6.50/1.76 % (2522253)------------------------------
% 6.50/1.76 % (2522253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.50/1.76 % (2522253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.76 % (2522253)CaDiCaL version: 2.1.3
% 6.50/1.76 % (2522253)Termination reason: Instruction limit
% 6.50/1.76 % (2522253)Termination phase: Saturation
% 6.50/1.76 % (2522253)Time elapsed: 0.116 s
% 6.50/1.76 % (2522253)Peak memory usage: 89 MB
% 6.50/1.76 % (2522253)Instructions burned: 181 (million)
% 6.50/1.76 % (2522262)Instruction limit reached!
% 6.50/1.76 % (2522262)------------------------------
% 6.50/1.76 % (2522262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.50/1.76 % (2522262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.76 % (2522262)CaDiCaL version: 2.1.3
% 6.50/1.76 % (2522262)Termination reason: Instruction limit
% 6.50/1.76 % (2522262)Termination phase: Saturation
% 6.50/1.76 % (2522262)Time elapsed: 0.036 s
% 6.50/1.76 % (2522262)Peak memory usage: 88 MB
% 6.50/1.76 % (2522262)Instructions burned: 148 (million)
% 6.50/1.76 % (2522263)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=312188540:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 20.96/3.65 % (2522264)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=316741262:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.96/3.65 % (2522267)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3350079156:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 20.96/3.65 % (2522266)lrs+10_64_to=lpo:sil=8000:random_seed=3193979224:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 20.96/3.65 % (2522267)Instruction limit reached!
% 20.96/3.65 % (2522267)------------------------------
% 20.96/3.65 % (2522267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.96/3.65 % (2522267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.96/3.65 % (2522267)CaDiCaL version: 2.1.3
% 20.96/3.65 % (2522267)Termination reason: Instruction limit
% 20.96/3.65 % (2522267)Termination phase: Saturation
% 20.96/3.65 % (2522267)Time elapsed: 0.037 s
% 20.96/3.65 % (2522267)Peak memory usage: 87 MB
% 20.96/3.65 % (2522267)Instructions burned: 200 (million)
% 20.96/3.65 % (2522263)Instruction limit reached!
% 20.96/3.65 % (2522263)------------------------------
% 20.96/3.65 % (2522263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.96/3.65 % (2522263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.96/3.65 % (2522263)CaDiCaL version: 2.1.3
% 20.96/3.65 % (2522263)Termination reason: Instruction limit
% 20.96/3.65 % (2522263)Termination phase: Saturation
% 20.96/3.65 % (2522263)Time elapsed: 0.094 s
% 20.96/3.65 % (2522263)Peak memory usage: 93 MB
% 20.96/3.65 % (2522263)Instructions burned: 191 (million)
% 20.96/3.65 % (2522266)Instruction limit reached!
% 20.96/3.65 % (2522266)------------------------------
% 20.96/3.65 % (2522266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.96/3.65 % (2522266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.96/3.65 % (2522266)CaDiCaL version: 2.1.3
% 20.96/3.65 % (2522266)Termination reason: Instruction limit
% 20.96/3.65 % (2522266)Termination phase: Saturation
% 20.96/3.65 % (2522266)Time elapsed: 0.056 s
% 20.96/3.65 % (2522266)Peak memory usage: 87 MB
% 20.96/3.65 % (2522266)Instructions burned: 128 (million)
% 20.96/3.65 % (2522264)Instruction limit reached!
% 20.96/3.65 % (2522264)------------------------------
% 20.96/3.65 % (2522264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.96/3.65 % (2522264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.96/3.65 % (2522264)CaDiCaL version: 2.1.3
% 20.96/3.65 % (2522264)Termination reason: Instruction limit
% 20.96/3.65 % (2522264)Termination phase: Saturation
% 20.96/3.65 % (2522264)Time elapsed: 0.132 s
% 20.96/3.65 % (2522264)Peak memory usage: 89 MB
% 20.96/3.65 % (2522264)Instructions burned: 219 (million)
% 20.96/3.65 % (2522272)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=689838682:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 20.96/3.65 % (2522273)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3897165442:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 20.96/3.65 % (2522272)Instruction limit reached!
% 20.96/3.65 % (2522272)------------------------------
% 20.96/3.65 % (2522272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.96/3.65 % (2522272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.96/3.65 % (2522272)CaDiCaL version: 2.1.3
% 20.96/3.65 % (2522272)Termination reason: Instruction limit
% 20.96/3.65 % (2522272)Termination phase: Saturation
% 20.96/3.65 % (2522272)Time elapsed: 0.056 s
% 20.96/3.65 % (2522272)Peak memory usage: 90 MB
% 20.96/3.65 % (2522272)Instructions burned: 160 (million)
% 20.96/3.65 % (2522274)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=3728719958:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 20.96/3.65 % (2522275)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3558920083:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 20.96/3.65 % (2522274)Instruction limit reached!
% 20.96/3.65 % (2522274)------------------------------
% 20.96/3.65 % (2522274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.32/5.53 % (2522274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.32/5.53 % (2522274)CaDiCaL version: 2.1.3
% 34.32/5.53 % (2522274)Termination reason: Instruction limit
% 34.32/5.53 % (2522274)Termination phase: Saturation
% 34.32/5.53 % (2522274)Time elapsed: 0.056 s
% 34.32/5.53 % (2522274)Peak memory usage: 90 MB
% 34.32/5.53 % (2522274)Instructions burned: 107 (million)
% 34.32/5.53 % (2522278)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=5090354:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 34.32/5.53 % (2522275)Instruction limit reached!
% 34.32/5.53 % (2522275)------------------------------
% 34.32/5.53 % (2522275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.32/5.53 % (2522275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.32/5.53 % (2522275)CaDiCaL version: 2.1.3
% 34.32/5.53 % (2522275)Termination reason: Instruction limit
% 34.32/5.53 % (2522275)Termination phase: Saturation
% 34.32/5.53 % (2522275)Time elapsed: 0.070 s
% 34.32/5.53 % (2522275)Peak memory usage: 88 MB
% 34.32/5.53 % (2522275)Instructions burned: 108 (million)
% 34.32/5.53 % (2522278)Instruction limit reached!
% 34.32/5.53 % (2522278)------------------------------
% 34.32/5.53 % (2522278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.32/5.53 % (2522278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.32/5.53 % (2522278)CaDiCaL version: 2.1.3
% 34.32/5.53 % (2522278)Termination reason: Instruction limit
% 34.32/5.53 % (2522278)Termination phase: Saturation
% 34.32/5.53 % (2522278)Time elapsed: 0.078 s
% 34.32/5.53 % (2522278)Peak memory usage: 89 MB
% 34.32/5.53 % (2522278)Instructions burned: 243 (million)
% 34.32/5.53 % (2522281)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4086351104:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 34.32/5.53 % (2522283)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1668639990:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 34.32/5.53 % (2522284)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2342751912:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 34.32/5.53 % (2522283)Instruction limit reached!
% 34.32/5.53 % (2522283)------------------------------
% 34.32/5.53 % (2522283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.32/5.53 % (2522283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.32/5.53 % (2522283)CaDiCaL version: 2.1.3
% 34.32/5.53 % (2522283)Termination reason: Instruction limit
% 34.32/5.53 % (2522283)Termination phase: Saturation
% 34.32/5.53 % (2522283)Time elapsed: 0.049 s
% 34.32/5.53 % (2522283)Peak memory usage: 87 MB
% 34.32/5.53 % (2522283)Instructions burned: 134 (million)
% 34.32/5.53 % (2522284)Instruction limit reached!
% 34.32/5.53 % (2522284)------------------------------
% 34.32/5.53 % (2522284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.32/5.53 % (2522284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.32/5.53 % (2522284)CaDiCaL version: 2.1.3
% 34.32/5.53 % (2522284)Termination reason: Instruction limit
% 34.32/5.53 % (2522284)Termination phase: Saturation
% 34.32/5.53 % (2522284)Time elapsed: 0.145 s
% 34.32/5.53 % (2522284)Peak memory usage: 102 MB
% 34.32/5.53 % (2522284)Instructions burned: 501 (million)
% 34.32/5.53 % (2522288)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3509131116:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 34.32/5.53 % (2522289)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2452255795:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 34.32/5.53 % (2522289)Instruction limit reached!
% 34.32/5.53 % (2522289)------------------------------
% 34.32/5.53 % (2522289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.32/5.53 % (2522289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.32/5.53 % (2522289)CaDiCaL version: 2.1.3
% 34.32/5.53 % (2522289)Termination reason: Instruction limit
% 34.32/5.53 % (2522289)Termination phase: Saturation
% 34.32/5.53 % (2522289)Time elapsed: 0.049 s
% 34.32/5.53 % (2522289)Peak memory usage: 87 MB
% 34.32/5.53 % (2522289)Instructions burned: 270 (million)
% 34.32/5.53 % (2522288)Instruction limit reached!
% 34.32/5.53 % (2522288)------------------------------
% 45.55/7.06 % (2522288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.55/7.06 % (2522288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.55/7.06 % (2522288)CaDiCaL version: 2.1.3
% 45.55/7.06 % (2522288)Termination reason: Instruction limit
% 45.55/7.06 % (2522288)Termination phase: Saturation
% 45.55/7.06 % (2522288)Time elapsed: 0.117 s
% 45.55/7.06 % (2522288)Peak memory usage: 92 MB
% 45.55/7.06 % (2522288)Instructions burned: 192 (million)
% 45.55/7.06 % (2522292)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2025331440:cond=on:i=156:bs=on:gtg=exists_all:er=known_2989 on theBenchmark for (2989ds/156Mi)
% 45.55/7.06 % (2522292)Instruction limit reached!
% 45.55/7.06 % (2522292)------------------------------
% 45.55/7.06 % (2522292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.55/7.06 % (2522292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.55/7.06 % (2522292)CaDiCaL version: 2.1.3
% 45.55/7.06 % (2522292)Termination reason: Instruction limit
% 45.55/7.06 % (2522292)Termination phase: Saturation
% 45.55/7.06 % (2522292)Time elapsed: 0.035 s
% 45.55/7.06 % (2522292)Peak memory usage: 87 MB
% 45.55/7.06 % (2522292)Instructions burned: 160 (million)
% 45.55/7.06 % (2522293)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=3778106691:i=3256:kws=precedence:bd=preordered:av=off_2989 on theBenchmark for (2989ds/3256Mi)
% 45.55/7.06 % (2522295)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4015369810:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi)
% 45.55/7.06 % (2522295)Instruction limit reached!
% 45.55/7.06 % (2522295)------------------------------
% 45.55/7.06 % (2522295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.55/7.06 % (2522295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.55/7.06 % (2522295)CaDiCaL version: 2.1.3
% 45.55/7.06 % (2522295)Termination reason: Instruction limit
% 45.55/7.06 % (2522295)Termination phase: Saturation
% 45.55/7.06 % (2522295)Time elapsed: 0.098 s
% 45.55/7.06 % (2522295)Peak memory usage: 87 MB
% 45.55/7.06 % (2522295)Instructions burned: 539 (million)
% 45.55/7.06 % (2522298)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4093165197:i=180:bd=preordered:av=off_2986 on theBenchmark for (2986ds/180Mi)
% 45.55/7.06 % (2522298)Instruction limit reached!
% 45.55/7.06 % (2522298)------------------------------
% 45.55/7.06 % (2522298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.55/7.06 % (2522298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.55/7.06 % (2522298)CaDiCaL version: 2.1.3
% 45.55/7.06 % (2522298)Termination reason: Instruction limit
% 45.55/7.06 % (2522298)Termination phase: Saturation
% 45.55/7.06 % (2522298)Time elapsed: 0.050 s
% 45.55/7.06 % (2522298)Peak memory usage: 93 MB
% 45.55/7.06 % (2522298)Instructions burned: 189 (million)
% 45.55/7.06 % (2522300)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=1120786745:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2984 on theBenchmark for (2984ds/10307Mi)
% 45.55/7.06 % (2522273)Instruction limit reached!
% 45.55/7.06 % (2522273)------------------------------
% 45.55/7.06 % (2522273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.55/7.06 % (2522273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.55/7.06 % (2522273)CaDiCaL version: 2.1.3
% 45.55/7.06 % (2522273)Termination reason: Instruction limit
% 45.55/7.06 % (2522273)Termination phase: Saturation
% 45.55/7.06 % (2522273)Time elapsed: 2.131 s
% 45.55/7.06 % (2522273)Peak memory usage: 148 MB
% 45.55/7.06 % (2522273)Instructions burned: 3395 (million)
% 45.55/7.06 % (2522302)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=1313658477:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 45.55/7.06 % (2522302)Instruction limit reached!
% 45.55/7.06 % (2522302)------------------------------
% 45.55/7.06 % (2522302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.55/7.06 % (2522302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.55/7.06 % (2522302)CaDiCaL version: 2.1.3
% 45.55/7.06 % (2522302)Termination reason: Instruction limit
% 45.55/7.06 % (2522302)Termination phase: Saturation
% 64.22/9.86 % (2522302)Time elapsed: 0.161 s
% 64.22/9.86 % (2522302)Peak memory usage: 89 MB
% 64.22/9.86 % (2522302)Instructions burned: 413 (million)
% 64.22/9.86 % (2522304)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=1798157076:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi)
% 64.22/9.86 % (2522293)Instruction limit reached!
% 64.22/9.86 % (2522293)------------------------------
% 64.22/9.86 % (2522293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.22/9.86 % (2522293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.22/9.86 % (2522293)CaDiCaL version: 2.1.3
% 64.22/9.86 % (2522293)Termination reason: Instruction limit
% 64.22/9.86 % (2522293)Termination phase: Saturation
% 64.22/9.86 % (2522293)Time elapsed: 1.978 s
% 64.22/9.86 % (2522293)Peak memory usage: 143 MB
% 64.22/9.86 % (2522293)Instructions burned: 3256 (million)
% 64.22/9.86 % (2522306)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=1619111233:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2967 on theBenchmark for (2967ds/303Mi)
% 64.22/9.86 % (2522306)Instruction limit reached!
% 64.22/9.86 % (2522306)------------------------------
% 64.22/9.86 % (2522306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.22/9.86 % (2522306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.22/9.86 % (2522306)CaDiCaL version: 2.1.3
% 64.22/9.86 % (2522306)Termination reason: Instruction limit
% 64.22/9.86 % (2522306)Termination phase: Saturation
% 64.22/9.86 % (2522306)Time elapsed: 0.173 s
% 64.22/9.86 % (2522306)Peak memory usage: 89 MB
% 64.22/9.86 % (2522306)Instructions burned: 304 (million)
% 64.22/9.86 % (2522308)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1278613055:st=4:i=720:sd=3:fsr=off:ss=axioms_2964 on theBenchmark for (2964ds/720Mi)
% 64.22/9.86 % (2522308)Instruction limit reached!
% 64.22/9.86 % (2522308)------------------------------
% 64.22/9.86 % (2522308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.22/9.86 % (2522308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.22/9.86 % (2522308)CaDiCaL version: 2.1.3
% 64.22/9.86 % (2522308)Termination reason: Instruction limit
% 64.22/9.86 % (2522308)Termination phase: Saturation
% 64.22/9.86 % (2522308)Time elapsed: 0.384 s
% 64.22/9.86 % (2522308)Peak memory usage: 93 MB
% 64.22/9.86 % (2522308)Instructions burned: 720 (million)
% 64.22/9.86 % (2522281)Instruction limit reached!
% 64.22/9.86 % (2522281)------------------------------
% 64.22/9.86 % (2522281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.22/9.86 % (2522281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.22/9.86 % (2522281)CaDiCaL version: 2.1.3
% 64.22/9.86 % (2522281)Termination reason: Instruction limit
% 64.22/9.86 % (2522281)Termination phase: Saturation
% 64.22/9.86 % (2522281)Time elapsed: 3.314 s
% 64.22/9.86 % (2522281)Peak memory usage: 151 MB
% 64.22/9.86 % (2522281)Instructions burned: 5209 (million)
% 64.22/9.86 % (2522310)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3694362124:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 64.22/9.86 % (2522311)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=660978174:i=2989:sd=3:ss=axioms:sgt=60_2959 on theBenchmark for (2959ds/2989Mi)
% 64.22/9.86 % (2522310)Instruction limit reached!
% 64.22/9.86 % (2522310)------------------------------
% 64.22/9.86 % (2522310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.22/9.86 % (2522310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.22/9.86 % (2522310)CaDiCaL version: 2.1.3
% 64.22/9.86 % (2522310)Termination reason: Instruction limit
% 64.22/9.86 % (2522310)Termination phase: Saturation
% 64.22/9.86 % (2522310)Time elapsed: 0.308 s
% 64.22/9.86 % (2522310)Peak memory usage: 89 MB
% 64.22/9.86 % (2522310)Instructions burned: 599 (million)
% 64.22/9.86 % (2522314)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=4248455973:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 64.22/9.86 % (2522300)Instruction limit reached!
% 64.22/9.86 % (2522300)------------------------------
% 93.16/13.89 % (2522300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.16/13.89 % (2522300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.16/13.89 % (2522300)CaDiCaL version: 2.1.3
% 93.16/13.89 % (2522300)Termination reason: Instruction limit
% 93.16/13.89 % (2522300)Termination phase: Saturation
% 93.16/13.89 % (2522300)Time elapsed: 3.249 s
% 93.16/13.89 % (2522300)Peak memory usage: 162 MB
% 93.16/13.89 % (2522300)Instructions burned: 10309 (million)
% 93.16/13.89 % (2522316)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=2777731453:i=2088:bd=preordered:av=off_2951 on theBenchmark for (2951ds/2088Mi)
% 93.16/13.89 % (2522316)Instruction limit reached!
% 93.16/13.89 % (2522316)------------------------------
% 93.16/13.89 % (2522316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.16/13.89 % (2522316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.16/13.89 % (2522316)CaDiCaL version: 2.1.3
% 93.16/13.89 % (2522316)Termination reason: Instruction limit
% 93.16/13.89 % (2522316)Termination phase: Saturation
% 93.16/13.89 % (2522316)Time elapsed: 0.788 s
% 93.16/13.89 % (2522316)Peak memory usage: 135 MB
% 93.16/13.89 % (2522316)Instructions burned: 2088 (million)
% 93.16/13.89 % (2522318)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3894765493:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi)
% 93.16/13.89 % (2522314)Instruction limit reached!
% 93.16/13.89 % (2522314)------------------------------
% 93.16/13.89 % (2522314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.16/13.89 % (2522314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.16/13.89 % (2522314)CaDiCaL version: 2.1.3
% 93.16/13.89 % (2522314)Termination reason: Instruction limit
% 93.16/13.89 % (2522314)Termination phase: Saturation
% 93.16/13.89 % (2522314)Time elapsed: 1.431 s
% 93.16/13.89 % (2522314)Peak memory usage: 136 MB
% 93.16/13.89 % (2522314)Instructions burned: 1998 (million)
% 93.16/13.89 % (2522320)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4185087361:i=433:bd=preordered_2939 on theBenchmark for (2939ds/433Mi)
% 93.16/13.89 % (2522318)Instruction limit reached!
% 93.16/13.89 % (2522318)------------------------------
% 93.16/13.89 % (2522318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.16/13.89 % (2522318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.16/13.89 % (2522318)CaDiCaL version: 2.1.3
% 93.16/13.89 % (2522318)Termination reason: Instruction limit
% 93.16/13.89 % (2522318)Termination phase: Saturation
% 93.16/13.89 % (2522318)Time elapsed: 0.322 s
% 93.16/13.89 % (2522318)Peak memory usage: 112 MB
% 93.16/13.89 % (2522318)Instructions burned: 1099 (million)
% 93.16/13.89 % (2522311)Instruction limit reached!
% 93.16/13.89 % (2522311)------------------------------
% 93.16/13.89 % (2522311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.16/13.89 % (2522311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.16/13.89 % (2522311)CaDiCaL version: 2.1.3
% 93.16/13.89 % (2522311)Termination reason: Instruction limit
% 93.16/13.89 % (2522311)Termination phase: Saturation
% 93.16/13.89 % (2522311)Time elapsed: 2.036 s
% 93.16/13.89 % (2522311)Peak memory usage: 140 MB
% 93.16/13.89 % (2522311)Instructions burned: 2989 (million)
% 93.16/13.89 % (2522322)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3748196228:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2938 on theBenchmark for (2938ds/2942Mi)
% 93.16/13.89 % (2522323)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3546723647:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2937 on theBenchmark for (2937ds/6922Mi)
% 93.16/13.89 % (2522320)Instruction limit reached!
% 93.16/13.89 % (2522320)------------------------------
% 93.16/13.89 % (2522320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.16/13.89 % (2522320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.16/13.89 % (2522320)CaDiCaL version: 2.1.3
% 93.16/13.89 % (2522320)Termination reason: Instruction limit
% 93.16/13.89 % (2522320)Termination phase: Saturation
% 93.16/13.89 % (2522320)Time elapsed: 0.254 s
% 93.16/13.89 % (2522320)Peak memory usage: 91 MB
% 93.16/13.89 % (2522320)Instructions burned: 433 (million)
% 110.43/16.21 % (2522326)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=3630235355:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2936 on theBenchmark for (2936ds/596Mi)
% 110.43/16.21 % (2522326)Instruction limit reached!
% 110.43/16.21 % (2522326)------------------------------
% 110.43/16.21 % (2522326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.43/16.21 % (2522326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.43/16.21 % (2522326)CaDiCaL version: 2.1.3
% 110.43/16.21 % (2522326)Termination reason: Instruction limit
% 110.43/16.21 % (2522326)Termination phase: Saturation
% 110.43/16.21 % (2522326)Time elapsed: 0.279 s
% 110.43/16.21 % (2522326)Peak memory usage: 103 MB
% 110.43/16.21 % (2522326)Instructions burned: 596 (million)
% 110.43/16.21 % (2522328)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=1210747659:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2931 on theBenchmark for (2931ds/4123Mi)
% 110.43/16.21 % (2522322)Instruction limit reached!
% 110.43/16.21 % (2522322)------------------------------
% 110.43/16.21 % (2522322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.43/16.21 % (2522322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.43/16.21 % (2522322)CaDiCaL version: 2.1.3
% 110.43/16.21 % (2522322)Termination reason: Instruction limit
% 110.43/16.21 % (2522322)Termination phase: Saturation
% 110.43/16.21 % (2522322)Time elapsed: 1.142 s
% 110.43/16.21 % (2522322)Peak memory usage: 140 MB
% 110.43/16.21 % (2522322)Instructions burned: 2942 (million)
% 110.43/16.21 % (2522330)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1440090422:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2925 on theBenchmark for (2925ds/16411Mi)
% 110.43/16.21 % (2522304)Instruction limit reached!
% 110.43/16.21 % (2522304)------------------------------
% 110.43/16.21 % (2522304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.43/16.21 % (2522304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.43/16.21 % (2522304)CaDiCaL version: 2.1.3
% 110.43/16.21 % (2522304)Termination reason: Instruction limit
% 110.43/16.21 % (2522304)Termination phase: Saturation
% 110.43/16.21 % (2522304)Time elapsed: 4.546 s
% 110.43/16.21 % (2522304)Peak memory usage: 179 MB
% 110.43/16.21 % (2522304)Instructions burned: 8479 (million)
% 110.43/16.21 % (2522332)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3290743360:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2923 on theBenchmark for (2923ds/1670Mi)
% 110.43/16.21 % (2522328)Instruction limit reached!
% 110.43/16.21 % (2522328)------------------------------
% 110.43/16.21 % (2522328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.43/16.21 % (2522328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.43/16.21 % (2522328)CaDiCaL version: 2.1.3
% 110.43/16.21 % (2522328)Termination reason: Instruction limit
% 110.43/16.21 % (2522328)Termination phase: Saturation
% 110.43/16.21 % (2522328)Time elapsed: 1.545 s
% 110.43/16.21 % (2522328)Peak memory usage: 155 MB
% 110.43/16.21 % (2522328)Instructions burned: 4124 (million)
% 110.43/16.21 % (2522334)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=26977659:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2915 on theBenchmark for (2915ds/1722Mi)
% 110.43/16.21 % (2522332)Instruction limit reached!
% 110.43/16.21 % (2522332)------------------------------
% 110.43/16.21 % (2522332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.43/16.21 % (2522332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.43/16.21 % (2522332)CaDiCaL version: 2.1.3
% 110.43/16.21 % (2522332)Termination reason: Instruction limit
% 110.43/16.21 % (2522332)Termination phase: Saturation
% 110.43/16.21 % (2522332)Time elapsed: 1.053 s
% 110.43/16.21 % (2522332)Peak memory usage: 133 MB
% 110.43/16.21 % (2522332)Instructions burned: 1671 (million)
% 110.43/16.21 % (2522336)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=753980525:cts=off:cond=on:i=9530:bs=on:fsd=on_2911 on theBenchmark for (2911ds/9530Mi)
% 110.43/16.21 % (2522334)Instruction limit reached!
% 127.98/19.00 % (2522334)------------------------------
% 127.98/19.00 % (2522334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.98/19.00 % (2522334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.98/19.00 % (2522334)CaDiCaL version: 2.1.3
% 127.98/19.00 % (2522334)Termination reason: Instruction limit
% 127.98/19.00 % (2522334)Termination phase: Saturation
% 127.98/19.00 % (2522334)Time elapsed: 0.633 s
% 127.98/19.00 % (2522334)Peak memory usage: 134 MB
% 127.98/19.00 % (2522334)Instructions burned: 1723 (million)
% 127.98/19.00 % (2522338)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3477607850:st=2:i=4495:sd=10:ss=included_2908 on theBenchmark for (2908ds/4495Mi)
% 127.98/19.00 % (2522323)Instruction limit reached!
% 127.98/19.00 % (2522323)------------------------------
% 127.98/19.00 % (2522323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.98/19.00 % (2522323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.98/19.00 % (2522323)CaDiCaL version: 2.1.3
% 127.98/19.00 % (2522323)Termination reason: Instruction limit
% 127.98/19.00 % (2522323)Termination phase: Saturation
% 127.98/19.00 % (2522323)Time elapsed: 3.741 s
% 127.98/19.00 % (2522323)Peak memory usage: 187 MB
% 127.98/19.00 % (2522323)Instructions burned: 6924 (million)
% 127.98/19.00 % (2522340)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=4142970025:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2898 on theBenchmark for (2898ds/4920Mi)
% 127.98/19.00 % (2522338)Instruction limit reached!
% 127.98/19.00 % (2522338)------------------------------
% 127.98/19.00 % (2522338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.98/19.00 % (2522338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.98/19.00 % (2522338)CaDiCaL version: 2.1.3
% 127.98/19.00 % (2522338)Termination reason: Instruction limit
% 127.98/19.00 % (2522338)Termination phase: Saturation
% 127.98/19.00 % (2522338)Time elapsed: 1.113 s
% 127.98/19.00 % (2522338)Peak memory usage: 130 MB
% 127.98/19.00 % (2522338)Instructions burned: 4498 (million)
% 127.98/19.00 % (2522342)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=833334794:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2895 on theBenchmark for (2895ds/2083Mi)
% 127.98/19.00 % (2522342)Instruction limit reached!
% 127.98/19.00 % (2522342)------------------------------
% 127.98/19.00 % (2522342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.98/19.00 % (2522342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.98/19.00 % (2522342)CaDiCaL version: 2.1.3
% 127.98/19.00 % (2522342)Termination reason: Instruction limit
% 127.98/19.00 % (2522342)Termination phase: Saturation
% 127.98/19.00 % (2522342)Time elapsed: 0.692 s
% 127.98/19.00 % (2522342)Peak memory usage: 134 MB
% 127.98/19.00 % (2522342)Instructions burned: 2084 (million)
% 127.98/19.00 % (2522344)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=2308469612:i=4629:av=off:gsp=on_2887 on theBenchmark for (2887ds/4629Mi)
% 127.98/19.00 % (2522344)Instruction limit reached!
% 127.98/19.00 % (2522344)------------------------------
% 127.98/19.00 % (2522344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.98/19.00 % (2522344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.98/19.00 % (2522344)CaDiCaL version: 2.1.3
% 127.98/19.00 % (2522344)Termination reason: Instruction limit
% 127.98/19.00 % (2522344)Termination phase: Saturation
% 127.98/19.00 % (2522344)Time elapsed: 1.469 s
% 127.98/19.00 % (2522344)Peak memory usage: 141 MB
% 127.98/19.00 % (2522344)Instructions burned: 4631 (million)
% 127.98/19.00 % (2522346)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=666584451:i=1258:av=off_2872 on theBenchmark for (2872ds/1258Mi)
% 127.98/19.00 % (2522346)Instruction limit reached!
% 127.98/19.00 % (2522346)------------------------------
% 127.98/19.00 % (2522346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.98/19.00 % (2522346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.98/19.00 % (2522346)CaDiCaL version: 2.1.3
% 127.98/19.00 % (2522346)Termination reason: Instruction limit
% 127.98/19.00 % (2522346)Termination phase: Saturation
% 127.98/19.00 % (2522346)Time elapsed: 0.362 s
% 127.98/19.00 % (2522346)Peak memory usage: 93 MB
% 152.51/22.16 % (2522346)Instructions burned: 1261 (million)
% 152.51/22.16 % (2522348)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4289673886:i=7343:av=off:ss=included_2867 on theBenchmark for (2867ds/7343Mi)
% 152.51/22.16 % (2522340)Instruction limit reached!
% 152.51/22.16 % (2522340)------------------------------
% 152.51/22.16 % (2522340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.51/22.16 % (2522340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.51/22.16 % (2522340)CaDiCaL version: 2.1.3
% 152.51/22.16 % (2522340)Termination reason: Instruction limit
% 152.51/22.16 % (2522340)Termination phase: Saturation
% 152.51/22.16 % (2522340)Time elapsed: 3.175 s
% 152.51/22.16 % (2522340)Peak memory usage: 149 MB
% 152.51/22.16 % (2522340)Instructions burned: 4920 (million)
% 152.51/22.16 % (2522350)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=381370512:i=1325:sd=2:ss=axioms:sgt=16_2865 on theBenchmark for (2865ds/1325Mi)
% 152.51/22.16 % (2522348)Refutation not found, incomplete strategy
% 152.51/22.16 % (2522348)------------------------------
% 152.51/22.16 % (2522348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.51/22.16 % (2522348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.51/22.16 % (2522348)CaDiCaL version: 2.1.3
% 152.51/22.16 % (2522348)Termination reason: Refutation not found, incomplete strategy
% 152.51/22.16 % (2522348)Time elapsed: 0.363 s
% 152.51/22.16 % (2522348)Peak memory usage: 127 MB
% 152.51/22.16 % (2522348)Instructions burned: 943 (million)
% 152.51/22.16 % (2522348)------------------------------
% 152.51/22.16 % (2522348)------------------------------
% 152.51/22.16 % (2522352)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=203191427:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2861 on theBenchmark for (2861ds/2646Mi)
% 152.51/22.16 % (2522350)Instruction limit reached!
% 152.51/22.16 % (2522350)------------------------------
% 152.51/22.16 % (2522350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.51/22.16 % (2522350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.51/22.16 % (2522350)CaDiCaL version: 2.1.3
% 152.51/22.16 % (2522350)Termination reason: Instruction limit
% 152.51/22.16 % (2522350)Termination phase: Saturation
% 152.51/22.16 % (2522350)Time elapsed: 0.789 s
% 152.51/22.16 % (2522350)Peak memory usage: 93 MB
% 152.51/22.16 % (2522350)Instructions burned: 1325 (million)
% 152.51/22.16 % (2522354)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1788723421:i=1489:sd=2:ep=R:ss=axioms_2856 on theBenchmark for (2856ds/1489Mi)
% 152.51/22.16 % (2522336)Instruction limit reached!
% 152.51/22.16 % (2522336)------------------------------
% 152.51/22.16 % (2522336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.51/22.16 % (2522336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.51/22.16 % (2522336)CaDiCaL version: 2.1.3
% 152.51/22.16 % (2522336)Termination reason: Instruction limit
% 152.51/22.16 % (2522336)Termination phase: Saturation
% 152.51/22.16 % (2522336)Time elapsed: 5.981 s
% 152.51/22.16 % (2522336)Peak memory usage: 156 MB
% 152.51/22.16 % (2522336)Instructions burned: 9530 (million)
% 152.51/22.16 % (2522352)Instruction limit reached!
% 152.51/22.16 % (2522352)------------------------------
% 152.51/22.16 % (2522352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.51/22.16 % (2522352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.51/22.16 % (2522352)CaDiCaL version: 2.1.3
% 152.51/22.16 % (2522352)Termination reason: Instruction limit
% 152.51/22.16 % (2522352)Termination phase: Saturation
% 152.51/22.16 % (2522352)Time elapsed: 1.060 s
% 152.51/22.16 % (2522352)Peak memory usage: 139 MB
% 152.51/22.16 % (2522352)Instructions burned: 2647 (million)
% 152.51/22.16 % (2522357)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3958778616:i=13942:kws=frequency_2850 on theBenchmark for (2850ds/13942Mi)
% 152.51/22.16 % (2522356)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=372644366:i=1503_2850 on theBenchmark for (2850ds/1503Mi)
% 152.51/22.16 % (2522354)Instruction limit reached!
% 152.51/22.16 % (2522354)------------------------------
% 152.51/22.16 % (2522354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.51/22.16 % (2522354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.05/25.08 % (2522354)CaDiCaL version: 2.1.3
% 173.05/25.08 % (2522354)Termination reason: Instruction limit
% 173.05/25.08 % (2522354)Termination phase: Saturation
% 173.05/25.08 % (2522354)Time elapsed: 1.051 s
% 173.05/25.08 % (2522354)Peak memory usage: 131 MB
% 173.05/25.08 % (2522354)Instructions burned: 1491 (million)
% 173.05/25.08 % (2522360)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=2487316703:i=3604:fsr=off:er=filter_2844 on theBenchmark for (2844ds/3604Mi)
% 173.05/25.08 % (2522356)Instruction limit reached!
% 173.05/25.08 % (2522356)------------------------------
% 173.05/25.08 % (2522356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.05/25.08 % (2522356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.05/25.08 % (2522356)CaDiCaL version: 2.1.3
% 173.05/25.08 % (2522356)Termination reason: Instruction limit
% 173.05/25.08 % (2522356)Termination phase: Saturation
% 173.05/25.08 % (2522356)Time elapsed: 0.930 s
% 173.05/25.08 % (2522356)Peak memory usage: 133 MB
% 173.05/25.08 % (2522356)Instructions burned: 1503 (million)
% 173.05/25.08 % (2522362)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3148826159:i=1876:sd=1:ss=included:sgt=32_2839 on theBenchmark for (2839ds/1876Mi)
% 173.05/25.08 % (2522362)Instruction limit reached!
% 173.05/25.08 % (2522362)------------------------------
% 173.05/25.08 % (2522362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.05/25.08 % (2522362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.05/25.08 % (2522362)CaDiCaL version: 2.1.3
% 173.05/25.08 % (2522362)Termination reason: Instruction limit
% 173.05/25.08 % (2522362)Termination phase: Saturation
% 173.05/25.08 % (2522362)Time elapsed: 1.210 s
% 173.05/25.08 % (2522362)Peak memory usage: 137 MB
% 173.05/25.08 % (2522362)Instructions burned: 1876 (million)
% 173.05/25.08 % (2522364)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=445002731:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2826 on theBenchmark for (2826ds/1932Mi)
% 173.05/25.08 % (2522330)Instruction limit reached!
% 173.05/25.08 % (2522330)------------------------------
% 173.05/25.08 % (2522330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.05/25.08 % (2522330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.05/25.08 % (2522330)CaDiCaL version: 2.1.3
% 173.05/25.08 % (2522330)Termination reason: Instruction limit
% 173.05/25.08 % (2522330)Termination phase: Saturation
% 173.05/25.08 % (2522330)Time elapsed: 10.265 s
% 173.05/25.08 % (2522330)Peak memory usage: 280 MB
% 173.05/25.08 % (2522330)Instructions burned: 16412 (million)
% 173.05/25.08 % (2522360)Instruction limit reached!
% 173.05/25.08 % (2522360)------------------------------
% 173.05/25.08 % (2522360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.05/25.08 % (2522360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.05/25.08 % (2522360)CaDiCaL version: 2.1.3
% 173.05/25.08 % (2522360)Termination reason: Instruction limit
% 173.05/25.08 % (2522360)Termination phase: Saturation
% 173.05/25.08 % (2522360)Time elapsed: 2.174 s
% 173.05/25.08 % (2522360)Peak memory usage: 153 MB
% 173.05/25.08 % (2522360)Instructions burned: 3606 (million)
% 173.05/25.08 % (2522366)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=1221158231:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2821 on theBenchmark for (2821ds/1980Mi)
% 173.05/25.08 % (2522367)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=2704103028:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2821 on theBenchmark for (2821ds/3902Mi)
% 173.05/25.08 % (2522364)Refutation not found, incomplete strategy
% 173.05/25.08 % (2522364)------------------------------
% 173.05/25.08 % (2522364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.05/25.08 % (2522364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.05/25.08 % (2522364)CaDiCaL version: 2.1.3
% 173.05/25.08 % (2522364)Termination reason: Refutation not found, incomplete strategy
% 173.05/25.08 % (2522364)Time elapsed: 0.597 s
% 173.05/25.08 % (2522364)Peak memory usage: 127 MB
% 173.05/25.08 % (2522364)Instructions burned: 911 (million)
% 173.05/25.08 % (2522364)------------------------------
% 192.20/27.83 % (2522364)------------------------------
% 192.20/27.83 % (2522370)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=359679756:avsq=on:i=3916:aac=none:amm=off_2816 on theBenchmark for (2816ds/3916Mi)
% 192.20/27.83 % (2522366)Instruction limit reached!
% 192.20/27.83 % (2522366)------------------------------
% 192.20/27.83 % (2522366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.20/27.83 % (2522366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.20/27.83 % (2522366)CaDiCaL version: 2.1.3
% 192.20/27.83 % (2522366)Termination reason: Instruction limit
% 192.20/27.83 % (2522366)Termination phase: Saturation
% 192.20/27.83 % (2522366)Time elapsed: 1.364 s
% 192.20/27.83 % (2522366)Peak memory usage: 135 MB
% 192.20/27.83 % (2522366)Instructions burned: 1980 (million)
% 192.20/27.83 % (2522372)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3833603385:cond=on:i=3940:av=off:er=known_2806 on theBenchmark for (2806ds/3940Mi)
% 192.20/27.83 % (2522357)Instruction limit reached!
% 192.20/27.83 % (2522357)------------------------------
% 192.20/27.83 % (2522357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.20/27.83 % (2522357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.20/27.83 % (2522357)CaDiCaL version: 2.1.3
% 192.20/27.83 % (2522357)Termination reason: Instruction limit
% 192.20/27.83 % (2522357)Termination phase: Saturation
% 192.20/27.83 % (2522357)Time elapsed: 4.834 s
% 192.20/27.83 % (2522357)Peak memory usage: 218 MB
% 192.20/27.83 % (2522357)Instructions burned: 13943 (million)
% 192.20/27.83 % (2522374)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=704886717:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2800 on theBenchmark for (2800ds/3980Mi)
% 192.20/27.83 % (2522370)Instruction limit reached!
% 192.20/27.83 % (2522370)------------------------------
% 192.20/27.83 % (2522370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.20/27.83 % (2522370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.20/27.83 % (2522370)CaDiCaL version: 2.1.3
% 192.20/27.83 % (2522370)Termination reason: Instruction limit
% 192.20/27.83 % (2522370)Termination phase: Saturation
% 192.20/27.83 % (2522370)Time elapsed: 1.578 s
% 192.20/27.83 % (2522370)Peak memory usage: 93 MB
% 192.20/27.83 % (2522370)Instructions burned: 3916 (million)
% 192.20/27.83 % (2522376)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=698676412:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2799 on theBenchmark for (2799ds/2087Mi)
% 192.20/27.83 % (2522367)Instruction limit reached!
% 192.20/27.83 % (2522367)------------------------------
% 192.20/27.83 % (2522367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.20/27.83 % (2522367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.20/27.83 % (2522367)CaDiCaL version: 2.1.3
% 192.20/27.83 % (2522367)Termination reason: Instruction limit
% 192.20/27.83 % (2522367)Termination phase: Saturation
% 192.20/27.83 % (2522367)Time elapsed: 2.191 s
% 192.20/27.83 % (2522367)Peak memory usage: 148 MB
% 192.20/27.83 % (2522367)Instructions burned: 3903 (million)
% 192.20/27.83 % (2522378)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1579683414:cts=off:cond=on:i=4272:bs=on:fsd=on_2798 on theBenchmark for (2798ds/4272Mi)
% 192.20/27.83 % (2522374)Instruction limit reached!
% 192.20/27.83 % (2522374)------------------------------
% 192.20/27.83 % (2522374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.20/27.83 % (2522374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.20/27.83 % (2522374)CaDiCaL version: 2.1.3
% 192.20/27.83 % (2522374)Termination reason: Instruction limit
% 192.20/27.83 % (2522374)Termination phase: Saturation
% 192.20/27.83 % (2522374)Time elapsed: 1.411 s
% 192.20/27.83 % (2522374)Peak memory usage: 157 MB
% 192.20/27.83 % (2522374)Instructions burned: 3980 (million)
% 192.20/27.83 % (2522376)Instruction limit reached!
% 192.20/27.83 % (2522376)------------------------------
% 192.20/27.83 % (2522376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.20/27.83 % (2522376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522376)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522376)Termination reason: Instruction limit
% 108.62/29.83 % (2522376)Termination phase: Saturation
% 108.62/29.83 % (2522376)Time elapsed: 1.322 s
% 108.62/29.83 % (2522376)Peak memory usage: 141 MB
% 108.62/29.83 % (2522376)Instructions burned: 2088 (million)
% 108.62/29.83 % (2522380)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2869871900:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2785 on theBenchmark for (2785ds/2197Mi)
% 108.62/29.83 % (2522381)dis+21_1_sil=8000:spb=goal_then_units:random_seed=393261055:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2784 on theBenchmark for (2784ds/6508Mi)
% 108.62/29.83 % (2522372)Instruction limit reached!
% 108.62/29.83 % (2522372)------------------------------
% 108.62/29.83 % (2522372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522372)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522372)Termination reason: Instruction limit
% 108.62/29.83 % (2522372)Termination phase: Saturation
% 108.62/29.83 % (2522372)Time elapsed: 2.398 s
% 108.62/29.83 % (2522372)Peak memory usage: 150 MB
% 108.62/29.83 % (2522372)Instructions burned: 3941 (million)
% 108.62/29.83 % (2522384)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=242867287:i=2330:fgj=on:av=off:fsr=off_2781 on theBenchmark for (2781ds/2330Mi)
% 108.62/29.83 % (2522380)Instruction limit reached!
% 108.62/29.83 % (2522380)------------------------------
% 108.62/29.83 % (2522380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522380)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522380)Termination reason: Instruction limit
% 108.62/29.83 % (2522380)Termination phase: Saturation
% 108.62/29.83 % (2522380)Time elapsed: 0.706 s
% 108.62/29.83 % (2522380)Peak memory usage: 143 MB
% 108.62/29.83 % (2522380)Instructions burned: 2198 (million)
% 108.62/29.83 % (2522386)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2472477493:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2777 on theBenchmark for (2777ds/7592Mi)
% 108.62/29.83 % (2522378)Instruction limit reached!
% 108.62/29.83 % (2522378)------------------------------
% 108.62/29.83 % (2522378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522378)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522378)Termination reason: Instruction limit
% 108.62/29.83 % (2522378)Termination phase: Saturation
% 108.62/29.83 % (2522378)Time elapsed: 2.701 s
% 108.62/29.83 % (2522378)Peak memory usage: 143 MB
% 108.62/29.83 % (2522378)Instructions burned: 4273 (million)
% 108.62/29.83 % (2522388)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=579155245:i=2693:kws=precedence:ins=1:av=off_2769 on theBenchmark for (2769ds/2693Mi)
% 108.62/29.83 % (2522384)Instruction limit reached!
% 108.62/29.83 % (2522384)------------------------------
% 108.62/29.83 % (2522384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522384)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522384)Termination reason: Instruction limit
% 108.62/29.83 % (2522384)Termination phase: Saturation
% 108.62/29.83 % (2522384)Time elapsed: 1.508 s
% 108.62/29.83 % (2522384)Peak memory usage: 137 MB
% 108.62/29.83 % (2522384)Instructions burned: 2330 (million)
% 108.62/29.83 % (2522390)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2900015185:i=28651:sd=4:ss=included:sgt=64_2765 on theBenchmark for (2765ds/28651Mi)
% 108.62/29.83 % (2522386)Instruction limit reached!
% 108.62/29.83 % (2522386)------------------------------
% 108.62/29.83 % (2522386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522386)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522386)Termination reason: Instruction limit
% 108.62/29.83 % (2522386)Termination phase: Saturation
% 108.62/29.83 % (2522386)Time elapsed: 1.999 s
% 108.62/29.83 % (2522386)Peak memory usage: 126 MB
% 108.62/29.83 % (2522386)Instructions burned: 7596 (million)
% 108.62/29.83 % (2522392)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1334622432:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2756 on theBenchmark for (2756ds/2700Mi)
% 108.62/29.83 % (2522381)Instruction limit reached!
% 108.62/29.83 % (2522381)------------------------------
% 108.62/29.83 % (2522381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522381)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522381)Termination reason: Instruction limit
% 108.62/29.83 % (2522381)Termination phase: Saturation
% 108.62/29.83 % (2522381)Time elapsed: 3.340 s
% 108.62/29.83 % (2522381)Peak memory usage: 143 MB
% 108.62/29.83 % (2522381)Instructions burned: 6509 (million)
% 108.62/29.83 % (2522388)Instruction limit reached!
% 108.62/29.83 % (2522388)------------------------------
% 108.62/29.83 % (2522388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522388)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522388)Termination reason: Instruction limit
% 108.62/29.83 % (2522388)Termination phase: Saturation
% 108.62/29.83 % (2522388)Time elapsed: 1.836 s
% 108.62/29.83 % (2522388)Peak memory usage: 139 MB
% 108.62/29.83 % (2522388)Instructions burned: 2694 (million)
% 108.62/29.83 % (2522394)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=2108807092:i=3196:nm=4_2750 on theBenchmark for (2750ds/3196Mi)
% 108.62/29.83 % (2522395)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=2345110359:cts=off:i=3254:av=off_2749 on theBenchmark for (2749ds/3254Mi)
% 108.62/29.83 % (2522392)Instruction limit reached!
% 108.62/29.83 % (2522392)------------------------------
% 108.62/29.83 % (2522392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522392)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522392)Termination reason: Instruction limit
% 108.62/29.83 % (2522392)Termination phase: Saturation
% 108.62/29.83 % (2522392)Time elapsed: 1.005 s
% 108.62/29.83 % (2522392)Peak memory usage: 140 MB
% 108.62/29.83 % (2522392)Instructions burned: 2702 (million)
% 108.62/29.83 % (2522398)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1136142907:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2745 on theBenchmark for (2745ds/3264Mi)
% 108.62/29.83 % (2522398)Instruction limit reached!
% 108.62/29.83 % (2522398)------------------------------
% 108.62/29.83 % (2522398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522398)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522398)Termination reason: Instruction limit
% 108.62/29.83 % (2522398)Termination phase: Saturation
% 108.62/29.83 % (2522398)Time elapsed: 1.225 s
% 108.62/29.83 % (2522398)Peak memory usage: 142 MB
% 108.62/29.83 % (2522398)Instructions burned: 3264 (million)
% 108.62/29.83 % (2522400)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=3778646780:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2732 on theBenchmark for (2732ds/9708Mi)
% 108.62/29.83 % (2522394)Instruction limit reached!
% 108.62/29.83 % (2522394)------------------------------
% 108.62/29.83 % (2522394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522394)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522394)Termination reason: Instruction limit
% 108.62/29.83 % (2522394)Termination phase: Saturation
% 108.62/29.83 % (2522394)Time elapsed: 1.854 s
% 108.62/29.83 % (2522394)Peak memory usage: 148 MB
% 108.62/29.83 % (2522394)Instructions burned: 3196 (million)
% 108.62/29.83 % (2522402)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2429225268:i=21997:s2at=5:gtg=all_2730 on theBenchmark for (2730ds/21997Mi)
% 108.62/29.83 % (2522395)Instruction limit reached!
% 108.62/29.83 % (2522395)------------------------------
% 108.62/29.83 % (2522395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.62/29.83 % (2522395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.62/29.83 % (2522395)CaDiCaL version: 2.1.3
% 108.62/29.83 % (2522395)Termination reason: Instruction limit
% 108.62/29.83 % (2522395)Termination phase: Saturation
% 108.62/29.83 % (2522395)Time elapsed: 2.043 s
% 108.62/29.83 % (2522395)Peak memory usage: 145 MB
% 108.62/29.83 % (2522395)Instructions burned: 3254 (million)
% 108.62/29.83 % (2522404)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4065050349:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2728 on theBenchmark for (2728ds/7551Mi)
% 108.62/29.83 % (2522400)First to succeed.
% 108.62/29.83 % (2522400)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2522243"
% 108.62/29.83 % (2522400)Refutation found. Thanks to Tanya!
% 108.62/29.83 % SZS status Unsatisfiable for theBenchmark
% 108.62/29.83 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/30.03 % (2522400)------------------------------
% 0.20/30.03 % (2522400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/30.03 % (2522400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/30.03 % (2522400)CaDiCaL version: 2.1.3
% 0.20/30.03 % (2522400)Termination reason: Refutation
% 0.20/30.03 % (2522400)Time elapsed: 2.116 s
% 0.20/30.03 % (2522400)Peak memory usage: 173 MB
% 0.20/30.03 % (2522400)Instructions burned: 6934 (million)
% 0.20/30.03 % (2522400)------------------------------
% 0.20/30.03 % (2522400)------------------------------
% 0.20/30.03 % (2522243)Success in time 29.166 s
% 0.20/30.03 % Vampire exiting
%------------------------------------------------------------------------------