%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BOO039-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:35:58 AM UTC 2026
% Result : Unsatisfiable 105.65s 27.22s
% Output : Refutation 188.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 13
% Syntax : Number of formulae : 212 ( 121 unt; 11 def)
% Number of atoms : 304 ( 205 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 186 ( 94 ~; 90 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-2 aty)
% Number of variables : 172 ( 0 sgn 172 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : nand(nand(X0,nand(nand(X1,X0),X0)),nand(X1,nand(X2,X0))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sh_1) ).
fof(f2,negated_conjecture,
( nand(nand(a,a),nand(b,a)) != a
| nand(a,nand(b,nand(a,c))) != nand(nand(nand(c,b),b),a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_meredith_2_basis) ).
fof(f3,plain,
( a != nand(nand(a,a),nand(b,a))
| nand(a,nand(b,nand(a,c))) != nand(nand(nand(c,b),b),a) ),
inference(reorient_equations,[],[f2]) ).
fof(f4,definition,
sF0 = nand(a,a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
nand(a,a) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = nand(b,a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
nand(b,a) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = nand(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
nand(sF0,sF1) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF3 = nand(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f11,plain,
nand(a,c) = sF3,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF4 = nand(b,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f13,plain,
nand(b,sF3) = sF4,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF5 = nand(a,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f15,plain,
nand(a,sF4) = sF5,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF6 = nand(c,b),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f17,plain,
nand(c,b) = sF6,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF7 = nand(sF6,b),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f19,plain,
nand(sF6,b) = sF7,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF8 = nand(sF7,a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f21,plain,
nand(sF7,a) = sF8,
inference(reorient_equations,[],[f20]) ).
fof(f22,plain,
( a != sF2
| sF5 != sF8 ),
inference(definition_folding,[],[f3,f21,f19,f17,f15,f13,f11,f9,f7,f5]) ).
fof(f24,definition,
( spl9_1
<=> sF5 = sF8 ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f26,plain,
( sF5 != sF8
| spl9_1 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f28,definition,
( spl9_2
<=> a = sF2 ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f29,plain,
( a = sF2
| ~ spl9_2 ),
inference(avatar_component_clause,[],[f28]) ).
fof(f31,plain,
( ~ spl9_1
| ~ spl9_2 ),
inference(avatar_split_clause,[],[f22,f28,f24]) ).
fof(f32,plain,
! [X2,X3,X0,X1] : nand(X2,nand(nand(X0,X2),X2)) = nand(nand(nand(X0,nand(X1,X2)),nand(X0,nand(X0,nand(X1,X2)))),nand(nand(X2,nand(nand(X0,X2),X2)),nand(X3,nand(X0,nand(X1,X2))))),
inference(superposition,[],[f1,f1]) ).
fof(f38,plain,
! [X0] : c = nand(nand(b,nand(sF6,b)),nand(c,nand(X0,b))),
inference(superposition,[],[f1,f17]) ).
fof(f39,plain,
! [X0] : sF6 = nand(nand(b,nand(sF7,b)),nand(sF6,nand(X0,b))),
inference(superposition,[],[f1,f19]) ).
fof(f41,plain,
! [X2,X3,X0,X1] : nand(nand(nand(X0,nand(X1,X2)),nand(nand(X3,nand(X0,nand(X1,X2))),nand(X0,nand(X1,X2)))),nand(X3,X0)) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f42,plain,
! [X0] : nand(nand(a,nand(nand(X0,a),a)),nand(X0,sF0)) = X0,
inference(superposition,[],[f1,f5]) ).
fof(f44,plain,
! [X0] : nand(nand(sF4,nand(nand(X0,sF4),sF4)),nand(X0,sF5)) = X0,
inference(superposition,[],[f1,f15]) ).
fof(f48,plain,
! [X0] : nand(nand(b,nand(nand(X0,b),b)),nand(X0,sF7)) = X0,
inference(superposition,[],[f1,f19]) ).
fof(f50,plain,
! [X2,X0,X1] : nand(X2,nand(nand(X0,X2),X2)) = nand(nand(nand(X1,X2),nand(nand(nand(X2,nand(nand(X0,X2),X2)),nand(X1,X2)),nand(X1,X2))),X0),
inference(superposition,[],[f1,f1]) ).
fof(f51,plain,
! [X0] : c = nand(nand(b,sF7),nand(c,nand(X0,b))),
inference(forward_demodulation,[],[f38,f19]) ).
fof(f67,plain,
! [X3,X0,X1] : nand(nand(X0,nand(nand(X3,X0),X0)),nand(X3,nand(X1,nand(nand(X0,X1),X1)))) = X3,
inference(superposition,[],[f41,f1]) ).
fof(f81,plain,
! [X2,X0,X1] : nand(nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),nand(X2,X0)) = X2,
inference(superposition,[],[f1,f41]) ).
fof(f559,plain,
! [X0,X1] : nand(X0,nand(nand(X0,X0),X0)) = nand(nand(X1,nand(nand(nand(X0,nand(nand(X0,X0),X0)),X1),X1)),X0),
inference(superposition,[],[f67,f1]) ).
fof(f565,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(X0,X0),X0)),
inference(superposition,[],[f32,f67]) ).
fof(f583,plain,
! [X0,X1] : nand(X0,X0) = nand(nand(X1,nand(nand(nand(X0,X0),X1),X1)),X0),
inference(forward_demodulation,[],[f559,f565]) ).
fof(f595,plain,
! [X0,X1] : nand(nand(X0,X0),nand(X0,nand(X1,X0))) = X0,
inference(superposition,[],[f1,f565]) ).
fof(f599,plain,
! [X0] : nand(nand(X0,X0),nand(X0,X0)) = X0,
inference(superposition,[],[f1,f565]) ).
fof(f691,plain,
! [X0,X1] : nand(nand(X1,nand(nand(X0,X1),X1)),nand(X0,X0)) = X0,
inference(superposition,[],[f583,f599]) ).
fof(f697,plain,
! [X0,X1] : nand(X1,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1)) = nand(nand(nand(X0,X1),nand(nand(nand(X0,X1),nand(X0,X1)),nand(X0,X1))),nand(nand(X0,X1),nand(X0,X1))),
inference(superposition,[],[f50,f583]) ).
fof(f757,plain,
! [X0,X1] : nand(X1,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1)) = nand(nand(nand(X0,X1),nand(X0,X1)),nand(nand(X0,X1),nand(X0,X1))),
inference(forward_demodulation,[],[f697,f565]) ).
fof(f765,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1)),
inference(forward_demodulation,[],[f757,f599]) ).
fof(f980,plain,
! [X0,X1] : nand(nand(X1,X1),nand(X0,X1)) = X1,
inference(superposition,[],[f595,f765]) ).
fof(f1394,plain,
! [X0,X1] : nand(X0,X1) = nand(nand(nand(X0,X1),nand(X0,X1)),X0),
inference(superposition,[],[f980,f81]) ).
fof(f1412,plain,
! [X0,X1] : nand(X1,X0) = nand(nand(nand(X1,X0),nand(X1,X0)),X0),
inference(superposition,[],[f980,f980]) ).
fof(f1416,plain,
a = nand(nand(a,a),sF1),
inference(superposition,[],[f980,f7]) ).
fof(f1419,plain,
sF1 = nand(nand(sF1,sF1),sF2),
inference(superposition,[],[f980,f9]) ).
fof(f1422,plain,
a = nand(nand(a,a),sF8),
inference(superposition,[],[f980,f21]) ).
fof(f1455,plain,
! [X0,X1] : nand(nand(X1,X0),nand(nand(nand(X0,X0),nand(X1,X0)),nand(X1,X0))) = X0,
inference(superposition,[],[f765,f980]) ).
fof(f1456,plain,
! [X0,X1] : nand(nand(X1,X0),nand(X0,nand(X1,X0))) = X0,
inference(forward_demodulation,[],[f1455,f980]) ).
fof(f1460,plain,
a = nand(sF0,sF8),
inference(forward_demodulation,[],[f1422,f5]) ).
fof(f1461,plain,
a = nand(sF0,sF1),
inference(forward_demodulation,[],[f1416,f5]) ).
fof(f1468,plain,
a = sF2,
inference(forward_demodulation,[],[f1461,f9]) ).
fof(f1471,plain,
spl9_2,
inference(avatar_split_clause,[],[f1468,f28]) ).
fof(f1595,plain,
( sF1 = nand(b,sF2)
| ~ spl9_2 ),
inference(superposition,[],[f7,f29]) ).
fof(f1596,plain,
( sF3 = nand(sF2,c)
| ~ spl9_2 ),
inference(superposition,[],[f11,f29]) ).
fof(f1597,plain,
( sF5 = nand(sF2,sF4)
| ~ spl9_2 ),
inference(superposition,[],[f15,f29]) ).
fof(f1598,plain,
( sF8 = nand(sF7,sF2)
| ~ spl9_2 ),
inference(superposition,[],[f21,f29]) ).
fof(f1668,plain,
( sF1 = nand(sF2,nand(nand(nand(sF1,sF1),sF2),sF2))
| ~ spl9_2 ),
inference(superposition,[],[f765,f1595]) ).
fof(f1671,plain,
( sF1 = nand(sF2,nand(sF1,sF2))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f1668,f1419]) ).
fof(f2317,plain,
! [X0,X1] : nand(X0,X1) = nand(X0,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X0),X0)),
inference(superposition,[],[f765,f1394]) ).
fof(f2359,plain,
! [X0,X1] : nand(X0,X1) = nand(X0,nand(nand(X0,X1),X0)),
inference(forward_demodulation,[],[f2317,f1394]) ).
fof(f2471,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(nand(X0,X1),X1)),
inference(superposition,[],[f2359,f765]) ).
fof(f2519,plain,
( sF1 = nand(b,nand(sF1,b))
| ~ spl9_2 ),
inference(superposition,[],[f2359,f1595]) ).
fof(f2654,plain,
sF4 = nand(sF3,nand(sF4,sF3)),
inference(superposition,[],[f2471,f13]) ).
fof(f2656,plain,
sF6 = nand(b,nand(sF6,b)),
inference(superposition,[],[f2471,f17]) ).
fof(f2667,plain,
sF7 = nand(b,nand(sF7,b)),
inference(superposition,[],[f2471,f19]) ).
fof(f2682,plain,
! [X0,X1] : nand(nand(X0,X1),nand(X0,X0)) = X0,
inference(superposition,[],[f691,f2471]) ).
fof(f2713,plain,
! [X2,X0,X1] : nand(nand(X0,nand(X1,X2)),nand(X0,X1)) = X0,
inference(superposition,[],[f81,f2471]) ).
fof(f2744,plain,
sF6 = nand(b,sF7),
inference(forward_demodulation,[],[f2656,f19]) ).
fof(f2942,plain,
! [X2,X0,X1] : nand(X0,nand(X1,X2)) = nand(nand(X1,nand(nand(nand(X0,nand(X1,X2)),X1),X1)),X0),
inference(superposition,[],[f1,f2713]) ).
fof(f2975,plain,
! [X2,X0,X1] : nand(X0,nand(X1,X2)) = nand(nand(nand(X0,nand(X1,X2)),X1),X0),
inference(forward_demodulation,[],[f2942,f2471]) ).
fof(f3399,plain,
! [X0,X1] : nand(X0,nand(nand(X1,X0),X0)) = nand(nand(nand(X0,X0),nand(X0,nand(X0,X0))),X1),
inference(superposition,[],[f50,f2682]) ).
fof(f3471,plain,
! [X0,X1] : nand(X0,nand(nand(X1,X0),X0)) = nand(X0,X1),
inference(forward_demodulation,[],[f3399,f1456]) ).
fof(f3510,plain,
! [X0,X1] : nand(nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1),nand(nand(X0,X1),nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1))) = nand(nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1),X1),
inference(superposition,[],[f3471,f765]) ).
fof(f3557,plain,
( nand(sF2,nand(sF1,sF2)) = nand(sF2,b)
| ~ spl9_2 ),
inference(superposition,[],[f3471,f1595]) ).
fof(f3558,plain,
nand(sF3,nand(sF4,sF3)) = nand(sF3,b),
inference(superposition,[],[f3471,f13]) ).
fof(f3577,plain,
! [X2,X0,X1] : nand(nand(X0,X1),nand(X1,nand(X2,X0))) = X1,
inference(superposition,[],[f1,f3471]) ).
fof(f3579,plain,
! [X2,X0,X1] : nand(X0,X1) = nand(nand(nand(X2,X0),nand(nand(nand(X0,X1),nand(X2,X0)),nand(X2,X0))),X1),
inference(superposition,[],[f50,f3471]) ).
fof(f3583,plain,
! [X0,X1] : nand(X1,X0) = nand(X0,X1),
inference(superposition,[],[f2471,f3471]) ).
fof(f3619,plain,
! [X2,X0,X1] : nand(X1,nand(nand(X2,X1),X1)) = nand(nand(nand(X0,X1),nand(X1,nand(nand(X2,X1),X1))),X2),
inference(superposition,[],[f50,f3471]) ).
fof(f3620,plain,
! [X2,X0,X1] : nand(nand(nand(X0,X1),X2),nand(X2,X0)) = X2,
inference(superposition,[],[f81,f3471]) ).
fof(f3638,plain,
! [X2,X0,X1] : nand(X2,X1) = nand(nand(nand(X0,X1),nand(X2,X1)),X2),
inference(forward_demodulation,[],[f3619,f2471]) ).
fof(f3658,plain,
! [X2,X0,X1] : nand(X0,X1) = nand(X1,nand(nand(X2,X0),nand(nand(nand(X0,X1),nand(X2,X0)),nand(X2,X0)))),
inference(forward_demodulation,[],[f3579,f3583]) ).
fof(f3672,plain,
sF4 = nand(sF3,b),
inference(forward_demodulation,[],[f3558,f2654]) ).
fof(f3673,plain,
( sF1 = nand(sF2,b)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f3557,f1671]) ).
fof(f3716,plain,
! [X0,X1] : nand(X1,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1)) = nand(nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1),nand(nand(X0,X1),nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1))),
inference(forward_demodulation,[],[f3510,f3583]) ).
fof(f3719,plain,
! [X2,X0,X1] : nand(X2,X1) = nand(X2,nand(nand(X0,X1),nand(X2,X1))),
inference(forward_demodulation,[],[f3638,f3583]) ).
fof(f3730,plain,
! [X2,X0,X1] : nand(X0,X1) = nand(X1,nand(nand(X0,X1),nand(X2,X0))),
inference(forward_demodulation,[],[f3658,f2471]) ).
fof(f3766,plain,
! [X0,X1] : nand(X1,nand(X1,nand(nand(nand(X0,X1),nand(X0,X1)),X1))) = nand(nand(X1,nand(nand(nand(X0,X1),nand(X0,X1)),X1)),nand(nand(X0,X1),nand(X1,nand(nand(nand(X0,X1),nand(X0,X1)),X1)))),
inference(forward_demodulation,[],[f3716,f3583]) ).
fof(f3794,plain,
! [X0,X1] : nand(X1,nand(X1,nand(X0,X1))) = nand(nand(X1,nand(X0,X1)),nand(nand(X0,X1),nand(X1,nand(X0,X1)))),
inference(forward_demodulation,[],[f3766,f1412]) ).
fof(f3802,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(X1,nand(X0,X1))),
inference(forward_demodulation,[],[f3794,f1456]) ).
fof(f4062,plain,
! [X0] : nand(nand(a,nand(nand(a,X0),a)),nand(X0,sF0)) = X0,
inference(superposition,[],[f42,f3583]) ).
fof(f4078,plain,
! [X0] : nand(nand(sF4,nand(nand(X0,sF4),sF4)),nand(sF5,X0)) = X0,
inference(superposition,[],[f44,f3583]) ).
fof(f4215,plain,
! [X0] : nand(nand(sF5,X0),nand(sF4,nand(nand(X0,sF4),sF4))) = X0,
inference(forward_demodulation,[],[f4078,f3583]) ).
fof(f4229,plain,
! [X0] : nand(nand(X0,sF0),nand(a,nand(nand(a,X0),a))) = X0,
inference(forward_demodulation,[],[f4062,f3583]) ).
fof(f4419,plain,
! [X0] : nand(nand(sF5,X0),nand(X0,sF4)) = X0,
inference(forward_demodulation,[],[f4215,f2471]) ).
fof(f4431,plain,
! [X0] : nand(nand(X0,sF0),nand(a,X0)) = X0,
inference(forward_demodulation,[],[f4229,f2359]) ).
fof(f4556,plain,
( ! [X0] : nand(nand(X0,sF0),nand(sF2,X0)) = X0
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4431,f29]) ).
fof(f4647,plain,
( sF6 = nand(nand(b,nand(sF7,b)),nand(sF6,sF1))
| ~ spl9_2 ),
inference(superposition,[],[f39,f3673]) ).
fof(f4648,plain,
( sF2 = nand(nand(b,nand(sF1,b)),nand(sF2,sF7))
| ~ spl9_2 ),
inference(superposition,[],[f48,f3673]) ).
fof(f4650,plain,
( c = nand(nand(b,sF7),nand(c,sF1))
| ~ spl9_2 ),
inference(superposition,[],[f51,f3673]) ).
fof(f4691,plain,
( c = nand(nand(c,sF1),nand(b,sF7))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4650,f3583]) ).
fof(f4693,plain,
( sF2 = nand(nand(sF2,sF7),nand(b,nand(sF1,b)))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4648,f3583]) ).
fof(f4694,plain,
( sF6 = nand(nand(sF6,sF1),nand(b,nand(sF7,b)))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4647,f3583]) ).
fof(f4705,plain,
( c = nand(nand(c,sF1),sF6)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4691,f2744]) ).
fof(f4707,plain,
( sF2 = nand(nand(sF2,sF7),sF1)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4693,f2519]) ).
fof(f4708,plain,
( sF6 = nand(nand(sF6,sF1),sF7)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4694,f2667]) ).
fof(f4712,plain,
( c = nand(sF6,nand(c,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4705,f3583]) ).
fof(f4714,plain,
( sF2 = nand(sF1,nand(sF2,sF7))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4707,f3583]) ).
fof(f4715,plain,
( sF6 = nand(sF7,nand(sF6,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4708,f3583]) ).
fof(f4718,plain,
( sF6 = nand(sF7,nand(sF1,sF6))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f4715,f3583]) ).
fof(f4925,plain,
! [X0,X1] : nand(nand(X1,X0),X0) = nand(X0,nand(X0,X1)),
inference(superposition,[],[f3802,f3471]) ).
fof(f4991,plain,
! [X0,X1] : nand(X0,nand(X0,X1)) = nand(X0,nand(X1,X0)),
inference(forward_demodulation,[],[f4925,f3583]) ).
fof(f5185,plain,
! [X0,X1] : nand(X1,X0) = nand(X0,nand(X0,nand(X0,X1))),
inference(superposition,[],[f3802,f4991]) ).
fof(f5831,plain,
( ! [X0] : nand(nand(sF1,X0),nand(X0,b)) = X0
| ~ spl9_2 ),
inference(superposition,[],[f3620,f1595]) ).
fof(f5832,plain,
! [X0] : nand(nand(sF4,X0),nand(X0,b)) = X0,
inference(superposition,[],[f3620,f13]) ).
fof(f5870,plain,
! [X2,X0,X1] : nand(X0,nand(X2,X1)) = nand(X0,nand(nand(X0,nand(X2,X1)),X1)),
inference(superposition,[],[f3620,f1]) ).
fof(f6000,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(nand(X1,nand(nand(nand(nand(X1,X2),X0),X1),X1)),X0),
inference(superposition,[],[f1,f3620]) ).
fof(f6045,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(X0,nand(X1,nand(nand(nand(nand(X1,X2),X0),X1),X1))),
inference(forward_demodulation,[],[f6000,f3583]) ).
fof(f6149,plain,
! [X2,X0,X1] : nand(X0,nand(X2,X1)) = nand(X0,nand(X1,nand(X0,nand(X2,X1)))),
inference(forward_demodulation,[],[f5870,f3583]) ).
fof(f6195,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(X0,nand(nand(nand(X1,X2),X0),X1)),
inference(forward_demodulation,[],[f6045,f2471]) ).
fof(f6274,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(X0,nand(X1,nand(nand(X1,X2),X0))),
inference(forward_demodulation,[],[f6195,f3583]) ).
fof(f7890,plain,
( sF2 = nand(sF1,nand(sF7,sF2))
| ~ spl9_2 ),
inference(superposition,[],[f6149,f4714]) ).
fof(f7945,plain,
( sF2 = nand(sF1,sF8)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f7890,f1598]) ).
fof(f8125,plain,
( sF3 = nand(nand(sF1,sF3),sF4)
| ~ spl9_2 ),
inference(superposition,[],[f5831,f3672]) ).
fof(f8187,plain,
( sF3 = nand(sF4,nand(sF1,sF3))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f8125,f3583]) ).
fof(f8702,plain,
nand(a,sF7) = nand(sF7,nand(sF7,sF8)),
inference(superposition,[],[f5185,f21]) ).
fof(f8797,plain,
nand(sF7,a) = nand(sF7,nand(sF7,sF8)),
inference(forward_demodulation,[],[f8702,f3583]) ).
fof(f8904,plain,
sF8 = nand(sF7,nand(sF7,sF8)),
inference(forward_demodulation,[],[f8797,f21]) ).
fof(f9008,plain,
sF8 = nand(sF7,nand(sF8,sF8)),
inference(superposition,[],[f6149,f8904]) ).
fof(f9083,plain,
( sF6 = nand(nand(sF1,nand(nand(sF6,sF1),sF1)),c)
| ~ spl9_2 ),
inference(superposition,[],[f1,f4712]) ).
fof(f9132,plain,
( sF6 = nand(c,nand(sF1,nand(nand(sF6,sF1),sF1)))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f9083,f3583]) ).
fof(f9147,plain,
( sF6 = nand(c,nand(sF6,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f9132,f2471]) ).
fof(f9153,plain,
( sF6 = nand(c,nand(sF1,sF6))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f9147,f3583]) ).
fof(f11131,plain,
! [X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,X1),X1)),
inference(superposition,[],[f3719,f1]) ).
fof(f11246,plain,
! [X0,X1] : nand(X0,X0) = nand(X0,nand(X1,nand(X0,X1))),
inference(forward_demodulation,[],[f11131,f3583]) ).
fof(f11488,plain,
( nand(sF1,sF1) = nand(sF1,nand(sF8,sF2))
| ~ spl9_2 ),
inference(superposition,[],[f11246,f7945]) ).
fof(f11503,plain,
nand(sF7,sF7) = nand(sF7,nand(a,sF8)),
inference(superposition,[],[f11246,f21]) ).
fof(f11507,plain,
! [X0,X1] : nand(X1,X1) = nand(X1,nand(X0,nand(X0,X1))),
inference(superposition,[],[f11246,f4991]) ).
fof(f11615,plain,
nand(sF7,sF7) = nand(sF7,nand(sF8,a)),
inference(forward_demodulation,[],[f11503,f3583]) ).
fof(f11625,plain,
( nand(sF1,sF1) = nand(sF1,nand(sF2,sF8))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f11488,f3583]) ).
fof(f11703,plain,
( nand(sF7,sF7) = nand(sF7,nand(sF8,sF2))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f11615,f29]) ).
fof(f11740,plain,
( nand(sF7,sF7) = nand(sF7,nand(sF2,sF8))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f11703,f3583]) ).
fof(f11840,plain,
nand(sF4,sF4) = nand(sF4,nand(a,sF5)),
inference(superposition,[],[f11507,f15]) ).
fof(f11885,plain,
! [X0,X1] : nand(X1,nand(X1,X0)) = nand(X1,nand(X0,X0)),
inference(superposition,[],[f6149,f11507]) ).
fof(f11990,plain,
nand(sF4,sF4) = nand(sF4,nand(sF5,a)),
inference(forward_demodulation,[],[f11840,f3583]) ).
fof(f12059,plain,
( nand(sF4,sF4) = nand(sF4,nand(sF5,sF2))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f11990,f29]) ).
fof(f12092,plain,
( nand(sF4,sF4) = nand(sF4,nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f12059,f3583]) ).
fof(f12203,plain,
! [X0,X1] : nand(X0,nand(X1,X0)) = nand(X0,nand(X1,X1)),
inference(superposition,[],[f4991,f11885]) ).
fof(f17511,plain,
( sF2 = nand(nand(sF4,sF2),sF1)
| ~ spl9_2 ),
inference(superposition,[],[f5832,f3673]) ).
fof(f17599,plain,
( sF2 = nand(sF1,nand(sF4,sF2))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f17511,f3583]) ).
fof(f17655,plain,
( sF2 = nand(sF1,nand(sF2,sF4))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f17599,f3583]) ).
fof(f17678,plain,
( sF2 = nand(sF1,sF5)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f17655,f1597]) ).
fof(f17692,plain,
( sF5 = nand(sF2,nand(sF5,b))
| ~ spl9_2 ),
inference(superposition,[],[f5831,f17678]) ).
fof(f17733,plain,
( nand(sF1,sF1) = nand(sF1,nand(sF5,sF2))
| ~ spl9_2 ),
inference(superposition,[],[f11246,f17678]) ).
fof(f17737,plain,
( nand(sF1,sF1) = nand(sF1,nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f17733,f3583]) ).
fof(f21373,plain,
( ! [X0] : nand(sF2,X0) = nand(X0,nand(nand(sF2,X0),sF1))
| ~ spl9_2 ),
inference(superposition,[],[f3730,f1595]) ).
fof(f21648,plain,
( ! [X0] : nand(sF2,X0) = nand(X0,nand(sF1,nand(sF2,X0)))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f21373,f3583]) ).
fof(f21859,plain,
( sF3 = nand(c,nand(sF1,sF3))
| ~ spl9_2 ),
inference(superposition,[],[f21648,f1596]) ).
fof(f24456,plain,
( nand(nand(sF5,b),sF2) = nand(sF2,nand(sF2,sF5))
| ~ spl9_2 ),
inference(superposition,[],[f5185,f17692]) ).
fof(f24474,plain,
( nand(sF2,nand(sF5,b)) = nand(sF2,nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f24456,f3583]) ).
fof(f24508,plain,
( sF5 = nand(sF2,nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f24474,f17692]) ).
fof(f34829,plain,
! [X0] : nand(sF5,X0) = nand(nand(sF4,nand(sF5,X0)),X0),
inference(superposition,[],[f3577,f4419]) ).
fof(f34926,plain,
! [X0] : nand(sF5,X0) = nand(X0,nand(sF4,nand(sF5,X0))),
inference(forward_demodulation,[],[f34829,f3583]) ).
fof(f41155,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(nand(X0,nand(X1,X2)),X1),nand(X0,nand(X1,X2)))),
inference(superposition,[],[f11507,f2975]) ).
fof(f41292,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(nand(X0,nand(X1,X2)),X1))),
inference(forward_demodulation,[],[f41155,f3583]) ).
fof(f41630,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(X1,nand(X0,nand(X1,X2))))),
inference(forward_demodulation,[],[f41292,f4991]) ).
fof(f41864,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(X1,X1))),
inference(forward_demodulation,[],[f41630,f12203]) ).
fof(f48855,plain,
! [X0] : nand(sF8,X0) = nand(X0,nand(sF7,nand(sF8,X0))),
inference(superposition,[],[f6274,f9008]) ).
fof(f83697,plain,
( nand(sF2,sF5) = nand(nand(sF1,nand(sF2,sF5)),nand(sF4,nand(sF2,sF5)))
| ~ spl9_2 ),
inference(superposition,[],[f34926,f21648]) ).
fof(f84062,plain,
( nand(sF2,sF5) = nand(nand(sF1,nand(sF2,sF5)),nand(sF4,sF4))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f83697,f12092]) ).
fof(f84194,plain,
( nand(sF2,sF5) = nand(nand(sF4,sF4),nand(sF1,nand(sF2,sF5)))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f84062,f3583]) ).
fof(f84259,plain,
( nand(sF2,sF5) = nand(nand(sF4,sF4),nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f84194,f17737]) ).
fof(f84292,plain,
( nand(sF2,sF5) = nand(nand(sF1,sF1),nand(sF4,sF4))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f84259,f3583]) ).
fof(f146801,plain,
( nand(sF2,sF8) = nand(nand(sF1,nand(sF2,sF8)),nand(sF7,nand(sF2,sF8)))
| ~ spl9_2 ),
inference(superposition,[],[f48855,f21648]) ).
fof(f147299,plain,
( nand(sF2,sF8) = nand(nand(sF1,nand(sF2,sF8)),nand(sF7,sF7))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f146801,f11740]) ).
fof(f147467,plain,
( nand(sF2,sF8) = nand(nand(sF7,sF7),nand(sF1,nand(sF2,sF8)))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f147299,f3583]) ).
fof(f147557,plain,
( nand(sF2,sF8) = nand(nand(sF7,sF7),nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f147467,f11625]) ).
fof(f147611,plain,
( nand(sF2,sF8) = nand(nand(sF1,sF1),nand(sF7,sF7))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f147557,f3583]) ).
fof(f176451,plain,
! [X2,X0,X1] : nand(nand(X1,X1),nand(X0,X0)) = nand(nand(X0,nand(X1,X2)),nand(X1,X1)),
inference(superposition,[],[f6274,f41864]) ).
fof(f178526,plain,
( nand(sF6,nand(sF1,sF1)) = nand(nand(sF1,sF1),nand(c,c))
| ~ spl9_2 ),
inference(superposition,[],[f176451,f9153]) ).
fof(f178527,plain,
( nand(sF3,nand(sF1,sF1)) = nand(nand(sF1,sF1),nand(c,c))
| ~ spl9_2 ),
inference(superposition,[],[f176451,f21859]) ).
fof(f178637,plain,
( nand(sF3,nand(sF1,sF1)) = nand(nand(sF1,sF1),nand(sF4,sF4))
| ~ spl9_2 ),
inference(superposition,[],[f176451,f8187]) ).
fof(f178678,plain,
( nand(sF6,nand(sF1,sF1)) = nand(nand(sF1,sF1),nand(sF7,sF7))
| ~ spl9_2 ),
inference(superposition,[],[f176451,f4718]) ).
fof(f179238,plain,
( nand(sF2,sF8) = nand(sF6,nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f178678,f147611]) ).
fof(f179272,plain,
( nand(sF2,sF5) = nand(sF3,nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f178637,f84292]) ).
fof(f179373,plain,
( nand(sF3,nand(sF1,sF1)) = nand(nand(c,c),nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f178527,f3583]) ).
fof(f179374,plain,
( nand(sF6,nand(sF1,sF1)) = nand(nand(c,c),nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f178526,f3583]) ).
fof(f179794,plain,
( nand(sF2,sF5) = nand(nand(c,c),nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f179373,f179272]) ).
fof(f179795,plain,
( nand(sF2,sF8) = nand(nand(c,c),nand(sF1,sF1))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f179374,f179238]) ).
fof(f180006,plain,
( nand(sF2,sF8) = nand(sF2,sF5)
| ~ spl9_2 ),
inference(forward_demodulation,[],[f179795,f179794]) ).
fof(f180267,plain,
( sF8 = nand(nand(sF8,sF0),nand(sF2,sF5))
| ~ spl9_2 ),
inference(superposition,[],[f4556,f180006]) ).
fof(f180437,plain,
( sF8 = nand(nand(sF2,sF5),nand(sF8,sF0))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f180267,f3583]) ).
fof(f180480,plain,
( sF8 = nand(nand(sF2,sF5),nand(sF0,sF8))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f180437,f3583]) ).
fof(f180501,plain,
( sF8 = nand(nand(sF0,sF8),nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f180480,f3583]) ).
fof(f180509,plain,
( sF8 = nand(a,nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f180501,f1460]) ).
fof(f180513,plain,
( sF8 = nand(sF2,nand(sF2,sF5))
| ~ spl9_2 ),
inference(forward_demodulation,[],[f180509,f29]) ).
fof(f180519,plain,
( sF5 = sF8
| ~ spl9_2 ),
inference(forward_demodulation,[],[f180513,f24508]) ).
fof(f180522,plain,
( $false
| spl9_1
| ~ spl9_2 ),
inference(forward_subsumption_resolution,[],[f180519,f26]) ).
fof(f180523,plain,
( spl9_1
| ~ spl9_2 ),
inference(avatar_contradiction_clause,[],[f180522]) ).
cnf(s1,plain,
( ~ spl9_1
| ~ spl9_2 ),
inference(sat_conversion,[],[f31]) ).
cnf(s2,plain,
spl9_2,
inference(sat_conversion,[],[f1471]) ).
cnf(s11,plain,
( spl9_1
| ~ spl9_2 ),
inference(sat_conversion,[],[f180523]) ).
cnf(s12,plain,
spl9_1,
inference(rat,[],[s11,s2]) ).
cnf(s13,plain,
$false,
inference(rat,[],[s1,s2,s12]) ).
fof(f180524,plain,
$false,
inference(avatar_sat_refutation,[],[s13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO039-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n004.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 21:05:07 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 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
% 11.96/2.39 % (776562)Input is clausal, will run a generic CNF schedule.
% 11.96/2.39 % (776569)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1946680903:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.96/2.39 % (776571)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1852164842:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.96/2.39 % (776567)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=3606393247:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.96/2.39 % (776570)lrs+10_1_sil=8000:sp=occurrence:random_seed=2960433833:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.96/2.39 % (776568)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=354940984:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.96/2.39 % (776572)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4006103969:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.96/2.39 % (776573)dis-21_1_sil=8000:lcm=predicate:random_seed=2699236980: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)
% 11.96/2.39 % (776573)Refutation not found, incomplete strategy
% 11.96/2.39 % (776573)------------------------------
% 11.96/2.39 % (776573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.39 % (776573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.39 % (776573)CaDiCaL version: 2.1.3
% 11.96/2.39 % (776573)Termination reason: Refutation not found, incomplete strategy
% 11.96/2.39 % (776573)Time elapsed: 0.001 s
% 11.96/2.39 % (776573)Peak memory usage: 88 MB
% 11.96/2.39 % (776571)Instruction limit reached!
% 11.96/2.39 % (776571)------------------------------
% 11.96/2.39 % (776571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.39 % (776571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.39 % (776571)CaDiCaL version: 2.1.3
% 11.96/2.39 % (776571)Termination reason: Instruction limit
% 11.96/2.39 % (776571)Termination phase: Saturation
% 11.96/2.39 % (776571)Time elapsed: 0.071 s
% 11.96/2.39 % (776571)Peak memory usage: 89 MB
% 11.96/2.39 % (776571)Instructions burned: 115 (million)
% 11.96/2.39 % (776570)Instruction limit reached!
% 11.96/2.39 % (776570)------------------------------
% 11.96/2.39 % (776570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.39 % (776570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.39 % (776570)CaDiCaL version: 2.1.3
% 11.96/2.39 % (776570)Termination reason: Instruction limit
% 11.96/2.39 % (776570)Termination phase: Saturation
% 11.96/2.39 % (776570)Time elapsed: 0.067 s
% 11.96/2.39 % (776570)Peak memory usage: 89 MB
% 11.96/2.39 % (776570)Instructions burned: 108 (million)
% 11.96/2.39 % (776572)Instruction limit reached!
% 11.96/2.39 % (776572)------------------------------
% 11.96/2.39 % (776572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.39 % (776572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.39 % (776572)CaDiCaL version: 2.1.3
% 11.96/2.39 % (776572)Termination reason: Instruction limit
% 11.96/2.39 % (776572)Termination phase: Saturation
% 11.96/2.39 % (776572)Time elapsed: 0.102 s
% 11.96/2.39 % (776572)Peak memory usage: 89 MB
% 11.96/2.39 % (776572)Instructions burned: 181 (million)
% 11.96/2.39 % (776581)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=1675298807:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.96/2.39 % (776581)Refutation not found, incomplete strategy
% 11.96/2.39 % (776581)------------------------------
% 11.96/2.39 % (776581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.96/2.39 % (776581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.96/2.39 % (776581)CaDiCaL version: 2.1.3
% 11.96/2.39 % (776581)Termination reason: Refutation not found, incomplete strategy
% 11.96/2.39 % (776581)Time elapsed: 0.001 s
% 11.96/2.39 % (776581)Peak memory usage: 88 MB
% 11.96/2.39 % (776582)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=32577001: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)
% 22.33/3.90 % (776582)Refutation not found, incomplete strategy
% 22.33/3.90 % (776582)------------------------------
% 22.33/3.90 % (776582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.33/3.90 % (776582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.33/3.90 % (776582)CaDiCaL version: 2.1.3
% 22.33/3.90 % (776582)Termination reason: Refutation not found, incomplete strategy
% 22.33/3.90 % (776582)Time elapsed: 0.001 s
% 22.33/3.90 % (776582)Peak memory usage: 88 MB
% 22.33/3.90 % (776583)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1505148193:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 22.33/3.90 % (776583)Refutation not found, incomplete strategy
% 22.33/3.90 % (776583)------------------------------
% 22.33/3.90 % (776583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.33/3.90 % (776583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.33/3.90 % (776583)CaDiCaL version: 2.1.3
% 22.33/3.90 % (776583)Termination reason: Refutation not found, incomplete strategy
% 22.33/3.90 % (776583)Time elapsed: 0.001 s
% 22.33/3.90 % (776583)Peak memory usage: 88 MB
% 22.33/3.90 % (776573)------------------------------
% 22.33/3.90 % (776573)------------------------------
% 22.33/3.90 % (776587)lrs+10_64_to=lpo:sil=8000:random_seed=300016288:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 22.33/3.90 % (776581)------------------------------
% 22.33/3.90 % (776581)------------------------------
% 22.33/3.90 % (776582)------------------------------
% 22.33/3.90 % (776582)------------------------------
% 22.33/3.90 % (776587)Instruction limit reached!
% 22.33/3.90 % (776587)------------------------------
% 22.33/3.90 % (776587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.33/3.90 % (776587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.33/3.90 % (776587)CaDiCaL version: 2.1.3
% 22.33/3.90 % (776587)Termination reason: Instruction limit
% 22.33/3.90 % (776587)Termination phase: Saturation
% 22.33/3.90 % (776587)Time elapsed: 0.078 s
% 22.33/3.90 % (776587)Peak memory usage: 88 MB
% 22.33/3.90 % (776587)Instructions burned: 126 (million)
% 22.33/3.90 % (776583)------------------------------
% 22.33/3.90 % (776583)------------------------------
% 22.33/3.90 % (776589)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2977734089:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 22.33/3.90 % (776590)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3407361929:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 22.33/3.90 % (776591)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1600607158:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 22.33/3.90 % (776592)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=2197157730:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 22.33/3.90 % (776590)Instruction limit reached!
% 22.33/3.90 % (776590)------------------------------
% 22.33/3.90 % (776590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.33/3.90 % (776590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.33/3.90 % (776590)CaDiCaL version: 2.1.3
% 22.33/3.90 % (776590)Termination reason: Instruction limit
% 22.33/3.90 % (776590)Termination phase: Saturation
% 22.33/3.90 % (776590)Time elapsed: 0.093 s
% 22.33/3.90 % (776590)Peak memory usage: 92 MB
% 22.33/3.90 % (776590)Instructions burned: 159 (million)
% 22.33/3.90 % (776589)Instruction limit reached!
% 22.33/3.90 % (776589)------------------------------
% 22.33/3.90 % (776589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.33/3.90 % (776589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.33/3.90 % (776589)CaDiCaL version: 2.1.3
% 22.33/3.90 % (776589)Termination reason: Instruction limit
% 22.33/3.90 % (776589)Termination phase: Saturation
% 22.33/3.90 % (776589)Time elapsed: 0.120 s
% 22.33/3.90 % (776589)Peak memory usage: 89 MB
% 22.33/3.90 % (776589)Instructions burned: 195 (million)
% 22.33/3.90 % (776592)Instruction limit reached!
% 22.33/3.90 % (776592)------------------------------
% 22.33/3.90 % (776592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.33/3.90 % (776592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.33/3.90 % (776592)CaDiCaL version: 2.1.3
% 44.01/6.82 % (776592)Termination reason: Instruction limit
% 44.01/6.82 % (776592)Termination phase: Saturation
% 44.01/6.82 % (776592)Time elapsed: 0.067 s
% 44.01/6.82 % (776592)Peak memory usage: 89 MB
% 44.01/6.82 % (776592)Instructions burned: 107 (million)
% 44.01/6.82 % (776598)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=845405086:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 44.01/6.82 % (776597)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=87015551:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 44.01/6.82 % (776597)Refutation not found, incomplete strategy
% 44.01/6.82 % (776597)------------------------------
% 44.01/6.82 % (776597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.01/6.82 % (776597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.01/6.82 % (776597)CaDiCaL version: 2.1.3
% 44.01/6.82 % (776597)Termination reason: Refutation not found, incomplete strategy
% 44.01/6.82 % (776597)Time elapsed: 0.001 s
% 44.01/6.82 % (776597)Peak memory usage: 88 MB
% 44.01/6.82 % (776599)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1441265104:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 44.01/6.82 % (776598)Instruction limit reached!
% 44.01/6.82 % (776598)------------------------------
% 44.01/6.82 % (776598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.01/6.82 % (776598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.01/6.82 % (776598)CaDiCaL version: 2.1.3
% 44.01/6.82 % (776598)Termination reason: Instruction limit
% 44.01/6.82 % (776598)Termination phase: Saturation
% 44.01/6.82 % (776598)Time elapsed: 0.137 s
% 44.01/6.82 % (776598)Peak memory usage: 92 MB
% 44.01/6.82 % (776598)Instructions burned: 243 (million)
% 44.01/6.82 % (776597)------------------------------
% 44.01/6.82 % (776597)------------------------------
% 44.01/6.82 % (776603)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3457692335:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 44.01/6.82 % (776603)Instruction limit reached!
% 44.01/6.82 % (776603)------------------------------
% 44.01/6.82 % (776603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.01/6.82 % (776603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.01/6.82 % (776603)CaDiCaL version: 2.1.3
% 44.01/6.82 % (776603)Termination reason: Instruction limit
% 44.01/6.82 % (776603)Termination phase: Saturation
% 44.01/6.82 % (776603)Time elapsed: 0.085 s
% 44.01/6.82 % (776603)Peak memory usage: 89 MB
% 44.01/6.82 % (776603)Instructions burned: 135 (million)
% 44.01/6.82 % (776604)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=998157600:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 44.01/6.82 % (776606)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=986641286:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 44.01/6.82 % (776606)Instruction limit reached!
% 44.01/6.82 % (776606)------------------------------
% 44.01/6.82 % (776606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.01/6.82 % (776606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.01/6.82 % (776606)CaDiCaL version: 2.1.3
% 44.01/6.82 % (776606)Termination reason: Instruction limit
% 44.01/6.82 % (776606)Termination phase: Saturation
% 44.01/6.82 % (776606)Time elapsed: 0.116 s
% 44.01/6.82 % (776606)Peak memory usage: 90 MB
% 44.01/6.82 % (776606)Instructions burned: 193 (million)
% 44.01/6.82 % (776604)Instruction limit reached!
% 44.01/6.82 % (776604)------------------------------
% 44.01/6.82 % (776604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.01/6.82 % (776604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.01/6.82 % (776604)CaDiCaL version: 2.1.3
% 44.01/6.82 % (776604)Termination reason: Instruction limit
% 44.01/6.82 % (776604)Termination phase: Saturation
% 44.01/6.82 % (776604)Time elapsed: 0.294 s
% 44.01/6.82 % (776604)Peak memory usage: 92 MB
% 44.01/6.82 % (776604)Instructions burned: 500 (million)
% 44.01/6.82 % (776609)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=337742354:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 44.01/6.82 % (776610)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1025992420:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 61.66/9.34 % (776609)Instruction limit reached!
% 61.66/9.34 % (776609)------------------------------
% 61.66/9.34 % (776609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.66/9.34 % (776609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.66/9.34 % (776609)CaDiCaL version: 2.1.3
% 61.66/9.34 % (776609)Termination reason: Instruction limit
% 61.66/9.34 % (776609)Termination phase: Saturation
% 61.66/9.34 % (776609)Time elapsed: 0.167 s
% 61.66/9.34 % (776609)Peak memory usage: 91 MB
% 61.66/9.34 % (776609)Instructions burned: 264 (million)
% 61.66/9.34 % (776610)Instruction limit reached!
% 61.66/9.34 % (776610)------------------------------
% 61.66/9.34 % (776610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.66/9.34 % (776610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.66/9.34 % (776610)CaDiCaL version: 2.1.3
% 61.66/9.34 % (776610)Termination reason: Instruction limit
% 61.66/9.34 % (776610)Termination phase: Saturation
% 61.66/9.34 % (776610)Time elapsed: 0.099 s
% 61.66/9.34 % (776610)Peak memory usage: 89 MB
% 61.66/9.34 % (776610)Instructions burned: 156 (million)
% 61.66/9.34 % (776613)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=3883616910:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 61.66/9.34 % (776614)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3649962034:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 61.66/9.34 % (776614)Instruction limit reached!
% 61.66/9.34 % (776614)------------------------------
% 61.66/9.34 % (776614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.66/9.34 % (776614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.66/9.34 % (776614)CaDiCaL version: 2.1.3
% 61.66/9.34 % (776614)Termination reason: Instruction limit
% 61.66/9.34 % (776614)Termination phase: Saturation
% 61.66/9.34 % (776614)Time elapsed: 0.286 s
% 61.66/9.34 % (776614)Peak memory usage: 98 MB
% 61.66/9.34 % (776614)Instructions burned: 539 (million)
% 61.66/9.34 % (776617)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=668424273:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 61.66/9.34 % (776617)Instruction limit reached!
% 61.66/9.34 % (776617)------------------------------
% 61.66/9.34 % (776617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.66/9.34 % (776617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.66/9.34 % (776617)CaDiCaL version: 2.1.3
% 61.66/9.34 % (776617)Termination reason: Instruction limit
% 61.66/9.34 % (776617)Termination phase: Saturation
% 61.66/9.34 % (776617)Time elapsed: 0.110 s
% 61.66/9.34 % (776617)Peak memory usage: 88 MB
% 61.66/9.34 % (776617)Instructions burned: 181 (million)
% 61.66/9.34 % (776619)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=4138752956:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 61.66/9.34 % (776591)Instruction limit reached!
% 61.66/9.34 % (776591)------------------------------
% 61.66/9.34 % (776591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.66/9.34 % (776591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.66/9.34 % (776591)CaDiCaL version: 2.1.3
% 61.66/9.34 % (776591)Termination reason: Instruction limit
% 61.66/9.34 % (776591)Termination phase: Saturation
% 61.66/9.34 % (776591)Time elapsed: 2.122 s
% 61.66/9.34 % (776591)Peak memory usage: 152 MB
% 61.66/9.34 % (776591)Instructions burned: 3394 (million)
% 61.66/9.34 % (776622)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=1347303213:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 61.66/9.34 % (776622)Instruction limit reached!
% 61.66/9.34 % (776622)------------------------------
% 61.66/9.34 % (776622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.66/9.34 % (776622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.66/9.34 % (776622)CaDiCaL version: 2.1.3
% 61.66/9.34 % (776622)Termination reason: Instruction limit
% 61.66/9.34 % (776622)Termination phase: Saturation
% 61.66/9.34 % (776622)Time elapsed: 0.239 s
% 61.66/9.34 % (776622)Peak memory usage: 99 MB
% 82.90/12.37 % (776622)Instructions burned: 413 (million)
% 82.90/12.37 % (776624)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=2997082153:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi)
% 82.90/12.37 % (776613)Instruction limit reached!
% 82.90/12.37 % (776613)------------------------------
% 82.90/12.37 % (776613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.90/12.37 % (776613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.90/12.37 % (776613)CaDiCaL version: 2.1.3
% 82.90/12.37 % (776613)Termination reason: Instruction limit
% 82.90/12.37 % (776613)Termination phase: Saturation
% 82.90/12.37 % (776613)Time elapsed: 1.995 s
% 82.90/12.37 % (776613)Peak memory usage: 146 MB
% 82.90/12.37 % (776613)Instructions burned: 3257 (million)
% 82.90/12.37 % (776626)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=1131341268:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 82.90/12.37 % (776626)Refutation not found, incomplete strategy
% 82.90/12.37 % (776626)------------------------------
% 82.90/12.37 % (776626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.90/12.37 % (776626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.90/12.37 % (776626)CaDiCaL version: 2.1.3
% 82.90/12.37 % (776626)Termination reason: Refutation not found, incomplete strategy
% 82.90/12.37 % (776626)Time elapsed: 0.001 s
% 82.90/12.37 % (776626)Peak memory usage: 88 MB
% 82.90/12.37 % (776599)Instruction limit reached!
% 82.90/12.37 % (776599)------------------------------
% 82.90/12.37 % (776599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.90/12.37 % (776599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.90/12.37 % (776599)CaDiCaL version: 2.1.3
% 82.90/12.37 % (776599)Termination reason: Instruction limit
% 82.90/12.37 % (776599)Termination phase: Saturation
% 82.90/12.37 % (776599)Time elapsed: 3.190 s
% 82.90/12.37 % (776599)Peak memory usage: 166 MB
% 82.90/12.37 % (776599)Instructions burned: 5208 (million)
% 82.90/12.37 % (776628)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1348593366:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi)
% 82.90/12.37 % (776628)Refutation not found, incomplete strategy
% 82.90/12.37 % (776628)------------------------------
% 82.90/12.37 % (776628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.90/12.37 % (776628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.90/12.37 % (776628)CaDiCaL version: 2.1.3
% 82.90/12.37 % (776628)Termination reason: Refutation not found, incomplete strategy
% 82.90/12.37 % (776628)Time elapsed: 0.001 s
% 82.90/12.37 % (776628)Peak memory usage: 88 MB
% 82.90/12.37 % (776626)------------------------------
% 82.90/12.37 % (776626)------------------------------
% 82.90/12.37 % (776630)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1358418851:i=598:bs=on:bd=preordered:av=off:ss=axioms_2956 on theBenchmark for (2956ds/598Mi)
% 82.90/12.37 % (776628)------------------------------
% 82.90/12.37 % (776628)------------------------------
% 82.90/12.37 % (776632)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2520097925:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi)
% 82.90/12.37 % (776630)Instruction limit reached!
% 82.90/12.37 % (776630)------------------------------
% 82.90/12.37 % (776630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.90/12.37 % (776630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.90/12.37 % (776630)CaDiCaL version: 2.1.3
% 82.90/12.37 % (776630)Termination reason: Instruction limit
% 82.90/12.37 % (776630)Termination phase: Saturation
% 82.90/12.37 % (776630)Time elapsed: 0.362 s
% 82.90/12.37 % (776630)Peak memory usage: 95 MB
% 82.90/12.37 % (776630)Instructions burned: 599 (million)
% 82.90/12.37 % (776634)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=462026687:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2951 on theBenchmark for (2951ds/1997Mi)
% 82.90/12.37 % (776634)Instruction limit reached!
% 82.90/12.37 % (776634)------------------------------
% 82.90/12.37 % (776634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.16/16.75 % (776634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.16/16.75 % (776634)CaDiCaL version: 2.1.3
% 114.16/16.75 % (776634)Termination reason: Instruction limit
% 114.16/16.75 % (776634)Termination phase: Saturation
% 114.16/16.75 % (776634)Time elapsed: 1.188 s
% 114.16/16.75 % (776634)Peak memory usage: 139 MB
% 114.16/16.75 % (776634)Instructions burned: 1997 (million)
% 114.16/16.75 % (776636)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=1024045978:i=2088:bd=preordered:av=off_2938 on theBenchmark for (2938ds/2088Mi)
% 114.16/16.75 % (776632)Instruction limit reached!
% 114.16/16.75 % (776632)------------------------------
% 114.16/16.75 % (776632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.16/16.75 % (776632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.16/16.75 % (776632)CaDiCaL version: 2.1.3
% 114.16/16.75 % (776632)Termination reason: Instruction limit
% 114.16/16.75 % (776632)Termination phase: Saturation
% 114.16/16.75 % (776632)Time elapsed: 1.724 s
% 114.16/16.75 % (776632)Peak memory usage: 147 MB
% 114.16/16.75 % (776632)Instructions burned: 2990 (million)
% 114.16/16.75 % (776638)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4214152368:i=1098:nicw=on_2936 on theBenchmark for (2936ds/1098Mi)
% 114.16/16.75 % (776638)Instruction limit reached!
% 114.16/16.75 % (776638)------------------------------
% 114.16/16.75 % (776638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.16/16.75 % (776638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.16/16.75 % (776638)CaDiCaL version: 2.1.3
% 114.16/16.75 % (776638)Termination reason: Instruction limit
% 114.16/16.75 % (776638)Termination phase: Saturation
% 114.16/16.75 % (776638)Time elapsed: 0.644 s
% 114.16/16.75 % (776638)Peak memory usage: 105 MB
% 114.16/16.75 % (776638)Instructions burned: 1099 (million)
% 114.16/16.75 % (776640)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2691458506:i=433:bd=preordered_2928 on theBenchmark for (2928ds/433Mi)
% 114.16/16.75 % (776640)Refutation not found, incomplete strategy
% 114.16/16.75 % (776640)------------------------------
% 114.16/16.75 % (776640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.16/16.75 % (776640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.16/16.75 % (776640)CaDiCaL version: 2.1.3
% 114.16/16.75 % (776640)Termination reason: Refutation not found, incomplete strategy
% 114.16/16.75 % (776640)Time elapsed: 0.001 s
% 114.16/16.75 % (776640)Peak memory usage: 88 MB
% 114.16/16.75 % (776640)Instructions burned: 1 (million)
% 114.16/16.75 % (776640)------------------------------
% 114.16/16.75 % (776640)------------------------------
% 114.16/16.75 % (776636)Instruction limit reached!
% 114.16/16.75 % (776636)------------------------------
% 114.16/16.75 % (776636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.16/16.75 % (776636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.16/16.75 % (776636)CaDiCaL version: 2.1.3
% 114.16/16.75 % (776636)Termination reason: Instruction limit
% 114.16/16.75 % (776636)Termination phase: Saturation
% 114.16/16.75 % (776636)Time elapsed: 1.285 s
% 114.16/16.75 % (776636)Peak memory usage: 138 MB
% 114.16/16.75 % (776636)Instructions burned: 2088 (million)
% 114.16/16.75 % (776642)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1021540477:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2924 on theBenchmark for (2924ds/2942Mi)
% 114.16/16.75 % (776643)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=794917700:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2923 on theBenchmark for (2923ds/6922Mi)
% 114.16/16.75 % (776624)Instruction limit reached!
% 114.16/16.75 % (776624)------------------------------
% 114.16/16.75 % (776624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.16/16.75 % (776624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.16/16.75 % (776624)CaDiCaL version: 2.1.3
% 114.16/16.75 % (776624)Termination reason: Instruction limit
% 114.16/16.75 % (776624)Termination phase: Saturation
% 114.16/16.75 % (776624)Time elapsed: 5.177 s
% 114.16/16.75 % (776624)Peak memory usage: 193 MB
% 114.16/16.75 % (776624)Instructions burned: 8478 (million)
% 114.16/16.75 % (776646)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=3329033287:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2914 on theBenchmark for (2914ds/596Mi)
% 135.29/19.82 % (776646)Refutation not found, incomplete strategy
% 135.29/19.82 % (776646)------------------------------
% 135.29/19.82 % (776646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.29/19.82 % (776646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.29/19.82 % (776646)CaDiCaL version: 2.1.3
% 135.29/19.82 % (776646)Termination reason: Refutation not found, incomplete strategy
% 135.29/19.82 % (776646)Time elapsed: 0.001 s
% 135.29/19.82 % (776646)Peak memory usage: 88 MB
% 135.29/19.82 % (776646)Instructions burned: 1 (million)
% 135.29/19.82 % (776646)------------------------------
% 135.29/19.82 % (776646)------------------------------
% 135.29/19.82 % (776619)Instruction limit reached!
% 135.29/19.82 % (776619)------------------------------
% 135.29/19.82 % (776619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.29/19.82 % (776619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.29/19.82 % (776619)CaDiCaL version: 2.1.3
% 135.29/19.82 % (776619)Termination reason: Instruction limit
% 135.29/19.82 % (776619)Termination phase: Saturation
% 135.29/19.82 % (776619)Time elapsed: 6.391 s
% 135.29/19.82 % (776619)Peak memory usage: 200 MB
% 135.29/19.82 % (776619)Instructions burned: 10307 (million)
% 135.29/19.82 % (776648)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=1769310035:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2910 on theBenchmark for (2910ds/4123Mi)
% 135.29/19.82 % (776649)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=594381310:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2909 on theBenchmark for (2909ds/16411Mi)
% 135.29/19.82 % (776642)Instruction limit reached!
% 135.29/19.82 % (776642)------------------------------
% 135.29/19.82 % (776642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.29/19.82 % (776642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.29/19.82 % (776642)CaDiCaL version: 2.1.3
% 135.29/19.82 % (776642)Termination reason: Instruction limit
% 135.29/19.82 % (776642)Termination phase: Saturation
% 135.29/19.82 % (776642)Time elapsed: 1.842 s
% 135.29/19.82 % (776642)Peak memory usage: 146 MB
% 135.29/19.82 % (776642)Instructions burned: 2943 (million)
% 135.29/19.82 % (776652)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=666238520:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2905 on theBenchmark for (2905ds/1670Mi)
% 135.29/19.82 % (776652)Instruction limit reached!
% 135.29/19.82 % (776652)------------------------------
% 135.29/19.82 % (776652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.29/19.82 % (776652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.29/19.82 % (776652)CaDiCaL version: 2.1.3
% 135.29/19.82 % (776652)Termination reason: Instruction limit
% 135.29/19.82 % (776652)Termination phase: Saturation
% 135.29/19.82 % (776652)Time elapsed: 1.038 s
% 135.29/19.82 % (776652)Peak memory usage: 136 MB
% 135.29/19.82 % (776652)Instructions burned: 1671 (million)
% 135.29/19.82 % (776654)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=972888027:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2893 on theBenchmark for (2893ds/1722Mi)
% 135.29/19.82 % (776648)Instruction limit reached!
% 135.29/19.82 % (776648)------------------------------
% 135.29/19.82 % (776648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.29/19.82 % (776648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.29/19.82 % (776648)CaDiCaL version: 2.1.3
% 135.29/19.82 % (776648)Termination reason: Instruction limit
% 135.29/19.82 % (776648)Termination phase: Saturation
% 135.29/19.82 % (776648)Time elapsed: 2.467 s
% 135.29/19.82 % (776648)Peak memory usage: 158 MB
% 135.29/19.82 % (776648)Instructions burned: 4123 (million)
% 135.29/19.82 % (776656)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=2505568439:cts=off:cond=on:i=9530:bs=on:fsd=on_2884 on theBenchmark for (2884ds/9530Mi)
% 135.29/19.82 % (776643)Instruction limit reached!
% 135.29/19.82 % (776643)------------------------------
% 154.49/22.46 % (776643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.49/22.46 % (776643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.49/22.46 % (776643)CaDiCaL version: 2.1.3
% 154.49/22.46 % (776643)Termination reason: Instruction limit
% 154.49/22.46 % (776643)Termination phase: Saturation
% 154.49/22.46 % (776643)Time elapsed: 3.997 s
% 154.49/22.46 % (776643)Peak memory usage: 156 MB
% 154.49/22.46 % (776643)Instructions burned: 6922 (million)
% 154.49/22.46 % (776658)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2970419891:st=2:i=4495:sd=10:ss=included_2882 on theBenchmark for (2882ds/4495Mi)
% 154.49/22.46 % (776654)Instruction limit reached!
% 154.49/22.46 % (776654)------------------------------
% 154.49/22.46 % (776654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.49/22.46 % (776654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.49/22.46 % (776654)CaDiCaL version: 2.1.3
% 154.49/22.46 % (776654)Termination reason: Instruction limit
% 154.49/22.46 % (776654)Termination phase: Saturation
% 154.49/22.46 % (776654)Time elapsed: 1.080 s
% 154.49/22.46 % (776654)Peak memory usage: 136 MB
% 154.49/22.46 % (776654)Instructions burned: 1722 (million)
% 154.49/22.46 % (776660)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=2406594403:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2881 on theBenchmark for (2881ds/4920Mi)
% 154.49/22.46 % (776658)Instruction limit reached!
% 154.49/22.46 % (776658)------------------------------
% 154.49/22.46 % (776658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.49/22.46 % (776658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.49/22.46 % (776658)CaDiCaL version: 2.1.3
% 154.49/22.46 % (776658)Termination reason: Instruction limit
% 154.49/22.46 % (776658)Termination phase: Saturation
% 154.49/22.46 % (776658)Time elapsed: 2.765 s
% 154.49/22.46 % (776658)Peak memory usage: 157 MB
% 154.49/22.46 % (776658)Instructions burned: 4496 (million)
% 154.49/22.46 % (776662)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=2196380091:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2853 on theBenchmark for (2853ds/2083Mi)
% 154.49/22.46 % (776660)Instruction limit reached!
% 154.49/22.46 % (776660)------------------------------
% 154.49/22.46 % (776660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.49/22.46 % (776660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.49/22.46 % (776660)CaDiCaL version: 2.1.3
% 154.49/22.46 % (776660)Termination reason: Instruction limit
% 154.49/22.46 % (776660)Termination phase: Saturation
% 154.49/22.46 % (776660)Time elapsed: 3.012 s
% 154.49/22.46 % (776660)Peak memory usage: 167 MB
% 154.49/22.46 % (776660)Instructions burned: 4921 (million)
% 154.49/22.46 % (776664)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=2857526218:i=4629:av=off:gsp=on_2849 on theBenchmark for (2849ds/4629Mi)
% 154.49/22.46 % (776664)Refutation not found, incomplete strategy
% 154.49/22.46 % (776664)------------------------------
% 154.49/22.46 % (776664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.49/22.46 % (776664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.49/22.46 % (776664)CaDiCaL version: 2.1.3
% 154.49/22.46 % (776664)Termination reason: Refutation not found, incomplete strategy
% 154.49/22.46 % (776664)Time elapsed: 0.567 s
% 154.49/22.46 % (776664)Peak memory usage: 127 MB
% 154.49/22.46 % (776664)Instructions burned: 857 (million)
% 154.49/22.46 % (776664)------------------------------
% 154.49/22.46 % (776664)------------------------------
% 154.49/22.46 % (776662)Instruction limit reached!
% 154.49/22.46 % (776662)------------------------------
% 154.49/22.46 % (776662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.49/22.46 % (776662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.49/22.46 % (776662)CaDiCaL version: 2.1.3
% 154.49/22.46 % (776662)Termination reason: Instruction limit
% 154.49/22.46 % (776662)Termination phase: Saturation
% 154.49/22.46 % (776662)Time elapsed: 1.284 s
% 154.49/22.46 % (776662)Peak memory usage: 139 MB
% 154.49/22.46 % (776662)Instructions burned: 2083 (million)
% 154.49/22.46 % (776666)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2000217683:i=1258:av=off_2840 on theBenchmark for (2840ds/1258Mi)
% 183.75/26.59 % (776667)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2036065363:i=7343:av=off:ss=included_2839 on theBenchmark for (2839ds/7343Mi)
% 183.75/26.59 % (776666)Instruction limit reached!
% 183.75/26.59 % (776666)------------------------------
% 183.75/26.59 % (776666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.75/26.59 % (776666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.75/26.59 % (776666)CaDiCaL version: 2.1.3
% 183.75/26.59 % (776666)Termination reason: Instruction limit
% 183.75/26.59 % (776666)Termination phase: Saturation
% 183.75/26.59 % (776666)Time elapsed: 0.680 s
% 183.75/26.59 % (776666)Peak memory usage: 105 MB
% 183.75/26.59 % (776666)Instructions burned: 1258 (million)
% 183.75/26.59 % (776670)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2904270050:i=1325:sd=2:ss=axioms:sgt=16_2832 on theBenchmark for (2832ds/1325Mi)
% 183.75/26.59 % (776670)Refutation not found, incomplete strategy
% 183.75/26.59 % (776670)------------------------------
% 183.75/26.59 % (776670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.75/26.59 % (776670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.75/26.59 % (776670)CaDiCaL version: 2.1.3
% 183.75/26.59 % (776670)Termination reason: Refutation not found, incomplete strategy
% 183.75/26.59 % (776670)Time elapsed: 0.001 s
% 183.75/26.59 % (776670)Peak memory usage: 88 MB
% 183.75/26.59 % (776670)------------------------------
% 183.75/26.59 % (776670)------------------------------
% 183.75/26.59 % (776672)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=1600026422:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2828 on theBenchmark for (2828ds/2646Mi)
% 183.75/26.59 % (776656)Instruction limit reached!
% 183.75/26.59 % (776656)------------------------------
% 183.75/26.59 % (776656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.75/26.59 % (776656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.75/26.59 % (776656)CaDiCaL version: 2.1.3
% 183.75/26.59 % (776656)Termination reason: Instruction limit
% 183.75/26.59 % (776656)Termination phase: Saturation
% 183.75/26.59 % (776656)Time elapsed: 5.844 s
% 183.75/26.59 % (776656)Peak memory usage: 191 MB
% 183.75/26.59 % (776656)Instructions burned: 9530 (million)
% 183.75/26.59 % (776674)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=332383967:i=1489:sd=2:ep=R:ss=axioms_2824 on theBenchmark for (2824ds/1489Mi)
% 183.75/26.59 % (776674)Refutation not found, incomplete strategy
% 183.75/26.59 % (776674)------------------------------
% 183.75/26.59 % (776674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.75/26.59 % (776674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.75/26.59 % (776674)CaDiCaL version: 2.1.3
% 183.75/26.59 % (776674)Termination reason: Refutation not found, incomplete strategy
% 183.75/26.59 % (776674)Time elapsed: 0.566 s
% 183.75/26.59 % (776674)Peak memory usage: 127 MB
% 183.75/26.59 % (776674)Instructions burned: 854 (million)
% 183.75/26.59 % (776674)------------------------------
% 183.75/26.59 % (776674)------------------------------
% 183.75/26.59 % (776676)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=219501219:i=1503_2815 on theBenchmark for (2815ds/1503Mi)
% 183.75/26.59 % (776672)Instruction limit reached!
% 183.75/26.59 % (776672)------------------------------
% 183.75/26.59 % (776672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.75/26.59 % (776672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.75/26.59 % (776672)CaDiCaL version: 2.1.3
% 183.75/26.59 % (776672)Termination reason: Instruction limit
% 183.75/26.59 % (776672)Termination phase: Saturation
% 183.75/26.59 % (776672)Time elapsed: 1.574 s
% 183.75/26.59 % (776672)Peak memory usage: 146 MB
% 183.75/26.59 % (776672)Instructions burned: 2647 (million)
% 183.75/26.59 % (776678)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1823701027:i=13942:kws=frequency_2811 on theBenchmark for (2811ds/13942Mi)
% 183.75/26.59 % (776676)Refutation not found, incomplete strategy
% 183.75/26.59 % (776676)------------------------------
% 183.75/26.59 % (776676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.75/26.59 % (776676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776676)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776676)Termination reason: Refutation not found, incomplete strategy
% 105.65/27.22 % (776676)Time elapsed: 0.584 s
% 105.65/27.22 % (776676)Peak memory usage: 128 MB
% 105.65/27.22 % (776676)Instructions burned: 888 (million)
% 105.65/27.22 % (776676)------------------------------
% 105.65/27.22 % (776676)------------------------------
% 105.65/27.22 % (776649)Instruction limit reached!
% 105.65/27.22 % (776649)------------------------------
% 105.65/27.22 % (776649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776649)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776649)Termination reason: Instruction limit
% 105.65/27.22 % (776649)Termination phase: Saturation
% 105.65/27.22 % (776649)Time elapsed: 10.310 s
% 105.65/27.22 % (776649)Peak memory usage: 229 MB
% 105.65/27.22 % (776649)Instructions burned: 16412 (million)
% 105.65/27.22 % (776680)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=3103654418:i=3604:fsr=off:er=filter_2805 on theBenchmark for (2805ds/3604Mi)
% 105.65/27.22 % (776681)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1454746596:i=1876:sd=1:ss=included:sgt=32_2805 on theBenchmark for (2805ds/1876Mi)
% 105.65/27.22 % (776667)Instruction limit reached!
% 105.65/27.22 % (776667)------------------------------
% 105.65/27.22 % (776667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776667)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776667)Termination reason: Instruction limit
% 105.65/27.22 % (776667)Termination phase: Saturation
% 105.65/27.22 % (776667)Time elapsed: 4.439 s
% 105.65/27.22 % (776667)Peak memory usage: 185 MB
% 105.65/27.22 % (776667)Instructions burned: 7344 (million)
% 105.65/27.22 % (776684)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=102934709:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2793 on theBenchmark for (2793ds/1932Mi)
% 105.65/27.22 % (776681)Instruction limit reached!
% 105.65/27.22 % (776681)------------------------------
% 105.65/27.22 % (776681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776681)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776681)Termination reason: Instruction limit
% 105.65/27.22 % (776681)Termination phase: Saturation
% 105.65/27.22 % (776681)Time elapsed: 1.191 s
% 105.65/27.22 % (776681)Peak memory usage: 136 MB
% 105.65/27.22 % (776681)Instructions burned: 1877 (million)
% 105.65/27.22 % (776686)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=4019804637:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2791 on theBenchmark for (2791ds/1980Mi)
% 105.65/27.22 % (776684)Refutation not found, incomplete strategy
% 105.65/27.22 % (776684)------------------------------
% 105.65/27.22 % (776684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776684)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776684)Termination reason: Refutation not found, incomplete strategy
% 105.65/27.22 % (776684)Time elapsed: 0.571 s
% 105.65/27.22 % (776684)Peak memory usage: 127 MB
% 105.65/27.22 % (776684)Instructions burned: 859 (million)
% 105.65/27.22 % (776684)------------------------------
% 105.65/27.22 % (776684)------------------------------
% 105.65/27.22 % (776688)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=1385569299:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2784 on theBenchmark for (2784ds/3902Mi)
% 105.65/27.22 % (776680)Instruction limit reached!
% 105.65/27.22 % (776680)------------------------------
% 105.65/27.22 % (776680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776680)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776680)Termination reason: Instruction limit
% 105.65/27.22 % (776680)Termination phase: Saturation
% 105.65/27.22 % (776680)Time elapsed: 2.273 s
% 105.65/27.22 % (776680)Peak memory usage: 150 MB
% 105.65/27.22 % (776680)Instructions burned: 3605 (million)
% 105.65/27.22 % (776690)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=35432999:avsq=on:i=3916:aac=none:amm=off_2781 on theBenchmark for (2781ds/3916Mi)
% 105.65/27.22 % (776686)Instruction limit reached!
% 105.65/27.22 % (776686)------------------------------
% 105.65/27.22 % (776686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776686)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776686)Termination reason: Instruction limit
% 105.65/27.22 % (776686)Termination phase: Saturation
% 105.65/27.22 % (776686)Time elapsed: 1.187 s
% 105.65/27.22 % (776686)Peak memory usage: 138 MB
% 105.65/27.22 % (776686)Instructions burned: 1980 (million)
% 105.65/27.22 % (776692)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2958148423:cond=on:i=3940:av=off:er=known_2778 on theBenchmark for (2778ds/3940Mi)
% 105.65/27.22 % (776688)Refutation not found, incomplete strategy
% 105.65/27.22 % (776688)------------------------------
% 105.65/27.22 % (776688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776688)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776688)Termination reason: Refutation not found, incomplete strategy
% 105.65/27.22 % (776688)Time elapsed: 0.572 s
% 105.65/27.22 % (776688)Peak memory usage: 127 MB
% 105.65/27.22 % (776688)Instructions burned: 860 (million)
% 105.65/27.22 % (776688)------------------------------
% 105.65/27.22 % (776688)------------------------------
% 105.65/27.22 % (776695)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3247547842:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2774 on theBenchmark for (2774ds/3980Mi)
% 105.65/27.22 % (776692)Instruction limit reached!
% 105.65/27.22 % (776692)------------------------------
% 105.65/27.22 % (776692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776692)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776692)Termination reason: Instruction limit
% 105.65/27.22 % (776692)Termination phase: Saturation
% 105.65/27.22 % (776692)Time elapsed: 2.266 s
% 105.65/27.22 % (776692)Peak memory usage: 158 MB
% 105.65/27.22 % (776692)Instructions burned: 3942 (million)
% 105.65/27.22 % (776697)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=3315407979:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2754 on theBenchmark for (2754ds/2087Mi)
% 105.65/27.22 % (776690)Instruction limit reached!
% 105.65/27.22 % (776690)------------------------------
% 105.65/27.22 % (776690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776690)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776690)Termination reason: Instruction limit
% 105.65/27.22 % (776690)Termination phase: Saturation
% 105.65/27.22 % (776690)Time elapsed: 2.787 s
% 105.65/27.22 % (776690)Peak memory usage: 131 MB
% 105.65/27.22 % (776690)Instructions burned: 3917 (million)
% 105.65/27.22 % (776699)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=2376676655:cts=off:cond=on:i=4272:bs=on:fsd=on_2752 on theBenchmark for (2752ds/4272Mi)
% 105.65/27.22 % (776695)Instruction limit reached!
% 105.65/27.22 % (776695)------------------------------
% 105.65/27.22 % (776695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776695)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776695)Termination reason: Instruction limit
% 105.65/27.22 % (776695)Termination phase: Saturation
% 105.65/27.22 % (776695)Time elapsed: 2.489 s
% 105.65/27.22 % (776695)Peak memory usage: 154 MB
% 105.65/27.22 % (776695)Instructions burned: 3982 (million)
% 105.65/27.22 % (776701)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3846407959:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2748 on theBenchmark for (2748ds/2197Mi)
% 105.65/27.22 % (776697)Instruction limit reached!
% 105.65/27.22 % (776697)------------------------------
% 105.65/27.22 % (776697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.65/27.22 % (776697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.65/27.22 % (776697)CaDiCaL version: 2.1.3
% 105.65/27.22 % (776697)Termination reason: Instruction limit
% 105.65/27.22 % (776697)Termination phase: Saturation
% 105.65/27.22 % (776697)Time elapsed: 1.285 s
% 105.65/27.22 % (776697)Peak memory usage: 142 MB
% 105.65/27.22 % (776697)Instructions burned: 2087 (million)
% 105.65/27.22 % (776703)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2788371712:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2740 on theBenchmark for (2740ds/6508Mi)
% 105.65/27.22 % (776678)First to succeed.
% 105.65/27.22 % (776678)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-776562"
% 105.65/27.22 % (776678)Refutation found. Thanks to Tanya!
% 105.65/27.22 % SZS status Unsatisfiable for theBenchmark
% 105.65/27.22 % SZS output start Proof for theBenchmark
% See solution above
% 188.83/27.41 % (776678)------------------------------
% 188.83/27.41 % (776678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 188.83/27.41 % (776678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.83/27.41 % (776678)CaDiCaL version: 2.1.3
% 188.83/27.41 % (776678)Termination reason: Refutation
% 188.83/27.41 % (776678)Time elapsed: 7.245 s
% 188.83/27.41 % (776678)Peak memory usage: 234 MB
% 188.83/27.41 % (776678)Instructions burned: 11328 (million)
% 188.83/27.41 % (776678)------------------------------
% 188.83/27.41 % (776678)------------------------------
% 188.83/27.41 % (776562)Success in time 26.572 s
% 188.83/27.41 % Vampire exiting
%------------------------------------------------------------------------------