%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG442-1 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:20:02 AM UTC 2026
% Result : Unsatisfiable 121.51s 17.98s
% Output : Refutation 123.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 16
% Syntax : Number of formulae : 124 ( 72 unt; 0 def)
% Number of atoms : 198 ( 12 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 149 ( 75 ~; 74 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-4 aty)
% Number of variables : 245 ( 245 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : m(X0,X0,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos) ).
fof(f2,axiom,
! [X0,X1] : m(X0,X1,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_001) ).
fof(f3,axiom,
! [X0] : u(X0,X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_002) ).
fof(f5,axiom,
! [X0,X1] : u(X0,X0,X1) = u(X0,X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_004) ).
fof(f6,axiom,
! [X0,X1] : u(X0,X0,X1) = u(X1,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_005) ).
fof(f7,axiom,
! [X0,X1] : v(X0,X0,X0,X1) = v(X0,X0,X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_006) ).
fof(f8,axiom,
! [X0,X1] : v(X0,X0,X1,X0) = v(X0,X1,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_007) ).
fof(f9,axiom,
! [X0,X1] : v(X0,X1,X0,X0) = v(X1,X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_008) ).
fof(f10,axiom,
! [X0,X1] : u(X0,X0,X1) = v(X0,X0,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_009) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| ~ r(X6,X7,X8)
| r(m(X0,X3,X6),m(X1,X4,X7),m(X2,X5,X8)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_010) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| ~ r(X6,X7,X8)
| r(u(X0,X3,X6),u(X1,X4,X7),u(X2,X5,X8)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_011) ).
fof(f13,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| ~ r(X6,X7,X8)
| ~ r(X9,X10,X11)
| r(v(X0,X3,X6,X9),v(X1,X4,X7,X10),v(X2,X5,X8,X11)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_012) ).
fof(f14,axiom,
r(a,a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_013) ).
fof(f15,axiom,
r(a,b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_014) ).
fof(f16,axiom,
r(b,a,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_015) ).
fof(f17,negated_conjecture,
~ r(a,a,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f18,plain,
! [X0,X1] : u(X0,X0,X1) = v(X0,X0,X1,X0),
inference(forward_demodulation,[],[f7,f10]) ).
fof(f21,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(m(a,X0,X3),m(a,X1,X4),m(b,X2,X5)) ),
inference(resolution,[],[f11,f14]) ).
fof(f22,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(m(b,X0,X3),m(a,X1,X4),m(a,X2,X5)) ),
inference(resolution,[],[f11,f16]) ).
fof(f23,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| ~ r(X6,X7,X8)
| r(v(a,X0,X3,X6),v(b,X1,X4,X7),v(a,X2,X5,X8)) ),
inference(resolution,[],[f13,f15]) ).
fof(f24,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| ~ r(X6,X7,X8)
| r(v(a,X0,X3,X6),v(a,X1,X4,X7),v(b,X2,X5,X8)) ),
inference(resolution,[],[f13,f14]) ).
fof(f25,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| ~ r(X6,X7,X8)
| r(v(b,X0,X3,X6),v(a,X1,X4,X7),v(a,X2,X5,X8)) ),
inference(resolution,[],[f13,f16]) ).
fof(f28,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(u(b,X0,X3),u(a,X1,X4),u(a,X2,X5)) ),
inference(resolution,[],[f12,f16]) ).
fof(f32,plain,
! [X0,X1] : v(X0,X1,X1,X1) = v(X1,X1,X0,X1),
inference(superposition,[],[f8,f9]) ).
fof(f33,plain,
! [X0,X1] : v(X0,X1,X1,X1) = u(X1,X1,X0),
inference(forward_demodulation,[],[f32,f18]) ).
fof(f66,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(v(b,a,X0,X3),v(a,a,X1,X4),v(a,b,X2,X5)) ),
inference(resolution,[],[f25,f14]) ).
fof(f67,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(v(b,b,X0,X3),v(a,a,X1,X4),v(a,a,X2,X5)) ),
inference(resolution,[],[f25,f16]) ).
fof(f70,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(v(a,b,X0,X3),v(b,a,X1,X4),v(a,a,X2,X5)) ),
inference(resolution,[],[f23,f16]) ).
fof(f71,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(v(a,a,X0,X3),v(a,b,X1,X4),v(b,a,X2,X5)) ),
inference(resolution,[],[f24,f15]) ).
fof(f73,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(v(a,b,X0,X3),v(a,a,X1,X4),v(b,a,X2,X5)) ),
inference(resolution,[],[f24,f16]) ).
fof(f74,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(u(b,a,X0),u(a,b,X1),u(a,a,X2)) ),
inference(resolution,[],[f28,f15]) ).
fof(f82,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,a,a,X0),v(a,a,b,X1),v(a,b,a,X2)) ),
inference(resolution,[],[f66,f15]) ).
fof(f83,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,a,a,X0),v(a,a,a,X1),v(a,b,b,X2)) ),
inference(resolution,[],[f66,f14]) ).
fof(f86,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,a,a,X0),u(a,a,X1),v(a,b,b,X2)) ),
inference(forward_demodulation,[],[f83,f10]) ).
fof(f89,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,b,a,X0),v(a,a,b,X1),v(a,a,a,X2)) ),
inference(resolution,[],[f67,f15]) ).
fof(f90,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,b,a,X0),v(a,a,a,X1),v(a,a,b,X2)) ),
inference(resolution,[],[f67,f14]) ).
fof(f93,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,b,a,X0),u(a,a,X1),v(a,a,b,X2)) ),
inference(forward_demodulation,[],[f90,f10]) ).
fof(f94,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(b,b,a,X0),v(a,a,b,X1),u(a,a,X2)) ),
inference(forward_demodulation,[],[f89,f10]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(a,b,a,X0),v(b,a,a,X1),v(a,a,b,X2)) ),
inference(resolution,[],[f70,f14]) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(a,b,a,X0),v(a,a,a,X1),v(b,a,b,X2)) ),
inference(resolution,[],[f73,f14]) ).
fof(f212,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(a,b,a,X0),u(a,a,X1),v(b,a,b,X2)) ),
inference(forward_demodulation,[],[f206,f10]) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(v(a,a,a,X0),v(a,b,a,X1),v(b,a,b,X2)) ),
inference(resolution,[],[f71,f14]) ).
fof(f225,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(u(a,a,X0),v(a,b,a,X1),v(b,a,b,X2)) ),
inference(forward_demodulation,[],[f221,f10]) ).
fof(f303,plain,
r(v(b,a,a,a),v(a,a,b,b),v(a,b,a,a)),
inference(resolution,[],[f82,f15]) ).
fof(f308,plain,
r(v(b,a,a,a),v(a,a,b,b),v(a,a,b,a)),
inference(forward_demodulation,[],[f303,f8]) ).
fof(f313,plain,
r(v(b,a,a,a),v(a,a,b,b),u(a,a,b)),
inference(forward_demodulation,[],[f308,f18]) ).
fof(f316,plain,
r(v(a,b,a,a),v(a,a,b,b),u(a,a,b)),
inference(forward_demodulation,[],[f313,f9]) ).
fof(f318,plain,
r(v(a,a,b,a),v(a,a,b,b),u(a,a,b)),
inference(forward_demodulation,[],[f316,f8]) ).
fof(f319,plain,
r(u(a,a,b),v(a,a,b,b),u(a,a,b)),
inference(forward_demodulation,[],[f318,f18]) ).
fof(f628,plain,
r(v(b,a,a,a),u(a,a,a),v(a,b,b,b)),
inference(resolution,[],[f86,f14]) ).
fof(f631,plain,
r(v(b,a,a,a),u(a,a,a),u(b,b,a)),
inference(forward_demodulation,[],[f628,f33]) ).
fof(f635,plain,
r(v(b,a,a,a),u(a,a,a),u(a,b,b)),
inference(forward_demodulation,[],[f631,f6]) ).
fof(f638,plain,
r(v(b,a,a,a),a,u(a,b,b)),
inference(forward_demodulation,[],[f635,f3]) ).
fof(f640,plain,
r(v(a,b,a,a),a,u(a,b,b)),
inference(forward_demodulation,[],[f638,f9]) ).
fof(f641,plain,
r(v(a,a,b,a),a,u(a,b,b)),
inference(forward_demodulation,[],[f640,f8]) ).
fof(f642,plain,
r(u(a,a,b),a,u(a,b,b)),
inference(forward_demodulation,[],[f641,f18]) ).
fof(f1009,plain,
r(v(b,b,a,a),u(a,a,b),v(a,a,b,a)),
inference(resolution,[],[f93,f15]) ).
fof(f1014,plain,
r(v(b,b,a,a),u(a,a,b),u(a,a,b)),
inference(forward_demodulation,[],[f1009,f18]) ).
fof(f1099,plain,
r(v(b,b,a,a),v(a,a,b,b),u(a,a,a)),
inference(resolution,[],[f94,f15]) ).
fof(f1104,plain,
r(v(b,b,a,a),v(a,a,b,b),a),
inference(forward_demodulation,[],[f1099,f3]) ).
fof(f1349,plain,
r(v(a,b,a,b),v(b,a,a,a),v(a,a,b,a)),
inference(resolution,[],[f198,f16]) ).
fof(f1352,plain,
r(v(a,b,a,b),v(b,a,a,a),u(a,a,b)),
inference(forward_demodulation,[],[f1349,f18]) ).
fof(f1368,plain,
r(v(a,b,a,b),v(a,b,a,a),u(a,a,b)),
inference(forward_demodulation,[],[f1352,f9]) ).
fof(f1377,plain,
r(v(a,b,a,b),v(a,a,b,a),u(a,a,b)),
inference(forward_demodulation,[],[f1368,f8]) ).
fof(f1386,plain,
r(v(a,b,a,b),u(a,a,b),u(a,a,b)),
inference(forward_demodulation,[],[f1377,f18]) ).
fof(f1766,plain,
r(u(b,a,a),u(a,b,a),u(a,a,b)),
inference(resolution,[],[f74,f14]) ).
fof(f1773,plain,
r(u(b,a,a),u(a,a,b),u(a,a,b)),
inference(forward_demodulation,[],[f1766,f5]) ).
fof(f1789,plain,
r(u(a,a,b),u(a,a,b),u(a,a,b)),
inference(forward_demodulation,[],[f1773,f6]) ).
fof(f1792,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r(X0,X1,X2)
| ~ r(X3,X4,X5)
| r(m(u(a,a,b),X0,X3),m(u(a,a,b),X1,X4),m(u(a,a,b),X2,X5)) ),
inference(resolution,[],[f1789,f11]) ).
fof(f2290,plain,
r(v(a,b,a,a),u(a,a,b),v(b,a,b,a)),
inference(resolution,[],[f212,f15]) ).
fof(f2292,plain,
r(v(a,b,a,b),u(a,a,a),v(b,a,b,a)),
inference(resolution,[],[f212,f16]) ).
fof(f2296,plain,
r(v(a,b,a,b),a,v(b,a,b,a)),
inference(forward_demodulation,[],[f2292,f3]) ).
fof(f2298,plain,
r(v(a,a,b,a),u(a,a,b),v(b,a,b,a)),
inference(forward_demodulation,[],[f2290,f8]) ).
fof(f2309,plain,
r(u(a,a,b),u(a,a,b),v(b,a,b,a)),
inference(forward_demodulation,[],[f2298,f18]) ).
fof(f3069,plain,
r(u(a,a,a),v(a,b,a,a),v(b,a,b,b)),
inference(resolution,[],[f225,f14]) ).
fof(f3077,plain,
r(u(a,a,a),v(a,b,a,a),v(a,b,b,b)),
inference(forward_demodulation,[],[f3069,f9]) ).
fof(f3091,plain,
r(u(a,a,a),v(a,b,a,a),u(b,b,a)),
inference(forward_demodulation,[],[f3077,f33]) ).
fof(f3103,plain,
r(u(a,a,a),v(a,b,a,a),u(a,b,b)),
inference(forward_demodulation,[],[f3091,f6]) ).
fof(f3105,plain,
r(u(a,a,a),v(a,a,b,a),u(a,b,b)),
inference(forward_demodulation,[],[f3103,f8]) ).
fof(f3106,plain,
r(u(a,a,a),u(a,a,b),u(a,b,b)),
inference(forward_demodulation,[],[f3105,f18]) ).
fof(f3107,plain,
r(a,u(a,a,b),u(a,b,b)),
inference(forward_demodulation,[],[f3106,f3]) ).
fof(f5141,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),u(a,a,b),X0),m(u(a,a,b),u(a,a,b),X1),m(u(a,a,b),v(b,a,b,a),X2)) ),
inference(resolution,[],[f1792,f2309]) ).
fof(f5145,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),u(a,a,b),X0),m(u(a,a,b),v(a,a,b,b),X1),m(u(a,a,b),u(a,a,b),X2)) ),
inference(resolution,[],[f1792,f319]) ).
fof(f5162,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),v(b,b,a,a),X0),m(u(a,a,b),u(a,a,b),X1),m(u(a,a,b),u(a,a,b),X2)) ),
inference(resolution,[],[f1792,f1014]) ).
fof(f5163,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),v(a,b,a,b),X0),m(u(a,a,b),u(a,a,b),X1),m(u(a,a,b),u(a,a,b),X2)) ),
inference(resolution,[],[f1792,f1386]) ).
fof(f5191,plain,
! [X2,X0,X1] :
( r(m(u(a,a,b),v(a,b,a,b),X0),m(u(a,a,b),u(a,a,b),X1),X2)
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f5163,f1]) ).
fof(f5192,plain,
! [X2,X0,X1] :
( r(m(u(a,a,b),v(b,b,a,a),X0),m(u(a,a,b),u(a,a,b),X1),X2)
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f5162,f1]) ).
fof(f5203,plain,
! [X2,X0,X1] :
( r(m(u(a,a,b),u(a,a,b),X0),m(u(a,a,b),v(a,a,b,b),X1),X2)
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f5145,f1]) ).
fof(f5207,plain,
! [X2,X0,X1] :
( r(m(u(a,a,b),u(a,a,b),X0),X1,m(u(a,a,b),v(b,a,b,a),X2))
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f5141,f1]) ).
fof(f5214,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),v(a,b,a,b),X0),X1,X2) ),
inference(forward_demodulation,[],[f5191,f1]) ).
fof(f5215,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),v(b,b,a,a),X0),X1,X2) ),
inference(forward_demodulation,[],[f5192,f1]) ).
fof(f5223,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(X0,m(u(a,a,b),v(a,a,b,b),X1),X2) ),
inference(forward_demodulation,[],[f5203,f1]) ).
fof(f5226,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(X0,X1,m(u(a,a,b),v(b,a,b,a),X2)) ),
inference(forward_demodulation,[],[f5207,f1]) ).
fof(f5488,plain,
r(v(b,b,a,a),m(u(a,a,b),v(a,a,b,b),v(a,a,b,b)),a),
inference(resolution,[],[f5223,f1104]) ).
fof(f5515,plain,
r(v(b,b,a,a),u(a,a,b),a),
inference(forward_demodulation,[],[f5488,f2]) ).
fof(f5894,plain,
r(v(a,b,a,b),a,m(u(a,a,b),v(b,a,b,a),v(b,a,b,a))),
inference(resolution,[],[f5226,f2296]) ).
fof(f5914,plain,
r(v(a,b,a,b),a,u(a,a,b)),
inference(forward_demodulation,[],[f5894,f2]) ).
fof(f7933,plain,
r(m(u(a,a,b),v(a,b,a,b),v(a,b,a,b)),a,u(a,a,b)),
inference(resolution,[],[f5914,f5214]) ).
fof(f7949,plain,
r(u(a,a,b),a,u(a,a,b)),
inference(forward_demodulation,[],[f7933,f2]) ).
fof(f13554,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(u(a,a,b),u(a,a,b),X0),m(u(a,a,b),a,X1),m(u(a,a,b),u(a,a,b),X2)) ),
inference(resolution,[],[f7949,f1792]) ).
fof(f13573,plain,
! [X2,X0,X1] :
( r(m(u(a,a,b),u(a,a,b),X0),m(u(a,a,b),a,X1),X2)
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f13554,f1]) ).
fof(f13609,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(X0,m(u(a,a,b),a,X1),X2) ),
inference(forward_demodulation,[],[f13573,f1]) ).
fof(f13724,plain,
r(b,m(u(a,a,b),a,a),a),
inference(resolution,[],[f13609,f16]) ).
fof(f13727,plain,
r(b,u(a,a,b),a),
inference(forward_demodulation,[],[f13724,f2]) ).
fof(f13772,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(b,b,X0),m(a,u(a,a,b),X1),m(a,a,X2)) ),
inference(resolution,[],[f13727,f22]) ).
fof(f13882,plain,
! [X2,X0,X1] :
( r(m(b,b,X0),m(a,u(a,a,b),X1),X2)
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f13772,f1]) ).
fof(f13901,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(X0,m(a,u(a,a,b),X1),X2) ),
inference(forward_demodulation,[],[f13882,f1]) ).
fof(f14139,plain,
r(v(b,b,a,a),m(a,u(a,a,b),u(a,a,b)),a),
inference(resolution,[],[f13901,f5515]) ).
fof(f14162,plain,
r(a,m(a,u(a,a,b),u(a,a,b)),u(a,b,b)),
inference(resolution,[],[f13901,f3107]) ).
fof(f14182,plain,
r(a,a,u(a,b,b)),
inference(forward_demodulation,[],[f14162,f2]) ).
fof(f14189,plain,
r(v(b,b,a,a),a,a),
inference(forward_demodulation,[],[f14139,f2]) ).
fof(f14267,plain,
r(m(u(a,a,b),v(b,b,a,a),v(b,b,a,a)),a,a),
inference(resolution,[],[f14189,f5215]) ).
fof(f14285,plain,
r(u(a,a,b),a,a),
inference(forward_demodulation,[],[f14267,f2]) ).
fof(f15582,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(a,a,X0),m(a,a,X1),m(b,u(a,b,b),X2)) ),
inference(resolution,[],[f14182,f21]) ).
fof(f15705,plain,
! [X2,X0,X1] :
( r(m(a,a,X0),X1,m(b,u(a,b,b),X2))
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f15582,f1]) ).
fof(f15732,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(X0,X1,m(b,u(a,b,b),X2)) ),
inference(forward_demodulation,[],[f15705,f1]) ).
fof(f15961,plain,
r(u(a,a,b),a,m(b,u(a,b,b),u(a,b,b))),
inference(resolution,[],[f15732,f642]) ).
fof(f16038,plain,
r(u(a,a,b),a,b),
inference(forward_demodulation,[],[f15961,f2]) ).
fof(f16043,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(a,u(a,a,b),X0),m(a,a,X1),m(b,b,X2)) ),
inference(resolution,[],[f16038,f21]) ).
fof(f16158,plain,
! [X2,X0,X1] :
( r(m(a,u(a,a,b),X0),m(a,a,X1),X2)
| ~ r(X0,X1,X2) ),
inference(forward_demodulation,[],[f16043,f1]) ).
fof(f16176,plain,
! [X2,X0,X1] :
( ~ r(X0,X1,X2)
| r(m(a,u(a,a,b),X0),X1,X2) ),
inference(forward_demodulation,[],[f16158,f1]) ).
fof(f16400,plain,
r(m(a,u(a,a,b),u(a,a,b)),a,a),
inference(resolution,[],[f16176,f14285]) ).
fof(f16471,plain,
r(a,a,a),
inference(forward_demodulation,[],[f16400,f2]) ).
fof(f16500,plain,
$false,
inference(forward_subsumption_resolution,[],[f16471,f17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG442-1 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.17 % Computer : n003.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Mon Sep 28 20:25:58 UTC 2026
% 0.11/0.17 % CPUTime :
% 0.11/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.20 Running first-order theorem proving
% 0.11/0.20 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
% 10.27/2.08 % (1951132)Input is clausal, will run a generic CNF schedule.
% 10.27/2.08 % (1951143)dis-21_1_sil=8000:lcm=predicate:random_seed=2128986411: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)
% 10.27/2.08 % (1951143)Refutation not found, incomplete strategy
% 10.27/2.08 % (1951143)------------------------------
% 10.27/2.08 % (1951143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/2.08 % (1951143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/2.08 % (1951143)CaDiCaL version: 2.1.3
% 10.27/2.08 % (1951143)Termination reason: Refutation not found, incomplete strategy
% 10.27/2.08 % (1951143)Time elapsed: 0.001 s
% 10.27/2.08 % (1951143)Peak memory usage: 88 MB
% 10.27/2.08 % (1951143)Instructions burned: 1 (million)
% 10.27/2.08 % (1951142)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1544314400:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.27/2.08 % (1951137)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=4237804122:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.27/2.08 % (1951141)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3318259153:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.27/2.08 % (1951138)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3237953452:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.27/2.08 % (1951140)lrs+10_1_sil=8000:sp=occurrence:random_seed=1777935131:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.27/2.08 % (1951139)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2391513723:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.27/2.08 % (1951141)Instruction limit reached!
% 10.27/2.08 % (1951141)------------------------------
% 10.27/2.08 % (1951141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/2.08 % (1951141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/2.08 % (1951141)CaDiCaL version: 2.1.3
% 10.27/2.08 % (1951141)Termination reason: Instruction limit
% 10.27/2.08 % (1951141)Termination phase: Saturation
% 10.27/2.08 % (1951141)Time elapsed: 0.059 s
% 10.27/2.08 % (1951141)Peak memory usage: 88 MB
% 10.27/2.08 % (1951141)Instructions burned: 116 (million)
% 10.27/2.08 % (1951140)Instruction limit reached!
% 10.27/2.08 % (1951140)------------------------------
% 10.27/2.08 % (1951140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/2.08 % (1951140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/2.08 % (1951140)CaDiCaL version: 2.1.3
% 10.27/2.08 % (1951140)Termination reason: Instruction limit
% 10.27/2.08 % (1951140)Termination phase: Saturation
% 10.27/2.08 % (1951140)Time elapsed: 0.060 s
% 10.27/2.08 % (1951140)Peak memory usage: 88 MB
% 10.27/2.08 % (1951140)Instructions burned: 107 (million)
% 10.27/2.08 % (1951142)Instruction limit reached!
% 10.27/2.08 % (1951142)------------------------------
% 10.27/2.08 % (1951142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/2.08 % (1951142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/2.08 % (1951142)CaDiCaL version: 2.1.3
% 10.27/2.08 % (1951142)Termination reason: Instruction limit
% 10.27/2.08 % (1951142)Termination phase: Saturation
% 10.27/2.08 % (1951142)Time elapsed: 0.107 s
% 10.27/2.08 % (1951142)Peak memory usage: 89 MB
% 10.27/2.08 % (1951142)Instructions burned: 181 (million)
% 10.27/2.08 % (1951143)------------------------------
% 10.27/2.08 % (1951143)------------------------------
% 10.27/2.08 % (1951152)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=159955239:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.27/2.08 % (1951152)Refutation not found, incomplete strategy
% 10.27/2.08 % (1951152)------------------------------
% 10.27/2.08 % (1951152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.27/2.08 % (1951152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.27/2.08 % (1951152)CaDiCaL version: 2.1.3
% 10.27/2.08 % (1951152)Termination reason: Refutation not found, incomplete strategy
% 10.27/2.08 % (1951152)Time elapsed: 0.001 s
% 18.53/3.26 % (1951152)Peak memory usage: 88 MB
% 18.53/3.26 % (1951152)Instructions burned: 1 (million)
% 18.53/3.26 % (1951151)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=4191665962:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 18.53/3.26 % (1951151)Refutation not found, incomplete strategy
% 18.53/3.26 % (1951151)------------------------------
% 18.53/3.26 % (1951151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.26 % (1951151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.26 % (1951151)CaDiCaL version: 2.1.3
% 18.53/3.26 % (1951151)Termination reason: Refutation not found, incomplete strategy
% 18.53/3.26 % (1951151)Time elapsed: 0.001 s
% 18.53/3.26 % (1951151)Peak memory usage: 88 MB
% 18.53/3.26 % (1951151)Instructions burned: 1 (million)
% 18.53/3.26 % (1951154)lrs+10_64_to=lpo:sil=8000:random_seed=522919300:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 18.53/3.26 % (1951153)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3766134540:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.53/3.26 % (1951153)Refutation not found, incomplete strategy
% 18.53/3.26 % (1951153)------------------------------
% 18.53/3.26 % (1951153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.26 % (1951153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.26 % (1951153)CaDiCaL version: 2.1.3
% 18.53/3.26 % (1951153)Termination reason: Refutation not found, incomplete strategy
% 18.53/3.26 % (1951153)Time elapsed: 0.001 s
% 18.53/3.26 % (1951153)Peak memory usage: 87 MB
% 18.53/3.26 % (1951154)Instruction limit reached!
% 18.53/3.26 % (1951154)------------------------------
% 18.53/3.26 % (1951154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.26 % (1951154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.26 % (1951154)CaDiCaL version: 2.1.3
% 18.53/3.26 % (1951154)Termination reason: Instruction limit
% 18.53/3.26 % (1951154)Termination phase: Saturation
% 18.53/3.26 % (1951154)Time elapsed: 0.073 s
% 18.53/3.26 % (1951154)Peak memory usage: 89 MB
% 18.53/3.26 % (1951154)Instructions burned: 127 (million)
% 18.53/3.26 % (1951153)------------------------------
% 18.53/3.26 % (1951153)------------------------------
% 18.53/3.26 % (1951159)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2632914313:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.53/3.26 % (1951152)------------------------------
% 18.53/3.26 % (1951152)------------------------------
% 18.53/3.26 % (1951151)------------------------------
% 18.53/3.26 % (1951151)------------------------------
% 18.53/3.26 % (1951160)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2107366098:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.53/3.26 % (1951160)Instruction limit reached!
% 18.53/3.26 % (1951160)------------------------------
% 18.53/3.26 % (1951160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.26 % (1951160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.26 % (1951160)CaDiCaL version: 2.1.3
% 18.53/3.26 % (1951160)Termination reason: Instruction limit
% 18.53/3.26 % (1951160)Termination phase: Saturation
% 18.53/3.26 % (1951160)Time elapsed: 0.048 s
% 18.53/3.26 % (1951160)Peak memory usage: 89 MB
% 18.53/3.26 % (1951160)Instructions burned: 159 (million)
% 18.53/3.26 % (1951159)Instruction limit reached!
% 18.53/3.26 % (1951159)------------------------------
% 18.53/3.26 % (1951159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.53/3.26 % (1951159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.53/3.26 % (1951159)CaDiCaL version: 2.1.3
% 18.53/3.26 % (1951159)Termination reason: Instruction limit
% 18.53/3.26 % (1951159)Termination phase: Saturation
% 18.53/3.26 % (1951159)Time elapsed: 0.124 s
% 18.53/3.26 % (1951159)Peak memory usage: 90 MB
% 18.53/3.26 % (1951159)Instructions burned: 195 (million)
% 18.53/3.26 % (1951163)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=1840205361:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 18.53/3.26 % (1951162)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3524893415:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.53/3.26 % (1951163)Instruction limit reached!
% 28.89/4.75 % (1951163)------------------------------
% 28.89/4.75 % (1951163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.89/4.75 % (1951163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.89/4.75 % (1951163)CaDiCaL version: 2.1.3
% 28.89/4.75 % (1951163)Termination reason: Instruction limit
% 28.89/4.75 % (1951163)Termination phase: Saturation
% 28.89/4.75 % (1951163)Time elapsed: 0.049 s
% 28.89/4.75 % (1951163)Peak memory usage: 89 MB
% 28.89/4.75 % (1951163)Instructions burned: 107 (million)
% 28.89/4.75 % (1951165)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3083357408:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 28.89/4.75 % (1951165)Refutation not found, incomplete strategy
% 28.89/4.75 % (1951165)------------------------------
% 28.89/4.75 % (1951165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.89/4.75 % (1951165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.89/4.75 % (1951165)CaDiCaL version: 2.1.3
% 28.89/4.75 % (1951165)Termination reason: Refutation not found, incomplete strategy
% 28.89/4.75 % (1951165)Time elapsed: 0.001 s
% 28.89/4.75 % (1951165)Peak memory usage: 87 MB
% 28.89/4.75 % (1951166)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1542410361:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 28.89/4.75 % (1951169)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=405418327:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 28.89/4.75 % (1951166)Instruction limit reached!
% 28.89/4.75 % (1951166)------------------------------
% 28.89/4.75 % (1951166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.89/4.75 % (1951166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.89/4.75 % (1951166)CaDiCaL version: 2.1.3
% 28.89/4.75 % (1951166)Termination reason: Instruction limit
% 28.89/4.75 % (1951166)Termination phase: Saturation
% 28.89/4.75 % (1951166)Time elapsed: 0.154 s
% 28.89/4.75 % (1951166)Peak memory usage: 90 MB
% 28.89/4.75 % (1951166)Instructions burned: 243 (million)
% 28.89/4.75 % (1951165)------------------------------
% 28.89/4.75 % (1951165)------------------------------
% 28.89/4.75 % (1951173)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2157720195:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 28.89/4.75 % (1951174)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3157622158:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 28.89/4.75 % (1951173)Instruction limit reached!
% 28.89/4.75 % (1951173)------------------------------
% 28.89/4.75 % (1951173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.89/4.75 % (1951173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.89/4.75 % (1951173)CaDiCaL version: 2.1.3
% 28.89/4.75 % (1951173)Termination reason: Instruction limit
% 28.89/4.75 % (1951173)Termination phase: Saturation
% 28.89/4.75 % (1951173)Time elapsed: 0.089 s
% 28.89/4.75 % (1951173)Peak memory usage: 89 MB
% 28.89/4.75 % (1951173)Instructions burned: 134 (million)
% 28.89/4.75 % (1951177)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1273988185:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 28.89/4.75 % (1951174)Instruction limit reached!
% 28.89/4.75 % (1951174)------------------------------
% 28.89/4.75 % (1951174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.89/4.75 % (1951174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.89/4.75 % (1951174)CaDiCaL version: 2.1.3
% 28.89/4.75 % (1951174)Termination reason: Instruction limit
% 28.89/4.75 % (1951174)Termination phase: Saturation
% 28.89/4.75 % (1951174)Time elapsed: 0.229 s
% 28.89/4.75 % (1951174)Peak memory usage: 93 MB
% 28.89/4.75 % (1951174)Instructions burned: 501 (million)
% 28.89/4.75 % (1951177)Instruction limit reached!
% 28.89/4.75 % (1951177)------------------------------
% 28.89/4.75 % (1951177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.89/4.75 % (1951177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.89/4.75 % (1951177)CaDiCaL version: 2.1.3
% 28.89/4.75 % (1951177)Termination reason: Instruction limit
% 28.89/4.75 % (1951177)Termination phase: Saturation
% 28.89/4.75 % (1951177)Time elapsed: 0.114 s
% 49.57/7.69 % (1951177)Peak memory usage: 91 MB
% 49.57/7.69 % (1951177)Instructions burned: 191 (million)
% 49.57/7.69 % (1951179)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3417157000:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 49.57/7.69 % (1951180)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2963153321:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 49.57/7.69 % (1951180)Instruction limit reached!
% 49.57/7.69 % (1951180)------------------------------
% 49.57/7.69 % (1951180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.57/7.69 % (1951180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.57/7.69 % (1951180)CaDiCaL version: 2.1.3
% 49.57/7.69 % (1951180)Termination reason: Instruction limit
% 49.57/7.69 % (1951180)Termination phase: Saturation
% 49.57/7.69 % (1951180)Time elapsed: 0.086 s
% 49.57/7.69 % (1951180)Peak memory usage: 88 MB
% 49.57/7.69 % (1951180)Instructions burned: 156 (million)
% 49.57/7.69 % (1951179)Instruction limit reached!
% 49.57/7.69 % (1951179)------------------------------
% 49.57/7.69 % (1951179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.57/7.69 % (1951179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.57/7.69 % (1951179)CaDiCaL version: 2.1.3
% 49.57/7.69 % (1951179)Termination reason: Instruction limit
% 49.57/7.69 % (1951179)Termination phase: Saturation
% 49.57/7.69 % (1951179)Time elapsed: 0.140 s
% 49.57/7.69 % (1951179)Peak memory usage: 89 MB
% 49.57/7.69 % (1951179)Instructions burned: 265 (million)
% 49.57/7.69 % (1951183)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=3357670423:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 49.57/7.69 % (1951184)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2821897163:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 49.57/7.69 % (1951184)Instruction limit reached!
% 49.57/7.69 % (1951184)------------------------------
% 49.57/7.69 % (1951184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.57/7.69 % (1951184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.57/7.69 % (1951184)CaDiCaL version: 2.1.3
% 49.57/7.69 % (1951184)Termination reason: Instruction limit
% 49.57/7.69 % (1951184)Termination phase: Saturation
% 49.57/7.69 % (1951184)Time elapsed: 0.222 s
% 49.57/7.69 % (1951184)Peak memory usage: 88 MB
% 49.57/7.69 % (1951184)Instructions burned: 538 (million)
% 49.57/7.69 % (1951187)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=394143549:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 49.57/7.69 % (1951162)Instruction limit reached!
% 49.57/7.69 % (1951162)------------------------------
% 49.57/7.69 % (1951162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.57/7.69 % (1951162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.57/7.69 % (1951162)CaDiCaL version: 2.1.3
% 49.57/7.69 % (1951162)Termination reason: Instruction limit
% 49.57/7.69 % (1951162)Termination phase: Saturation
% 49.57/7.69 % (1951162)Time elapsed: 1.564 s
% 49.57/7.69 % (1951162)Peak memory usage: 138 MB
% 49.57/7.69 % (1951162)Instructions burned: 3395 (million)
% 49.57/7.69 % (1951187)Instruction limit reached!
% 49.57/7.69 % (1951187)------------------------------
% 49.57/7.69 % (1951187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.57/7.69 % (1951187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.57/7.69 % (1951187)CaDiCaL version: 2.1.3
% 49.57/7.69 % (1951187)Termination reason: Instruction limit
% 49.57/7.69 % (1951187)Termination phase: Saturation
% 49.57/7.69 % (1951187)Time elapsed: 0.080 s
% 49.57/7.69 % (1951187)Peak memory usage: 89 MB
% 49.57/7.69 % (1951187)Instructions burned: 181 (million)
% 49.57/7.69 % (1951189)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=4267807384:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 49.57/7.69 % (1951190)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=3467239397:i=412:gtgl=4:gtg=exists_all_2977 on theBenchmark for (2977ds/412Mi)
% 49.57/7.69 % (1951190)Instruction limit reached!
% 49.57/7.69 % (1951190)------------------------------
% 69.52/10.45 % (1951190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.52/10.45 % (1951190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.52/10.45 % (1951190)CaDiCaL version: 2.1.3
% 69.52/10.45 % (1951190)Termination reason: Instruction limit
% 69.52/10.45 % (1951190)Termination phase: Saturation
% 69.52/10.45 % (1951190)Time elapsed: 0.205 s
% 69.52/10.45 % (1951190)Peak memory usage: 90 MB
% 69.52/10.45 % (1951190)Instructions burned: 413 (million)
% 69.52/10.45 % (1951193)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=1690609047:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 69.52/10.45 % (1951183)Instruction limit reached!
% 69.52/10.45 % (1951183)------------------------------
% 69.52/10.45 % (1951183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.52/10.45 % (1951183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.52/10.45 % (1951183)CaDiCaL version: 2.1.3
% 69.52/10.45 % (1951183)Termination reason: Instruction limit
% 69.52/10.45 % (1951183)Termination phase: Saturation
% 69.52/10.45 % (1951183)Time elapsed: 1.754 s
% 69.52/10.45 % (1951183)Peak memory usage: 155 MB
% 69.52/10.45 % (1951183)Instructions burned: 3258 (million)
% 69.52/10.45 % (1951169)Instruction limit reached!
% 69.52/10.45 % (1951169)------------------------------
% 69.52/10.45 % (1951169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.52/10.45 % (1951169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.52/10.45 % (1951169)CaDiCaL version: 2.1.3
% 69.52/10.45 % (1951169)Termination reason: Instruction limit
% 69.52/10.45 % (1951169)Termination phase: Saturation
% 69.52/10.45 % (1951169)Time elapsed: 2.712 s
% 69.52/10.45 % (1951169)Peak memory usage: 145 MB
% 69.52/10.45 % (1951169)Instructions burned: 5208 (million)
% 69.52/10.45 % (1951195)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=105642430:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi)
% 69.52/10.45 % (1951196)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1477327810:st=4:i=720:sd=3:fsr=off:ss=axioms_2963 on theBenchmark for (2963ds/720Mi)
% 69.52/10.45 % (1951196)Refutation not found, incomplete strategy
% 69.52/10.45 % (1951196)------------------------------
% 69.52/10.45 % (1951196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.52/10.45 % (1951196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.52/10.45 % (1951196)CaDiCaL version: 2.1.3
% 69.52/10.45 % (1951196)Termination reason: Refutation not found, incomplete strategy
% 69.52/10.45 % (1951196)Time elapsed: 0.001 s
% 69.52/10.45 % (1951196)Peak memory usage: 88 MB
% 69.52/10.45 % (1951196)Instructions burned: 1 (million)
% 69.52/10.45 % (1951195)Instruction limit reached!
% 69.52/10.45 % (1951195)------------------------------
% 69.52/10.45 % (1951195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.52/10.45 % (1951195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.52/10.45 % (1951195)CaDiCaL version: 2.1.3
% 69.52/10.45 % (1951195)Termination reason: Instruction limit
% 69.52/10.45 % (1951195)Termination phase: Saturation
% 69.52/10.45 % (1951195)Time elapsed: 0.144 s
% 69.52/10.45 % (1951195)Peak memory usage: 92 MB
% 69.52/10.45 % (1951195)Instructions burned: 304 (million)
% 69.52/10.45 % (1951199)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2488345607:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi)
% 69.52/10.45 % (1951199)Refutation not found, incomplete strategy
% 69.52/10.45 % (1951199)------------------------------
% 69.52/10.45 % (1951199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.52/10.45 % (1951199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.52/10.45 % (1951199)CaDiCaL version: 2.1.3
% 69.52/10.45 % (1951199)Termination reason: Refutation not found, incomplete strategy
% 69.52/10.45 % (1951199)Time elapsed: 0.0000 s
% 69.52/10.45 % (1951199)Peak memory usage: 86 MB
% 69.52/10.45 % (1951196)------------------------------
% 69.52/10.45 % (1951196)------------------------------
% 69.52/10.45 % (1951201)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1738880865:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi)
% 100.29/14.94 % (1951199)------------------------------
% 100.29/14.94 % (1951199)------------------------------
% 100.29/14.94 % (1951203)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=1069047735:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2957 on theBenchmark for (2957ds/1997Mi)
% 100.29/14.94 % (1951203)Instruction limit reached!
% 100.29/14.94 % (1951203)------------------------------
% 100.29/14.94 % (1951203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.29/14.94 % (1951203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.29/14.94 % (1951203)CaDiCaL version: 2.1.3
% 100.29/14.94 % (1951203)Termination reason: Instruction limit
% 100.29/14.94 % (1951203)Termination phase: Saturation
% 100.29/14.94 % (1951203)Time elapsed: 1.183 s
% 100.29/14.94 % (1951203)Peak memory usage: 138 MB
% 100.29/14.94 % (1951203)Instructions burned: 1998 (million)
% 100.29/14.94 % (1951205)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=55338399:i=2088:bd=preordered:av=off_2944 on theBenchmark for (2944ds/2088Mi)
% 100.29/14.94 % (1951201)Instruction limit reached!
% 100.29/14.94 % (1951201)------------------------------
% 100.29/14.94 % (1951201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.29/14.94 % (1951201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.29/14.94 % (1951201)CaDiCaL version: 2.1.3
% 100.29/14.94 % (1951201)Termination reason: Instruction limit
% 100.29/14.94 % (1951201)Termination phase: Saturation
% 100.29/14.94 % (1951201)Time elapsed: 1.706 s
% 100.29/14.94 % (1951201)Peak memory usage: 136 MB
% 100.29/14.94 % (1951201)Instructions burned: 2990 (million)
% 100.29/14.94 % (1951207)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2931784237:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi)
% 100.29/14.94 % (1951207)Instruction limit reached!
% 100.29/14.94 % (1951207)------------------------------
% 100.29/14.94 % (1951207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.29/14.94 % (1951207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.29/14.94 % (1951207)CaDiCaL version: 2.1.3
% 100.29/14.94 % (1951207)Termination reason: Instruction limit
% 100.29/14.94 % (1951207)Termination phase: Saturation
% 100.29/14.94 % (1951207)Time elapsed: 0.497 s
% 100.29/14.94 % (1951207)Peak memory usage: 104 MB
% 100.29/14.94 % (1951207)Instructions burned: 1099 (million)
% 100.29/14.94 % (1951209)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2625459281:i=433:bd=preordered_2935 on theBenchmark for (2935ds/433Mi)
% 100.29/14.94 % (1951209)Refutation not found, incomplete strategy
% 100.29/14.94 % (1951209)------------------------------
% 100.29/14.94 % (1951209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.29/14.94 % (1951209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.29/14.94 % (1951209)CaDiCaL version: 2.1.3
% 100.29/14.94 % (1951209)Termination reason: Refutation not found, incomplete strategy
% 100.29/14.94 % (1951209)Time elapsed: 0.001 s
% 100.29/14.94 % (1951209)Peak memory usage: 88 MB
% 100.29/14.94 % (1951209)------------------------------
% 100.29/14.94 % (1951209)------------------------------
% 100.29/14.94 % (1951205)Instruction limit reached!
% 100.29/14.94 % (1951205)------------------------------
% 100.29/14.94 % (1951205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.29/14.94 % (1951205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.29/14.94 % (1951205)CaDiCaL version: 2.1.3
% 100.29/14.94 % (1951205)Termination reason: Instruction limit
% 100.29/14.94 % (1951205)Termination phase: Saturation
% 100.29/14.94 % (1951205)Time elapsed: 1.223 s
% 100.29/14.94 % (1951205)Peak memory usage: 136 MB
% 100.29/14.94 % (1951205)Instructions burned: 2088 (million)
% 100.29/14.94 % (1951211)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=603450693:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2931 on theBenchmark for (2931ds/2942Mi)
% 100.29/14.94 % (1951212)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1429324404:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2931 on theBenchmark for (2931ds/6922Mi)
% 100.29/14.94 % (1951193)Instruction limit reached!
% 110.71/16.20 % (1951193)------------------------------
% 110.71/16.20 % (1951193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.71/16.20 % (1951193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.71/16.20 % (1951193)CaDiCaL version: 2.1.3
% 110.71/16.20 % (1951193)Termination reason: Instruction limit
% 110.71/16.20 % (1951193)Termination phase: Saturation
% 110.71/16.20 % (1951193)Time elapsed: 4.300 s
% 110.71/16.20 % (1951193)Peak memory usage: 205 MB
% 110.71/16.20 % (1951193)Instructions burned: 8478 (million)
% 110.71/16.20 % (1951215)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=2799258522:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2929 on theBenchmark for (2929ds/596Mi)
% 110.71/16.20 % (1951215)Instruction limit reached!
% 110.71/16.20 % (1951215)------------------------------
% 110.71/16.20 % (1951215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.71/16.20 % (1951215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.71/16.20 % (1951215)CaDiCaL version: 2.1.3
% 110.71/16.20 % (1951215)Termination reason: Instruction limit
% 110.71/16.20 % (1951215)Termination phase: Saturation
% 110.71/16.20 % (1951215)Time elapsed: 0.263 s
% 110.71/16.20 % (1951215)Peak memory usage: 98 MB
% 110.71/16.20 % (1951215)Instructions burned: 596 (million)
% 110.71/16.20 % (1951217)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=331868470:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2925 on theBenchmark for (2925ds/4123Mi)
% 110.71/16.20 % (1951189)Instruction limit reached!
% 110.71/16.20 % (1951189)------------------------------
% 110.71/16.20 % (1951189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.71/16.20 % (1951189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.71/16.20 % (1951189)CaDiCaL version: 2.1.3
% 110.71/16.20 % (1951189)Termination reason: Instruction limit
% 110.71/16.20 % (1951189)Termination phase: Saturation
% 110.71/16.20 % (1951189)Time elapsed: 5.313 s
% 110.71/16.20 % (1951189)Peak memory usage: 184 MB
% 110.71/16.20 % (1951189)Instructions burned: 10308 (million)
% 110.71/16.20 % (1951219)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2405977902:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2922 on theBenchmark for (2922ds/16411Mi)
% 110.71/16.20 % (1951211)Instruction limit reached!
% 110.71/16.20 % (1951211)------------------------------
% 110.71/16.20 % (1951211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.71/16.20 % (1951211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.71/16.20 % (1951211)CaDiCaL version: 2.1.3
% 110.71/16.20 % (1951211)Termination reason: Instruction limit
% 110.71/16.20 % (1951211)Termination phase: Saturation
% 110.71/16.20 % (1951211)Time elapsed: 1.594 s
% 110.71/16.20 % (1951211)Peak memory usage: 133 MB
% 110.71/16.20 % (1951211)Instructions burned: 2944 (million)
% 110.71/16.20 % (1951221)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3559423477:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2914 on theBenchmark for (2914ds/1670Mi)
% 110.71/16.20 % (1951221)Instruction limit reached!
% 110.71/16.20 % (1951221)------------------------------
% 110.71/16.20 % (1951221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.71/16.20 % (1951221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.71/16.20 % (1951221)CaDiCaL version: 2.1.3
% 110.71/16.20 % (1951221)Termination reason: Instruction limit
% 110.71/16.20 % (1951221)Termination phase: Saturation
% 110.71/16.20 % (1951221)Time elapsed: 0.985 s
% 110.71/16.20 % (1951221)Peak memory usage: 137 MB
% 110.71/16.20 % (1951221)Instructions burned: 1672 (million)
% 110.71/16.20 % (1951217)Instruction limit reached!
% 110.71/16.20 % (1951217)------------------------------
% 110.71/16.20 % (1951217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.71/16.20 % (1951217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.71/16.20 % (1951217)CaDiCaL version: 2.1.3
% 110.71/16.20 % (1951217)Termination reason: Instruction limit
% 110.71/16.20 % (1951217)Termination phase: Saturation
% 110.71/16.20 % (1951217)Time elapsed: 2.200 s
% 110.71/16.20 % (1951217)Peak memory usage: 160 MB
% 110.71/16.20 % (1951217)Instructions burned: 4124 (million)
% 110.71/16.20 % (1951223)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=426642742:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2903 on theBenchmark for (2903ds/1722Mi)
% 118.53/17.39 % (1951224)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=3104157196:cts=off:cond=on:i=9530:bs=on:fsd=on_2901 on theBenchmark for (2901ds/9530Mi)
% 118.53/17.39 % (1951212)Instruction limit reached!
% 118.53/17.39 % (1951212)------------------------------
% 118.53/17.39 % (1951212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.53/17.39 % (1951212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.53/17.39 % (1951212)CaDiCaL version: 2.1.3
% 118.53/17.39 % (1951212)Termination reason: Instruction limit
% 118.53/17.39 % (1951212)Termination phase: Saturation
% 118.53/17.39 % (1951212)Time elapsed: 3.525 s
% 118.53/17.39 % (1951212)Peak memory usage: 192 MB
% 118.53/17.39 % (1951212)Instructions burned: 6924 (million)
% 118.53/17.39 % (1951227)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2337952967:st=2:i=4495:sd=10:ss=included_2894 on theBenchmark for (2894ds/4495Mi)
% 118.53/17.39 % (1951223)Instruction limit reached!
% 118.53/17.39 % (1951223)------------------------------
% 118.53/17.39 % (1951223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.53/17.39 % (1951223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.53/17.39 % (1951223)CaDiCaL version: 2.1.3
% 118.53/17.39 % (1951223)Termination reason: Instruction limit
% 118.53/17.39 % (1951223)Termination phase: Saturation
% 118.53/17.39 % (1951223)Time elapsed: 1.055 s
% 118.53/17.39 % (1951223)Peak memory usage: 138 MB
% 118.53/17.39 % (1951223)Instructions burned: 1723 (million)
% 118.53/17.39 % (1951229)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=2810842465:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2891 on theBenchmark for (2891ds/4920Mi)
% 118.53/17.39 % (1951227)Instruction limit reached!
% 118.53/17.39 % (1951227)------------------------------
% 118.53/17.39 % (1951227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.53/17.39 % (1951227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.53/17.39 % (1951227)CaDiCaL version: 2.1.3
% 118.53/17.39 % (1951227)Termination reason: Instruction limit
% 118.53/17.39 % (1951227)Termination phase: Saturation
% 118.53/17.39 % (1951227)Time elapsed: 2.989 s
% 118.53/17.39 % (1951227)Peak memory usage: 148 MB
% 118.53/17.39 % (1951227)Instructions burned: 4496 (million)
% 118.53/17.39 % (1951229)Instruction limit reached!
% 118.53/17.39 % (1951229)------------------------------
% 118.53/17.39 % (1951229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.53/17.39 % (1951229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.53/17.39 % (1951229)CaDiCaL version: 2.1.3
% 118.53/17.39 % (1951229)Termination reason: Instruction limit
% 118.53/17.39 % (1951229)Termination phase: Saturation
% 118.53/17.39 % (1951229)Time elapsed: 2.706 s
% 118.53/17.39 % (1951229)Peak memory usage: 146 MB
% 118.53/17.39 % (1951229)Instructions burned: 4920 (million)
% 118.53/17.39 % (1951231)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=2152312969:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2863 on theBenchmark for (2863ds/2083Mi)
% 118.53/17.39 % (1951232)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=6425023:i=4629:av=off:gsp=on_2862 on theBenchmark for (2862ds/4629Mi)
% 118.53/17.39 % (1951224)Instruction limit reached!
% 118.53/17.39 % (1951224)------------------------------
% 118.53/17.39 % (1951224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.53/17.39 % (1951224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.53/17.39 % (1951224)CaDiCaL version: 2.1.3
% 118.53/17.39 % (1951224)Termination reason: Instruction limit
% 118.53/17.39 % (1951224)Termination phase: Saturation
% 118.53/17.39 % (1951224)Time elapsed: 4.153 s
% 118.53/17.39 % (1951224)Peak memory usage: 146 MB
% 118.53/17.39 % (1951224)Instructions burned: 9531 (million)
% 118.53/17.39 % (1951236)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2581713180:i=1258:av=off_2858 on theBenchmark for (2858ds/1258Mi)
% 118.53/17.39 % (1951236)Refutation not found, incomplete strategy
% 121.51/17.98 % (1951236)------------------------------
% 121.51/17.98 % (1951236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951236)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951236)Termination reason: Refutation not found, incomplete strategy
% 121.51/17.98 % (1951236)Time elapsed: 0.057 s
% 121.51/17.98 % (1951236)Peak memory usage: 87 MB
% 121.51/17.98 % (1951236)Instructions burned: 114 (million)
% 121.51/17.98 % (1951232)Refutation not found, incomplete strategy
% 121.51/17.98 % (1951232)------------------------------
% 121.51/17.98 % (1951232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951232)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951232)Termination reason: Refutation not found, incomplete strategy
% 121.51/17.98 % (1951232)Time elapsed: 0.572 s
% 121.51/17.98 % (1951232)Peak memory usage: 127 MB
% 121.51/17.98 % (1951232)Instructions burned: 857 (million)
% 121.51/17.98 % (1951236)------------------------------
% 121.51/17.98 % (1951236)------------------------------
% 121.51/17.98 % (1951232)------------------------------
% 121.51/17.98 % (1951232)------------------------------
% 121.51/17.98 % (1951238)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1544739304:i=7343:av=off:ss=included_2854 on theBenchmark for (2854ds/7343Mi)
% 121.51/17.98 % (1951239)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3800959049:i=1325:sd=2:ss=axioms:sgt=16_2853 on theBenchmark for (2853ds/1325Mi)
% 121.51/17.98 % (1951239)Refutation not found, incomplete strategy
% 121.51/17.98 % (1951239)------------------------------
% 121.51/17.98 % (1951239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951239)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951239)Termination reason: Refutation not found, incomplete strategy
% 121.51/17.98 % (1951239)Time elapsed: 0.001 s
% 121.51/17.98 % (1951239)Peak memory usage: 88 MB
% 121.51/17.98 % (1951231)Instruction limit reached!
% 121.51/17.98 % (1951231)------------------------------
% 121.51/17.98 % (1951231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951231)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951231)Termination reason: Instruction limit
% 121.51/17.98 % (1951231)Termination phase: Saturation
% 121.51/17.98 % (1951231)Time elapsed: 1.110 s
% 121.51/17.98 % (1951231)Peak memory usage: 129 MB
% 121.51/17.98 % (1951231)Instructions burned: 2084 (million)
% 121.51/17.98 % (1951239)------------------------------
% 121.51/17.98 % (1951239)------------------------------
% 121.51/17.98 % (1951242)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=3138866555:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2850 on theBenchmark for (2850ds/2646Mi)
% 121.51/17.98 % (1951243)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=8340348:i=1489:sd=2:ep=R:ss=axioms_2849 on theBenchmark for (2849ds/1489Mi)
% 121.51/17.98 [W928 20:26:14.615869838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.615913245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.615957299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.615969179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.615994686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616015326 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616041640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616052660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616076674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616087264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616111324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 [W928 20:26:14.616121907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.51/17.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.51/17.98 % (1951243)Refutation not found, incomplete strategy
% 121.51/17.98 % (1951243)------------------------------
% 121.51/17.98 % (1951243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951243)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951243)Termination reason: Refutation not found, incomplete strategy
% 121.51/17.98 % (1951243)Time elapsed: 0.547 s
% 121.51/17.98 % (1951243)Peak memory usage: 125 MB
% 121.51/17.98 % (1951243)Instructions burned: 827 (million)
% 121.51/17.98 % (1951243)------------------------------
% 121.51/17.98 % (1951243)------------------------------
% 121.51/17.98 % (1951246)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=4245578279:i=1503_2840 on theBenchmark for (2840ds/1503Mi)
% 121.51/17.98 % (1951246)Refutation not found, incomplete strategy
% 121.51/17.98 % (1951246)------------------------------
% 121.51/17.98 % (1951246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951246)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951246)Termination reason: Refutation not found, incomplete strategy
% 121.51/17.98 % (1951246)Time elapsed: 0.570 s
% 121.51/17.98 % (1951246)Peak memory usage: 128 MB
% 121.51/17.98 % (1951246)Instructions burned: 857 (million)
% 121.51/17.98 % (1951219)Instruction limit reached!
% 121.51/17.98 % (1951219)------------------------------
% 121.51/17.98 % (1951219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951219)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951219)Termination reason: Instruction limit
% 121.51/17.98 % (1951219)Termination phase: Saturation
% 121.51/17.98 % (1951219)Time elapsed: 8.906 s
% 121.51/17.98 % (1951219)Peak memory usage: 275 MB
% 121.51/17.98 % (1951219)Instructions burned: 16412 (million)
% 121.51/17.98 % (1951242)Instruction limit reached!
% 121.51/17.98 % (1951242)------------------------------
% 121.51/17.98 % (1951242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/17.98 % (1951242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/17.98 % (1951242)CaDiCaL version: 2.1.3
% 121.51/17.98 % (1951242)Termination reason: Instruction limit
% 121.51/17.98 % (1951242)Termination phase: Saturation
% 121.51/17.98 % (1951242)Time elapsed: 1.701 s
% 121.51/17.98 % (1951242)Peak memory usage: 139 MB
% 121.51/17.98 % (1951242)Instructions burned: 2646 (million)
% 121.51/17.98 % (1951249)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=2932659512:i=3604:fsr=off:er=filter_2832 on theBenchmark for (2832ds/3604Mi)
% 121.51/17.98 % (1951248)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3001013631:i=13942:kws=frequency_2832 on theBenchmark for (2832ds/13942Mi)
% 121.51/17.98 % (1951246)------------------------------
% 121.51/17.98 % (1951246)------------------------------
% 121.51/17.98 % (1951238)First to succeed.
% 121.51/17.98 % (1951238)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1951132"
% 121.51/17.98 % (1951252)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=4008785292:i=1876:sd=1:ss=included:sgt=32_2830 on theBenchmark for (2830ds/1876Mi)
% 121.51/17.98 % (1951238)Refutation found. Thanks to Tanya!
% 121.51/17.98 % SZS status Unsatisfiable for theBenchmark
% 121.51/17.98 % SZS output start Proof for theBenchmark
% See solution above
% 123.30/18.18 % (1951238)------------------------------
% 123.30/18.18 % (1951238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.30/18.18 % (1951238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.30/18.18 % (1951238)CaDiCaL version: 2.1.3
% 123.30/18.18 % (1951238)Termination reason: Refutation
% 123.30/18.18 % (1951238)Time elapsed: 2.339 s
% 123.30/18.18 % (1951238)Peak memory usage: 160 MB
% 123.30/18.18 % (1951238)Instructions burned: 4124 (million)
% 123.30/18.18 % (1951238)------------------------------
% 123.30/18.18 % (1951238)------------------------------
% 123.30/18.18 % (1951132)Success in time 17.345 s
% 123.30/18.18 % Vampire exiting
%------------------------------------------------------------------------------