%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ANA005-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:30:50 AM UTC 2026
% Result : Unsatisfiable 192.90s 38.83s
% Output : Refutation 270.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 21
% Syntax : Number of formulae : 81 ( 8 unt; 0 def)
% Number of atoms : 257 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 309 ( 133 ~; 176 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 123 ( 123 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : less_or_equalish(absolute(add(X0,X1)),add(absolute(X0),absolute(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absolute_sum_less_or_equal_sum_of_absolutes1) ).
fof(f2,axiom,
! [X0,X1] : less_or_equalish(minimum(X0,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum2) ).
fof(f5,axiom,
! [X0,X1] :
( less_or_equalish(X0,minimum(X1,X0))
| ~ less_or_equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum8) ).
fof(f6,axiom,
! [X2,X0,X1] :
( less_or_equalish(add(X0,X2),X1)
| ~ less_or_equalish(X2,half(X1))
| ~ less_or_equalish(X0,half(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal_sum_of_halves) ).
fof(f7,axiom,
! [X0] :
( ~ less_or_equalish(half(X0),n0)
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_and_half) ).
fof(f8,axiom,
! [X0,X1] :
( less_or_equalish(X1,X0)
| less_or_equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_less_or_equal) ).
fof(f9,axiom,
! [X2,X0,X1] :
( less_or_equalish(X0,X2)
| ~ less_or_equalish(X1,X2)
| ~ less_or_equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_less_or_equal) ).
fof(f10,axiom,
! [X0,X1] : equalish(add(X0,X1),add(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_add) ).
fof(f11,axiom,
! [X2,X0,X1] : equalish(add(add(X0,X1),X2),add(X0,add(X1,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_add) ).
fof(f12,axiom,
! [X0,X1] :
( equalish(X1,X0)
| ~ equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry) ).
fof(f13,axiom,
! [X2,X0,X1] :
( equalish(X0,X2)
| ~ equalish(X1,X2)
| ~ equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
fof(f14,axiom,
! [X2,X0,X1] :
( ~ equalish(X0,X1)
| ~ less_or_equalish(X0,X2)
| less_or_equalish(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal_substitution1) ).
fof(f15,axiom,
! [X0,X1] :
( equalish(absolute(X0),absolute(X1))
| ~ equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absolute_substitution) ).
fof(f16,axiom,
! [X2,X0,X1] :
( equalish(add(X0,X2),add(X1,X2))
| ~ equalish(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',add_substitution1) ).
fof(f18,axiom,
! [X0] :
( ~ less_or_equalish(delta_1(X0),n0)
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
fof(f19,axiom,
! [X0] :
( ~ less_or_equalish(delta_2(X0),n0)
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
fof(f20,axiom,
! [X0,X1] :
( less_or_equalish(absolute(add(f(X1),negate(f(a_real_number)))),X0)
| ~ less_or_equalish(absolute(add(X1,negate(a_real_number))),delta_1(X0))
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
fof(f21,axiom,
! [X0,X1] :
( less_or_equalish(absolute(add(g(X1),negate(g(a_real_number)))),X0)
| ~ less_or_equalish(absolute(add(X1,negate(a_real_number))),delta_2(X0))
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
fof(f22,axiom,
~ less_or_equalish(epsilon_0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
fof(f23,axiom,
! [X0] :
( less_or_equalish(absolute(add(xs(X0),negate(a_real_number))),X0)
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
fof(f24,negated_conjecture,
! [X0] :
( ~ less_or_equalish(absolute(add(add(f(xs(X0)),g(xs(X0))),add(negate(f(a_real_number)),negate(g(a_real_number))))),epsilon_0)
| less_or_equalish(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
fof(f43,plain,
! [X2,X0,X1] :
( less_or_equalish(absolute(X1),X2)
| ~ less_or_equalish(absolute(X0),X2)
| ~ equalish(X0,X1) ),
inference(resolution,[],[f15,f14]) ).
fof(f45,plain,
! [X0,X1] :
( ~ equalish(X0,add(add(f(xs(X1)),g(xs(X1))),add(negate(f(a_real_number)),negate(g(a_real_number)))))
| ~ less_or_equalish(absolute(X0),epsilon_0)
| less_or_equalish(X1,n0) ),
inference(resolution,[],[f43,f24]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ equalish(X2,add(add(f(xs(X1)),g(xs(X1))),add(negate(f(a_real_number)),negate(g(a_real_number)))))
| less_or_equalish(X1,n0)
| ~ less_or_equalish(absolute(X0),epsilon_0)
| ~ equalish(X0,X2) ),
inference(resolution,[],[f45,f13]) ).
fof(f411,plain,
! [X0,X1] :
( ~ equalish(X1,add(add(add(f(xs(X0)),g(xs(X0))),negate(f(a_real_number))),negate(g(a_real_number))))
| ~ less_or_equalish(absolute(X1),epsilon_0)
| less_or_equalish(X0,n0) ),
inference(resolution,[],[f139,f11]) ).
fof(f421,plain,
! [X2,X0,X1] :
( ~ equalish(X2,add(add(add(f(xs(X1)),g(xs(X1))),negate(f(a_real_number))),negate(g(a_real_number))))
| less_or_equalish(X1,n0)
| ~ less_or_equalish(absolute(X0),epsilon_0)
| ~ equalish(X0,X2) ),
inference(resolution,[],[f411,f13]) ).
fof(f442,plain,
! [X2,X0,X1] :
( ~ equalish(add(add(add(f(xs(X0)),g(xs(X0))),negate(f(a_real_number))),negate(g(a_real_number))),X2)
| ~ less_or_equalish(absolute(X1),epsilon_0)
| ~ equalish(X1,X2)
| less_or_equalish(X0,n0) ),
inference(resolution,[],[f421,f12]) ).
fof(f697,plain,
! [X2,X0,X1] :
( ~ equalish(add(add(f(xs(X2)),g(xs(X2))),negate(f(a_real_number))),X1)
| ~ equalish(X0,add(X1,negate(g(a_real_number))))
| less_or_equalish(X2,n0)
| ~ less_or_equalish(absolute(X0),epsilon_0) ),
inference(resolution,[],[f442,f16]) ).
fof(f745,plain,
! [X0,X1] :
( ~ equalish(X0,add(add(f(xs(X1)),add(g(xs(X1)),negate(f(a_real_number)))),negate(g(a_real_number))))
| less_or_equalish(X1,n0)
| ~ less_or_equalish(absolute(X0),epsilon_0) ),
inference(resolution,[],[f697,f11]) ).
fof(f754,plain,
! [X2,X0,X1] :
( ~ equalish(X2,add(add(f(xs(X0)),add(g(xs(X0)),negate(f(a_real_number)))),negate(g(a_real_number))))
| ~ less_or_equalish(absolute(X1),epsilon_0)
| less_or_equalish(X0,n0)
| ~ equalish(X1,X2) ),
inference(resolution,[],[f745,f13]) ).
fof(f758,plain,
! [X2,X0,X1] :
( ~ equalish(X2,add(f(xs(X1)),add(g(xs(X1)),negate(f(a_real_number)))))
| less_or_equalish(X1,n0)
| ~ equalish(X0,add(X2,negate(g(a_real_number))))
| ~ less_or_equalish(absolute(X0),epsilon_0) ),
inference(resolution,[],[f754,f16]) ).
fof(f812,plain,
! [X2,X3,X0,X1] :
( ~ equalish(X3,add(f(xs(X0)),add(g(xs(X0)),negate(f(a_real_number)))))
| ~ equalish(X1,add(X2,negate(g(a_real_number))))
| ~ less_or_equalish(absolute(X1),epsilon_0)
| less_or_equalish(X0,n0)
| ~ equalish(X2,X3) ),
inference(resolution,[],[f758,f13]) ).
fof(f909,plain,
! [X2,X0,X1] :
( ~ equalish(X1,add(add(f(xs(X2)),g(xs(X2))),negate(f(a_real_number))))
| ~ less_or_equalish(absolute(X0),epsilon_0)
| less_or_equalish(X2,n0)
| ~ equalish(X0,add(X1,negate(g(a_real_number)))) ),
inference(resolution,[],[f812,f11]) ).
fof(f923,plain,
! [X0,X1] :
( ~ equalish(X0,add(add(negate(f(a_real_number)),add(f(xs(X1)),g(xs(X1)))),negate(g(a_real_number))))
| less_or_equalish(X1,n0)
| ~ less_or_equalish(absolute(X0),epsilon_0) ),
inference(resolution,[],[f909,f10]) ).
fof(f931,plain,
! [X2,X0,X1] :
( ~ equalish(X2,add(add(negate(f(a_real_number)),add(f(xs(X0)),g(xs(X0)))),negate(g(a_real_number))))
| ~ less_or_equalish(absolute(X1),epsilon_0)
| less_or_equalish(X0,n0)
| ~ equalish(X1,X2) ),
inference(resolution,[],[f923,f13]) ).
fof(f935,plain,
! [X2,X0,X1] :
( ~ equalish(X2,add(negate(f(a_real_number)),add(f(xs(X1)),g(xs(X1)))))
| less_or_equalish(X1,n0)
| ~ equalish(X0,add(X2,negate(g(a_real_number))))
| ~ less_or_equalish(absolute(X0),epsilon_0) ),
inference(resolution,[],[f931,f16]) ).
fof(f956,plain,
! [X0,X1] :
( ~ equalish(X1,add(add(add(negate(f(a_real_number)),f(xs(X0))),g(xs(X0))),negate(g(a_real_number))))
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(X1),epsilon_0) ),
inference(resolution,[],[f935,f11]) ).
fof(f966,plain,
! [X0,X1] :
( ~ equalish(add(add(add(negate(f(a_real_number)),f(xs(X0))),g(xs(X0))),negate(g(a_real_number))),X1)
| ~ less_or_equalish(absolute(X1),epsilon_0)
| less_or_equalish(X0,n0) ),
inference(resolution,[],[f956,f12]) ).
fof(f967,plain,
! [X0] :
( ~ less_or_equalish(absolute(add(add(negate(f(a_real_number)),f(xs(X0))),add(g(xs(X0)),negate(g(a_real_number))))),epsilon_0)
| less_or_equalish(X0,n0) ),
inference(resolution,[],[f966,f11]) ).
fof(f977,plain,
! [X0,X1] :
( ~ less_or_equalish(absolute(add(add(negate(f(a_real_number)),f(xs(X0))),add(g(xs(X0)),negate(g(a_real_number))))),X1)
| ~ less_or_equalish(X1,epsilon_0)
| less_or_equalish(X0,n0) ),
inference(resolution,[],[f967,f9]) ).
fof(f982,plain,
! [X0] :
( ~ less_or_equalish(add(absolute(add(negate(f(a_real_number)),f(xs(X0)))),absolute(add(g(xs(X0)),negate(g(a_real_number))))),epsilon_0)
| less_or_equalish(X0,n0) ),
inference(resolution,[],[f977,f1]) ).
fof(f1316,plain,
! [X0] :
( ~ less_or_equalish(absolute(add(g(xs(X0)),negate(g(a_real_number)))),half(epsilon_0))
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(X0)))),half(epsilon_0)) ),
inference(resolution,[],[f982,f6]) ).
fof(f1321,plain,
! [X0] :
( ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(X0)))),half(epsilon_0))
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(add(xs(X0),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f1316,f21]) ).
fof(f1328,plain,
! [X0,X1] :
( ~ less_or_equalish(absolute(add(xs(X0),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equalish(X0,n0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(absolute(X1),half(epsilon_0))
| ~ equalish(X1,add(negate(f(a_real_number)),f(xs(X0)))) ),
inference(resolution,[],[f1321,f43]) ).
fof(f1330,plain,
! [X0,X1] :
( ~ less_or_equalish(absolute(add(xs(X0),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equalish(X0,n0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(X1,half(epsilon_0))
| ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(X0)))),X1) ),
inference(resolution,[],[f1321,f9]) ).
fof(f1332,plain,
! [X0] :
( less_or_equalish(delta_2(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(X0,half(epsilon_0))
| ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(delta_2(half(epsilon_0)))))),X0)
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(resolution,[],[f1330,f23]) ).
fof(f1337,plain,
! [X0] :
( ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(delta_2(half(epsilon_0)))))),X0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(X0,half(epsilon_0))
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(duplicate_literal_removal,[],[f1332]) ).
fof(f1346,plain,
! [X0] :
( ~ less_or_equalish(minimum(X0,absolute(add(negate(f(a_real_number)),f(xs(delta_2(half(epsilon_0))))))),half(epsilon_0))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_2(half(epsilon_0)),n0)
| ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(delta_2(half(epsilon_0)))))),X0) ),
inference(resolution,[],[f1337,f5]) ).
fof(f1375,plain,
( ~ less_or_equalish(absolute(add(negate(f(a_real_number)),f(xs(delta_2(half(epsilon_0)))))),half(epsilon_0))
| less_or_equalish(delta_2(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f1346,f2]) ).
fof(f1380,plain,
! [X0] :
( ~ equalish(X0,add(negate(f(a_real_number)),f(xs(delta_2(half(epsilon_0))))))
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(absolute(X0),half(epsilon_0))
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(resolution,[],[f1375,f43]) ).
fof(f1401,plain,
( ~ less_or_equalish(absolute(add(f(xs(delta_2(half(epsilon_0)))),negate(f(a_real_number)))),half(epsilon_0))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(resolution,[],[f1380,f10]) ).
fof(f1407,plain,
( less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_2(half(epsilon_0)),n0)
| ~ less_or_equalish(absolute(add(xs(delta_2(half(epsilon_0))),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f1401,f20]) ).
fof(f1412,plain,
( ~ less_or_equalish(absolute(add(xs(delta_2(half(epsilon_0))),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equalish(delta_2(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(duplicate_literal_removal,[],[f1407]) ).
fof(f1417,plain,
! [X0] :
( ~ less_or_equalish(absolute(add(xs(delta_2(half(epsilon_0))),negate(a_real_number))),X0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(X0,delta_1(half(epsilon_0)))
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(resolution,[],[f1412,f9]) ).
fof(f1419,plain,
( less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(delta_2(half(epsilon_0)),delta_1(half(epsilon_0)))
| less_or_equalish(delta_2(half(epsilon_0)),n0)
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(resolution,[],[f1417,f23]) ).
fof(f1432,plain,
( ~ less_or_equalish(delta_2(half(epsilon_0)),delta_1(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_2(half(epsilon_0)),n0) ),
inference(duplicate_literal_removal,[],[f1419]) ).
fof(f1435,plain,
! [X0] :
( less_or_equalish(delta_2(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(X0,delta_1(half(epsilon_0)))
| ~ less_or_equalish(delta_2(half(epsilon_0)),X0) ),
inference(resolution,[],[f1432,f9]) ).
fof(f1437,plain,
! [X0] :
( less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(X0,delta_1(half(epsilon_0)))
| ~ less_or_equalish(delta_2(half(epsilon_0)),X0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f1435,f19]) ).
fof(f1442,plain,
! [X0] :
( ~ less_or_equalish(delta_2(half(epsilon_0)),X0)
| ~ less_or_equalish(X0,delta_1(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(duplicate_literal_removal,[],[f1437]) ).
fof(f1447,plain,
! [X0] :
( ~ less_or_equalish(minimum(X0,delta_2(half(epsilon_0))),delta_1(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(delta_2(half(epsilon_0)),X0) ),
inference(resolution,[],[f1442,f5]) ).
fof(f1468,plain,
( ~ less_or_equalish(delta_2(half(epsilon_0)),delta_1(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f1447,f2]) ).
fof(f1473,plain,
( less_or_equalish(delta_1(half(epsilon_0)),delta_2(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f1468,f8]) ).
fof(f2156,plain,
! [X2,X0,X1] :
( ~ equalish(X1,add(negate(f(a_real_number)),f(xs(X0))))
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(absolute(X1),half(epsilon_0))
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(X2),delta_2(half(epsilon_0)))
| ~ equalish(X2,add(xs(X0),negate(a_real_number))) ),
inference(resolution,[],[f1328,f43]) ).
fof(f2168,plain,
! [X0,X1] :
( ~ less_or_equalish(absolute(add(f(xs(X0)),negate(f(a_real_number)))),half(epsilon_0))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(X1),delta_2(half(epsilon_0)))
| ~ equalish(X1,add(xs(X0),negate(a_real_number))) ),
inference(resolution,[],[f2156,f10]) ).
fof(f2439,plain,
! [X0,X1] :
( less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(X1),delta_2(half(epsilon_0)))
| ~ equalish(X1,add(xs(X0),negate(a_real_number)))
| ~ less_or_equalish(absolute(add(xs(X0),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f2168,f20]) ).
fof(f2444,plain,
! [X0,X1] :
( ~ less_or_equalish(absolute(add(xs(X0),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equalish(X0,n0)
| ~ less_or_equalish(absolute(X1),delta_2(half(epsilon_0)))
| ~ equalish(X1,add(xs(X0),negate(a_real_number)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(duplicate_literal_removal,[],[f2439]) ).
fof(f2446,plain,
! [X0] :
( less_or_equalish(delta_1(half(epsilon_0)),n0)
| ~ less_or_equalish(absolute(X0),delta_2(half(epsilon_0)))
| ~ equalish(X0,add(xs(delta_1(half(epsilon_0))),negate(a_real_number)))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_1(half(epsilon_0)),n0) ),
inference(resolution,[],[f2444,f23]) ).
fof(f2451,plain,
! [X0] :
( ~ equalish(X0,add(xs(delta_1(half(epsilon_0))),negate(a_real_number)))
| ~ less_or_equalish(absolute(X0),delta_2(half(epsilon_0)))
| less_or_equalish(delta_1(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(duplicate_literal_removal,[],[f2446]) ).
fof(f2456,plain,
! [X0,X1] :
( ~ equalish(X1,add(xs(delta_1(half(epsilon_0))),negate(a_real_number)))
| less_or_equalish(delta_1(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(absolute(X0),delta_2(half(epsilon_0)))
| ~ equalish(X0,X1) ),
inference(resolution,[],[f2451,f13]) ).
fof(f2496,plain,
! [X0,X1] :
( ~ equalish(add(xs(delta_1(half(epsilon_0))),negate(a_real_number)),X1)
| less_or_equalish(half(epsilon_0),n0)
| ~ less_or_equalish(absolute(X0),delta_2(half(epsilon_0)))
| ~ equalish(X0,X1)
| less_or_equalish(delta_1(half(epsilon_0)),n0) ),
inference(resolution,[],[f2456,f12]) ).
fof(f2586,plain,
! [X0] :
( ~ equalish(X0,add(negate(a_real_number),xs(delta_1(half(epsilon_0)))))
| ~ less_or_equalish(absolute(X0),delta_2(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_1(half(epsilon_0)),n0) ),
inference(resolution,[],[f2496,f10]) ).
fof(f2644,plain,
( ~ less_or_equalish(absolute(add(xs(delta_1(half(epsilon_0))),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_1(half(epsilon_0)),n0) ),
inference(resolution,[],[f2586,f10]) ).
fof(f2655,plain,
! [X0] :
( ~ less_or_equalish(absolute(add(xs(delta_1(half(epsilon_0))),negate(a_real_number))),X0)
| less_or_equalish(delta_1(half(epsilon_0)),n0)
| ~ less_or_equalish(X0,delta_2(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f2644,f9]) ).
fof(f2659,plain,
( less_or_equalish(delta_1(half(epsilon_0)),n0)
| ~ less_or_equalish(delta_1(half(epsilon_0)),delta_2(half(epsilon_0)))
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(delta_1(half(epsilon_0)),n0) ),
inference(resolution,[],[f2655,f23]) ).
fof(f2680,plain,
( ~ less_or_equalish(delta_1(half(epsilon_0)),delta_2(half(epsilon_0)))
| less_or_equalish(delta_1(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(duplicate_literal_removal,[],[f2659]) ).
fof(f2681,plain,
( less_or_equalish(delta_1(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f2680,f1473]) ).
fof(f2690,plain,
( less_or_equalish(delta_1(half(epsilon_0)),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(duplicate_literal_removal,[],[f2681]) ).
fof(f2691,plain,
( less_or_equalish(half(epsilon_0),n0)
| less_or_equalish(half(epsilon_0),n0) ),
inference(resolution,[],[f2690,f18]) ).
fof(f2696,plain,
less_or_equalish(half(epsilon_0),n0),
inference(duplicate_literal_removal,[],[f2691]) ).
fof(f2697,plain,
less_or_equalish(epsilon_0,n0),
inference(resolution,[],[f2696,f7]) ).
fof(f2700,plain,
$false,
inference(resolution,[],[f2697,f22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA005-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 % Computer : n001.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.23 % CPULimit : 300
% 0.08/0.23 % WCLimit : 300
% 0.08/0.23 % DateTime : Mon Sep 28 20:32:34 UTC 2026
% 0.08/0.24 % CPUTime :
% 0.08/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.30 Running first-order theorem proving
% 0.25/0.30 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
% 19.87/3.62 % (686436)Input is clausal, will run a generic CNF schedule.
% 19.87/3.62 % (686442)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3684347626:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.87/3.62 % (686447)dis-21_1_sil=8000:lcm=predicate:random_seed=2409649204: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)
% 19.87/3.62 % (686447)Instruction limit reached!
% 19.87/3.62 % (686447)------------------------------
% 19.87/3.62 % (686447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.62 % (686447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.62 % (686447)CaDiCaL version: 2.1.3
% 19.87/3.62 % (686447)Termination reason: Instruction limit
% 19.87/3.62 % (686447)Termination phase: Saturation
% 19.87/3.62 % (686447)Time elapsed: 0.080 s
% 19.87/3.62 % (686447)Peak memory usage: 89 MB
% 19.87/3.62 % (686447)Instructions burned: 117 (million)
% 19.87/3.62 % (686444)lrs+10_1_sil=8000:sp=occurrence:random_seed=637060728:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.87/3.62 % (686441)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=3909104881:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.87/3.62 % (686445)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2003034646:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.87/3.62 % (686446)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1064064732:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.87/3.62 % (686443)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1071766287:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.87/3.62 % (686444)Instruction limit reached!
% 19.87/3.62 % (686444)------------------------------
% 19.87/3.62 % (686444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.62 % (686444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.62 % (686444)CaDiCaL version: 2.1.3
% 19.87/3.62 % (686444)Termination reason: Instruction limit
% 19.87/3.62 % (686444)Termination phase: Saturation
% 19.87/3.62 % (686444)Time elapsed: 0.097 s
% 19.87/3.62 % (686444)Peak memory usage: 88 MB
% 19.87/3.62 % (686444)Instructions burned: 107 (million)
% 19.87/3.62 % (686445)Instruction limit reached!
% 19.87/3.62 % (686445)------------------------------
% 19.87/3.62 % (686445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.62 % (686445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.62 % (686445)CaDiCaL version: 2.1.3
% 19.87/3.62 % (686445)Termination reason: Instruction limit
% 19.87/3.62 % (686445)Termination phase: Saturation
% 19.87/3.62 % (686445)Time elapsed: 0.106 s
% 19.87/3.62 % (686445)Peak memory usage: 88 MB
% 19.87/3.62 % (686445)Instructions burned: 115 (million)
% 19.87/3.62 % (686446)Instruction limit reached!
% 19.87/3.62 % (686446)------------------------------
% 19.87/3.62 % (686446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.62 % (686446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.62 % (686446)CaDiCaL version: 2.1.3
% 19.87/3.62 % (686446)Termination reason: Instruction limit
% 19.87/3.62 % (686446)Termination phase: Saturation
% 19.87/3.62 % (686446)Time elapsed: 0.180 s
% 19.87/3.62 % (686446)Peak memory usage: 89 MB
% 19.87/3.62 % (686446)Instructions burned: 180 (million)
% 19.87/3.62 % (686450)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=1861559812:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 19.87/3.62 % (686450)Instruction limit reached!
% 19.87/3.62 % (686450)------------------------------
% 19.87/3.62 % (686450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.62 % (686450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.62 % (686450)CaDiCaL version: 2.1.3
% 19.87/3.62 % (686450)Termination reason: Instruction limit
% 19.87/3.62 % (686450)Termination phase: Saturation
% 19.87/3.62 % (686450)Time elapsed: 0.099 s
% 19.87/3.62 % (686450)Peak memory usage: 88 MB
% 19.87/3.62 % (686450)Instructions burned: 145 (million)
% 19.87/3.62 % (686456)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3772148805:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 39.15/6.29 % (686457)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1991342668:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 39.15/6.29 % (686458)lrs+10_64_to=lpo:sil=8000:random_seed=2440800740:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 39.15/6.29 % (686456)Instruction limit reached!
% 39.15/6.29 % (686456)------------------------------
% 39.15/6.29 % (686456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.15/6.29 % (686456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/6.29 % (686456)CaDiCaL version: 2.1.3
% 39.15/6.29 % (686456)Termination reason: Instruction limit
% 39.15/6.29 % (686456)Termination phase: Saturation
% 39.15/6.29 % (686456)Time elapsed: 0.182 s
% 39.15/6.29 % (686456)Peak memory usage: 90 MB
% 39.15/6.29 % (686456)Instructions burned: 189 (million)
% 39.15/6.29 % (686458)Instruction limit reached!
% 39.15/6.29 % (686458)------------------------------
% 39.15/6.29 % (686458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.15/6.29 % (686458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/6.29 % (686458)CaDiCaL version: 2.1.3
% 39.15/6.29 % (686458)Termination reason: Instruction limit
% 39.15/6.29 % (686458)Termination phase: Saturation
% 39.15/6.29 % (686458)Time elapsed: 0.104 s
% 39.15/6.29 % (686458)Peak memory usage: 89 MB
% 39.15/6.29 % (686458)Instructions burned: 126 (million)
% 39.15/6.29 % (686457)Instruction limit reached!
% 39.15/6.29 % (686457)------------------------------
% 39.15/6.29 % (686457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.15/6.29 % (686457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/6.29 % (686457)CaDiCaL version: 2.1.3
% 39.15/6.29 % (686457)Termination reason: Instruction limit
% 39.15/6.29 % (686457)Termination phase: Saturation
% 39.15/6.29 % (686457)Time elapsed: 0.192 s
% 39.15/6.29 % (686457)Peak memory usage: 88 MB
% 39.15/6.29 % (686457)Instructions burned: 219 (million)
% 39.15/6.29 % (686461)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1327802325:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 39.15/6.29 % (686465)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3953688119:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 39.15/6.29 % (686461)Instruction limit reached!
% 39.15/6.29 % (686461)------------------------------
% 39.15/6.29 % (686461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.15/6.29 % (686461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/6.29 % (686461)CaDiCaL version: 2.1.3
% 39.15/6.29 % (686461)Termination reason: Instruction limit
% 39.15/6.29 % (686461)Termination phase: Saturation
% 39.15/6.29 % (686461)Time elapsed: 0.165 s
% 39.15/6.29 % (686461)Peak memory usage: 88 MB
% 39.15/6.29 % (686461)Instructions burned: 194 (million)
% 39.15/6.29 % (686464)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1200606422:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 39.15/6.29 % (686466)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=4064401294:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 39.15/6.29 % (686466)Instruction limit reached!
% 39.15/6.29 % (686466)------------------------------
% 39.15/6.29 % (686466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.15/6.29 % (686466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/6.29 % (686466)CaDiCaL version: 2.1.3
% 39.15/6.29 % (686466)Termination reason: Instruction limit
% 39.15/6.29 % (686466)Termination phase: Saturation
% 39.15/6.29 % (686466)Time elapsed: 0.100 s
% 39.15/6.29 % (686466)Peak memory usage: 89 MB
% 39.15/6.29 % (686466)Instructions burned: 106 (million)
% 39.15/6.29 % (686464)Instruction limit reached!
% 39.15/6.29 % (686464)------------------------------
% 39.15/6.29 % (686464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.15/6.29 % (686464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.15/6.29 % (686464)CaDiCaL version: 2.1.3
% 39.15/6.29 % (686464)Termination reason: Instruction limit
% 39.15/6.29 % (686464)Termination phase: Saturation
% 39.15/6.29 % (686464)Time elapsed: 0.164 s
% 73.58/11.06 % (686464)Peak memory usage: 89 MB
% 73.58/11.06 % (686464)Instructions burned: 157 (million)
% 73.58/11.06 % (686469)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1499699375:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 73.58/11.06 % (686469)Instruction limit reached!
% 73.58/11.06 % (686469)------------------------------
% 73.58/11.06 % (686469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.58/11.06 % (686469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.58/11.06 % (686469)CaDiCaL version: 2.1.3
% 73.58/11.06 % (686469)Termination reason: Instruction limit
% 73.58/11.06 % (686469)Termination phase: Saturation
% 73.58/11.06 % (686469)Time elapsed: 0.083 s
% 73.58/11.06 % (686469)Peak memory usage: 88 MB
% 73.58/11.06 % (686469)Instructions burned: 107 (million)
% 73.58/11.06 % (686473)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1915419193:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 73.58/11.06 % (686472)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2489838839:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 73.58/11.06 % (686476)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=735341944:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 73.58/11.06 % (686472)Instruction limit reached!
% 73.58/11.06 % (686472)------------------------------
% 73.58/11.06 % (686472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.58/11.06 % (686472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.58/11.06 % (686472)CaDiCaL version: 2.1.3
% 73.58/11.06 % (686472)Termination reason: Instruction limit
% 73.58/11.06 % (686472)Termination phase: Saturation
% 73.58/11.06 % (686472)Time elapsed: 0.259 s
% 73.58/11.06 % (686472)Peak memory usage: 89 MB
% 73.58/11.06 % (686472)Instructions burned: 242 (million)
% 73.58/11.06 % (686476)Instruction limit reached!
% 73.58/11.06 % (686476)------------------------------
% 73.58/11.06 % (686476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.58/11.06 % (686476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.58/11.06 % (686476)CaDiCaL version: 2.1.3
% 73.58/11.06 % (686476)Termination reason: Instruction limit
% 73.58/11.06 % (686476)Termination phase: Saturation
% 73.58/11.06 % (686476)Time elapsed: 0.097 s
% 73.58/11.06 % (686476)Peak memory usage: 87 MB
% 73.58/11.06 % (686476)Instructions burned: 134 (million)
% 73.58/11.06 % (686481)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3518341902:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 73.58/11.06 % (686482)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2757186849:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 73.58/11.06 % (686482)Instruction limit reached!
% 73.58/11.06 % (686482)------------------------------
% 73.58/11.06 % (686482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.58/11.06 % (686482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.58/11.06 % (686482)CaDiCaL version: 2.1.3
% 73.58/11.06 % (686482)Termination reason: Instruction limit
% 73.58/11.06 % (686482)Termination phase: Saturation
% 73.58/11.06 % (686482)Time elapsed: 0.164 s
% 73.58/11.06 % (686482)Peak memory usage: 90 MB
% 73.58/11.06 % (686482)Instructions burned: 191 (million)
% 73.58/11.06 % (686481)Instruction limit reached!
% 73.58/11.06 % (686481)------------------------------
% 73.58/11.06 % (686481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.58/11.06 % (686481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.58/11.06 % (686481)CaDiCaL version: 2.1.3
% 73.58/11.06 % (686481)Termination reason: Instruction limit
% 73.58/11.06 % (686481)Termination phase: Saturation
% 73.58/11.06 % (686481)Time elapsed: 0.464 s
% 73.58/11.06 % (686481)Peak memory usage: 97 MB
% 73.58/11.06 % (686481)Instructions burned: 499 (million)
% 73.58/11.06 % (686485)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1949919729:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 73.58/11.06 % (686485)Instruction limit reached!
% 73.58/11.06 % (686485)------------------------------
% 73.58/11.06 % (686485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.58/11.06 % (686485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.56/14.85 % (686485)CaDiCaL version: 2.1.3
% 99.56/14.85 % (686485)Termination reason: Instruction limit
% 99.56/14.85 % (686485)Termination phase: Saturation
% 99.56/14.85 % (686485)Time elapsed: 0.244 s
% 99.56/14.85 % (686485)Peak memory usage: 92 MB
% 99.56/14.85 % (686485)Instructions burned: 264 (million)
% 99.56/14.85 % (686486)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1131357207:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 99.56/14.85 % (686486)Instruction limit reached!
% 99.56/14.85 % (686486)------------------------------
% 99.56/14.85 % (686486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.56/14.85 % (686486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.56/14.85 % (686486)CaDiCaL version: 2.1.3
% 99.56/14.85 % (686486)Termination reason: Instruction limit
% 99.56/14.85 % (686486)Termination phase: Saturation
% 99.56/14.85 % (686486)Time elapsed: 0.161 s
% 99.56/14.85 % (686486)Peak memory usage: 90 MB
% 99.56/14.85 % (686486)Instructions burned: 156 (million)
% 99.56/14.85 % (686489)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=2835996729:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 99.56/14.85 % (686490)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3440571650:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 99.56/14.85 % (686490)Instruction limit reached!
% 99.56/14.85 % (686490)------------------------------
% 99.56/14.85 % (686490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.56/14.85 % (686490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.56/14.85 % (686490)CaDiCaL version: 2.1.3
% 99.56/14.85 % (686490)Termination reason: Instruction limit
% 99.56/14.85 % (686490)Termination phase: Saturation
% 99.56/14.85 % (686490)Time elapsed: 0.424 s
% 99.56/14.85 % (686490)Peak memory usage: 89 MB
% 99.56/14.85 % (686490)Instructions burned: 538 (million)
% 99.56/14.85 % (686493)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2646774017:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi)
% 99.56/14.85 % (686493)Instruction limit reached!
% 99.56/14.85 % (686493)------------------------------
% 99.56/14.85 % (686493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.56/14.85 % (686493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.56/14.85 % (686493)CaDiCaL version: 2.1.3
% 99.56/14.85 % (686493)Termination reason: Instruction limit
% 99.56/14.85 % (686493)Termination phase: Saturation
% 99.56/14.85 % (686493)Time elapsed: 0.170 s
% 99.56/14.85 % (686493)Peak memory usage: 90 MB
% 99.56/14.85 % (686493)Instructions burned: 180 (million)
% 99.56/14.85 % (686465)Instruction limit reached!
% 99.56/14.85 % (686465)------------------------------
% 99.56/14.85 % (686465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.56/14.85 % (686465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.56/14.85 % (686465)CaDiCaL version: 2.1.3
% 99.56/14.85 % (686465)Termination reason: Instruction limit
% 99.56/14.85 % (686465)Termination phase: Saturation
% 99.56/14.85 % (686465)Time elapsed: 3.338 s
% 99.56/14.85 % (686465)Peak memory usage: 142 MB
% 99.56/14.85 % (686465)Instructions burned: 3394 (million)
% 99.56/14.85 % (686495)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=1066820855:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 99.56/14.85 % (686496)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=64817882:i=412:gtgl=4:gtg=exists_all_2955 on theBenchmark for (2955ds/412Mi)
% 99.56/14.85 % (686496)Instruction limit reached!
% 99.56/14.85 % (686496)------------------------------
% 99.56/14.85 % (686496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.56/14.85 % (686496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.56/14.85 % (686496)CaDiCaL version: 2.1.3
% 99.56/14.85 % (686496)Termination reason: Instruction limit
% 99.56/14.85 % (686496)Termination phase: Saturation
% 99.56/14.85 % (686496)Time elapsed: 0.481 s
% 99.56/14.85 % (686496)Peak memory usage: 92 MB
% 99.56/14.85 % (686496)Instructions burned: 412 (million)
% 99.56/14.85 % (686499)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=772911665:s2pl=no:i=8478:s2at=4:nm=6_2947 on theBenchmark for (2947ds/8478Mi)
% 145.81/21.25 % (686489)Instruction limit reached!
% 145.81/21.25 % (686489)------------------------------
% 145.81/21.25 % (686489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.81/21.25 % (686489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.81/21.25 % (686489)CaDiCaL version: 2.1.3
% 145.81/21.25 % (686489)Termination reason: Instruction limit
% 145.81/21.25 % (686489)Termination phase: Saturation
% 145.81/21.25 % (686489)Time elapsed: 3.187 s
% 145.81/21.25 % (686489)Peak memory usage: 153 MB
% 145.81/21.25 % (686489)Instructions burned: 3256 (million)
% 145.81/21.25 % (686473)Instruction limit reached!
% 145.81/21.25 % (686473)------------------------------
% 145.81/21.25 % (686473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.81/21.25 % (686473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.81/21.25 % (686473)CaDiCaL version: 2.1.3
% 145.81/21.25 % (686473)Termination reason: Instruction limit
% 145.81/21.25 % (686473)Termination phase: Saturation
% 145.81/21.25 % (686473)Time elapsed: 5.091 s
% 145.81/21.25 % (686473)Peak memory usage: 158 MB
% 145.81/21.25 % (686473)Instructions burned: 5208 (million)
% 145.81/21.25 % (686501)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=3607413712:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2936 on theBenchmark for (2936ds/303Mi)
% 145.81/21.25 % (686501)Instruction limit reached!
% 145.81/21.25 % (686501)------------------------------
% 145.81/21.25 % (686501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.81/21.25 % (686501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.81/21.25 % (686501)CaDiCaL version: 2.1.3
% 145.81/21.25 % (686501)Termination reason: Instruction limit
% 145.81/21.25 % (686501)Termination phase: Saturation
% 145.81/21.25 % (686501)Time elapsed: 0.268 s
% 145.81/21.25 % (686501)Peak memory usage: 91 MB
% 145.81/21.25 % (686501)Instructions burned: 303 (million)
% 145.81/21.25 % (686502)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2781876427:st=4:i=720:sd=3:fsr=off:ss=axioms_2933 on theBenchmark for (2933ds/720Mi)
% 145.81/21.25 % (686504)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1413219221:i=598:bs=on:bd=preordered:av=off:ss=axioms_2930 on theBenchmark for (2930ds/598Mi)
% 145.81/21.25 % (686502)Instruction limit reached!
% 145.81/21.25 % (686502)------------------------------
% 145.81/21.25 % (686502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.81/21.25 % (686502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.81/21.25 % (686502)CaDiCaL version: 2.1.3
% 145.81/21.25 % (686502)Termination reason: Instruction limit
% 145.81/21.25 % (686502)Termination phase: Saturation
% 145.81/21.25 % (686502)Time elapsed: 0.650 s
% 145.81/21.25 % (686502)Peak memory usage: 94 MB
% 145.81/21.25 % (686502)Instructions burned: 721 (million)
% 145.81/21.25 % (686504)Instruction limit reached!
% 145.81/21.25 % (686504)------------------------------
% 145.81/21.25 % (686504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.81/21.25 % (686504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.81/21.25 % (686504)CaDiCaL version: 2.1.3
% 145.81/21.25 % (686504)Termination reason: Instruction limit
% 145.81/21.25 % (686504)Termination phase: Saturation
% 145.81/21.25 % (686504)Time elapsed: 0.571 s
% 145.81/21.25 % (686504)Peak memory usage: 91 MB
% 145.81/21.25 % (686504)Instructions burned: 599 (million)
% 145.81/21.25 % (686507)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3125944696:i=2989:sd=3:ss=axioms:sgt=60_2923 on theBenchmark for (2923ds/2989Mi)
% 145.81/21.25 % (686508)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=2102513806:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2921 on theBenchmark for (2921ds/1997Mi)
% 145.81/21.25 % (686508)Instruction limit reached!
% 145.81/21.25 % (686508)------------------------------
% 145.81/21.25 % (686508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.81/21.25 % (686508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.81/21.25 % (686508)CaDiCaL version: 2.1.3
% 145.81/21.25 % (686508)Termination reason: Instruction limit
% 201.47/29.05 % (686508)Termination phase: Saturation
% 201.47/29.05 % (686508)Time elapsed: 2.204 s
% 201.47/29.05 % (686508)Peak memory usage: 137 MB
% 201.47/29.05 % (686508)Instructions burned: 1997 (million)
% 201.47/29.05 % (686511)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=459897090:i=2088:bd=preordered:av=off_2896 on theBenchmark for (2896ds/2088Mi)
% 201.47/29.05 % (686507)Instruction limit reached!
% 201.47/29.05 % (686507)------------------------------
% 201.47/29.05 % (686507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.47/29.05 % (686507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.47/29.05 % (686507)CaDiCaL version: 2.1.3
% 201.47/29.05 % (686507)Termination reason: Instruction limit
% 201.47/29.05 % (686507)Termination phase: Saturation
% 201.47/29.05 % (686507)Time elapsed: 3.392 s
% 201.47/29.05 % (686507)Peak memory usage: 144 MB
% 201.47/29.05 % (686507)Instructions burned: 2989 (million)
% 201.47/29.05 % (686513)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2516214633:i=1098:nicw=on_2886 on theBenchmark for (2886ds/1098Mi)
% 201.47/29.05 % (686513)Instruction limit reached!
% 201.47/29.05 % (686513)------------------------------
% 201.47/29.05 % (686513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.47/29.05 % (686513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.47/29.05 % (686513)CaDiCaL version: 2.1.3
% 201.47/29.05 % (686513)Termination reason: Instruction limit
% 201.47/29.05 % (686513)Termination phase: Saturation
% 201.47/29.05 % (686513)Time elapsed: 0.923 s
% 201.47/29.05 % (686513)Peak memory usage: 108 MB
% 201.47/29.05 % (686513)Instructions burned: 1099 (million)
% 201.47/29.05 % (686515)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3720891846:i=433:bd=preordered_2874 on theBenchmark for (2874ds/433Mi)
% 201.47/29.05 % (686511)Instruction limit reached!
% 201.47/29.05 % (686511)------------------------------
% 201.47/29.05 % (686511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.47/29.05 % (686511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.47/29.05 % (686511)CaDiCaL version: 2.1.3
% 201.47/29.05 % (686511)Termination reason: Instruction limit
% 201.47/29.05 % (686511)Termination phase: Saturation
% 201.47/29.05 % (686511)Time elapsed: 2.272 s
% 201.47/29.05 % (686511)Peak memory usage: 136 MB
% 201.47/29.05 % (686511)Instructions burned: 2088 (million)
% 201.47/29.05 % (686495)Instruction limit reached!
% 201.47/29.05 % (686495)------------------------------
% 201.47/29.05 % (686495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.47/29.05 % (686495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.47/29.05 % (686495)CaDiCaL version: 2.1.3
% 201.47/29.05 % (686495)Termination reason: Instruction limit
% 201.47/29.05 % (686495)Termination phase: Saturation
% 201.47/29.05 % (686495)Time elapsed: 8.623 s
% 201.47/29.05 % (686495)Peak memory usage: 150 MB
% 201.47/29.05 % (686495)Instructions burned: 10307 (million)
% 201.47/29.05 % (686517)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3593540770:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2871 on theBenchmark for (2871ds/2942Mi)
% 201.47/29.05 % (686515)Instruction limit reached!
% 201.47/29.05 % (686515)------------------------------
% 201.47/29.05 % (686515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.47/29.05 % (686515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.47/29.05 % (686515)CaDiCaL version: 2.1.3
% 201.47/29.05 % (686515)Termination reason: Instruction limit
% 201.47/29.05 % (686515)Termination phase: Saturation
% 201.47/29.05 % (686515)Time elapsed: 0.427 s
% 201.47/29.05 % (686515)Peak memory usage: 96 MB
% 201.47/29.05 % (686515)Instructions burned: 433 (million)
% 201.47/29.05 % (686519)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1744687868:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2868 on theBenchmark for (2868ds/6922Mi)
% 201.47/29.05 % (686520)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=1750494169:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2867 on theBenchmark for (2867ds/596Mi)
% 201.47/29.05 % (686520)Instruction limit reached!
% 201.47/29.05 % (686520)------------------------------
% 201.47/29.05 % (686520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.68/31.54 % (686520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.68/31.54 % (686520)CaDiCaL version: 2.1.3
% 218.68/31.54 % (686520)Termination reason: Instruction limit
% 218.68/31.54 % (686520)Termination phase: Saturation
% 218.68/31.54 % (686520)Time elapsed: 0.509 s
% 218.68/31.54 % (686520)Peak memory usage: 95 MB
% 218.68/31.54 % (686520)Instructions burned: 596 (million)
% 218.68/31.54 % (686499)Instruction limit reached!
% 218.68/31.54 % (686499)------------------------------
% 218.68/31.54 % (686499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.68/31.54 % (686499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.68/31.54 % (686499)CaDiCaL version: 2.1.3
% 218.68/31.54 % (686499)Termination reason: Instruction limit
% 218.68/31.54 % (686499)Termination phase: Saturation
% 218.68/31.54 % (686499)Time elapsed: 8.771 s
% 218.68/31.54 % (686499)Peak memory usage: 205 MB
% 218.68/31.54 % (686499)Instructions burned: 8478 (million)
% 218.68/31.54 % (686523)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=807087438:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2858 on theBenchmark for (2858ds/4123Mi)
% 218.68/31.54 % (686524)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1940858273:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2856 on theBenchmark for (2856ds/16411Mi)
% 218.68/31.54 % (686517)Instruction limit reached!
% 218.68/31.54 % (686517)------------------------------
% 218.68/31.54 % (686517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.68/31.54 % (686517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.68/31.54 % (686517)CaDiCaL version: 2.1.3
% 218.68/31.54 % (686517)Termination reason: Instruction limit
% 218.68/31.54 % (686517)Termination phase: Saturation
% 218.68/31.54 % (686517)Time elapsed: 3.019 s
% 218.68/31.54 % (686517)Peak memory usage: 136 MB
% 218.68/31.54 % (686517)Instructions burned: 2942 (million)
% 218.68/31.54 % (686527)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3065566480:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2837 on theBenchmark for (2837ds/1670Mi)
% 218.68/31.54 % (686527)Instruction limit reached!
% 218.68/31.54 % (686527)------------------------------
% 218.68/31.54 % (686527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.68/31.54 % (686527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.68/31.54 % (686527)CaDiCaL version: 2.1.3
% 218.68/31.54 % (686527)Termination reason: Instruction limit
% 218.68/31.54 % (686527)Termination phase: Saturation
% 218.68/31.54 % (686527)Time elapsed: 1.707 s
% 218.68/31.54 % (686527)Peak memory usage: 136 MB
% 218.68/31.54 % (686527)Instructions burned: 1671 (million)
% 218.68/31.54 % (686523)Instruction limit reached!
% 218.68/31.54 % (686523)------------------------------
% 218.68/31.54 % (686523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.68/31.54 % (686523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.68/31.54 % (686523)CaDiCaL version: 2.1.3
% 218.68/31.54 % (686523)Termination reason: Instruction limit
% 218.68/31.54 % (686523)Termination phase: Saturation
% 218.68/31.54 % (686523)Time elapsed: 4.099 s
% 218.68/31.54 % (686523)Peak memory usage: 160 MB
% 218.68/31.54 % (686523)Instructions burned: 4124 (million)
% 218.68/31.54 % (686533)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=2575703760:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2817 on theBenchmark for (2817ds/1722Mi)
% 218.68/31.54 % (686534)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=314745923:cts=off:cond=on:i=9530:bs=on:fsd=on_2814 on theBenchmark for (2814ds/9530Mi)
% 218.68/31.54 % (686533)Instruction limit reached!
% 218.68/31.54 % (686533)------------------------------
% 218.68/31.54 % (686533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.68/31.54 % (686533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.68/31.54 % (686533)CaDiCaL version: 2.1.3
% 218.68/31.54 % (686533)Termination reason: Instruction limit
% 218.68/31.54 % (686533)Termination phase: Saturation
% 218.68/31.54 % (686533)Time elapsed: 1.952 s
% 218.68/31.54 % (686533)Peak memory usage: 135 MB
% 238.71/34.37 % (686533)Instructions burned: 1722 (million)
% 238.71/34.37 % (686519)Instruction limit reached!
% 238.71/34.37 % (686519)------------------------------
% 238.71/34.37 % (686519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.71/34.37 % (686519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.71/34.37 % (686519)CaDiCaL version: 2.1.3
% 238.71/34.37 % (686519)Termination reason: Instruction limit
% 238.71/34.37 % (686519)Termination phase: Saturation
% 238.71/34.37 % (686519)Time elapsed: 7.324 s
% 238.71/34.37 % (686519)Peak memory usage: 188 MB
% 238.71/34.37 % (686519)Instructions burned: 6922 (million)
% 238.71/34.37 % (686537)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1006288568:st=2:i=4495:sd=10:ss=included_2794 on theBenchmark for (2794ds/4495Mi)
% 238.71/34.37 % (686539)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=3388754787:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2791 on theBenchmark for (2791ds/4920Mi)
% 238.71/34.37 % (686537)Instruction limit reached!
% 238.71/34.37 % (686537)------------------------------
% 238.71/34.37 % (686537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.71/34.37 % (686537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.71/34.37 % (686537)CaDiCaL version: 2.1.3
% 238.71/34.37 % (686537)Termination reason: Instruction limit
% 238.71/34.37 % (686537)Termination phase: Saturation
% 238.71/34.37 % (686537)Time elapsed: 4.538 s
% 238.71/34.37 % (686537)Peak memory usage: 152 MB
% 238.71/34.37 % (686537)Instructions burned: 4496 (million)
% 238.71/34.37 % (686543)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=2528833689:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2746 on theBenchmark for (2746ds/2083Mi)
% 238.71/34.37 % (686539)Instruction limit reached!
% 238.71/34.37 % (686539)------------------------------
% 238.71/34.37 % (686539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.71/34.37 % (686539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.71/34.37 % (686539)CaDiCaL version: 2.1.3
% 238.71/34.37 % (686539)Termination reason: Instruction limit
% 238.71/34.37 % (686539)Termination phase: Saturation
% 238.71/34.37 % (686539)Time elapsed: 5.0000 s
% 238.71/34.37 % (686539)Peak memory usage: 155 MB
% 238.71/34.37 % (686539)Instructions burned: 4920 (million)
% 238.71/34.37 % (686545)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=771741002:i=4629:av=off:gsp=on_2738 on theBenchmark for (2738ds/4629Mi)
% 238.71/34.37 % (686543)Instruction limit reached!
% 238.71/34.37 % (686543)------------------------------
% 238.71/34.37 % (686543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.71/34.37 % (686543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.71/34.37 % (686543)CaDiCaL version: 2.1.3
% 238.71/34.37 % (686543)Termination reason: Instruction limit
% 238.71/34.37 % (686543)Termination phase: Saturation
% 238.71/34.37 % (686543)Time elapsed: 1.811 s
% 238.71/34.37 % (686543)Peak memory usage: 132 MB
% 238.71/34.37 % (686543)Instructions burned: 2084 (million)
% 238.71/34.37 % (686590)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3256891231:i=1258:av=off_2725 on theBenchmark for (2725ds/1258Mi)
% 238.71/34.37 % (686534)Instruction limit reached!
% 238.71/34.37 % (686534)------------------------------
% 238.71/34.37 % (686534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.71/34.37 % (686534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.71/34.37 % (686534)CaDiCaL version: 2.1.3
% 238.71/34.37 % (686534)Termination reason: Instruction limit
% 238.71/34.37 % (686534)Termination phase: Saturation
% 238.71/34.37 % (686534)Time elapsed: 8.991 s
% 238.71/34.37 % (686534)Peak memory usage: 196 MB
% 238.71/34.37 % (686534)Instructions burned: 9530 (million)
% 238.71/34.37 % (686592)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3956797081:i=7343:av=off:ss=included_2721 on theBenchmark for (2721ds/7343Mi)
% 238.71/34.37 % (686590)Instruction limit reached!
% 238.71/34.37 % (686590)------------------------------
% 238.71/34.37 % (686590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.71/34.37 % (686590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.27/37.80 % (686590)CaDiCaL version: 2.1.3
% 262.27/37.80 % (686590)Termination reason: Instruction limit
% 262.27/37.80 % (686590)Termination phase: Saturation
% 262.27/37.80 % (686590)Time elapsed: 0.643 s
% 262.27/37.80 % (686590)Peak memory usage: 91 MB
% 262.27/37.80 % (686590)Instructions burned: 1258 (million)
% 262.27/37.80 % (686594)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3671445168:i=1325:sd=2:ss=axioms:sgt=16_2716 on theBenchmark for (2716ds/1325Mi)
% 262.27/37.80 % (686524)Instruction limit reached!
% 262.27/37.80 % (686524)------------------------------
% 262.27/37.80 % (686524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 262.27/37.80 % (686524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.27/37.80 % (686524)CaDiCaL version: 2.1.3
% 262.27/37.80 % (686524)Termination reason: Instruction limit
% 262.27/37.80 % (686524)Termination phase: Saturation
% 262.27/37.80 % (686524)Time elapsed: 14.185 s
% 262.27/37.80 % (686524)Peak memory usage: 174 MB
% 262.27/37.80 % (686524)Instructions burned: 16413 (million)
% 262.27/37.80 % (686596)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=586563552:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2711 on theBenchmark for (2711ds/2646Mi)
% 262.27/37.80 % (686594)Instruction limit reached!
% 262.27/37.80 % (686594)------------------------------
% 262.27/37.80 % (686594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 262.27/37.80 % (686594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.27/37.80 % (686594)CaDiCaL version: 2.1.3
% 262.27/37.80 % (686594)Termination reason: Instruction limit
% 262.27/37.80 % (686594)Termination phase: Saturation
% 262.27/37.80 % (686594)Time elapsed: 0.660 s
% 262.27/37.80 % (686594)Peak memory usage: 92 MB
% 262.27/37.80 % (686594)Instructions burned: 1325 (million)
% 262.27/37.80 % (686598)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=430799010:i=1489:sd=2:ep=R:ss=axioms_2708 on theBenchmark for (2708ds/1489Mi)
% 262.27/37.80 % (686545)Instruction limit reached!
% 262.27/37.80 % (686545)------------------------------
% 262.27/37.80 % (686545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 262.27/37.80 % (686545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.27/37.80 % (686545)CaDiCaL version: 2.1.3
% 262.27/37.80 % (686545)Termination reason: Instruction limit
% 262.27/37.80 % (686545)Termination phase: Saturation
% 262.27/37.80 % (686545)Time elapsed: 2.854 s
% 262.27/37.80 % (686545)Peak memory usage: 152 MB
% 262.27/37.80 % (686545)Instructions burned: 4631 (million)
% 262.27/37.80 % (686600)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=813783029:i=1503_2706 on theBenchmark for (2706ds/1503Mi)
% 262.27/37.80 % (686598)Instruction limit reached!
% 262.27/37.80 % (686598)------------------------------
% 262.27/37.80 % (686598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 262.27/37.80 % (686598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.27/37.80 % (686598)CaDiCaL version: 2.1.3
% 262.27/37.80 % (686598)Termination reason: Instruction limit
% 262.27/37.80 % (686598)Termination phase: Saturation
% 262.27/37.80 % (686598)Time elapsed: 0.932 s
% 262.27/37.80 % (686598)Peak memory usage: 134 MB
% 262.27/37.80 % (686598)Instructions burned: 1489 (million)
% 262.27/37.80 % (686602)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=392053010:i=13942:kws=frequency_2697 on theBenchmark for (2697ds/13942Mi)
% 262.27/37.80 % (686600)Instruction limit reached!
% 262.27/37.80 % (686600)------------------------------
% 262.27/37.80 % (686600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 262.27/37.80 % (686600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.27/37.80 % (686600)CaDiCaL version: 2.1.3
% 262.27/37.80 % (686600)Termination reason: Instruction limit
% 262.27/37.80 % (686600)Termination phase: Saturation
% 262.27/37.80 % (686600)Time elapsed: 0.944 s
% 262.27/37.80 % (686600)Peak memory usage: 133 MB
% 262.27/37.80 % (686600)Instructions burned: 1503 (million)
% 262.27/37.80 % (686604)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=3504047071:i=3604:fsr=off:er=filter_2695 on theBenchmark for (2695ds/3604Mi)
% 262.27/37.80 % (686596)Instruction limit reached!
% 262.27/37.80 % (686596)------------------------------
% 192.90/38.83 % (686596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686596)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686596)Termination reason: Instruction limit
% 192.90/38.83 % (686596)Termination phase: Saturation
% 192.90/38.83 % (686596)Time elapsed: 1.760 s
% 192.90/38.83 % (686596)Peak memory usage: 141 MB
% 192.90/38.83 % (686596)Instructions burned: 2647 (million)
% 192.90/38.83 % (686606)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=171455352:i=1876:sd=1:ss=included:sgt=32_2692 on theBenchmark for (2692ds/1876Mi)
% 192.90/38.83 % (686604)Instruction limit reached!
% 192.90/38.83 % (686604)------------------------------
% 192.90/38.83 % (686604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686604)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686604)Termination reason: Instruction limit
% 192.90/38.83 % (686604)Termination phase: Saturation
% 192.90/38.83 % (686604)Time elapsed: 1.472 s
% 192.90/38.83 % (686604)Peak memory usage: 153 MB
% 192.90/38.83 % (686604)Instructions burned: 3607 (million)
% 192.90/38.83 % (686606)Instruction limit reached!
% 192.90/38.83 % (686606)------------------------------
% 192.90/38.83 % (686606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686606)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686606)Termination reason: Instruction limit
% 192.90/38.83 % (686606)Termination phase: Saturation
% 192.90/38.83 % (686606)Time elapsed: 1.157 s
% 192.90/38.83 % (686606)Peak memory usage: 133 MB
% 192.90/38.83 % (686606)Instructions burned: 1877 (million)
% 192.90/38.83 % (686592)Instruction limit reached!
% 192.90/38.83 % (686592)------------------------------
% 192.90/38.83 % (686592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686592)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686592)Termination reason: Instruction limit
% 192.90/38.83 % (686592)Termination phase: Saturation
% 192.90/38.83 % (686592)Time elapsed: 4.149 s
% 192.90/38.83 % (686592)Peak memory usage: 171 MB
% 192.90/38.83 % (686592)Instructions burned: 7344 (million)
% 192.90/38.83 % (686608)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=4117160561:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2679 on theBenchmark for (2679ds/1932Mi)
% 192.90/38.83 % (686609)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=611071335:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2678 on theBenchmark for (2678ds/1980Mi)
% 192.90/38.83 % (686610)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=4221709728:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2678 on theBenchmark for (2678ds/3902Mi)
% 192.90/38.83 % (686608)Instruction limit reached!
% 192.90/38.83 % (686608)------------------------------
% 192.90/38.83 % (686608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686608)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686608)Termination reason: Instruction limit
% 192.90/38.83 % (686608)Termination phase: Saturation
% 192.90/38.83 % (686608)Time elapsed: 0.700 s
% 192.90/38.83 % (686608)Peak memory usage: 136 MB
% 192.90/38.83 % (686608)Instructions burned: 1933 (million)
% 192.90/38.83 % (686614)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=4098091956:avsq=on:i=3916:aac=none:amm=off_2670 on theBenchmark for (2670ds/3916Mi)
% 192.90/38.83 % (686609)Instruction limit reached!
% 192.90/38.83 % (686609)------------------------------
% 192.90/38.83 % (686609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686609)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686609)Termination reason: Instruction limit
% 192.90/38.83 % (686609)Termination phase: Saturation
% 192.90/38.83 % (686609)Time elapsed: 1.339 s
% 192.90/38.83 % (686609)Peak memory usage: 134 MB
% 192.90/38.83 % (686609)Instructions burned: 1980 (million)
% 192.90/38.83 % (686616)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3223255758:cond=on:i=3940:av=off:er=known_2663 on theBenchmark for (2663ds/3940Mi)
% 192.90/38.83 % (686614)Instruction limit reached!
% 192.90/38.83 % (686614)------------------------------
% 192.90/38.83 % (686614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686614)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686614)Termination reason: Instruction limit
% 192.90/38.83 % (686614)Termination phase: Saturation
% 192.90/38.83 % (686614)Time elapsed: 1.020 s
% 192.90/38.83 % (686614)Peak memory usage: 111 MB
% 192.90/38.83 % (686614)Instructions burned: 3920 (million)
% 192.90/38.83 % (686618)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1518581506:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2659 on theBenchmark for (2659ds/3980Mi)
% 192.90/38.83 % (686610)Instruction limit reached!
% 192.90/38.83 % (686610)------------------------------
% 192.90/38.83 % (686610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686610)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686610)Termination reason: Instruction limit
% 192.90/38.83 % (686610)Termination phase: Saturation
% 192.90/38.83 % (686610)Time elapsed: 2.531 s
% 192.90/38.83 % (686610)Peak memory usage: 156 MB
% 192.90/38.83 % (686610)Instructions burned: 3902 (million)
% 192.90/38.83 % (686620)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=1310856328:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2651 on theBenchmark for (2651ds/2087Mi)
% 192.90/38.83 % (686618)Instruction limit reached!
% 192.90/38.83 % (686618)------------------------------
% 192.90/38.83 % (686618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686618)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686618)Termination reason: Instruction limit
% 192.90/38.83 % (686618)Termination phase: Saturation
% 192.90/38.83 % (686618)Time elapsed: 1.290 s
% 192.90/38.83 % (686618)Peak memory usage: 146 MB
% 192.90/38.83 % (686618)Instructions burned: 3984 (million)
% 192.90/38.83 % (686639)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=2731823420:cts=off:cond=on:i=4272:bs=on:fsd=on_2644 on theBenchmark for (2644ds/4272Mi)
% 192.90/38.83 % (686616)Instruction limit reached!
% 192.90/38.83 % (686616)------------------------------
% 192.90/38.83 % (686616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686616)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686616)Termination reason: Instruction limit
% 192.90/38.83 % (686616)Termination phase: Saturation
% 192.90/38.83 % (686616)Time elapsed: 2.307 s
% 192.90/38.83 % (686616)Peak memory usage: 150 MB
% 192.90/38.83 % (686616)Instructions burned: 3941 (million)
% 192.90/38.83 % (686738)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2163539530:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2638 on theBenchmark for (2638ds/2197Mi)
% 192.90/38.83 % (686620)Instruction limit reached!
% 192.90/38.83 % (686620)------------------------------
% 192.90/38.83 % (686620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686620)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686620)Termination reason: Instruction limit
% 192.90/38.83 % (686620)Termination phase: Saturation
% 192.90/38.83 % (686620)Time elapsed: 1.401 s
% 192.90/38.83 % (686620)Peak memory usage: 138 MB
% 192.90/38.83 % (686620)Instructions burned: 2088 (million)
% 192.90/38.83 % (686740)dis+21_1_sil=8000:spb=goal_then_units:random_seed=687080671:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2635 on theBenchmark for (2635ds/6508Mi)
% 192.90/38.83 % (686639)Instruction limit reached!
% 192.90/38.83 % (686639)------------------------------
% 192.90/38.83 % (686639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686639)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686639)Termination reason: Instruction limit
% 192.90/38.83 % (686639)Termination phase: Saturation
% 192.90/38.83 % (686639)Time elapsed: 1.428 s
% 192.90/38.83 % (686639)Peak memory usage: 155 MB
% 192.90/38.83 % (686639)Instructions burned: 4273 (million)
% 192.90/38.83 % (686742)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=906369982:i=2330:fgj=on:av=off:fsr=off_2629 on theBenchmark for (2629ds/2330Mi)
% 192.90/38.83 % (686738)Instruction limit reached!
% 192.90/38.83 % (686738)------------------------------
% 192.90/38.83 % (686738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.90/38.83 % (686738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.90/38.83 % (686738)CaDiCaL version: 2.1.3
% 192.90/38.83 % (686738)Termination reason: Instruction limit
% 192.90/38.83 % (686738)Termination phase: Saturation
% 192.90/38.83 % (686738)Time elapsed: 1.350 s
% 192.90/38.83 % (686738)Peak memory usage: 140 MB
% 192.90/38.83 % (686738)Instructions burned: 2198 (million)
% 192.90/38.83 % (686744)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2925270846:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2623 on theBenchmark for (2623ds/7592Mi)
% 192.90/38.83 % (686742)First to succeed.
% 192.90/38.83 % (686742)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-686436"
% 192.90/38.83 % (686742)Refutation found. Thanks to Tanya!
% 192.90/38.83 % SZS status Unsatisfiable for theBenchmark
% 192.90/38.83 % SZS output start Proof for theBenchmark
% See solution above
% 270.51/39.03 % (686742)------------------------------
% 270.51/39.03 % (686742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.51/39.03 % (686742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.51/39.03 % (686742)CaDiCaL version: 2.1.3
% 270.51/39.03 % (686742)Termination reason: Refutation
% 270.51/39.03 % (686742)Time elapsed: 0.636 s
% 270.51/39.03 % (686742)Peak memory usage: 133 MB
% 270.51/39.03 % (686742)Instructions burned: 1683 (million)
% 270.51/39.03 % (686742)------------------------------
% 270.51/39.03 % (686742)------------------------------
% 270.51/39.03 % (686436)Success in time 38.076 s
% 270.51/39.03 % Vampire exiting
%------------------------------------------------------------------------------